mirror of
https://github.com/erg-lang/erg.git
synced 2025-10-02 21:44:34 +00:00
fix: type variable linking bug
This commit is contained in:
parent
f22afbef10
commit
c0d784302b
2 changed files with 151 additions and 55 deletions
|
@ -4530,20 +4530,37 @@ impl Type {
|
||||||
return tv;
|
return tv;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
let fv_clone = fv.deep_clone();
|
|
||||||
if let Some((sub, sup)) = fv.get_subsup() {
|
if let Some((sub, sup)) = fv.get_subsup() {
|
||||||
fv.dummy_link();
|
fv.dummy_link();
|
||||||
let sub = f(sub);
|
let new_sub = f(sub.clone());
|
||||||
let sup = f(sup);
|
let new_sup = f(sup.clone());
|
||||||
fv.undo();
|
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() {
|
} else if let Some(ty) = fv.get_type() {
|
||||||
fv_clone.update_constraint(Constraint::new_type_of(f(ty)), true);
|
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)
|
||||||
}
|
}
|
||||||
if let Some(name) = fv.unbound_name() {
|
|
||||||
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
|
|
||||||
}
|
|
||||||
Self::FreeVar(fv_clone)
|
|
||||||
}
|
}
|
||||||
Self::Refinement(mut refine) => {
|
Self::Refinement(mut refine) => {
|
||||||
refine.t = Box::new(f(*refine.t));
|
refine.t = Box::new(f(*refine.t));
|
||||||
|
@ -4616,6 +4633,7 @@ impl Type {
|
||||||
self.map(&mut |t| t._replace(target, to, tvs), tvs)
|
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 {
|
fn _replace_tp(self, target: &TyParam, to: &TyParam, tvs: &SharedFrees) -> Type {
|
||||||
match self {
|
match self {
|
||||||
Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked()._replace_tp(target, to, tvs),
|
Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked()._replace_tp(target, to, tvs),
|
||||||
|
@ -4625,23 +4643,37 @@ impl Type {
|
||||||
return tv;
|
return tv;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
let fv_clone = fv.deep_clone();
|
|
||||||
if let Some((sub, sup)) = fv.get_subsup() {
|
if let Some((sub, sup)) = fv.get_subsup() {
|
||||||
fv.dummy_link();
|
fv.dummy_link();
|
||||||
let sub = sub._replace_tp(target, to, tvs);
|
let new_sub = sub.clone()._replace_tp(target, to, tvs);
|
||||||
let sup = sup._replace_tp(target, to, tvs);
|
let new_sup = sup.clone()._replace_tp(target, to, tvs);
|
||||||
fv.undo();
|
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() {
|
} else if let Some(ty) = fv.get_type() {
|
||||||
fv_clone.update_constraint(
|
let new_ty = ty.clone()._replace_tp(target, to, tvs);
|
||||||
Constraint::new_type_of(ty._replace_tp(target, to, tvs)),
|
if new_ty != ty {
|
||||||
true,
|
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)
|
||||||
}
|
}
|
||||||
if let Some(name) = fv.unbound_name() {
|
|
||||||
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
|
|
||||||
}
|
|
||||||
Self::FreeVar(fv_clone)
|
|
||||||
}
|
}
|
||||||
Self::Refinement(mut refine) => {
|
Self::Refinement(mut refine) => {
|
||||||
refine.t = Box::new(refine.t._replace_tp(target, to, tvs));
|
refine.t = Box::new(refine.t._replace_tp(target, to, tvs));
|
||||||
|
@ -4729,20 +4761,37 @@ impl Type {
|
||||||
return tv;
|
return tv;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
let fv_clone = fv.deep_clone();
|
|
||||||
if let Some((sub, sup)) = fv.get_subsup() {
|
if let Some((sub, sup)) = fv.get_subsup() {
|
||||||
fv.dummy_link();
|
fv.dummy_link();
|
||||||
let sub = sub.map_tp(f, tvs);
|
let new_sub = sub.clone().map_tp(f, tvs);
|
||||||
let sup = sup.map_tp(f, tvs);
|
let new_sup = sup.clone().map_tp(f, tvs);
|
||||||
fv.undo();
|
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() {
|
} else if let Some(ty) = fv.get_type() {
|
||||||
fv_clone.update_constraint(Constraint::new_type_of(ty.map_tp(f, tvs)), true);
|
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)
|
||||||
}
|
}
|
||||||
if let Some(name) = fv.unbound_name() {
|
|
||||||
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
|
|
||||||
}
|
|
||||||
Self::FreeVar(fv_clone)
|
|
||||||
}
|
}
|
||||||
Self::Refinement(mut refine) => {
|
Self::Refinement(mut refine) => {
|
||||||
refine.t = Box::new(refine.t.map_tp(f, tvs));
|
refine.t = Box::new(refine.t.map_tp(f, tvs));
|
||||||
|
@ -4818,21 +4867,37 @@ impl Type {
|
||||||
return Ok(tv);
|
return Ok(tv);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
let fv_clone = fv.deep_clone();
|
|
||||||
if let Some((sub, sup)) = fv.get_subsup() {
|
if let Some((sub, sup)) = fv.get_subsup() {
|
||||||
fv.dummy_link();
|
fv.dummy_link();
|
||||||
let sub = sub.try_map_tp(f, tvs)?;
|
let new_sub = sub.clone().try_map_tp(f, tvs)?;
|
||||||
let sup = sup.try_map_tp(f, tvs)?;
|
let new_sup = sup.clone().try_map_tp(f, tvs)?;
|
||||||
fv.undo();
|
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() {
|
} else if let Some(ty) = fv.get_type() {
|
||||||
fv_clone
|
let new_ty = ty.clone().try_map_tp(f, tvs)?;
|
||||||
.update_constraint(Constraint::new_type_of(ty.try_map_tp(f, tvs)?), true);
|
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))
|
||||||
}
|
}
|
||||||
if let Some(name) = fv.unbound_name() {
|
|
||||||
tvs.insert_tv(name, Self::FreeVar(fv_clone.clone()));
|
|
||||||
}
|
|
||||||
Ok(Self::FreeVar(fv_clone))
|
|
||||||
}
|
}
|
||||||
Self::Refinement(mut refine) => {
|
Self::Refinement(mut refine) => {
|
||||||
refine.t = Box::new(refine.t.try_map_tp(f, tvs)?);
|
refine.t = Box::new(refine.t.try_map_tp(f, tvs)?);
|
||||||
|
@ -6128,4 +6193,20 @@ mod tests {
|
||||||
assert!(subr.is_recursive());
|
assert!(subr.is_recursive());
|
||||||
assert!(sup.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)
|
||||||
|
);
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -1571,11 +1571,16 @@ impl TyParam {
|
||||||
if let Some(tp) = tvs.get_tp(&name) {
|
if let Some(tp) = tvs.get_tp(&name) {
|
||||||
return tp;
|
return tp;
|
||||||
}
|
}
|
||||||
let typ = fv.get_type().unwrap()._replace(target, to, tvs);
|
let typ = fv.get_type().unwrap();
|
||||||
let fv_clone = fv.deep_clone();
|
let new_typ = typ.clone()._replace(target, to, tvs);
|
||||||
fv_clone.update_type(typ);
|
if new_typ != typ {
|
||||||
tvs.insert_tp(name, Self::FreeVar(fv_clone.clone()));
|
let fv_clone = fv.deep_clone();
|
||||||
Self::FreeVar(fv_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::Type(t) => Self::t(t._replace(target, to, tvs)),
|
||||||
Self::Erased(t) => Self::erased(t._replace(target, to, tvs)),
|
Self::Erased(t) => Self::erased(t._replace(target, to, tvs)),
|
||||||
|
@ -1927,12 +1932,17 @@ impl TyParam {
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
let typ = fv.get_type().unwrap();
|
let typ = fv.get_type().unwrap();
|
||||||
let fv_clone = fv.deep_clone();
|
let new_typ = typ.clone().map_tp(f, tvs);
|
||||||
fv_clone.update_type(typ.map_tp(f, tvs));
|
if typ != new_typ {
|
||||||
if let Some(name) = fv_clone.unbound_name() {
|
let fv_clone = fv.deep_clone();
|
||||||
tvs.insert_tp(name, TyParam::FreeVar(fv_clone.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::FreeVar(_) => self,
|
||||||
TyParam::App { name, args } => {
|
TyParam::App { name, args } => {
|
||||||
|
@ -1996,13 +2006,18 @@ impl TyParam {
|
||||||
return tp;
|
return tp;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
let fv_clone = fv.deep_clone();
|
|
||||||
let typ = fv.get_type().unwrap();
|
let typ = fv.get_type().unwrap();
|
||||||
fv_clone.update_type(f(typ));
|
let new_typ = f(typ.clone());
|
||||||
if let Some(name) = fv_clone.unbound_name() {
|
if typ != new_typ {
|
||||||
tvs.insert_tp(name, TyParam::FreeVar(fv_clone.clone()));
|
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::FreeVar(_) => self,
|
||||||
TyParam::App { name, args } => {
|
TyParam::App { name, args } => {
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue