refactor: link -> destructive_link

This commit is contained in:
Shunsuke Shibayama 2023-08-06 20:13:45 +09:00
parent 5dec24a3bf
commit 142db9b697
8 changed files with 52 additions and 37 deletions

View file

@ -1318,7 +1318,7 @@ impl Context {
let (sub, sup) = fv.get_subsup().unwrap();
if self.is_trait(&sup) && !self.trait_impl_exists(&sub, &sup) {
// link to `Never` to prevent double errors from being reported
lhs.link(&Never);
lhs.destructive_link(&Never);
let sub = if cfg!(feature = "debug") {
sub
} else {
@ -2037,7 +2037,7 @@ impl Context {
if let Some((sub, sup)) = fv.get_subsup() {
if self.is_trait(&sup) && !self.trait_impl_exists(&sub, &sup) {
// to prevent double error reporting
lhs.link(&TyParam::t(Never));
lhs.destructive_link(&TyParam::t(Never));
let sub = if cfg!(feature = "debug") {
sub
} else {
@ -2114,7 +2114,7 @@ impl Context {
if let Some((sub, sup)) = fv.get_subsup() {
if self.is_trait(&sup) && !self.trait_impl_exists(&sub, &sup) {
// to prevent double error reporting
lhs.link(&TyParam::t(Never));
lhs.destructive_link(&TyParam::t(Never));
let sub = if cfg!(feature = "debug") {
sub
} else {

View file

@ -151,7 +151,7 @@ impl Generalizer {
if sub == sup {
let t = self.generalize_t(sub, uninit);
let res = FreeVar(fv);
res.link(&t);
res.destructive_link(&t);
res
} else if sup != Obj
&& !self.qnames.contains(&fv.unbound_name().unwrap())
@ -551,7 +551,7 @@ impl<'c, 'q, 'l, L: Locational> Dereferencer<'c, 'q, 'l, L> {
Ok(ty)
}
Err(errs) => {
Type::FreeVar(fv).link(&Never);
Type::FreeVar(fv).destructive_link(&Never);
Err(errs)
}
}

View file

@ -1386,7 +1386,7 @@ impl Context {
let non_default_params = pos_args.iter().map(|a| anon(a.expr.t())).collect();
let subr_t = subr_t(kind, non_default_params, None, vec![], ret_t);
self.occur(&subr_t, instance, obj)?;
instance.link(&subr_t);
instance.destructive_link(&subr_t);
Ok(SubstituteResult::Ok)
}
}

View file

@ -163,7 +163,7 @@ impl TyVarCache {
if let Ok(inst) = <&Type>::try_from(inst) {
self.update_tyvar(inst, tv, ctx);
} else if let TyParam::FreeVar(_fv) = inst {
inst.link(&TyParam::t(tv.clone()));
inst.destructive_link(&TyParam::t(tv.clone()));
} else {
unreachable!()
}
@ -182,7 +182,7 @@ impl TyVarCache {
if let Ok(inst) = <&Type>::try_from(inst) {
self.update_tyvar(inst, tv, ctx);
} else if let TyParam::FreeVar(_fv) = inst {
inst.link(&TyParam::t(tv.clone()));
inst.destructive_link(&TyParam::t(tv.clone()));
} else {
unreachable!()
}
@ -198,7 +198,7 @@ impl TyVarCache {
// T <: Eq(T <: Eq(T <: ...))
let Type::FreeVar(free_inst) = inst else { todo!("{inst}") };
if free_inst.constraint_is_uninited() {
inst.link(tv);
inst.destructive_link(tv);
} else {
// inst: ?T(<: Int) => old_sub: Never, old_sup: Int
// tv: ?T(:> Nat) => new_sub: Nat, new_sup: Obj
@ -269,7 +269,7 @@ impl TyVarCache {
}
};
if free_inst.constraint_is_uninited() {
inst.link(tp);
inst.destructive_link(tp);
} else {
let old_type = free_inst.get_type().unwrap();
let Ok(tv) = <&FreeTyParam>::try_from(tp) else { todo!("{tp}") };

View file

@ -978,7 +978,7 @@ impl Context {
return res;
};
if let Some(_fv) = vi.t.as_free() {
vi.t.link(&typ);
vi.t.destructive_link(&typ);
}
res
}

View file

@ -27,7 +27,6 @@ use super::initialize::const_func::sub_tpdict_get;
pub struct Unifier<'c, 'l, L: Locational> {
ctx: &'c Context,
loc: &'l L,
#[allow(unused)]
undoable: bool,
param_name: Option<Str>,
}
@ -288,10 +287,10 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
{
if sub_fv.level().unwrap() > sup_fv.level().unwrap() {
if !sub_fv.is_generalized() {
maybe_sub.link(maybe_sup);
maybe_sub.link(maybe_sup, self.undoable);
}
} else if !sup_fv.is_generalized() {
maybe_sup.link(maybe_sub);
maybe_sup.link(maybe_sub, self.undoable);
}
Ok(())
}
@ -317,7 +316,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
sub_fv.update_constraint(new_constraint, false);
}
} else {
maybe_sub.link(sup_tp);
maybe_sub.link(sup_tp, self.undoable);
}
Ok(())
} else if allow_divergence
@ -325,7 +324,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
|| self.ctx.eq_tp(sup_tp, &TyParam::value(NegInf)))
&& self.ctx.subtype_of(&fv_t, &mono("Num"))
{
maybe_sub.link(sup_tp);
maybe_sub.link(sup_tp, self.undoable);
Ok(())
} else {
Err(TyCheckErrors::from(TyCheckError::unreachable(
@ -357,7 +356,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
sup_fv.update_constraint(new_constraint, false);
}
} else {
maybe_sup.link(sub_tp);
maybe_sup.link(sub_tp, self.undoable);
}
Ok(())
} else if allow_divergence
@ -365,7 +364,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
|| self.ctx.eq_tp(sub_tp, &TyParam::value(NegInf)))
&& self.ctx.subtype_of(&fv_t, &mono("Num"))
{
maybe_sup.link(sub_tp);
maybe_sup.link(sub_tp, self.undoable);
Ok(())
} else {
Err(TyCheckErrors::from(TyCheckError::unreachable(
@ -752,21 +751,21 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
.cmp(&sup_fv.level().unwrap_or(GENERIC_LEVEL))
{
std::cmp::Ordering::Less => {
maybe_sub.link(&union);
maybe_sup.link(maybe_sub);
maybe_sub.link(&union, self.undoable);
maybe_sup.link(maybe_sub, self.undoable);
}
std::cmp::Ordering::Greater => {
maybe_sup.link(&union);
maybe_sub.link(maybe_sup);
maybe_sup.link(&union, self.undoable);
maybe_sub.link(maybe_sup, self.undoable);
}
std::cmp::Ordering::Equal => {
// choose named one
if sup_fv.is_named_unbound() {
maybe_sup.link(&union);
maybe_sub.link(maybe_sup);
maybe_sup.link(&union, self.undoable);
maybe_sub.link(maybe_sup, self.undoable);
} else {
maybe_sub.link(&union);
maybe_sup.link(maybe_sub);
maybe_sub.link(&union, self.undoable);
maybe_sup.link(maybe_sub, self.undoable);
}
}
}
@ -779,20 +778,20 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
{
std::cmp::Ordering::Less => {
sub_fv.update_constraint(new_constraint, false);
maybe_sup.link(maybe_sub);
maybe_sup.link(maybe_sub, self.undoable);
}
std::cmp::Ordering::Greater => {
sup_fv.update_constraint(new_constraint, false);
maybe_sub.link(maybe_sup);
maybe_sub.link(maybe_sup, self.undoable);
}
std::cmp::Ordering::Equal => {
// choose named one
if sup_fv.is_named_unbound() {
sup_fv.update_constraint(new_constraint, false);
maybe_sub.link(maybe_sup);
maybe_sub.link(maybe_sup, self.undoable);
} else {
sub_fv.update_constraint(new_constraint, false);
maybe_sup.link(maybe_sub);
maybe_sup.link(maybe_sub, self.undoable);
}
}
}
@ -867,7 +866,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
// self.sub_unify(&intersec, &lsup, loc, param_name)?;
// self.sub_unify(&lsub, &union, loc, param_name)?;
if union == intersec {
maybe_sup.link(&union);
maybe_sup.link(&union, self.undoable);
} else {
let new_constraint = Constraint::new_sandwiched(union, intersec);
sup_fv.update_constraint(new_constraint, false);
@ -953,7 +952,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
}
}
if sup.contains_union(&new_sub) {
maybe_sup.link(&new_sub); // Bool <: ?T <: Bool or Y ==> ?T == Bool
maybe_sup.link(&new_sub, self.undoable); // Bool <: ?T <: Bool or Y ==> ?T == Bool
} else {
let constr = Constraint::new_sandwiched(new_sub, mem::take(&mut sup));
sup_fv.update_constraint(constr, true);
@ -1020,7 +1019,7 @@ impl<'c, 'l, L: Locational> Unifier<'c, 'l, L> {
&& !new_sup.is_unbound_var()
&& !sub.is_unbound_var()
{
maybe_sub.link(&sub);
maybe_sub.link(&sub, self.undoable);
} else {
let constr = Constraint::new_sandwiched(sub, new_sup);
sub_fv.update_constraint(constr, true);

View file

@ -2445,7 +2445,7 @@ impl Type {
Type::FreeVar(fv) if fv.is_unbound() => {
let (sub, _sup) = fv.get_subsup().unwrap();
sub.coerce();
self.link(&sub);
self.destructive_link(&sub);
}
Type::And(l, r) | Type::Or(l, r) => {
l.coerce();
@ -3157,7 +3157,7 @@ impl Type {
}
/// interior-mut
pub(crate) fn link(&self, to: &Type) {
pub(crate) fn destructive_link(&self, to: &Type) {
if self.addr_eq(to) {
return;
}
@ -3166,7 +3166,7 @@ impl Type {
}
match self {
Self::FreeVar(fv) => fv.link(to),
Self::Refinement(refine) => refine.t.link(to),
Self::Refinement(refine) => refine.t.destructive_link(to),
_ => panic!("{self} is not a free variable"),
}
}
@ -3186,6 +3186,14 @@ impl Type {
}
}
pub(crate) fn link(&self, to: &Type, undoable: bool) {
if undoable {
self.undoable_link(to);
} else {
self.destructive_link(to);
}
}
fn inc_undo_count(&self) {
match self {
Self::FreeVar(fv) => fv.inc_undo_count(),

View file

@ -1258,7 +1258,7 @@ impl TyParam {
}
/// interior-mut
pub(crate) fn link(&self, to: &TyParam) {
pub(crate) fn destructive_link(&self, to: &TyParam) {
if self.addr_eq(to) {
return;
}
@ -1289,6 +1289,14 @@ impl TyParam {
}
}
pub(crate) fn link(&self, to: &TyParam, undoable: bool) {
if undoable {
self.undoable_link(to);
} else {
self.destructive_link(to);
}
}
fn inc_undo_count(&self) {
match self {
Self::FreeVar(fv) => fv.inc_undo_count(),