feat: add RMul, RDiv

* `And` has the default type index
* impl `Dimension` traits
This commit is contained in:
Shunsuke Shibayama 2024-09-20 20:31:03 +09:00
parent 4651a383ae
commit ff53af0cb6
17 changed files with 323 additions and 118 deletions

View file

@ -56,7 +56,7 @@ fn comp_item_kind(t: &Type, muty: Mutability) -> CompletionItemKind {
CompletionItemKind::VARIABLE CompletionItemKind::VARIABLE
} }
} }
Type::And(tys) => { Type::And(tys, _) => {
for k in tys.iter().map(|t| comp_item_kind(t, muty)) { for k in tys.iter().map(|t| comp_item_kind(t, muty)) {
if k != CompletionItemKind::VARIABLE { if k != CompletionItemKind::VARIABLE {
return k; return k;

View file

@ -827,7 +827,7 @@ impl Context {
(lhs, Or(ors)) => ors.iter().all(|or| self.supertype_of(lhs, or)), (lhs, Or(ors)) => ors.iter().all(|or| self.supertype_of(lhs, or)),
// Hash and Eq :> HashEq and ... == true // Hash and Eq :> HashEq and ... == true
// Add(T) and Eq :> Add(Int) and Eq == true // Add(T) and Eq :> Add(Int) and Eq == true
(And(l), And(r)) => { (And(l, _), And(r, _)) => {
if r.iter().any(|r| l.iter().all(|l| self.supertype_of(l, r))) { if r.iter().any(|r| l.iter().all(|l| self.supertype_of(l, r))) {
return true; return true;
} }
@ -843,9 +843,9 @@ impl Context {
false false
} }
// (Num and Show) :> Show == false // (Num and Show) :> Show == false
(And(ands), rhs) => ands.iter().all(|and| self.supertype_of(and, rhs)), (And(ands, _), rhs) => ands.iter().all(|and| self.supertype_of(and, rhs)),
// Show :> (Num and Show) == true // Show :> (Num and Show) == true
(lhs, And(ands)) => ands.iter().any(|and| self.supertype_of(lhs, and)), (lhs, And(ands, _)) => ands.iter().any(|and| self.supertype_of(lhs, and)),
// Not(Eq) :> Float == !(Eq :> Float) == true // Not(Eq) :> Float == !(Eq :> Float) == true
(Not(_), Obj) => false, (Not(_), Obj) => false,
(Not(l), rhs) => !self.supertype_of(l, rhs), (Not(l), rhs) => !self.supertype_of(l, rhs),
@ -1097,6 +1097,23 @@ impl Context {
Variance::Covariant => self.supertype_of(sup, sub), Variance::Covariant => self.supertype_of(sup, sub),
Variance::Invariant => self.same_type_of(sup, sub), Variance::Invariant => self.same_type_of(sup, sub),
}, },
(TyParam::Type(sup), TyParam::Value(ValueObj::Type(sub))) => match variance {
Variance::Contravariant => self.subtype_of(sup, sub.typ()),
Variance::Covariant => self.supertype_of(sup, sub.typ()),
Variance::Invariant => self.same_type_of(sup, sub.typ()),
},
(TyParam::Value(ValueObj::Type(sup)), TyParam::Type(sub)) => match variance {
Variance::Contravariant => self.subtype_of(sup.typ(), sub),
Variance::Covariant => self.supertype_of(sup.typ(), sub),
Variance::Invariant => self.same_type_of(sup.typ(), sub),
},
(TyParam::Value(ValueObj::Type(sup)), TyParam::Value(ValueObj::Type(sub))) => {
match variance {
Variance::Contravariant => self.subtype_of(sup.typ(), sub.typ()),
Variance::Covariant => self.supertype_of(sup.typ(), sub.typ()),
Variance::Invariant => self.same_type_of(sup.typ(), sub.typ()),
}
}
( (
TyParam::App { name, args }, TyParam::App { name, args },
TyParam::App { TyParam::App {
@ -1485,7 +1502,7 @@ impl Context {
}, },
(other, or @ Or(_)) | (or @ Or(_), other) => self.union_add(or, other), (other, or @ Or(_)) | (or @ Or(_), other) => self.union_add(or, other),
// (A and B) or C ==> (A or C) and (B or C) // (A and B) or C ==> (A or C) and (B or C)
(And(ands), other) | (other, And(ands)) => { (And(ands, _), other) | (other, And(ands, _)) => {
let mut t = Type::Obj; let mut t = Type::Obj;
for branch in ands.iter() { for branch in ands.iter() {
let union = self.union(branch, other); let union = self.union(branch, other);
@ -1705,7 +1722,9 @@ impl Context {
(_, Not(r)) => self.diff(lhs, r), (_, Not(r)) => self.diff(lhs, r),
(Not(l), _) => self.diff(rhs, l), (Not(l), _) => self.diff(rhs, l),
// A and B and A == A and B // A and B and A == A and B
(other, and @ And(_)) | (and @ And(_), other) => self.intersection_add(and, other), (other, and @ And(_, _)) | (and @ And(_, _), other) => {
self.intersection_add(and, other)
}
// (A or B) and C == (A and C) or (B and C) // (A or B) and C == (A and C) or (B and C)
(Or(ors), other) | (other, Or(ors)) => { (Or(ors), other) | (other, Or(ors)) => {
if ors.iter().any(|t| t.has_unbound_var()) { if ors.iter().any(|t| t.has_unbound_var()) {
@ -2003,7 +2022,7 @@ impl Context {
Or(ors) => ors Or(ors) => ors
.iter() .iter()
.fold(Obj, |l, r| self.intersection(&l, &self.complement(r))), .fold(Obj, |l, r| self.intersection(&l, &self.complement(r))),
And(ands) => ands And(ands, _) => ands
.iter() .iter()
.fold(Never, |l, r| self.union(&l, &self.complement(r))), .fold(Never, |l, r| self.union(&l, &self.complement(r))),
other => not(other.clone()), other => not(other.clone()),

View file

@ -2285,7 +2285,7 @@ impl Context {
Err((t, errs)) Err((t, errs))
} }
} }
Type::And(ands) => { Type::And(ands, _) => {
let mut new_ands = set! {}; let mut new_ands = set! {};
for and in ands.into_iter() { for and in ands.into_iter() {
match self.eval_t_params(and, level, t_loc) { match self.eval_t_params(and, level, t_loc) {

View file

@ -289,13 +289,13 @@ impl Generalizer {
} }
proj_call(lhs, attr_name, args) proj_call(lhs, attr_name, args)
} }
And(ands) => { And(ands, idx) => {
// not `self.intersection` because types are generalized // not `self.intersection` because types are generalized
let ands = ands let ands = ands
.into_iter() .into_iter()
.map(|t| self.generalize_t(t, uninit)) .map(|t| self.generalize_t(t, uninit))
.collect(); .collect();
Type::checked_and(ands) Type::checked_and(ands, idx)
} }
Or(ors) => { Or(ors) => {
// not `self.union` because types are generalized // not `self.union` because types are generalized
@ -1049,7 +1049,7 @@ impl<'c, 'q, 'l, L: Locational> Dereferencer<'c, 'q, 'l, L> {
let pred = self.deref_pred(*refine.pred)?; let pred = self.deref_pred(*refine.pred)?;
Ok(refinement(refine.var, t, pred)) Ok(refinement(refine.var, t, pred))
} }
And(ands) => { And(ands, _) => {
let mut new_ands = vec![]; let mut new_ands = vec![];
for t in ands.into_iter() { for t in ands.into_iter() {
new_ands.push(self.deref_tyvar(t)?); new_ands.push(self.deref_tyvar(t)?);

View file

@ -116,7 +116,7 @@ impl Context {
return Some(hint); return Some(hint);
} }
} }
(Type::And(tys), found) if tys.len() == 2 => { (Type::And(tys, _), found) if tys.len() == 2 => {
let mut iter = tys.iter(); let mut iter = tys.iter();
let l = iter.next().unwrap(); let l = iter.next().unwrap();
let r = iter.next().unwrap(); let r = iter.next().unwrap();

View file

@ -4119,6 +4119,39 @@ impl Context {
Immutable, Immutable,
Visibility::BUILTIN_PUBLIC, Visibility::BUILTIN_PUBLIC,
); );
let mut dimension_to_float = Self::builtin_methods(Some(mono(TO_FLOAT)), 1);
dimension_to_float.register_builtin_erg_impl(
FUNDAMENTAL_FLOAT,
fn0_met(dimension_t.clone(), Float).quantify(),
Immutable,
Visibility::BUILTIN_PUBLIC,
);
dimension.register_trait_methods(dimension_t.clone(), dimension_to_float);
let mut dimension_to_int = Self::builtin_methods(Some(mono(TO_INT)), 1);
dimension_to_int.register_builtin_erg_impl(
FUNDAMENTAL_INT,
fn0_met(dimension_t.clone(), Int).quantify(),
Immutable,
Visibility::BUILTIN_PUBLIC,
);
dimension.register_trait_methods(dimension_t.clone(), dimension_to_int);
let mut dimension_eq = Self::builtin_methods(Some(mono(EQ)), 2);
let t = fn1_met(dimension_t.clone(), dimension_t.clone(), Bool).quantify();
dimension_eq.register_builtin_erg_impl(OP_EQ, t, Immutable, Visibility::BUILTIN_PUBLIC);
dimension.register_trait_methods(dimension_t.clone(), dimension_eq);
let mut dimension_partial_ord = Self::builtin_methods(Some(mono(PARTIAL_ORD)), 2);
dimension_partial_ord.register_builtin_erg_impl(
OP_PARTIAL_CMP,
fn1_met(
dimension_t.clone(),
dimension_t.clone(),
mono(ORDERING) | NoneType,
)
.quantify(),
Const,
Visibility::BUILTIN_PUBLIC,
);
dimension.register_trait_methods(dimension_t.clone(), dimension_partial_ord);
let mut dimension_add = let mut dimension_add =
Self::builtin_methods(Some(poly(ADD, vec![ty_tp(dimension_t.clone())])), 2); Self::builtin_methods(Some(poly(ADD, vec![ty_tp(dimension_t.clone())])), 2);
let t = fn1_met( let t = fn1_met(
@ -4181,6 +4214,17 @@ impl Context {
ValueObj::builtin_class(dimension_added_t), ValueObj::builtin_class(dimension_added_t),
); );
dimension.register_trait_methods(dimension_t.clone(), dimension_mul); dimension.register_trait_methods(dimension_t.clone(), dimension_mul);
let mut dimension_rmul =
Self::builtin_methods(Some(poly(RMUL, vec![ty_tp(Ty.clone())])), 2);
let t = fn1_met(dimension_t.clone(), Ty.clone(), dimension_t.clone()).quantify();
dimension_rmul.register_builtin_erg_impl(OP_RMUL, t, Immutable, Visibility::BUILTIN_PUBLIC);
dimension_rmul.register_builtin_const(
OUTPUT,
Visibility::BUILTIN_PUBLIC,
None,
ValueObj::builtin_class(dimension_t.clone()),
);
dimension.register_trait_methods(dimension_t.clone(), dimension_rmul);
let mut dimension_div = let mut dimension_div =
Self::builtin_methods(Some(poly(DIV, vec![ty_tp(dimension2_t.clone())])), 2); Self::builtin_methods(Some(poly(DIV, vec![ty_tp(dimension2_t.clone())])), 2);
let dimension_subtracted_t = poly( let dimension_subtracted_t = poly(
@ -4210,6 +4254,17 @@ impl Context {
ValueObj::builtin_class(dimension_subtracted_t), ValueObj::builtin_class(dimension_subtracted_t),
); );
dimension.register_trait_methods(dimension_t.clone(), dimension_div); dimension.register_trait_methods(dimension_t.clone(), dimension_div);
let mut dimension_rdiv =
Self::builtin_methods(Some(poly(RDIV, vec![ty_tp(Ty.clone())])), 2);
let t = fn1_met(dimension_t.clone(), Ty.clone(), dimension_t.clone()).quantify();
dimension_rdiv.register_builtin_erg_impl(OP_RDIV, t, Immutable, Visibility::BUILTIN_PUBLIC);
dimension_rdiv.register_builtin_const(
OUTPUT,
Visibility::BUILTIN_PUBLIC,
None,
ValueObj::builtin_class(dimension_t.clone()),
);
dimension.register_trait_methods(dimension_t.clone(), dimension_rdiv);
let mut base_exception = Self::builtin_mono_class(BASE_EXCEPTION, 2); let mut base_exception = Self::builtin_mono_class(BASE_EXCEPTION, 2);
base_exception.register_superclass(Obj, &obj); base_exception.register_superclass(Obj, &obj);
base_exception.register_builtin_erg_impl( base_exception.register_builtin_erg_impl(

View file

@ -1005,7 +1005,11 @@ impl Context {
Some(FUNC_SUB), Some(FUNC_SUB),
); );
let L = mono_q(TY_L, subtypeof(poly(MUL, params.clone()))); let L = mono_q(TY_L, subtypeof(poly(MUL, params.clone())));
let op_t = bin_op(L.clone(), R.clone(), proj(L, OUTPUT)).quantify(); let L2 = type_q(TY_L);
let R2 = mono_q(TY_R, subtypeof(poly(RMUL, vec![ty_tp(L2.clone())])));
let op_t = (bin_op(L.clone(), R.clone(), proj(L, OUTPUT)).quantify()
& bin_op(L2.clone(), R2.clone(), proj(R2, OUTPUT)).quantify())
.with_default_intersec_index(0);
self.register_builtin_py_impl( self.register_builtin_py_impl(
OP_MUL, OP_MUL,
op_t, op_t,
@ -1014,7 +1018,11 @@ impl Context {
Some(FUNC_MUL), Some(FUNC_MUL),
); );
let L = mono_q(TY_L, subtypeof(poly(DIV, params.clone()))); let L = mono_q(TY_L, subtypeof(poly(DIV, params.clone())));
let op_t = bin_op(L.clone(), R.clone(), proj(L, OUTPUT)).quantify(); let L2 = type_q(TY_L);
let R2 = mono_q(TY_R, subtypeof(poly(RDIV, vec![ty_tp(L2.clone())])));
let op_t = (bin_op(L.clone(), R.clone(), proj(L, OUTPUT)).quantify()
& bin_op(L2.clone(), R2.clone(), proj(R2, OUTPUT)).quantify())
.with_default_intersec_index(0);
self.register_builtin_py_impl( self.register_builtin_py_impl(
OP_DIV, OP_DIV,
op_t, op_t,

View file

@ -133,6 +133,8 @@ const ATTR_TRACEBACK: &str = "traceback";
const ADD: &str = "Add"; const ADD: &str = "Add";
const SUB: &str = "Sub"; const SUB: &str = "Sub";
const MUL: &str = "Mul"; const MUL: &str = "Mul";
const RMUL: &str = "RMul";
const RDIV: &str = "RDiv";
const DIV: &str = "Div"; const DIV: &str = "Div";
const FLOOR_DIV: &str = "FloorDiv"; const FLOOR_DIV: &str = "FloorDiv";
const POS: &str = "Pos"; const POS: &str = "Pos";
@ -564,6 +566,8 @@ const OP_SUB: &str = "__sub__";
const OP_MUL: &str = "__mul__"; const OP_MUL: &str = "__mul__";
const OP_DIV: &str = "__div__"; const OP_DIV: &str = "__div__";
const OP_FLOOR_DIV: &str = "__floordiv__"; const OP_FLOOR_DIV: &str = "__floordiv__";
const OP_RMUL: &str = "__rmul__";
const OP_RDIV: &str = "__rdiv__";
const OP_ABS: &str = "__abs__"; const OP_ABS: &str = "__abs__";
const OP_PARTIAL_CMP: &str = "__partial_cmp__"; const OP_PARTIAL_CMP: &str = "__partial_cmp__";
const OP_AND: &str = "__and__"; const OP_AND: &str = "__and__";

View file

@ -587,6 +587,23 @@ impl Context {
let op_t = fn0_met(_Slf.clone(), proj(_Slf, OUTPUT)).quantify(); let op_t = fn0_met(_Slf.clone(), proj(_Slf, OUTPUT)).quantify();
neg.register_builtin_erg_decl(OP_NEG, op_t, Visibility::BUILTIN_PUBLIC); neg.register_builtin_erg_decl(OP_NEG, op_t, Visibility::BUILTIN_PUBLIC);
neg.register_builtin_erg_decl(OUTPUT, Type, Visibility::BUILTIN_PUBLIC); neg.register_builtin_erg_decl(OUTPUT, Type, Visibility::BUILTIN_PUBLIC);
/* RMul */
let L = mono_q(TY_L, instanceof(Type));
let rparams = vec![PS::t(TY_L, false, WithDefault)];
let ty_rparams = vec![ty_tp(L.clone())];
let mut rmul = Self::builtin_poly_trait(RMUL, rparams.clone(), 2);
rmul.register_superclass(poly(OUTPUT, vec![ty_tp(L.clone())]), &output);
let RSlf = mono_q(SELF, subtypeof(poly(RMUL, ty_rparams.clone())));
let op_t = fn1_met(RSlf.clone(), L.clone(), proj(RSlf, OUTPUT)).quantify();
rmul.register_builtin_erg_decl(OP_RMUL, op_t, Visibility::BUILTIN_PUBLIC);
rmul.register_builtin_erg_decl(OUTPUT, Type, Visibility::BUILTIN_PUBLIC);
/* RDiv */
let mut rdiv = Self::builtin_poly_trait(RDIV, rparams.clone(), 2);
rdiv.register_superclass(poly(OUTPUT, vec![ty_tp(L.clone())]), &output);
let RSlf = mono_q(SELF, subtypeof(poly(RDIV, ty_rparams.clone())));
let op_t = fn1_met(RSlf.clone(), L.clone(), proj(RSlf, OUTPUT)).quantify();
rdiv.register_builtin_erg_decl(OP_RDIV, op_t, Visibility::BUILTIN_PUBLIC);
rdiv.register_builtin_erg_decl(OUTPUT, Type, Visibility::BUILTIN_PUBLIC);
/* Num */ /* Num */
let num = Self::builtin_mono_trait(NUM, 2); let num = Self::builtin_mono_trait(NUM, 2);
// num.register_superclass(poly(ADD, vec![]), &add); // num.register_superclass(poly(ADD, vec![]), &add);
@ -832,7 +849,15 @@ impl Context {
None, None,
); );
self.register_builtin_type(mono(POS), pos, vis.clone(), Const, Some(POS)); self.register_builtin_type(mono(POS), pos, vis.clone(), Const, Some(POS));
self.register_builtin_type(mono(NEG), neg, vis, Const, Some(NEG)); self.register_builtin_type(mono(NEG), neg, vis.clone(), Const, Some(NEG));
self.register_builtin_type(
poly(RMUL, ty_rparams.clone()),
rmul,
vis.clone(),
Const,
Some(RMUL),
);
self.register_builtin_type(poly(RDIV, ty_rparams), rdiv, vis.clone(), Const, Some(RDIV));
self.register_const_param_defaults( self.register_const_param_defaults(
ADD, ADD,
vec![ConstTemplate::Obj(ValueObj::builtin_type(Slf.clone()))], vec![ConstTemplate::Obj(ValueObj::builtin_type(Slf.clone()))],

View file

@ -1229,6 +1229,9 @@ impl Context {
} }
} }
} }
if let Some(default) = instance.default_intersection_type() {
return Ok(default.clone());
}
let Type::Subr(subr_t) = input_t else { let Type::Subr(subr_t) = input_t else {
unreachable!() unreachable!()
}; };
@ -1952,7 +1955,7 @@ impl Context {
res res
} }
} }
Type::And(_) => { Type::And(_, _) => {
let instance = self.resolve_overload( let instance = self.resolve_overload(
obj, obj,
instance.clone(), instance.clone(),
@ -2852,11 +2855,11 @@ impl Context {
pub(crate) fn type_params_variance(&self) -> Vec<Variance> { pub(crate) fn type_params_variance(&self) -> Vec<Variance> {
let match_tp_name = |tp: &TyParam, name: &VarName| -> bool { let match_tp_name = |tp: &TyParam, name: &VarName| -> bool {
if let Ok(free) = <&FreeTyParam>::try_from(tp) { if let Ok(free) = <&FreeTyParam>::try_from(tp) {
if let Some(prev) = free.get_previous() { if let Some(prev) = free.get_undoable_root() {
return prev.unbound_name().as_ref() == Some(name.inspect()); return prev.unbound_name().as_ref() == Some(name.inspect());
} }
} else if let Ok(free) = <&FreeTyVar>::try_from(tp) { } else if let Ok(free) = <&FreeTyVar>::try_from(tp) {
if let Some(prev) = free.get_previous() { if let Some(prev) = free.get_undoable_root() {
return prev.unbound_name().as_ref() == Some(name.inspect()); return prev.unbound_name().as_ref() == Some(name.inspect());
} }
} }
@ -3014,7 +3017,7 @@ impl Context {
self.get_nominal_super_type_ctxs(&Type) self.get_nominal_super_type_ctxs(&Type)
} }
} }
Type::And(tys) => { Type::And(tys, _) => {
let mut acc = vec![]; let mut acc = vec![];
for ctxs in tys for ctxs in tys
.iter() .iter()
@ -3366,7 +3369,7 @@ impl Context {
match trait_ { match trait_ {
// And(Add, Sub) == intersection({Int <: Add(Int), Bool <: Add(Bool) ...}, {Int <: Sub(Int), ...}) // And(Add, Sub) == intersection({Int <: Add(Int), Bool <: Add(Bool) ...}, {Int <: Sub(Int), ...})
// == {Int <: Add(Int) and Sub(Int), ...} // == {Int <: Add(Int) and Sub(Int), ...}
Type::And(tys) => { Type::And(tys, _) => {
let impls = tys let impls = tys
.iter() .iter()
.flat_map(|ty| self.get_trait_impls(ty)) .flat_map(|ty| self.get_trait_impls(ty))
@ -3956,7 +3959,7 @@ impl Context {
pub fn is_class(&self, typ: &Type) -> bool { pub fn is_class(&self, typ: &Type) -> bool {
match typ { match typ {
Type::And(_) => false, Type::And(_, _) => false,
Type::Never => true, Type::Never => true,
Type::FreeVar(fv) if fv.is_linked() => self.is_class(&fv.crack()), Type::FreeVar(fv) if fv.is_linked() => self.is_class(&fv.crack()),
Type::FreeVar(_) => false, Type::FreeVar(_) => false,
@ -3983,7 +3986,7 @@ impl Context {
Type::Never => false, Type::Never => false,
Type::FreeVar(fv) if fv.is_linked() => self.is_class(&fv.crack()), Type::FreeVar(fv) if fv.is_linked() => self.is_class(&fv.crack()),
Type::FreeVar(_) => false, Type::FreeVar(_) => false,
Type::And(tys) => tys.iter().any(|t| self.is_trait(t)), Type::And(tys, _) => tys.iter().any(|t| self.is_trait(t)),
Type::Or(tys) => tys.iter().all(|t| self.is_trait(t)), Type::Or(tys) => tys.iter().all(|t| self.is_trait(t)),
Type::Proj { lhs, rhs } => self Type::Proj { lhs, rhs } => self
.get_proj_candidates(lhs, rhs) .get_proj_candidates(lhs, rhs)

View file

@ -953,7 +953,7 @@ impl Context {
let t = self.instantiate_t_inner(*t, tmp_tv_cache, loc)?; let t = self.instantiate_t_inner(*t, tmp_tv_cache, loc)?;
Ok(t.structuralize()) Ok(t.structuralize())
} }
And(tys) => { And(tys, _) => {
let mut new_tys = vec![]; let mut new_tys = vec![];
for ty in tys.iter().cloned() { for ty in tys.iter().cloned() {
new_tys.push(self.instantiate_t_inner(ty, tmp_tv_cache, loc)?); new_tys.push(self.instantiate_t_inner(ty, tmp_tv_cache, loc)?);
@ -1004,7 +1004,7 @@ impl Context {
let t = fv.crack().clone(); let t = fv.crack().clone();
self.instantiate(t, callee) self.instantiate(t, callee)
} }
And(tys) => { And(tys, _idx) => {
let tys = tys let tys = tys
.into_iter() .into_iter()
.map(|t| self.instantiate(t, callee)) .map(|t| self.instantiate(t, callee))
@ -1036,7 +1036,7 @@ impl Context {
)?; )?;
} }
} }
Type::And(tys) => { Type::And(tys, _) => {
for ty in tys { for ty in tys {
if let Some(self_t) = ty.self_t() { if let Some(self_t) = ty.self_t() {
self.sub_unify( self.sub_unify(
@ -1068,7 +1068,7 @@ impl Context {
let t = fv.crack().clone(); let t = fv.crack().clone();
self.instantiate_dummy(t) self.instantiate_dummy(t)
} }
And(tys) => { And(tys, _) => {
let tys = tys let tys = tys
.into_iter() .into_iter()
.map(|t| self.instantiate_dummy(t)) .map(|t| self.instantiate_dummy(t))

View file

@ -158,7 +158,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
Ok(()) Ok(())
} }
// FIXME: This is not correct, we must visit all permutations of the types // FIXME: This is not correct, we must visit all permutations of the types
(And(l), And(r)) if l.len() == r.len() => { (And(l, _), And(r, _)) if l.len() == r.len() => {
let mut r = r.clone(); let mut r = r.clone();
for _ in 0..r.len() { for _ in 0..r.len() {
if l.iter() if l.iter()
@ -199,7 +199,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
self.ctx.caused_by(), self.ctx.caused_by(),
))) )))
} }
(lhs, And(tys)) => { (lhs, And(tys, _)) => {
for ty in tys.iter() { for ty in tys.iter() {
self.occur_inner(lhs, ty)?; self.occur_inner(lhs, ty)?;
} }
@ -211,7 +211,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
} }
Ok(()) Ok(())
} }
(And(tys), rhs) => { (And(tys, _), rhs) => {
for ty in tys.iter() { for ty in tys.iter() {
self.occur_inner(ty, rhs)?; self.occur_inner(ty, rhs)?;
} }
@ -322,7 +322,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
} }
Ok(()) Ok(())
} }
(lhs, And(tys)) => { (lhs, And(tys, _)) => {
for ty in tys.iter() { for ty in tys.iter() {
self.occur_inner(lhs, ty)?; self.occur_inner(lhs, ty)?;
} }
@ -334,7 +334,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
} }
Ok(()) Ok(())
} }
(And(tys), rhs) => { (And(tys, _), rhs) => {
for ty in tys.iter() { for ty in tys.iter() {
self.occur_inner(ty, rhs)?; self.occur_inner(ty, rhs)?;
} }
@ -1300,7 +1300,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
maybe_sup.update_tyvar(union, intersec, self.undoable, false); maybe_sup.update_tyvar(union, intersec, self.undoable, false);
} }
// TODO: Preferentially compare same-structure types (e.g. K(?T) <: K(?U)) // TODO: Preferentially compare same-structure types (e.g. K(?T) <: K(?U))
(And(ltys), And(rtys)) => { (And(ltys, _), And(rtys, _)) => {
let mut ltys_ = ltys.clone(); let mut ltys_ = ltys.clone();
let mut rtys_ = rtys.clone(); let mut rtys_ = rtys.clone();
// Show and EqHash and T <: Eq and Show and Ord // Show and EqHash and T <: Eq and Show and Ord
@ -1741,13 +1741,13 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
} }
} }
// X <: (Y and Z) is valid when X <: Y and X <: Z // X <: (Y and Z) is valid when X <: Y and X <: Z
(_, And(tys)) => { (_, And(tys, _)) => {
for ty in tys { for ty in tys {
self.sub_unify(maybe_sub, ty)?; self.sub_unify(maybe_sub, ty)?;
} }
} }
// (X and Y) <: Z is valid when X <: Z or Y <: Z // (X and Y) <: Z is valid when X <: Z or Y <: Z
(And(tys), _) => { (And(tys, _), _) => {
for ty in tys { for ty in tys {
if self.ctx.subtype_of(ty, maybe_sup) { if self.ctx.subtype_of(ty, maybe_sup) {
return self.sub_unify(ty, maybe_sup); return self.sub_unify(ty, maybe_sup);
@ -2022,7 +2022,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> {
return None; return None;
} }
} }
(And(tys), other) | (other, And(tys)) => { (And(tys, _), other) | (other, And(tys, _)) => {
let mut unified = Obj; let mut unified = Obj;
for ty in tys { for ty in tys {
if let Some(t) = self.unify(ty, other) { if let Some(t) = self.unify(ty, other) {

View file

@ -35,26 +35,49 @@ I = TypeVar("I", bound=int)
Θ = TypeVar("Θ", bound=int) Θ = TypeVar("Θ", bound=int)
N = TypeVar("N", bound=int) N = TypeVar("N", bound=int)
J = TypeVar("J", bound=int) J = TypeVar("J", bound=int)
class Dimension(float, Generic[Ty, M, L, T, I, Θ, N, J]): class Dimension(Generic[Ty, M, L, T, I, Θ, N, J]):
def value(self) -> float: val: float
return float(self) def __init__(self, val: float):
self.val = val
def __float__(self):
return float(self.val)
def __int__(self):
return int(self.val)
def __str__(self): def __str__(self):
return f"Dimension({float(self)})" return f"Dimension({self.val})"
def __add__(self, other): def __add__(self, other):
return Dimension(float(self) + other) return Dimension(self.val + other)
def __radd__(self, other):
return Dimension(other + self.val)
def __sub__(self, other): def __sub__(self, other):
return Dimension(float(self) - other) return Dimension(self.val - other)
def __rsub__(self, other):
return Dimension(other - self.val)
def __mul__(self, other): def __mul__(self, other):
return Dimension(float(self) * other) return Dimension(self.val * other)
def __rmul__(self, other): def __rmul__(self, other):
return Dimension(other * float(self)) return Dimension(other * self.val)
def __truediv__(self, other): def __truediv__(self, other):
return Dimension(float(self) / other) return Dimension(self.val / other)
def __floordiv__(self, other): def __floordiv__(self, other):
return Dimension(float(self) // other) return Dimension(self.val // other)
def __rtruediv__(self, other): def __rtruediv__(self, other):
return Dimension(other / float(self)) return Dimension(other / self.val)
def __rfloordiv__(self, other): def __rfloordiv__(self, other):
return Dimension(other // float(self)) return Dimension(other // self.val)
def __eq__(self, other):
return self.val == other.val
def __ne__(self, other):
return self.val != other.val
def __lt__(self, other):
return self.val < other.val
def __le__(self, other):
return self.val <= other.val
def __gt__(self, other):
return self.val > other.val
def __ge__(self, other):
return self.val >= other.val
def value(self):
return self.val
def type_check(self, t: type) -> bool: def type_check(self, t: type) -> bool:
return t.__name__ == "Dimension" return t.__name__ == "Dimension"

View file

@ -1490,7 +1490,7 @@ impl<A: ASTBuildable> GenericASTLowerer<A> {
} }
_ => {} _ => {}
}, },
Type::And(tys) => { Type::And(tys, _) => {
for ty in tys { for ty in tys {
self.push_guard(nth, kind, ty); self.push_guard(nth, kind, ty);
} }

View file

@ -545,6 +545,13 @@ impl<T> FreeKind<T> {
_ => {} _ => {}
} }
} }
pub fn get_previous(&self) -> Option<&FreeKind<T>> {
match self {
Self::UndoableLinked { previous, .. } => Some(previous),
_ => None,
}
}
} }
#[derive(Debug, Clone)] #[derive(Debug, Clone)]
@ -1208,6 +1215,20 @@ impl<T: Clone + Send + Sync + 'static> Free<T> {
.ok() .ok()
} }
pub fn get_undoable_root(&self) -> Option<Ref<FreeKind<T>>> {
let mut prev = Ref::map(self.get_previous()?, |f| f.as_ref());
loop {
match Ref::filter_map(prev, |f| f.get_previous()) {
Ok(p) => prev = p,
Err(p) => {
prev = p;
break;
}
}
}
Some(prev)
}
pub fn detach(&self) -> Self { pub fn detach(&self) -> Self {
match self.clone().unwrap_unbound() { match self.clone().unwrap_unbound() {
(Some(name), lev, constraint) => Self::new_named_unbound(name, lev, constraint), (Some(name), lev, constraint) => Self::new_named_unbound(name, lev, constraint),

View file

@ -1078,6 +1078,10 @@ impl RefinementType {
pub fn invert(self) -> Self { pub fn invert(self) -> Self {
Self::new(self.var, Type::Obj, !*self.pred) Self::new(self.var, Type::Obj, !*self.pred)
} }
pub fn map_t(self, f: &mut impl FnMut(Type) -> Type) -> Self {
Self::new(self.var, f(*self.t), *self.pred)
}
} }
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
@ -1356,7 +1360,8 @@ pub enum Type {
Refinement(RefinementType), Refinement(RefinementType),
// e.g. |T: Type| T -> T // e.g. |T: Type| T -> T
Quantified(Box<Type>), Quantified(Box<Type>),
And(Vec<Type>), /// usize: default type index
And(Vec<Type>, Option<usize>),
Or(Set<Type>), Or(Set<Type>),
Not(Box<Type>), Not(Box<Type>),
// NOTE: It was found that adding a new variant above `Poly` may cause a subtyping bug, // NOTE: It was found that adding a new variant above `Poly` may cause a subtyping bug,
@ -1450,7 +1455,7 @@ impl PartialEq for Type {
(Self::NamedTuple(lhs), Self::NamedTuple(rhs)) => lhs == rhs, (Self::NamedTuple(lhs), Self::NamedTuple(rhs)) => lhs == rhs,
(Self::Refinement(l), Self::Refinement(r)) => l == r, (Self::Refinement(l), Self::Refinement(r)) => l == r,
(Self::Quantified(l), Self::Quantified(r)) => l == r, (Self::Quantified(l), Self::Quantified(r)) => l == r,
(Self::And(l), Self::And(r)) => { (Self::And(l, _), Self::And(r, _)) => {
l.iter().collect::<Set<_>>().linear_eq(&r.iter().collect()) l.iter().collect::<Set<_>>().linear_eq(&r.iter().collect())
} }
(Self::Or(l), Self::Or(r)) => l.linear_eq(r), (Self::Or(l), Self::Or(r)) => l.linear_eq(r),
@ -1607,7 +1612,7 @@ impl LimitedDisplay for Type {
write!(f, "|")?; write!(f, "|")?;
quantified.limited_fmt(f, limit - 1) quantified.limited_fmt(f, limit - 1)
} }
Self::And(ands) => { Self::And(ands, _) => {
for (i, ty) in ands.iter().enumerate() { for (i, ty) in ands.iter().enumerate() {
if i > 0 { if i > 0 {
write!(f, " and ")?; write!(f, " and ")?;
@ -1802,18 +1807,18 @@ impl BitAnd for Type {
type Output = Self; type Output = Self;
fn bitand(self, rhs: Self) -> Self::Output { fn bitand(self, rhs: Self) -> Self::Output {
match (self, rhs) { match (self, rhs) {
(Self::And(l), Self::And(r)) => Self::And([l, r].concat()), (Self::And(l, _), Self::And(r, _)) => Self::And([l, r].concat(), None),
(Self::Obj, other) | (other, Self::Obj) => other, (Self::Obj, other) | (other, Self::Obj) => other,
(Self::Never, _) | (_, Self::Never) => Self::Never, (Self::Never, _) | (_, Self::Never) => Self::Never,
(Self::And(mut l), r) => { (Self::And(mut l, idx), r) => {
l.push(r); l.push(r);
Self::And(l) Self::And(l, idx)
} }
(l, Self::And(mut r)) => { (l, Self::And(mut r, idx)) => {
r.push(l); r.push(l);
Self::And(r) Self::And(r, idx)
} }
(l, r) => Self::checked_and(vec![l, r]), (l, r) => Self::checked_and(vec![l, r], None),
} }
} }
} }
@ -1949,7 +1954,7 @@ impl HasLevel for Type {
.filter_map(|o| *o) .filter_map(|o| *o)
.min() .min()
} }
Self::And(tys) => tys.iter().filter_map(|t| t.level()).min(), Self::And(tys, _) => tys.iter().filter_map(|t| t.level()).min(),
Self::Or(tys) => tys.iter().filter_map(|t| t.level()).min(), Self::Or(tys) => tys.iter().filter_map(|t| t.level()).min(),
Self::Not(ty) => ty.level(), Self::Not(ty) => ty.level(),
Self::Record(attrs) => attrs.values().filter_map(|t| t.level()).min(), Self::Record(attrs) => attrs.values().filter_map(|t| t.level()).min(),
@ -2031,7 +2036,7 @@ impl HasLevel for Type {
Self::Quantified(quant) => { Self::Quantified(quant) => {
quant.set_level(level); quant.set_level(level);
} }
Self::And(tys) => { Self::And(tys, _) => {
for t in tys.iter() { for t in tys.iter() {
t.set_level(level); t.set_level(level);
} }
@ -2190,7 +2195,7 @@ impl StructuralEq for Type {
(Self::Guard(l), Self::Guard(r)) => l.structural_eq(r), (Self::Guard(l), Self::Guard(r)) => l.structural_eq(r),
// NG: (l.structural_eq(l2) && r.structural_eq(r2)) // NG: (l.structural_eq(l2) && r.structural_eq(r2))
// || (l.structural_eq(r2) && r.structural_eq(l2)) // || (l.structural_eq(r2) && r.structural_eq(l2))
(Self::And(self_ands), Self::And(other_ands)) => { (Self::And(self_ands, _), Self::And(other_ands, _)) => {
let self_ands = self_ands.iter().collect::<Set<_>>(); let self_ands = self_ands.iter().collect::<Set<_>>();
let other_ands = other_ands.iter().collect::<Set<_>>(); let other_ands = other_ands.iter().collect::<Set<_>>();
if self_ands.len() != other_ands.len() { if self_ands.len() != other_ands.len() {
@ -2310,20 +2315,20 @@ impl Type {
} }
} }
pub fn checked_and(tys: Vec<Type>) -> Self { pub fn checked_and(tys: Vec<Type>, idx: Option<usize>) -> Self {
if tys.is_empty() { if tys.is_empty() {
panic!("tys is empty"); panic!("tys is empty");
} else if tys.len() == 1 { } else if tys.len() == 1 {
tys.into_iter().next().unwrap() tys.into_iter().next().unwrap()
} else { } else {
Self::And(tys) Self::And(tys, idx)
} }
} }
pub fn quantify(self) -> Self { pub fn quantify(self) -> Self {
debug_assert!(self.is_subr(), "{self} is not subr"); debug_assert!(self.is_subr(), "{self} is not subr");
match self { match self {
Self::And(tys) => Self::And(tys.into_iter().map(|t| t.quantify()).collect()), Self::And(tys, idx) => Self::And(tys.into_iter().map(|t| t.quantify()).collect(), idx),
other => Self::Quantified(Box::new(other)), other => Self::Quantified(Box::new(other)),
} }
} }
@ -2421,7 +2426,7 @@ impl Type {
Self::Quantified(t) => t.is_procedure(), Self::Quantified(t) => t.is_procedure(),
Self::Subr(subr) if subr.kind == SubrKind::Proc => true, Self::Subr(subr) if subr.kind == SubrKind::Proc => true,
Self::Refinement(refine) => refine.t.is_procedure(), Self::Refinement(refine) => refine.t.is_procedure(),
Self::And(tys) => tys.iter().any(|t| t.is_procedure()), Self::And(tys, _) => tys.iter().any(|t| t.is_procedure()),
_ => false, _ => false,
} }
} }
@ -2439,7 +2444,7 @@ impl Type {
name.ends_with('!') name.ends_with('!')
} }
Self::Refinement(refine) => refine.t.is_mut_type(), Self::Refinement(refine) => refine.t.is_mut_type(),
Self::And(tys) => tys.iter().any(|t| t.is_mut_type()), Self::And(tys, _) => tys.iter().any(|t| t.is_mut_type()),
_ => false, _ => false,
} }
} }
@ -2458,7 +2463,7 @@ impl Type {
Self::Poly { name, params, .. } if &name[..] == "Tuple" => params.is_empty(), Self::Poly { name, params, .. } if &name[..] == "Tuple" => params.is_empty(),
Self::Refinement(refine) => refine.t.is_nonelike(), Self::Refinement(refine) => refine.t.is_nonelike(),
Self::Bounded { sup, .. } => sup.is_nonelike(), Self::Bounded { sup, .. } => sup.is_nonelike(),
Self::And(tys) => tys.iter().any(|t| t.is_nonelike()), Self::And(tys, _) => tys.iter().any(|t| t.is_nonelike()),
_ => false, _ => false,
} }
} }
@ -2541,7 +2546,7 @@ impl Type {
pub fn is_intersection_type(&self) -> bool { pub fn is_intersection_type(&self) -> bool {
match self { match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_intersection_type(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_intersection_type(),
Self::And(_) => true, Self::And(_, _) => true,
Self::Refinement(refine) => refine.t.is_intersection_type(), Self::Refinement(refine) => refine.t.is_intersection_type(),
_ => false, _ => false,
} }
@ -2559,7 +2564,7 @@ impl Type {
Self::Refinement(refine) => refine.t.union_size(), Self::Refinement(refine) => refine.t.union_size(),
Self::Ref(t) => t.union_size(), Self::Ref(t) => t.union_size(),
Self::RefMut { before, after: _ } => before.union_size(), Self::RefMut { before, after: _ } => before.union_size(),
Self::And(tys) => tys.iter().map(|ty| ty.union_size()).max().unwrap_or(1), Self::And(tys, _) => tys.iter().map(|ty| ty.union_size()).max().unwrap_or(1),
Self::Not(ty) => ty.union_size(), Self::Not(ty) => ty.union_size(),
Self::Callable { param_ts, return_t } => param_ts Self::Callable { param_ts, return_t } => param_ts
.iter() .iter()
@ -2600,7 +2605,7 @@ impl Type {
match self { match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_refinement(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_refinement(),
Self::Refinement(_) => true, Self::Refinement(_) => true,
Self::And(tys) => tys.iter().any(|t| t.is_refinement()), Self::And(tys, _) => tys.iter().any(|t| t.is_refinement()),
_ => false, _ => false,
} }
} }
@ -2609,7 +2614,7 @@ impl Type {
match self { match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_singleton_refinement(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_singleton_refinement(),
Self::Refinement(refine) => matches!(refine.pred.as_ref(), Predicate::Equal { .. }), Self::Refinement(refine) => matches!(refine.pred.as_ref(), Predicate::Equal { .. }),
Self::And(tys) => tys.iter().any(|t| t.is_singleton_refinement()), Self::And(tys, _) => tys.iter().any(|t| t.is_singleton_refinement()),
_ => false, _ => false,
} }
} }
@ -2619,7 +2624,7 @@ impl Type {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_record(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_record(),
Self::Record(_) => true, Self::Record(_) => true,
Self::Refinement(refine) => refine.t.is_record(), Self::Refinement(refine) => refine.t.is_record(),
Self::And(tys) => tys.iter().any(|t| t.is_record()), Self::And(tys, _) => tys.iter().any(|t| t.is_record()),
_ => false, _ => false,
} }
} }
@ -2633,7 +2638,7 @@ impl Type {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_erg_module(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_erg_module(),
Self::Refinement(refine) => refine.t.is_erg_module(), Self::Refinement(refine) => refine.t.is_erg_module(),
Self::Poly { name, .. } => &name[..] == "Module", Self::Poly { name, .. } => &name[..] == "Module",
Self::And(tys) => tys.iter().any(|t| t.is_erg_module()), Self::And(tys, _) => tys.iter().any(|t| t.is_erg_module()),
_ => false, _ => false,
} }
} }
@ -2643,7 +2648,7 @@ impl Type {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_py_module(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_py_module(),
Self::Refinement(refine) => refine.t.is_py_module(), Self::Refinement(refine) => refine.t.is_py_module(),
Self::Poly { name, .. } => &name[..] == "PyModule", Self::Poly { name, .. } => &name[..] == "PyModule",
Self::And(tys) => tys.iter().any(|t| t.is_py_module()), Self::And(tys, _) => tys.iter().any(|t| t.is_py_module()),
_ => false, _ => false,
} }
} }
@ -2654,7 +2659,7 @@ impl Type {
Self::Refinement(refine) => refine.t.is_method(), Self::Refinement(refine) => refine.t.is_method(),
Self::Subr(subr) => subr.is_method(), Self::Subr(subr) => subr.is_method(),
Self::Quantified(quant) => quant.is_method(), Self::Quantified(quant) => quant.is_method(),
Self::And(tys) => tys.iter().any(|t| t.is_method()), Self::And(tys, _) => tys.iter().any(|t| t.is_method()),
_ => false, _ => false,
} }
} }
@ -2665,7 +2670,7 @@ impl Type {
Self::Subr(_) => true, Self::Subr(_) => true,
Self::Quantified(quant) => quant.is_subr(), Self::Quantified(quant) => quant.is_subr(),
Self::Refinement(refine) => refine.t.is_subr(), Self::Refinement(refine) => refine.t.is_subr(),
Self::And(tys) => tys.iter().any(|t| t.is_subr()), Self::And(tys, _) => tys.iter().any(|t| t.is_subr()),
_ => false, _ => false,
} }
} }
@ -2676,7 +2681,7 @@ impl Type {
Self::Subr(subr) => Some(subr.kind), Self::Subr(subr) => Some(subr.kind),
Self::Refinement(refine) => refine.t.subr_kind(), Self::Refinement(refine) => refine.t.subr_kind(),
Self::Quantified(quant) => quant.subr_kind(), Self::Quantified(quant) => quant.subr_kind(),
Self::And(tys) => tys Self::And(tys, _) => tys
.iter() .iter()
.filter_map(|t| t.subr_kind()) .filter_map(|t| t.subr_kind())
.fold(None, |a, b| Some(a? | b)), .fold(None, |a, b| Some(a? | b)),
@ -2689,7 +2694,7 @@ impl Type {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_quantified_subr(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_quantified_subr(),
Self::Quantified(_) => true, Self::Quantified(_) => true,
Self::Refinement(refine) => refine.t.is_quantified_subr(), Self::Refinement(refine) => refine.t.is_quantified_subr(),
Self::And(tys) => tys.iter().any(|t| t.is_quantified_subr()), Self::And(tys, _) => tys.iter().any(|t| t.is_quantified_subr()),
_ => false, _ => false,
} }
} }
@ -2726,7 +2731,7 @@ impl Type {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_iterable(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_iterable(),
Self::Poly { name, .. } => &name[..] == "Iterable", Self::Poly { name, .. } => &name[..] == "Iterable",
Self::Refinement(refine) => refine.t.is_iterable(), Self::Refinement(refine) => refine.t.is_iterable(),
Self::And(tys) => tys.iter().any(|t| t.is_iterable()), Self::And(tys, _) => tys.iter().any(|t| t.is_iterable()),
_ => false, _ => false,
} }
} }
@ -2817,7 +2822,7 @@ impl Type {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_structural(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_structural(),
Self::Structural(_) => true, Self::Structural(_) => true,
Self::Refinement(refine) => refine.t.is_structural(), Self::Refinement(refine) => refine.t.is_structural(),
Self::And(tys) => tys.iter().any(|t| t.is_structural()), Self::And(tys, _) => tys.iter().any(|t| t.is_structural()),
_ => false, _ => false,
} }
} }
@ -2827,7 +2832,7 @@ impl Type {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_failure(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_failure(),
Self::Refinement(refine) => refine.t.is_failure(), Self::Refinement(refine) => refine.t.is_failure(),
Self::Failure => true, Self::Failure => true,
Self::And(tys) => tys.iter().any(|t| t.is_failure()), Self::And(tys, _) => tys.iter().any(|t| t.is_failure()),
_ => false, _ => false,
} }
} }
@ -2922,7 +2927,7 @@ impl Type {
Self::ProjCall { lhs, args, .. } => { Self::ProjCall { lhs, args, .. } => {
lhs.has_type_satisfies(f) || args.iter().any(|tp| tp.has_type_satisfies(f)) lhs.has_type_satisfies(f) || args.iter().any(|tp| tp.has_type_satisfies(f))
} }
Self::And(tys) => tys.iter().any(f), Self::And(tys, _) => tys.iter().any(f),
Self::Or(tys) => tys.iter().any(f), Self::Or(tys) => tys.iter().any(f),
Self::Not(t) => f(t), Self::Not(t) => f(t),
Self::Ref(t) => f(t), Self::Ref(t) => f(t),
@ -2991,7 +2996,7 @@ impl Type {
Self::ProjCall { lhs, args, .. } => { Self::ProjCall { lhs, args, .. } => {
lhs.contains_type(target) || args.iter().any(|t| t.contains_type(target)) lhs.contains_type(target) || args.iter().any(|t| t.contains_type(target))
} }
Self::And(tys) => tys.iter().any(|t| t.contains_type(target)), Self::And(tys, _) => tys.iter().any(|t| t.contains_type(target)),
Self::Or(tys) => tys.iter().any(|t| t.contains_type(target)), Self::Or(tys) => tys.iter().any(|t| t.contains_type(target)),
Self::Not(t) => t.contains_type(target), Self::Not(t) => t.contains_type(target),
Self::Ref(t) => t.contains_type(target), Self::Ref(t) => t.contains_type(target),
@ -3029,7 +3034,7 @@ impl Type {
Self::ProjCall { lhs, args, .. } => { Self::ProjCall { lhs, args, .. } => {
lhs.contains_tp(target) || args.iter().any(|t| t.contains_tp(target)) lhs.contains_tp(target) || args.iter().any(|t| t.contains_tp(target))
} }
Self::And(tys) => tys.iter().any(|t| t.contains_tp(target)), Self::And(tys, _) => tys.iter().any(|t| t.contains_tp(target)),
Self::Or(tys) => tys.iter().any(|t| t.contains_tp(target)), Self::Or(tys) => tys.iter().any(|t| t.contains_tp(target)),
Self::Not(t) => t.contains_tp(target), Self::Not(t) => t.contains_tp(target),
Self::Ref(t) => t.contains_tp(target), Self::Ref(t) => t.contains_tp(target),
@ -3063,7 +3068,7 @@ impl Type {
Self::ProjCall { lhs, args, .. } => { Self::ProjCall { lhs, args, .. } => {
lhs.contains_value(target) || args.iter().any(|t| t.contains_value(target)) lhs.contains_value(target) || args.iter().any(|t| t.contains_value(target))
} }
Self::And(tys) => tys.iter().any(|t| t.contains_value(target)), Self::And(tys, _) => tys.iter().any(|t| t.contains_value(target)),
Self::Or(tys) => tys.iter().any(|t| t.contains_value(target)), Self::Or(tys) => tys.iter().any(|t| t.contains_value(target)),
Self::Not(t) => t.contains_value(target), Self::Not(t) => t.contains_value(target),
Self::Ref(t) => t.contains_value(target), Self::Ref(t) => t.contains_value(target),
@ -3107,7 +3112,7 @@ impl Type {
Self::ProjCall { lhs, args, .. } => { Self::ProjCall { lhs, args, .. } => {
lhs.contains_type(self) || args.iter().any(|t| t.contains_type(self)) lhs.contains_type(self) || args.iter().any(|t| t.contains_type(self))
} }
Self::And(tys) => tys.iter().any(|t| t.contains_type(self)), Self::And(tys, _) => tys.iter().any(|t| t.contains_type(self)),
Self::Or(tys) => tys.iter().any(|t| t.contains_type(self)), Self::Or(tys) => tys.iter().any(|t| t.contains_type(self)),
Self::Not(t) => t.contains_type(self), Self::Not(t) => t.contains_type(self),
Self::Ref(t) => t.contains_type(self), Self::Ref(t) => t.contains_type(self),
@ -3178,7 +3183,7 @@ impl Type {
Self::Inf => Str::ever("Inf"), Self::Inf => Str::ever("Inf"),
Self::NegInf => Str::ever("NegInf"), Self::NegInf => Str::ever("NegInf"),
Self::Mono(name) => name.clone(), Self::Mono(name) => name.clone(),
Self::And(_) => Str::ever("And"), Self::And(_, _) => Str::ever("And"),
Self::Not(_) => Str::ever("Not"), Self::Not(_) => Str::ever("Not"),
Self::Or(_) => Str::ever("Or"), Self::Or(_) => Str::ever("Or"),
Self::Ref(_) => Str::ever("Ref"), Self::Ref(_) => Str::ever("Ref"),
@ -3270,7 +3275,7 @@ impl Type {
match self { match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().contains_intersec(typ), Self::FreeVar(fv) if fv.is_linked() => fv.crack().contains_intersec(typ),
Self::Refinement(refine) => refine.t.contains_intersec(typ), Self::Refinement(refine) => refine.t.contains_intersec(typ),
Self::And(tys) => tys.iter().any(|t| t.contains_intersec(typ)), Self::And(tys, _) => tys.iter().any(|t| t.contains_intersec(typ)),
_ => self == typ, _ => self == typ,
} }
} }
@ -3321,11 +3326,35 @@ impl Type {
.into_iter() .into_iter()
.map(|t| t.quantify()) .map(|t| t.quantify())
.collect(), .collect(),
Type::And(tys) => tys.clone(), Type::And(tys, _) => tys.clone(),
_ => vec![self.clone()], _ => vec![self.clone()],
} }
} }
pub fn default_intersection_type(&self) -> Option<Type> {
match self {
Type::FreeVar(fv) if fv.is_linked() => fv.crack().default_intersection_type(),
Type::Refinement(refine) => refine.t.default_intersection_type(),
Type::Quantified(tys) => tys.default_intersection_type().map(|t| t.quantify()),
Type::And(tys, idx) => idx.and_then(|idx| tys.get(idx).cloned()),
_ => None,
}
}
pub fn with_default_intersec_index(self, idx: usize) -> Self {
match self {
Type::FreeVar(fv) if fv.is_linked() => {
fv.unwrap_linked().with_default_intersec_index(idx)
}
Type::And(tys, _) => Type::And(tys, Some(idx)),
Type::Quantified(tys) => tys.with_default_intersec_index(idx).quantify(),
Type::Refinement(refine) => {
Type::Refinement(refine.map_t(&mut |t| t.with_default_intersec_index(idx)))
}
_ => self,
}
}
pub fn tvar_name(&self) -> Option<Str> { pub fn tvar_name(&self) -> Option<Str> {
match self { match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().tvar_name(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().tvar_name(),
@ -3397,7 +3426,7 @@ impl Type {
match self { match self {
Self::FreeVar(fv) if fv.is_unbound() => true, Self::FreeVar(fv) if fv.is_unbound() => true,
Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_totally_unbound(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_totally_unbound(),
Self::And(tys) => tys.iter().all(|t| t.is_totally_unbound()), Self::And(tys, _) => tys.iter().all(|t| t.is_totally_unbound()),
Self::Or(tys) => tys.iter().all(|t| t.is_totally_unbound()), Self::Or(tys) => tys.iter().all(|t| t.is_totally_unbound()),
Self::Not(t) => t.is_totally_unbound(), Self::Not(t) => t.is_totally_unbound(),
_ => false, _ => false,
@ -3509,7 +3538,7 @@ impl Type {
sub.destructive_coerce(); sub.destructive_coerce();
self.destructive_link(&sub); self.destructive_link(&sub);
} }
Type::And(tys) => { Type::And(tys, _) => {
for t in tys { for t in tys {
t.destructive_coerce(); t.destructive_coerce();
} }
@ -3570,7 +3599,7 @@ impl Type {
sub.undoable_coerce(list); sub.undoable_coerce(list);
self.undoable_link(&sub, list); self.undoable_link(&sub, list);
} }
Type::And(tys) => { Type::And(tys, _) => {
for t in tys { for t in tys {
t.undoable_coerce(list); t.undoable_coerce(list);
} }
@ -3637,7 +3666,7 @@ impl Type {
.map(|t| t.qvars_inner()) .map(|t| t.qvars_inner())
.unwrap_or_else(|| set! {}), .unwrap_or_else(|| set! {}),
), ),
Self::And(tys) => tys Self::And(tys, _) => tys
.iter() .iter()
.fold(set! {}, |acc, t| acc.concat(t.qvars_inner())), .fold(set! {}, |acc, t| acc.concat(t.qvars_inner())),
Self::Or(tys) => tys Self::Or(tys) => tys
@ -3785,7 +3814,7 @@ impl Type {
Self::Refinement(refine) => refine.t.typarams_len(), Self::Refinement(refine) => refine.t.typarams_len(),
// REVIEW: // REVIEW:
Self::Ref(_) | Self::RefMut { .. } => Some(1), Self::Ref(_) | Self::RefMut { .. } => Some(1),
Self::And(tys) => Some(tys.len()), Self::And(tys, _) => Some(tys.len()),
Self::Or(tys) => Some(tys.len()), Self::Or(tys) => Some(tys.len()),
Self::Not(_) => Some(1), Self::Not(_) => Some(1),
Self::Subr(subr) => Some( Self::Subr(subr) => Some(
@ -3852,7 +3881,7 @@ impl Type {
Self::FreeVar(_unbound) => vec![], Self::FreeVar(_unbound) => vec![],
Self::Refinement(refine) => refine.t.typarams(), Self::Refinement(refine) => refine.t.typarams(),
Self::Ref(t) | Self::RefMut { before: t, .. } => vec![TyParam::t(*t.clone())], Self::Ref(t) | Self::RefMut { before: t, .. } => vec![TyParam::t(*t.clone())],
Self::And(tys) => tys.iter().cloned().map(TyParam::t).collect(), Self::And(tys, _) => tys.iter().cloned().map(TyParam::t).collect(),
Self::Or(tys) => tys.iter().cloned().map(TyParam::t).collect(), Self::Or(tys) => tys.iter().cloned().map(TyParam::t).collect(),
Self::Not(t) => vec![TyParam::t(*t.clone())], Self::Not(t) => vec![TyParam::t(*t.clone())],
Self::Subr(subr) => subr.typarams(), Self::Subr(subr) => subr.typarams(),
@ -4074,7 +4103,9 @@ impl Type {
let r = r.iter().map(|(k, v)| (k.clone(), v.derefine())).collect(); let r = r.iter().map(|(k, v)| (k.clone(), v.derefine())).collect();
Self::NamedTuple(r) Self::NamedTuple(r)
} }
Self::And(tys) => Self::checked_and(tys.iter().map(|t| t.derefine()).collect()), Self::And(tys, idx) => {
Self::checked_and(tys.iter().map(|t| t.derefine()).collect(), *idx)
}
Self::Or(tys) => Self::checked_or(tys.iter().map(|t| t.derefine()).collect()), Self::Or(tys) => Self::checked_or(tys.iter().map(|t| t.derefine()).collect()),
Self::Not(ty) => !ty.derefine(), Self::Not(ty) => !ty.derefine(),
Self::Proj { lhs, rhs } => lhs.derefine().proj(rhs.clone()), Self::Proj { lhs, rhs } => lhs.derefine().proj(rhs.clone()),
@ -4148,7 +4179,7 @@ impl Type {
}); });
self self
} }
Self::And(tys) => Self::checked_and( Self::And(tys, idx) => Self::checked_and(
tys.into_iter() tys.into_iter()
.filter_map(|t| { .filter_map(|t| {
if t.addr_eq(target) { if t.addr_eq(target) {
@ -4158,6 +4189,7 @@ impl Type {
} }
}) })
.collect(), .collect(),
idx,
), ),
Self::Or(tys) => Self::checked_or( Self::Or(tys) => Self::checked_or(
tys.into_iter() tys.into_iter()
@ -4224,11 +4256,12 @@ impl Type {
before: Box::new(before.eliminate_recursion(target)), before: Box::new(before.eliminate_recursion(target)),
after: after.map(|t| Box::new(t.eliminate_recursion(target))), after: after.map(|t| Box::new(t.eliminate_recursion(target))),
}, },
Self::And(tys) => Self::checked_and( Self::And(tys, idx) => Self::checked_and(
tys.into_iter() tys.into_iter()
.filter(|t| !t.addr_eq(target)) .filter(|t| !t.addr_eq(target))
.map(|t| t.eliminate_recursion(target)) .map(|t| t.eliminate_recursion(target))
.collect(), .collect(),
idx,
), ),
Self::Or(tys) => Self::checked_or( Self::Or(tys) => Self::checked_or(
tys.into_iter() tys.into_iter()
@ -4262,9 +4295,10 @@ impl Type {
pub(crate) fn eliminate_and_or_recursion(self, target: &Type) -> Self { pub(crate) fn eliminate_and_or_recursion(self, target: &Type) -> Self {
match self { match self {
Self::And(tys) => { Self::And(tys, idx) => Self::checked_and(
Self::checked_and(tys.into_iter().filter(|t| !t.addr_eq(target)).collect()) tys.into_iter().filter(|t| !t.addr_eq(target)).collect(),
} idx,
),
Self::Or(tys) => { Self::Or(tys) => {
Self::checked_or(tys.into_iter().filter(|t| !t.addr_eq(target)).collect()) Self::checked_or(tys.into_iter().filter(|t| !t.addr_eq(target)).collect())
} }
@ -4400,7 +4434,9 @@ impl Type {
before: Box::new(before.map(f)), before: Box::new(before.map(f)),
after: after.map(|t| Box::new(t.map(f))), after: after.map(|t| Box::new(t.map(f))),
}, },
Self::And(tys) => Self::checked_and(tys.into_iter().map(|t| t.map(f)).collect()), Self::And(tys, idx) => {
Self::checked_and(tys.into_iter().map(|t| t.map(f)).collect(), idx)
}
Self::Or(tys) => Self::checked_or(tys.into_iter().map(|t| t.map(f)).collect()), Self::Or(tys) => Self::checked_or(tys.into_iter().map(|t| t.map(f)).collect()),
Self::Not(ty) => !ty.map(f), Self::Not(ty) => !ty.map(f),
Self::Proj { lhs, rhs } => lhs.map(f).proj(rhs), Self::Proj { lhs, rhs } => lhs.map(f).proj(rhs),
@ -4494,9 +4530,10 @@ impl Type {
before: Box::new(before._replace_tp(target, to)), before: Box::new(before._replace_tp(target, to)),
after: after.map(|t| Box::new(t._replace_tp(target, to))), after: after.map(|t| Box::new(t._replace_tp(target, to))),
}, },
Self::And(tys) => { Self::And(tys, idx) => Self::checked_and(
Self::checked_and(tys.into_iter().map(|t| t._replace_tp(target, to)).collect()) tys.into_iter().map(|t| t._replace_tp(target, to)).collect(),
} idx,
),
Self::Or(tys) => { Self::Or(tys) => {
Self::checked_or(tys.into_iter().map(|t| t._replace_tp(target, to)).collect()) Self::checked_or(tys.into_iter().map(|t| t._replace_tp(target, to)).collect())
} }
@ -4575,7 +4612,9 @@ impl Type {
before: Box::new(before.map_tp(f)), before: Box::new(before.map_tp(f)),
after: after.map(|t| Box::new(t.map_tp(f))), after: after.map(|t| Box::new(t.map_tp(f))),
}, },
Self::And(tys) => Self::checked_and(tys.into_iter().map(|t| t.map_tp(f)).collect()), Self::And(tys, idx) => {
Self::checked_and(tys.into_iter().map(|t| t.map_tp(f)).collect(), idx)
}
Self::Or(tys) => Self::checked_or(tys.into_iter().map(|t| t.map_tp(f)).collect()), Self::Or(tys) => Self::checked_or(tys.into_iter().map(|t| t.map_tp(f)).collect()),
Self::Not(ty) => !ty.map_tp(f), Self::Not(ty) => !ty.map_tp(f),
Self::Proj { lhs, rhs } => lhs.map_tp(f).proj(rhs), Self::Proj { lhs, rhs } => lhs.map_tp(f).proj(rhs),
@ -4664,10 +4703,11 @@ impl Type {
after, after,
}) })
} }
Self::And(tys) => Ok(Self::checked_and( Self::And(tys, idx) => Ok(Self::checked_and(
tys.into_iter() tys.into_iter()
.map(|t| t.try_map_tp(f)) .map(|t| t.try_map_tp(f))
.collect::<Result<_, _>>()?, .collect::<Result<_, _>>()?,
idx,
)), )),
Self::Or(tys) => Ok(Self::checked_or( Self::Or(tys) => Ok(Self::checked_or(
tys.into_iter() tys.into_iter()
@ -4706,10 +4746,11 @@ impl Type {
*refine.t = refine.t.replace_param(target, to); *refine.t = refine.t.replace_param(target, to);
Self::Refinement(refine) Self::Refinement(refine)
} }
Self::And(tys) => Self::And( Self::And(tys, idx) => Self::And(
tys.into_iter() tys.into_iter()
.map(|t| t.replace_param(target, to)) .map(|t| t.replace_param(target, to))
.collect(), .collect(),
idx,
), ),
Self::Guard(guard) => Self::Guard(guard.replace_param(target, to)), Self::Guard(guard) => Self::Guard(guard.replace_param(target, to)),
_ => self, _ => self,
@ -4718,7 +4759,7 @@ impl Type {
pub fn eliminate_and_or(&mut self) { pub fn eliminate_and_or(&mut self) {
match self { match self {
Self::And(tys) if tys.len() == 1 => { Self::And(tys, _) if tys.len() == 1 => {
*self = tys.remove(0); *self = tys.remove(0);
} }
Self::Or(tys) if tys.len() == 1 => { Self::Or(tys) if tys.len() == 1 => {
@ -4795,7 +4836,9 @@ impl Type {
} }
Self::NamedTuple(r) Self::NamedTuple(r)
} }
Self::And(tys) => Self::checked_and(tys.into_iter().map(|t| t.normalize()).collect()), Self::And(tys, idx) => {
Self::checked_and(tys.into_iter().map(|t| t.normalize()).collect(), idx)
}
Self::Or(tys) => Self::checked_or(tys.into_iter().map(|t| t.normalize()).collect()), Self::Or(tys) => Self::checked_or(tys.into_iter().map(|t| t.normalize()).collect()),
Self::Not(ty) => !ty.normalize(), Self::Not(ty) => !ty.normalize(),
Self::Structural(ty) => ty.normalize().structuralize(), Self::Structural(ty) => ty.normalize().structuralize(),
@ -4828,8 +4871,8 @@ impl Type {
free.get_sub().unwrap_or(self.clone()) free.get_sub().unwrap_or(self.clone())
} else { } else {
match self { match self {
Self::And(tys) => { Self::And(tys, idx) => {
Self::checked_and(tys.iter().map(|t| t.lower_bounded()).collect()) Self::checked_and(tys.iter().map(|t| t.lower_bounded()).collect(), *idx)
} }
Self::Or(tys) => Self::checked_or(tys.iter().map(|t| t.lower_bounded()).collect()), Self::Or(tys) => Self::checked_or(tys.iter().map(|t| t.lower_bounded()).collect()),
Self::Not(ty) => !ty.lower_bounded(), Self::Not(ty) => !ty.lower_bounded(),
@ -4848,8 +4891,8 @@ impl Type {
free.get_super().unwrap_or(self.clone()) free.get_super().unwrap_or(self.clone())
} else { } else {
match self { match self {
Self::And(tys) => { Self::And(tys, idx) => {
Self::checked_and(tys.iter().map(|t| t.upper_bounded()).collect()) Self::checked_and(tys.iter().map(|t| t.upper_bounded()).collect(), *idx)
} }
Self::Or(tys) => Self::checked_or(tys.iter().map(|t| t.upper_bounded()).collect()), Self::Or(tys) => Self::checked_or(tys.iter().map(|t| t.upper_bounded()).collect()),
Self::Not(ty) => !ty.upper_bounded(), Self::Not(ty) => !ty.upper_bounded(),
@ -5024,7 +5067,7 @@ impl Type {
match self { match self {
Self::FreeVar(fv) if fv.is_linked() => fv.crack().ands(), Self::FreeVar(fv) if fv.is_linked() => fv.crack().ands(),
Self::Refinement(refine) => refine.t.ands(), Self::Refinement(refine) => refine.t.ands(),
Self::And(tys) => tys.clone(), Self::And(tys, _) => tys.clone(),
_ => vec![self.clone()], _ => vec![self.clone()],
} }
} }
@ -5082,7 +5125,7 @@ impl Type {
Self::Callable { param_ts, .. } => { Self::Callable { param_ts, .. } => {
param_ts.iter().flat_map(|t| t.contained_ts()).collect() param_ts.iter().flat_map(|t| t.contained_ts()).collect()
} }
Self::And(tys) => tys.iter().flat_map(|t| t.contained_ts()).collect(), Self::And(tys, _) => tys.iter().flat_map(|t| t.contained_ts()).collect(),
Self::Or(tys) => tys.iter().flat_map(|t| t.contained_ts()).collect(), Self::Or(tys) => tys.iter().flat_map(|t| t.contained_ts()).collect(),
Self::Not(t) => t.contained_ts(), Self::Not(t) => t.contained_ts(),
Self::Bounded { sub, sup } => sub.contained_ts().union(&sup.contained_ts()), Self::Bounded { sub, sup } => sub.contained_ts().union(&sup.contained_ts()),
@ -5152,7 +5195,7 @@ impl Type {
} }
return_t.dereference(); return_t.dereference();
} }
Self::And(tys) => { Self::And(tys, _) => {
*tys = std::mem::take(tys) *tys = std::mem::take(tys)
.into_iter() .into_iter()
.map(|mut t| { .map(|mut t| {
@ -5283,7 +5326,7 @@ impl Type {
set.extend(return_t.variables()); set.extend(return_t.variables());
set set
} }
Self::And(tys) => tys.iter().flat_map(|t| t.variables()).collect(), Self::And(tys, _) => tys.iter().flat_map(|t| t.variables()).collect(),
Self::Or(tys) => tys.iter().flat_map(|t| t.variables()).collect(), Self::Or(tys) => tys.iter().flat_map(|t| t.variables()).collect(),
Self::Not(ty) => ty.variables(), Self::Not(ty) => ty.variables(),
Self::Bounded { sub, sup } => sub.variables().union(&sup.variables()), Self::Bounded { sub, sup } => sub.variables().union(&sup.variables()),
@ -5397,7 +5440,7 @@ impl<'t> ReplaceTable<'t> {
} }
} }
// FIXME: // FIXME:
(Type::And(tys), Type::And(tys2)) => { (Type::And(tys, _), Type::And(tys2, _)) => {
for (l, r) in tys.iter().zip(tys2.iter()) { for (l, r) in tys.iter().zip(tys2.iter()) {
self.iterate(l, r); self.iterate(l, r);
} }

View file

@ -11,3 +11,7 @@ j: Joule
f _: Kg = None f _: Kg = None
f kg f kg
f kg/m*m f kg/m*m
w = 2.0kg
assert w >= 1.0kg
assert int(w.value()) == 2