fix: sub-unification bug

This commit is contained in:
Shunsuke Shibayama 2024-08-23 12:10:10 +09:00
parent 7f16461767
commit 837414929c
4 changed files with 310 additions and 99 deletions

View file

@ -292,6 +292,15 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
Ok(())
}
(ValueObj::Dict(sub), ValueObj::Dict(sup)) => {
if sub.len() == 1 && sup.len() == 1 {
let sub_key = sub.keys().next().unwrap();
let sup_key = sup.keys().next().unwrap();
self.sub_unify_value(sub_key, sup_key)?;
let sub_value = sub.values().next().unwrap();
let sup_value = sup.values().next().unwrap();
self.sub_unify_value(sub_value, sup_value)?;
return Ok(());
}
for (sub_k, sub_v) in sub.iter() {
if let Some(sup_v) = sup.get(sub_k) {
self.sub_unify_value(sub_v, sup_v)?;

View file

@ -233,10 +233,7 @@ impl ParamTy {
}
}
pub fn map_type<F>(self, f: F) -> Self
where
F: FnOnce(Type) -> Type,
{
pub fn map_type(self, f: impl FnOnce(Type) -> Type) -> Self {
match self {
Self::Pos(ty) => Self::Pos(f(ty)),
Self::Kw { name, ty } => Self::Kw { name, ty: f(ty) },
@ -248,10 +245,7 @@ impl ParamTy {
}
}
pub fn map_default_type<F>(self, f: F) -> Self
where
F: FnOnce(Type) -> Type,
{
pub fn map_default_type(self, f: impl FnOnce(Type) -> Type) -> Self {
match self {
Self::KwWithDefault { name, ty, default } => Self::KwWithDefault {
name,
@ -521,19 +515,37 @@ impl SubrType {
|| self.return_t.contains_tp(target)
}
pub fn map(self, f: impl Fn(Type) -> Type) -> Self {
pub fn map(self, f: impl Fn(Type) -> Type + Copy) -> Self {
Self::new(
self.kind,
self.non_default_params
.into_iter()
.map(|pt| pt.map_type(&f))
.map(|pt| pt.map_type(f))
.collect(),
self.var_params.map(|pt| pt.map_type(&f)),
self.var_params.map(|pt| pt.map_type(f)),
self.default_params
.into_iter()
.map(|pt| pt.map_type(&f).map_default_type(&f))
.map(|pt| pt.map_type(f).map_default_type(f))
.collect(),
self.kw_var_params.map(|pt| pt.map_type(&f)),
self.kw_var_params.map(|pt| pt.map_type(f)),
f(*self.return_t),
)
}
pub fn map_tp(self, f: impl Fn(TyParam) -> TyParam + Copy) -> Self {
let f = |t: Type| t.map_tp(f);
Self::new(
self.kind,
self.non_default_params
.into_iter()
.map(|pt| pt.map_type(f))
.collect(),
self.var_params.map(|pt| pt.map_type(f)),
self.default_params
.into_iter()
.map(|pt| pt.map_type(f).map_default_type(f))
.collect(),
self.kw_var_params.map(|pt| pt.map_type(f)),
f(*self.return_t),
)
}
@ -2725,6 +2737,14 @@ impl Type {
<&FreeTyVar>::try_from(self).ok()
}
pub fn into_free(self) -> Option<FreeTyVar> {
match self {
Type::FreeVar(fv) => Some(fv),
Type::Refinement(refine) => refine.t.into_free(),
_ => None,
}
}
pub fn contains_tvar(&self, target: &FreeTyVar) -> bool {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().contains_tvar(target),
@ -4288,6 +4308,83 @@ impl Type {
}
}
fn map_tp(self, f: impl Fn(TyParam) -> TyParam + Copy) -> Type {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.unwrap_linked().map_tp(f),
Self::FreeVar(fv) => {
let fv_clone = fv.deep_clone();
if let Some((sub, sup)) = fv_clone.get_subsup() {
fv.dummy_link();
fv_clone.dummy_link();
let sub = sub.map_tp(f);
let sup = sup.map_tp(f);
fv.undo();
fv_clone.undo();
fv_clone.update_constraint(Constraint::new_sandwiched(sub, sup), true);
} else if let Some(ty) = fv_clone.get_type() {
fv_clone.update_constraint(Constraint::new_type_of(ty.map_tp(f)), true);
}
Self::FreeVar(fv_clone)
}
Self::Refinement(mut refine) => {
refine.t = Box::new(refine.t.map_tp(f));
// refine.pred = refine.pred.replace_tp(target, to);
Self::Refinement(refine)
}
Self::Record(mut rec) => {
for v in rec.values_mut() {
*v = std::mem::take(v).map_tp(f);
}
Self::Record(rec)
}
Self::NamedTuple(mut r) => {
for (_, v) in r.iter_mut() {
*v = std::mem::take(v).map_tp(f);
}
Self::NamedTuple(r)
}
Self::Subr(subr) => Self::Subr(subr.map_tp(f)),
Self::Callable { param_ts, return_t } => {
let param_ts = param_ts.into_iter().map(|t| t.map_tp(f)).collect();
let return_t = Box::new(return_t.map_tp(f));
Self::Callable { param_ts, return_t }
}
Self::Quantified(quant) => quant.map_tp(f).quantify(),
Self::Poly { name, params } => {
let params = params.into_iter().map(|tp| tp.map(f)).collect();
Self::Poly { name, params }
}
Self::Ref(t) => Self::Ref(Box::new(t.map_tp(f))),
Self::RefMut { before, after } => Self::RefMut {
before: Box::new(before.map_tp(f)),
after: after.map(|t| Box::new(t.map_tp(f))),
},
Self::And(l, r) => l.map_tp(f) & r.map_tp(f),
Self::Or(l, r) => l.map_tp(f) | r.map_tp(f),
Self::Not(ty) => !ty.map_tp(f),
Self::Proj { lhs, rhs } => lhs.map_tp(f).proj(rhs),
Self::ProjCall {
lhs,
attr_name,
args,
} => {
let args = args.into_iter().map(|tp| tp.map(f)).collect();
proj_call(lhs.map(f), attr_name, args)
}
Self::Structural(ty) => ty.map_tp(f).structuralize(),
Self::Guard(guard) => Self::Guard(GuardType::new(
guard.namespace,
guard.target.clone(),
guard.to.map_tp(f),
)),
Self::Bounded { sub, sup } => Self::Bounded {
sub: Box::new(sub.map_tp(f)),
sup: Box::new(sup.map_tp(f)),
},
other => other,
}
}
fn replace_param(self, target: &str, to: &str) -> Self {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().clone().replace_param(target, to),

View file

@ -1217,7 +1217,7 @@ impl TyParam {
Self::BinOp { lhs, rhs, .. } => lhs.qvars().concat(rhs.qvars()),
Self::App { args, .. } => args.iter().fold(set! {}, |acc, p| acc.concat(p.qvars())),
Self::Erased(t) => t.qvars(),
Self::Value(ValueObj::Type(t)) => t.typ().qvars(),
Self::Value(val) => val.qvars(),
_ => set! {},
}
}
@ -1239,7 +1239,7 @@ impl TyParam {
Self::BinOp { lhs, rhs, .. } => lhs.has_qvar() || rhs.has_qvar(),
Self::App { args, .. } => args.iter().any(|p| p.has_qvar()),
Self::Erased(t) => t.has_qvar(),
Self::Value(ValueObj::Type(t)) => t.typ().has_qvar(),
Self::Value(val) => val.has_qvar(),
_ => false,
}
}
@ -1262,7 +1262,7 @@ impl TyParam {
Self::UnaryOp { val, .. } => val.contains_tvar(target),
Self::BinOp { lhs, rhs, .. } => lhs.contains_tvar(target) || rhs.contains_tvar(target),
Self::App { args, .. } => args.iter().any(|p| p.contains_tvar(target)),
Self::Value(ValueObj::Type(t)) => t.typ().contains_tvar(target),
Self::Value(val) => val.contains_tvar(target),
_ => false,
}
}
@ -1289,7 +1289,7 @@ impl TyParam {
Self::UnaryOp { val, .. } => val.contains_type(target),
Self::BinOp { lhs, rhs, .. } => lhs.contains_type(target) || rhs.contains_type(target),
Self::App { args, .. } => args.iter().any(|p| p.contains_type(target)),
Self::Value(ValueObj::Type(t)) => t.typ().contains_type(target),
Self::Value(val) => val.contains_type(target),
_ => false,
}
}
@ -1319,7 +1319,7 @@ impl TyParam {
Self::UnaryOp { val, .. } => val.contains_tp(target),
Self::BinOp { lhs, rhs, .. } => lhs.contains_tp(target) || rhs.contains_tp(target),
Self::App { args, .. } => args.iter().any(|p| p.contains_tp(target)),
Self::Value(ValueObj::Type(t)) => t.typ().contains_tp(target),
Self::Value(val) => val.contains_tp(target),
_ => false,
}
}
@ -1381,7 +1381,7 @@ impl TyParam {
.iter()
.any(|(k, v)| k.contains_tp(self) || v.contains_tp(self)),
Self::Type(t) => t.contains_tp(self),
Self::Value(ValueObj::Type(t)) => t.typ().contains_tp(self),
Self::Value(val) => val.contains_tp(self),
Self::Erased(t) => t.contains_tp(self),
_ => false,
}
@ -1418,7 +1418,7 @@ impl TyParam {
Self::BinOp { lhs, rhs, .. } => lhs.has_unbound_var() || rhs.has_unbound_var(),
Self::App { args, .. } => args.iter().any(|p| p.has_unbound_var()),
Self::Erased(t) => t.has_unbound_var(),
Self::Value(ValueObj::Type(t)) => t.typ().has_unbound_var(),
Self::Value(val) => val.has_unbound_var(),
_ => false,
}
}
@ -1451,7 +1451,7 @@ impl TyParam {
}
Self::App { args, .. } => args.iter().any(|p| p.has_undoable_linked_var()),
Self::Erased(t) => t.has_undoable_linked_var(),
Self::Value(ValueObj::Type(t)) => t.typ().has_undoable_linked_var(),
Self::Value(val) => val.has_undoable_linked_var(),
_ => false,
}
}
@ -1560,9 +1560,7 @@ impl TyParam {
}
Self::Type(t) => Self::t(t._replace(target, to)),
Self::Erased(t) => Self::erased(t._replace(target, to)),
Self::Value(ValueObj::Type(t)) => {
Self::value(ValueObj::Type(t.mapped_t(|t| t._replace(target, to))))
}
Self::Value(val) => Self::Value(val.replace_t(target, to)),
_ => self.map(|tp| tp.replace_t(target, to)),
}
}
@ -1709,7 +1707,7 @@ impl TyParam {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().typarams(),
Self::Type(t) => t.typarams(),
Self::Value(ValueObj::Type(t)) => t.typ().typarams(),
Self::Value(val) => val.typarams(),
Self::App { args, .. } => args.clone(),
_ => vec![],
}
@ -1719,7 +1717,7 @@ impl TyParam {
match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().contained_ts(),
Self::Type(t) => t.contained_ts(),
Self::Value(ValueObj::Type(t)) => t.typ().contained_ts(),
Self::Value(val) => val.contained_ts(),
Self::App { args, .. } => args
.iter()
.fold(set! {}, |acc, p| acc.concat(p.contained_ts())),
@ -1738,7 +1736,7 @@ impl TyParam {
fv.update_init();
}
Self::Type(t) => t.dereference(),
Self::Value(ValueObj::Type(t)) => t.typ_mut().dereference(),
Self::Value(val) => val.dereference(),
Self::App { args, .. } => {
for arg in args {
arg.dereference();
@ -1855,12 +1853,12 @@ impl TyParam {
set
}
Self::Type(t) | Self::Erased(t) => t.variables(),
Self::Value(ValueObj::Type(t)) => t.typ().variables(),
Self::Value(val) => val.variables(),
_ => set! {},
}
}
pub fn map(self, f: impl Fn(TyParam) -> TyParam) -> TyParam {
pub fn map(self, f: impl Fn(TyParam) -> TyParam + Copy) -> TyParam {
match self {
TyParam::FreeVar(fv) if fv.is_linked() => f(fv.unwrap_linked()),
TyParam::App { name, args } => {
@ -1904,13 +1902,14 @@ impl TyParam {
attr,
},
TyParam::ProjCall { obj, attr, args } => {
let new_args = args.into_iter().map(&f).collect::<Vec<_>>();
let new_args = args.into_iter().map(f).collect::<Vec<_>>();
TyParam::ProjCall {
obj: Box::new(f(*obj)),
attr,
args: new_args,
}
}
TyParam::Value(val) => TyParam::Value(val.map_t(&mut |t| t.map_tp(f))),
self_ => self_,
}
}

View file

@ -26,6 +26,7 @@ use self::value_set::inner_class;
use super::codeobj::{tuple_into_bytes, CodeObj};
use super::constructors::{dict_t, list_t, refinement, set_t, tuple_t, unsized_list_t};
use super::free::{Constraint, FreeTyVar};
use super::typaram::{OpKind, TyParam};
use super::{ConstSubr, Field, HasType, Predicate, Type};
use super::{CONTAINER_OMIT_THRESHOLD, STR_OMIT_THRESHOLD};
@ -1610,96 +1611,42 @@ impl ValueObj {
}
}
pub fn replace_t(self, target: &Type, to: &Type) -> Self {
pub fn map_t(self, f: &mut impl FnMut(Type) -> Type) -> Self {
match self {
ValueObj::Type(obj) => ValueObj::Type(obj.mapped_t(|t| t._replace(target, to))),
ValueObj::List(lis) => ValueObj::List(
lis.iter()
.map(|v| v.clone().replace_t(target, to))
.collect(),
),
ValueObj::Tuple(tup) => ValueObj::Tuple(
tup.iter()
.map(|v| v.clone().replace_t(target, to))
.collect(),
),
ValueObj::Set(st) => {
ValueObj::Set(st.iter().map(|v| v.clone().replace_t(target, to)).collect())
ValueObj::Type(obj) => ValueObj::Type(obj.mapped_t(f)),
ValueObj::List(lis) => ValueObj::List(lis.iter().map(|v| v.clone().map_t(f)).collect()),
ValueObj::Tuple(tup) => {
ValueObj::Tuple(tup.iter().map(|v| v.clone().map_t(f)).collect())
}
ValueObj::Set(st) => ValueObj::Set(st.iter().map(|v| v.clone().map_t(f)).collect()),
ValueObj::Dict(dict) => ValueObj::Dict(
dict.iter()
.map(|(k, v)| {
(
k.clone().replace_t(target, to),
v.clone().replace_t(target, to),
)
})
.map(|(k, v)| (k.clone().map_t(f), v.clone().map_t(f)))
.collect(),
),
ValueObj::Record(rec) => ValueObj::Record(
rec.iter()
.map(|(k, v)| (k.clone(), v.clone().replace_t(target, to)))
.map(|(k, v)| (k.clone(), v.clone().map_t(f)))
.collect(),
),
ValueObj::DataClass { name, fields } => ValueObj::DataClass {
name,
fields: fields
.iter()
.map(|(k, v)| (k.clone(), v.clone().replace_t(target, to)))
.map(|(k, v)| (k.clone(), v.clone().map_t(f)))
.collect(),
},
ValueObj::UnsizedList(elem) => {
ValueObj::UnsizedList(Box::new(elem.clone().replace_t(target, to)))
}
ValueObj::UnsizedList(elem) => ValueObj::UnsizedList(Box::new(elem.clone().map_t(f))),
self_ => self_,
}
}
pub fn replace_t(self, target: &Type, to: &Type) -> Self {
self.map_t(&mut |t| t._replace(target, to))
}
pub fn replace_tp(self, target: &TyParam, to: &TyParam) -> Self {
match self {
ValueObj::Type(obj) => ValueObj::Type(obj.mapped_t(|t| t._replace_tp(target, to))),
ValueObj::List(lis) => ValueObj::List(
lis.iter()
.map(|v| v.clone().replace_tp(target, to))
.collect(),
),
ValueObj::Tuple(tup) => ValueObj::Tuple(
tup.iter()
.map(|v| v.clone().replace_tp(target, to))
.collect(),
),
ValueObj::Set(st) => ValueObj::Set(
st.iter()
.map(|v| v.clone().replace_tp(target, to))
.collect(),
),
ValueObj::Dict(dict) => ValueObj::Dict(
dict.iter()
.map(|(k, v)| {
(
k.clone().replace_tp(target, to),
v.clone().replace_tp(target, to),
)
})
.collect(),
),
ValueObj::Record(rec) => ValueObj::Record(
rec.iter()
.map(|(k, v)| (k.clone(), v.clone().replace_tp(target, to)))
.collect(),
),
ValueObj::DataClass { name, fields } => ValueObj::DataClass {
name,
fields: fields
.iter()
.map(|(k, v)| (k.clone(), v.clone().replace_tp(target, to)))
.collect(),
},
ValueObj::UnsizedList(elem) => {
ValueObj::UnsizedList(Box::new(elem.clone().replace_tp(target, to)))
}
self_ => self_,
}
self.map_t(&mut |t| t._replace_tp(target, to))
}
pub fn contains(&self, val: &ValueObj) -> bool {
@ -1714,6 +1661,165 @@ impl ValueObj {
_ => self == val,
}
}
pub fn contains_type(&self, target: &Type) -> bool {
match self {
Self::Type(t) => t.typ().contains_type(target),
Self::List(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.contains_type(target)),
Self::UnsizedList(elem) => elem.contains_type(target),
Self::Set(ts) => ts.iter().any(|t| t.contains_type(target)),
Self::Dict(ts) => ts
.iter()
.any(|(k, v)| k.contains_type(target) || v.contains_type(target)),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().any(|(_, tp)| tp.contains_type(target))
}
_ => false,
}
}
pub fn contains_tp(&self, target: &TyParam) -> bool {
match self {
Self::Type(t) => t.typ().contains_tp(target),
Self::List(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.contains_tp(target)),
Self::UnsizedList(elem) => elem.contains_tp(target),
Self::Set(ts) => ts.iter().any(|t| t.contains_tp(target)),
Self::Dict(ts) => ts
.iter()
.any(|(k, v)| k.contains_tp(target) || v.contains_tp(target)),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().any(|(_, tp)| tp.contains_tp(target))
}
_ => false,
}
}
pub fn has_unbound_var(&self) -> bool {
match self {
Self::Type(t) => t.typ().has_unbound_var(),
Self::List(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.has_unbound_var()),
Self::UnsizedList(elem) => elem.has_unbound_var(),
Self::Set(ts) => ts.iter().any(|t| t.has_unbound_var()),
Self::Dict(ts) => ts
.iter()
.any(|(k, v)| k.has_unbound_var() || v.has_unbound_var()),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().any(|(_, tp)| tp.has_unbound_var())
}
_ => false,
}
}
pub fn has_undoable_linked_var(&self) -> bool {
match self {
Self::Type(t) => t.typ().has_undoable_linked_var(),
Self::List(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.has_undoable_linked_var()),
Self::UnsizedList(elem) => elem.has_undoable_linked_var(),
Self::Set(ts) => ts.iter().any(|t| t.has_undoable_linked_var()),
Self::Dict(ts) => ts
.iter()
.any(|(k, v)| k.has_undoable_linked_var() || v.has_undoable_linked_var()),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().any(|(_, tp)| tp.has_undoable_linked_var())
}
_ => false,
}
}
pub fn has_qvar(&self) -> bool {
match self {
Self::Type(t) => t.typ().has_qvar(),
Self::List(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.has_qvar()),
Self::UnsizedList(elem) => elem.has_qvar(),
Self::Set(ts) => ts.iter().any(|t| t.has_qvar()),
Self::Dict(ts) => ts.iter().any(|(k, v)| k.has_qvar() || v.has_qvar()),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().any(|(_, tp)| tp.has_qvar())
}
_ => false,
}
}
pub fn contains_tvar(&self, target: &FreeTyVar) -> bool {
match self {
Self::Type(t) => t.typ().contains_tvar(target),
Self::List(ts) | Self::Tuple(ts) => ts.iter().any(|t| t.contains_tvar(target)),
Self::UnsizedList(elem) => elem.contains_tvar(target),
Self::Set(ts) => ts.iter().any(|t| t.contains_tvar(target)),
Self::Dict(ts) => ts
.iter()
.any(|(k, v)| k.contains_tvar(target) || v.contains_tvar(target)),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().any(|(_, tp)| tp.contains_tvar(target))
}
_ => false,
}
}
pub fn qvars(&self) -> Set<(Str, Constraint)> {
match self {
Self::Type(t) => t.typ().qvars(),
Self::List(ts) | Self::Tuple(ts) => ts.iter().flat_map(|t| t.qvars()).collect(),
Self::UnsizedList(elem) => elem.qvars(),
Self::Set(ts) => ts.iter().flat_map(|t| t.qvars()).collect(),
Self::Dict(ts) => ts
.iter()
.flat_map(|(k, v)| k.qvars().concat(v.qvars()))
.collect(),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().flat_map(|(_, tp)| tp.qvars()).collect()
}
_ => Set::new(),
}
}
pub fn typarams(&self) -> Vec<TyParam> {
match self {
Self::Type(t) => t.typ().typarams(),
_ => Vec::new(),
}
}
pub fn contained_ts(&self) -> Set<Type> {
match self {
Self::Type(t) => t.typ().contained_ts(),
Self::List(ts) | Self::Tuple(ts) => ts.iter().flat_map(|t| t.contained_ts()).collect(),
Self::UnsizedList(elem) => elem.contained_ts(),
Self::Set(ts) => ts.iter().flat_map(|t| t.contained_ts()).collect(),
Self::Dict(ts) => ts
.iter()
.flat_map(|(k, v)| k.contained_ts().concat(v.contained_ts()))
.collect(),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().flat_map(|(_, tp)| tp.contained_ts()).collect()
}
_ => Set::new(),
}
}
pub fn dereference(&mut self) {
*self = std::mem::take(self).map_t(&mut |mut t| {
t.dereference();
t
});
}
pub fn variables(&self) -> Set<Str> {
match self {
Self::Type(t) => t.typ().variables(),
Self::List(ts) | Self::Tuple(ts) => ts.iter().flat_map(|t| t.variables()).collect(),
Self::UnsizedList(elem) => elem.variables(),
Self::Set(ts) => ts.iter().flat_map(|t| t.variables()).collect(),
Self::Dict(ts) => ts
.iter()
.flat_map(|(k, v)| k.variables().concat(v.variables()))
.collect(),
Self::Record(rec) | Self::DataClass { fields: rec, .. } => {
rec.iter().flat_map(|(_, tp)| tp.variables()).collect()
}
_ => Set::new(),
}
}
}
pub mod value_set {