Update mod.rs

This commit is contained in:
Shunsuke Shibayama 2023-10-01 13:11:44 +09:00
parent 4869bfad7b
commit cb66bcabaa

View file

@ -2671,45 +2671,68 @@ impl Type {
} }
} }
/// returns top-level qvars.
/// see also: `qvars_inner`
pub fn qvars(&self) -> Set<(Str, Constraint)> { pub fn qvars(&self) -> Set<(Str, Constraint)> {
match self { match self {
Self::FreeVar(fv) if fv.is_linked() => fv.unsafe_crack().qvars(), Self::Quantified(quant) => quant.qvars_inner(),
_ => self.qvars_inner(),
}
}
/// ```erg
/// (|T|(T) -> T).qvars() == {T}
/// (|T|(T) -> T).qvars_inner() == {}
/// ((|T|(T) -> T) and (Int -> Int)).qvars() == {}
/// ```
fn qvars_inner(&self) -> Set<(Str, Constraint)> {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.unsafe_crack().qvars_inner(),
Self::FreeVar(fv) if !fv.constraint_is_uninited() => { Self::FreeVar(fv) if !fv.constraint_is_uninited() => {
let base = set! {(fv.unbound_name().unwrap(), fv.constraint().unwrap())}; let base = set! {(fv.unbound_name().unwrap(), fv.constraint().unwrap())};
if let Some((sub, sup)) = fv.get_subsup() { if let Some((sub, sup)) = fv.get_subsup() {
fv.do_avoiding_recursion(|| base.concat(sub.qvars()).concat(sup.qvars())) fv.do_avoiding_recursion(|| {
base.concat(sub.qvars_inner()).concat(sup.qvars_inner())
})
} else if let Some(ty) = fv.get_type() { } else if let Some(ty) = fv.get_type() {
fv.do_avoiding_recursion(|| base.concat(ty.qvars())) fv.do_avoiding_recursion(|| base.concat(ty.qvars_inner()))
} else { } else {
base base
} }
} }
Self::Ref(ty) => ty.qvars(), Self::Ref(ty) => ty.qvars_inner(),
Self::RefMut { before, after } => before Self::RefMut { before, after } => before.qvars_inner().concat(
.qvars() after
.concat(after.as_ref().map(|t| t.qvars()).unwrap_or_else(|| set! {})), .as_ref()
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs.qvars().concat(rhs.qvars()), .map(|t| t.qvars_inner())
Self::Not(ty) => ty.qvars(), .unwrap_or_else(|| set! {}),
),
Self::And(lhs, rhs) | Self::Or(lhs, rhs) => lhs.qvars_inner().concat(rhs.qvars_inner()),
Self::Not(ty) => ty.qvars_inner(),
Self::Callable { param_ts, return_t } => param_ts Self::Callable { param_ts, return_t } => param_ts
.iter() .iter()
.fold(set! {}, |acc, t| acc.concat(t.qvars())) .fold(set! {}, |acc, t| acc.concat(t.qvars_inner()))
.concat(return_t.qvars()), .concat(return_t.qvars_inner()),
Self::Subr(subr) => subr.qvars(), Self::Subr(subr) => subr.qvars(),
Self::Record(r) => r.values().fold(set! {}, |acc, t| acc.concat(t.qvars())), Self::Record(r) => r
Self::NamedTuple(r) => r.iter().fold(set! {}, |acc, (_, t)| acc.concat(t.qvars())), .values()
Self::Refinement(refine) => refine.t.qvars().concat(refine.pred.qvars()), .fold(set! {}, |acc, t| acc.concat(t.qvars_inner())),
Self::NamedTuple(r) => r
.iter()
.fold(set! {}, |acc, (_, t)| acc.concat(t.qvars_inner())),
Self::Refinement(refine) => refine.t.qvars_inner().concat(refine.pred.qvars()),
// ((|T| T -> T) and U).qvars() == U.qvars() // ((|T| T -> T) and U).qvars() == U.qvars()
// Self::Quantified(quant) => quant.qvars(), // Self::Quantified(quant) => quant.qvars(),
Self::Poly { params, .. } => params Self::Poly { params, .. } => params
.iter() .iter()
.fold(set! {}, |acc, tp| acc.concat(tp.qvars())), .fold(set! {}, |acc, tp| acc.concat(tp.qvars())),
Self::Proj { lhs, .. } => lhs.qvars(), Self::Proj { lhs, .. } => lhs.qvars_inner(),
Self::ProjCall { lhs, args, .. } => lhs Self::ProjCall { lhs, args, .. } => lhs
.qvars() .qvars()
.concat(args.iter().fold(set! {}, |acc, tp| acc.concat(tp.qvars()))), .concat(args.iter().fold(set! {}, |acc, tp| acc.concat(tp.qvars()))),
Self::Structural(ty) => ty.qvars(), Self::Structural(ty) => ty.qvars_inner(),
Self::Guard(guard) => guard.to.qvars(), Self::Guard(guard) => guard.to.qvars_inner(),
Self::Bounded { sub, sup } => sub.qvars().concat(sup.qvars()), Self::Bounded { sub, sup } => sub.qvars_inner().concat(sup.qvars_inner()),
_ => set! {}, _ => set! {},
} }
} }