Skip to content

Commit

Permalink
fix: type variable linking bug
Browse files Browse the repository at this point in the history
  • Loading branch information
@mtshiba
mtshiba committed Nov 7, 2024
1 parent f22afbe commit c0d7843
Show file tree
Hide file tree
Showing 2 changed files with 151 additions and 55 deletions.
161 changes: 121 additions & 40 deletions crates/erg_compiler/ty/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4530,20 +4530,37 @@ impl Type {
return tv;
}
}
let fv_clone = fv.deep_clone();
if let Some((sub, sup)) = fv.get_subsup() {
fv.dummy_link();
let sub = f(sub);
let sup = f(sup);
let new_sub = f(sub.clone());
let new_sup = f(sup.clone());
fv.undo();
fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
if new_sub != sub || new_sup != sup {
let fv_clone = fv.deep_clone();
fv_clone
.update_constraint(Constraint::new_sandwiched(new_sub, new_sup), true);
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
}
Self::FreeVar(fv_clone)
} else {
Self::FreeVar(fv)
}
} else if let Some(ty) = fv.get_type() {
fv_clone.update_constraint(Constraint::new_type_of(f(ty)), true);
}
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
let new_ty = f(ty.clone());
if new_ty != ty {
let fv_clone = fv.deep_clone();
fv_clone.update_constraint(Constraint::new_type_of(new_ty), true);
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
}
Self::FreeVar(fv_clone)
} else {
Self::FreeVar(fv)
}
} else {
Self::FreeVar(fv)
}
Self::FreeVar(fv_clone)
}
Self::Refinement(mut refine) => {
refine.t = Box::new(f(*refine.t));
Expand Down Expand Up @@ -4616,6 +4633,7 @@ impl Type {
self.map(&mut |t| t._replace(target, to, tvs), tvs)
}

/// `?T(<: Int).replace(Int, Nat) == ?T'(<: Nat)`
fn _replace_tp(self, target: &TyParam, to: &TyParam, tvs: &SharedFrees) -> Type {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked()._replace_tp(target, to, tvs),
Expand All @@ -4625,23 +4643,37 @@ impl Type {
return tv;
}
}
let fv_clone = fv.deep_clone();
if let Some((sub, sup)) = fv.get_subsup() {
fv.dummy_link();
let sub = sub._replace_tp(target, to, tvs);
let sup = sup._replace_tp(target, to, tvs);
let new_sub = sub.clone()._replace_tp(target, to, tvs);
let new_sup = sup.clone()._replace_tp(target, to, tvs);
fv.undo();
fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
if new_sub != sub || new_sup != sup {
let fv_clone = fv.deep_clone();
fv_clone
.update_constraint(Constraint::new_sandwiched(new_sub, new_sup), true);
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
}
Self::FreeVar(fv_clone)
} else {
Self::FreeVar(fv)
}
} else if let Some(ty) = fv.get_type() {
fv_clone.update_constraint(
Constraint::new_type_of(ty._replace_tp(target, to, tvs)),
true,
);
}
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
let new_ty = ty.clone()._replace_tp(target, to, tvs);
if new_ty != ty {
let fv_clone = fv.deep_clone();
fv_clone.update_constraint(Constraint::new_type_of(new_ty), true);
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
}
Self::FreeVar(fv_clone)
} else {
Self::FreeVar(fv)
}
} else {
Self::FreeVar(fv)
}
Self::FreeVar(fv_clone)
}
Self::Refinement(mut refine) => {
refine.t = Box::new(refine.t._replace_tp(target, to, tvs));
Expand Down Expand Up @@ -4729,20 +4761,37 @@ impl Type {
return tv;
}
}
let fv_clone = fv.deep_clone();
if let Some((sub, sup)) = fv.get_subsup() {
fv.dummy_link();
let sub = sub.map_tp(f, tvs);
let sup = sup.map_tp(f, tvs);
let new_sub = sub.clone().map_tp(f, tvs);
let new_sup = sup.clone().map_tp(f, tvs);
fv.undo();
fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
if new_sub != sub || new_sup != sup {
let fv_clone = fv.deep_clone();
fv_clone
.update_constraint(Constraint::new_sandwiched(new_sub, new_sup), true);
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
}
Self::FreeVar(fv_clone)
} else {
Self::FreeVar(fv)
}
} else if let Some(ty) = fv.get_type() {
fv_clone.update_constraint(Constraint::new_type_of(ty.map_tp(f, tvs)), true);
}
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
let new_ty = ty.clone().map_tp(f, tvs);
if new_ty != ty {
let fv_clone = fv.deep_clone();
fv_clone.update_constraint(Constraint::new_type_of(new_ty), true);
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
}
Self::FreeVar(fv_clone)
} else {
Self::FreeVar(fv)
}
} else {
Self::FreeVar(fv)
}
Self::FreeVar(fv_clone)
}
Self::Refinement(mut refine) => {
refine.t = Box::new(refine.t.map_tp(f, tvs));
Expand Down Expand Up @@ -4818,21 +4867,37 @@ impl Type {
return Ok(tv);
}
}
let fv_clone = fv.deep_clone();
if let Some((sub, sup)) = fv.get_subsup() {
fv.dummy_link();
let sub = sub.try_map_tp(f, tvs)?;
let sup = sup.try_map_tp(f, tvs)?;
let new_sub = sub.clone().try_map_tp(f, tvs)?;
let new_sup = sup.clone().try_map_tp(f, tvs)?;
fv.undo();
fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
if new_sub != sub || new_sup != sup {
let fv_clone = fv.deep_clone();
fv_clone
.update_constraint(Constraint::new_sandwiched(new_sub, new_sup), true);
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
}
Ok(Self::FreeVar(fv_clone))
} else {
Ok(Self::FreeVar(fv))
}
} else if let Some(ty) = fv.get_type() {
fv_clone
.update_constraint(Constraint::new_type_of(ty.try_map_tp(f, tvs)?), true);
}
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
let new_ty = ty.clone().try_map_tp(f, tvs)?;
if new_ty != ty {
let fv_clone = fv.deep_clone();
fv_clone.update_constraint(Constraint::new_type_of(new_ty), true);
if let Some(name) = fv.unbound_name() {
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
}
Ok(Self::FreeVar(fv_clone))
} else {
Ok(Self::FreeVar(fv))
}
} else {
Ok(Self::FreeVar(fv))
}
Ok(Self::FreeVar(fv_clone))
}
Self::Refinement(mut refine) => {
refine.t = Box::new(refine.t.try_map_tp(f, tvs)?);
Expand Down Expand Up @@ -6128,4 +6193,20 @@ mod tests {
assert!(subr.is_recursive());
assert!(sup.is_recursive());
}

#[test]
fn test_link() {
let t = named_free_var("T".into(), 1, Constraint::new_type_of(Type::Type));
let u = free_var(1, Constraint::new_type_of(Type::Type));
let v = t.clone();
u.link(&unknown_len_list_t(t.clone()), None);
t.destructive_link(&Type::Int);
assert_eq!(v, Type::Int);
assert_eq!(
u,
unknown_len_list_t(Type::Int),
"{u} != {}",
unknown_len_list_t(Type::Int)
);
}
}
45 changes: 30 additions & 15 deletions crates/erg_compiler/ty/typaram.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1571,11 +1571,16 @@ impl TyParam {
if let Some(tp) = tvs.get_tp(&name) {
return tp;
}
let typ = fv.get_type().unwrap()._replace(target, to, tvs);
let fv_clone = fv.deep_clone();
fv_clone.update_type(typ);
tvs.insert_tp(name, Self::FreeVar(fv_clone.clone()));
Self::FreeVar(fv_clone)
let typ = fv.get_type().unwrap();
let new_typ = typ.clone()._replace(target, to, tvs);
if new_typ != typ {
let fv_clone = fv.deep_clone();
fv_clone.update_type(new_typ);
tvs.insert_tp(name, Self::FreeVar(fv_clone.clone()));
Self::FreeVar(fv_clone)
} else {
Self::FreeVar(fv)
}
}
Self::Type(t) => Self::t(t._replace(target, to, tvs)),
Self::Erased(t) => Self::erased(t._replace(target, to, tvs)),
Expand Down Expand Up @@ -1927,12 +1932,17 @@ impl TyParam {
}
}
let typ = fv.get_type().unwrap();
let fv_clone = fv.deep_clone();
fv_clone.update_type(typ.map_tp(f, tvs));
if let Some(name) = fv_clone.unbound_name() {
tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
let new_typ = typ.clone().map_tp(f, tvs);
if typ != new_typ {
let fv_clone = fv.deep_clone();
fv_clone.update_type(new_typ);
if let Some(name) = fv_clone.unbound_name() {
tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
}
TyParam::FreeVar(fv_clone)
} else {
TyParam::FreeVar(fv)
}
TyParam::FreeVar(fv_clone)
}
TyParam::FreeVar(_) => self,
TyParam::App { name, args } => {
Expand Down Expand Up @@ -1996,13 +2006,18 @@ impl TyParam {
return tp;
}
}
let fv_clone = fv.deep_clone();
let typ = fv.get_type().unwrap();
fv_clone.update_type(f(typ));
if let Some(name) = fv_clone.unbound_name() {
tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
let new_typ = f(typ.clone());
if typ != new_typ {
let fv_clone = fv.deep_clone();
fv_clone.update_type(new_typ);
if let Some(name) = fv_clone.unbound_name() {
tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
}
TyParam::FreeVar(fv_clone)
} else {
TyParam::FreeVar(fv)
}
TyParam::FreeVar(fv_clone)
}
TyParam::FreeVar(_) => self,
TyParam::App { name, args } => {
Expand Down

0 comments on commit c0d7843

Please sign in to comment.