From ff53af0cb643157df4b34c38d5546fa90839aa48 Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Fri, 20 Sep 2024 20:31:03 +0900 Subject: [PATCH] feat: add `RMul, RDiv` * `And` has the default type index * impl `Dimension` traits --- crates/els/completion.rs | 2 +- crates/erg_compiler/context/compare.rs | 31 ++- crates/erg_compiler/context/eval.rs | 2 +- crates/erg_compiler/context/generalize.rs | 6 +- crates/erg_compiler/context/hint.rs | 2 +- .../context/initialize/classes.rs | 55 ++++++ .../erg_compiler/context/initialize/funcs.rs | 12 +- crates/erg_compiler/context/initialize/mod.rs | 4 + .../erg_compiler/context/initialize/traits.rs | 27 ++- crates/erg_compiler/context/inquire.rs | 17 +- crates/erg_compiler/context/instantiate.rs | 8 +- crates/erg_compiler/context/unify.rs | 18 +- .../erg_compiler/lib/core/_erg_std_prelude.py | 47 +++-- crates/erg_compiler/lower.rs | 2 +- crates/erg_compiler/ty/free.rs | 21 ++ crates/erg_compiler/ty/mod.rs | 183 +++++++++++------- examples/use_unit.er | 4 + 17 files changed, 323 insertions(+), 118 deletions(-) diff --git a/crates/els/completion.rs b/crates/els/completion.rs index 13cb818ff..1c97c6daf 100644 --- a/crates/els/completion.rs +++ b/crates/els/completion.rs @@ -56,7 +56,7 @@ fn comp_item_kind(t: &Type, muty: Mutability) -> CompletionItemKind { CompletionItemKind::VARIABLE } } - Type::And(tys) => { + Type::And(tys, _) => { for k in tys.iter().map(|t| comp_item_kind(t, muty)) { if k != CompletionItemKind::VARIABLE { return k; diff --git a/crates/erg_compiler/context/compare.rs b/crates/erg_compiler/context/compare.rs index c2b816dfe..dc8d10531 100644 --- a/crates/erg_compiler/context/compare.rs +++ b/crates/erg_compiler/context/compare.rs @@ -827,7 +827,7 @@ impl Context { (lhs, Or(ors)) => ors.iter().all(|or| self.supertype_of(lhs, or)), // Hash and Eq :> HashEq and ... == 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))) { return true; } @@ -843,9 +843,9 @@ impl Context { 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 - (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(_), Obj) => false, (Not(l), rhs) => !self.supertype_of(l, rhs), @@ -1097,6 +1097,23 @@ impl Context { Variance::Covariant => self.supertype_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 { @@ -1485,7 +1502,7 @@ impl Context { }, (other, or @ Or(_)) | (or @ Or(_), other) => self.union_add(or, other), // (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; for branch in ands.iter() { let union = self.union(branch, other); @@ -1705,7 +1722,9 @@ impl Context { (_, Not(r)) => self.diff(lhs, r), (Not(l), _) => self.diff(rhs, l), // 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) (Or(ors), other) | (other, Or(ors)) => { if ors.iter().any(|t| t.has_unbound_var()) { @@ -2003,7 +2022,7 @@ impl Context { Or(ors) => ors .iter() .fold(Obj, |l, r| self.intersection(&l, &self.complement(r))), - And(ands) => ands + And(ands, _) => ands .iter() .fold(Never, |l, r| self.union(&l, &self.complement(r))), other => not(other.clone()), diff --git a/crates/erg_compiler/context/eval.rs b/crates/erg_compiler/context/eval.rs index 61531a765..60d160fcd 100644 --- a/crates/erg_compiler/context/eval.rs +++ b/crates/erg_compiler/context/eval.rs @@ -2285,7 +2285,7 @@ impl Context { Err((t, errs)) } } - Type::And(ands) => { + Type::And(ands, _) => { let mut new_ands = set! {}; for and in ands.into_iter() { match self.eval_t_params(and, level, t_loc) { diff --git a/crates/erg_compiler/context/generalize.rs b/crates/erg_compiler/context/generalize.rs index d8899e701..49b343df4 100644 --- a/crates/erg_compiler/context/generalize.rs +++ b/crates/erg_compiler/context/generalize.rs @@ -289,13 +289,13 @@ impl Generalizer { } proj_call(lhs, attr_name, args) } - And(ands) => { + And(ands, idx) => { // not `self.intersection` because types are generalized let ands = ands .into_iter() .map(|t| self.generalize_t(t, uninit)) .collect(); - Type::checked_and(ands) + Type::checked_and(ands, idx) } Or(ors) => { // 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)?; Ok(refinement(refine.var, t, pred)) } - And(ands) => { + And(ands, _) => { let mut new_ands = vec![]; for t in ands.into_iter() { new_ands.push(self.deref_tyvar(t)?); diff --git a/crates/erg_compiler/context/hint.rs b/crates/erg_compiler/context/hint.rs index b7b795224..a45a7b098 100644 --- a/crates/erg_compiler/context/hint.rs +++ b/crates/erg_compiler/context/hint.rs @@ -116,7 +116,7 @@ impl Context { 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 l = iter.next().unwrap(); let r = iter.next().unwrap(); diff --git a/crates/erg_compiler/context/initialize/classes.rs b/crates/erg_compiler/context/initialize/classes.rs index 84204f23a..5145da490 100644 --- a/crates/erg_compiler/context/initialize/classes.rs +++ b/crates/erg_compiler/context/initialize/classes.rs @@ -4119,6 +4119,39 @@ impl Context { Immutable, 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 = Self::builtin_methods(Some(poly(ADD, vec![ty_tp(dimension_t.clone())])), 2); let t = fn1_met( @@ -4181,6 +4214,17 @@ impl Context { ValueObj::builtin_class(dimension_added_t), ); 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 = Self::builtin_methods(Some(poly(DIV, vec![ty_tp(dimension2_t.clone())])), 2); let dimension_subtracted_t = poly( @@ -4210,6 +4254,17 @@ impl Context { ValueObj::builtin_class(dimension_subtracted_t), ); 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); base_exception.register_superclass(Obj, &obj); base_exception.register_builtin_erg_impl( diff --git a/crates/erg_compiler/context/initialize/funcs.rs b/crates/erg_compiler/context/initialize/funcs.rs index a1542a6a6..261627406 100644 --- a/crates/erg_compiler/context/initialize/funcs.rs +++ b/crates/erg_compiler/context/initialize/funcs.rs @@ -1005,7 +1005,11 @@ impl Context { Some(FUNC_SUB), ); 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( OP_MUL, op_t, @@ -1014,7 +1018,11 @@ impl Context { Some(FUNC_MUL), ); 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( OP_DIV, op_t, diff --git a/crates/erg_compiler/context/initialize/mod.rs b/crates/erg_compiler/context/initialize/mod.rs index 51dcb4f02..acbdcbc8b 100644 --- a/crates/erg_compiler/context/initialize/mod.rs +++ b/crates/erg_compiler/context/initialize/mod.rs @@ -133,6 +133,8 @@ const ATTR_TRACEBACK: &str = "traceback"; const ADD: &str = "Add"; const SUB: &str = "Sub"; const MUL: &str = "Mul"; +const RMUL: &str = "RMul"; +const RDIV: &str = "RDiv"; const DIV: &str = "Div"; const FLOOR_DIV: &str = "FloorDiv"; const POS: &str = "Pos"; @@ -564,6 +566,8 @@ const OP_SUB: &str = "__sub__"; const OP_MUL: &str = "__mul__"; const OP_DIV: &str = "__div__"; const OP_FLOOR_DIV: &str = "__floordiv__"; +const OP_RMUL: &str = "__rmul__"; +const OP_RDIV: &str = "__rdiv__"; const OP_ABS: &str = "__abs__"; const OP_PARTIAL_CMP: &str = "__partial_cmp__"; const OP_AND: &str = "__and__"; diff --git a/crates/erg_compiler/context/initialize/traits.rs b/crates/erg_compiler/context/initialize/traits.rs index ba94cb30b..a16c8c5a2 100644 --- a/crates/erg_compiler/context/initialize/traits.rs +++ b/crates/erg_compiler/context/initialize/traits.rs @@ -587,6 +587,23 @@ impl Context { 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(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 */ let num = Self::builtin_mono_trait(NUM, 2); // num.register_superclass(poly(ADD, vec![]), &add); @@ -832,7 +849,15 @@ impl Context { None, ); 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( ADD, vec![ConstTemplate::Obj(ValueObj::builtin_type(Slf.clone()))], diff --git a/crates/erg_compiler/context/inquire.rs b/crates/erg_compiler/context/inquire.rs index 143388f73..a73d85912 100644 --- a/crates/erg_compiler/context/inquire.rs +++ b/crates/erg_compiler/context/inquire.rs @@ -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 { unreachable!() }; @@ -1952,7 +1955,7 @@ impl Context { res } } - Type::And(_) => { + Type::And(_, _) => { let instance = self.resolve_overload( obj, instance.clone(), @@ -2852,11 +2855,11 @@ impl Context { pub(crate) fn type_params_variance(&self) -> Vec { let match_tp_name = |tp: &TyParam, name: &VarName| -> bool { 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()); } } 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()); } } @@ -3014,7 +3017,7 @@ impl Context { self.get_nominal_super_type_ctxs(&Type) } } - Type::And(tys) => { + Type::And(tys, _) => { let mut acc = vec![]; for ctxs in tys .iter() @@ -3366,7 +3369,7 @@ impl Context { match trait_ { // And(Add, Sub) == intersection({Int <: Add(Int), Bool <: Add(Bool) ...}, {Int <: Sub(Int), ...}) // == {Int <: Add(Int) and Sub(Int), ...} - Type::And(tys) => { + Type::And(tys, _) => { let impls = tys .iter() .flat_map(|ty| self.get_trait_impls(ty)) @@ -3956,7 +3959,7 @@ impl Context { pub fn is_class(&self, typ: &Type) -> bool { match typ { - Type::And(_) => false, + Type::And(_, _) => false, Type::Never => true, Type::FreeVar(fv) if fv.is_linked() => self.is_class(&fv.crack()), Type::FreeVar(_) => false, @@ -3983,7 +3986,7 @@ impl Context { Type::Never => false, Type::FreeVar(fv) if fv.is_linked() => self.is_class(&fv.crack()), 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::Proj { lhs, rhs } => self .get_proj_candidates(lhs, rhs) diff --git a/crates/erg_compiler/context/instantiate.rs b/crates/erg_compiler/context/instantiate.rs index be4028548..62a637ced 100644 --- a/crates/erg_compiler/context/instantiate.rs +++ b/crates/erg_compiler/context/instantiate.rs @@ -953,7 +953,7 @@ impl Context { let t = self.instantiate_t_inner(*t, tmp_tv_cache, loc)?; Ok(t.structuralize()) } - And(tys) => { + And(tys, _) => { let mut new_tys = vec![]; for ty in tys.iter().cloned() { new_tys.push(self.instantiate_t_inner(ty, tmp_tv_cache, loc)?); @@ -1004,7 +1004,7 @@ impl Context { let t = fv.crack().clone(); self.instantiate(t, callee) } - And(tys) => { + And(tys, _idx) => { let tys = tys .into_iter() .map(|t| self.instantiate(t, callee)) @@ -1036,7 +1036,7 @@ impl Context { )?; } } - Type::And(tys) => { + Type::And(tys, _) => { for ty in tys { if let Some(self_t) = ty.self_t() { self.sub_unify( @@ -1068,7 +1068,7 @@ impl Context { let t = fv.crack().clone(); self.instantiate_dummy(t) } - And(tys) => { + And(tys, _) => { let tys = tys .into_iter() .map(|t| self.instantiate_dummy(t)) diff --git a/crates/erg_compiler/context/unify.rs b/crates/erg_compiler/context/unify.rs index cbefbfa1d..b49b8d328 100644 --- a/crates/erg_compiler/context/unify.rs +++ b/crates/erg_compiler/context/unify.rs @@ -158,7 +158,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { Ok(()) } // 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(); for _ in 0..r.len() { if l.iter() @@ -199,7 +199,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { self.ctx.caused_by(), ))) } - (lhs, And(tys)) => { + (lhs, And(tys, _)) => { for ty in tys.iter() { self.occur_inner(lhs, ty)?; } @@ -211,7 +211,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { } Ok(()) } - (And(tys), rhs) => { + (And(tys, _), rhs) => { for ty in tys.iter() { self.occur_inner(ty, rhs)?; } @@ -322,7 +322,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { } Ok(()) } - (lhs, And(tys)) => { + (lhs, And(tys, _)) => { for ty in tys.iter() { self.occur_inner(lhs, ty)?; } @@ -334,7 +334,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { } Ok(()) } - (And(tys), rhs) => { + (And(tys, _), rhs) => { for ty in tys.iter() { 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); } // 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 rtys_ = rtys.clone(); // 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 - (_, And(tys)) => { + (_, And(tys, _)) => { for ty in tys { self.sub_unify(maybe_sub, ty)?; } } // (X and Y) <: Z is valid when X <: Z or Y <: Z - (And(tys), _) => { + (And(tys, _), _) => { for ty in tys { if self.ctx.subtype_of(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; } } - (And(tys), other) | (other, And(tys)) => { + (And(tys, _), other) | (other, And(tys, _)) => { let mut unified = Obj; for ty in tys { if let Some(t) = self.unify(ty, other) { diff --git a/crates/erg_compiler/lib/core/_erg_std_prelude.py b/crates/erg_compiler/lib/core/_erg_std_prelude.py index f36927e23..c96bf40d8 100644 --- a/crates/erg_compiler/lib/core/_erg_std_prelude.py +++ b/crates/erg_compiler/lib/core/_erg_std_prelude.py @@ -35,26 +35,49 @@ class Never: Θ = TypeVar("Θ", bound=int) N = TypeVar("N", bound=int) J = TypeVar("J", bound=int) -class Dimension(float, Generic[Ty, M, L, T, I, Θ, N, J]): - def value(self) -> float: - return float(self) +class Dimension(Generic[Ty, M, L, T, I, Θ, N, J]): + val: float + 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): - return f"Dimension({float(self)})" + return f"Dimension({self.val})" 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): - return Dimension(float(self) - other) + return Dimension(self.val - other) + def __rsub__(self, other): + return Dimension(other - self.val) def __mul__(self, other): - return Dimension(float(self) * other) + return Dimension(self.val * other) def __rmul__(self, other): - return Dimension(other * float(self)) + return Dimension(other * self.val) def __truediv__(self, other): - return Dimension(float(self) / other) + return Dimension(self.val / other) def __floordiv__(self, other): - return Dimension(float(self) // other) + return Dimension(self.val // other) def __rtruediv__(self, other): - return Dimension(other / float(self)) + return Dimension(other / self.val) 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: return t.__name__ == "Dimension" diff --git a/crates/erg_compiler/lower.rs b/crates/erg_compiler/lower.rs index 5d6724137..2a2d752f4 100644 --- a/crates/erg_compiler/lower.rs +++ b/crates/erg_compiler/lower.rs @@ -1490,7 +1490,7 @@ impl GenericASTLowerer { } _ => {} }, - Type::And(tys) => { + Type::And(tys, _) => { for ty in tys { self.push_guard(nth, kind, ty); } diff --git a/crates/erg_compiler/ty/free.rs b/crates/erg_compiler/ty/free.rs index e9cad3bfb..8e158eec9 100644 --- a/crates/erg_compiler/ty/free.rs +++ b/crates/erg_compiler/ty/free.rs @@ -545,6 +545,13 @@ impl FreeKind { _ => {} } } + + pub fn get_previous(&self) -> Option<&FreeKind> { + match self { + Self::UndoableLinked { previous, .. } => Some(previous), + _ => None, + } + } } #[derive(Debug, Clone)] @@ -1208,6 +1215,20 @@ impl Free { .ok() } + pub fn get_undoable_root(&self) -> Option>> { + 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 { match self.clone().unwrap_unbound() { (Some(name), lev, constraint) => Self::new_named_unbound(name, lev, constraint), diff --git a/crates/erg_compiler/ty/mod.rs b/crates/erg_compiler/ty/mod.rs index 4022b17f2..1fe79288c 100644 --- a/crates/erg_compiler/ty/mod.rs +++ b/crates/erg_compiler/ty/mod.rs @@ -1078,6 +1078,10 @@ impl RefinementType { pub fn invert(self) -> Self { 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)] @@ -1356,7 +1360,8 @@ pub enum Type { Refinement(RefinementType), // e.g. |T: Type| T -> T Quantified(Box), - And(Vec), + /// usize: default type index + And(Vec, Option), Or(Set), Not(Box), // 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::Refinement(l), Self::Refinement(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::>().linear_eq(&r.iter().collect()) } (Self::Or(l), Self::Or(r)) => l.linear_eq(r), @@ -1607,7 +1612,7 @@ impl LimitedDisplay for Type { write!(f, "|")?; quantified.limited_fmt(f, limit - 1) } - Self::And(ands) => { + Self::And(ands, _) => { for (i, ty) in ands.iter().enumerate() { if i > 0 { write!(f, " and ")?; @@ -1802,18 +1807,18 @@ impl BitAnd for Type { type Output = Self; fn bitand(self, rhs: Self) -> Self::Output { 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::Never, _) | (_, Self::Never) => Self::Never, - (Self::And(mut l), r) => { + (Self::And(mut l, idx), 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); - 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) .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::Not(ty) => ty.level(), Self::Record(attrs) => attrs.values().filter_map(|t| t.level()).min(), @@ -2031,7 +2036,7 @@ impl HasLevel for Type { Self::Quantified(quant) => { quant.set_level(level); } - Self::And(tys) => { + Self::And(tys, _) => { for t in tys.iter() { t.set_level(level); } @@ -2190,7 +2195,7 @@ impl StructuralEq for Type { (Self::Guard(l), Self::Guard(r)) => l.structural_eq(r), // NG: (l.structural_eq(l2) && r.structural_eq(r2)) // || (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::>(); let other_ands = other_ands.iter().collect::>(); if self_ands.len() != other_ands.len() { @@ -2310,20 +2315,20 @@ impl Type { } } - pub fn checked_and(tys: Vec) -> Self { + pub fn checked_and(tys: Vec, idx: Option) -> Self { if tys.is_empty() { panic!("tys is empty"); } else if tys.len() == 1 { tys.into_iter().next().unwrap() } else { - Self::And(tys) + Self::And(tys, idx) } } pub fn quantify(self) -> Self { debug_assert!(self.is_subr(), "{self} is not subr"); 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)), } } @@ -2421,7 +2426,7 @@ impl Type { Self::Quantified(t) => t.is_procedure(), Self::Subr(subr) if subr.kind == SubrKind::Proc => true, 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, } } @@ -2439,7 +2444,7 @@ impl Type { name.ends_with('!') } 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, } } @@ -2458,7 +2463,7 @@ impl Type { Self::Poly { name, params, .. } if &name[..] == "Tuple" => params.is_empty(), Self::Refinement(refine) => refine.t.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, } } @@ -2541,7 +2546,7 @@ impl Type { pub fn is_intersection_type(&self) -> bool { match self { 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(), _ => false, } @@ -2559,7 +2564,7 @@ impl Type { Self::Refinement(refine) => refine.t.union_size(), Self::Ref(t) => t.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::Callable { param_ts, return_t } => param_ts .iter() @@ -2600,7 +2605,7 @@ impl Type { match self { Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_refinement(), Self::Refinement(_) => true, - Self::And(tys) => tys.iter().any(|t| t.is_refinement()), + Self::And(tys, _) => tys.iter().any(|t| t.is_refinement()), _ => false, } } @@ -2609,7 +2614,7 @@ impl Type { match self { Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_singleton_refinement(), 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, } } @@ -2619,7 +2624,7 @@ impl Type { Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_record(), Self::Record(_) => true, 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, } } @@ -2633,7 +2638,7 @@ impl Type { Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_erg_module(), Self::Refinement(refine) => refine.t.is_erg_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, } } @@ -2643,7 +2648,7 @@ impl Type { Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_py_module(), Self::Refinement(refine) => refine.t.is_py_module(), 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, } } @@ -2654,7 +2659,7 @@ impl Type { Self::Refinement(refine) => refine.t.is_method(), Self::Subr(subr) => subr.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, } } @@ -2665,7 +2670,7 @@ impl Type { Self::Subr(_) => true, Self::Quantified(quant) => quant.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, } } @@ -2676,7 +2681,7 @@ impl Type { Self::Subr(subr) => Some(subr.kind), Self::Refinement(refine) => refine.t.subr_kind(), Self::Quantified(quant) => quant.subr_kind(), - Self::And(tys) => tys + Self::And(tys, _) => tys .iter() .filter_map(|t| t.subr_kind()) .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::Quantified(_) => true, 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, } } @@ -2726,7 +2731,7 @@ impl Type { Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_iterable(), Self::Poly { name, .. } => &name[..] == "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, } } @@ -2817,7 +2822,7 @@ impl Type { Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_structural(), Self::Structural(_) => true, 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, } } @@ -2827,7 +2832,7 @@ impl Type { Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_failure(), Self::Refinement(refine) => refine.t.is_failure(), Self::Failure => true, - Self::And(tys) => tys.iter().any(|t| t.is_failure()), + Self::And(tys, _) => tys.iter().any(|t| t.is_failure()), _ => false, } } @@ -2922,7 +2927,7 @@ impl Type { Self::ProjCall { lhs, args, .. } => { 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::Not(t) => f(t), Self::Ref(t) => f(t), @@ -2991,7 +2996,7 @@ impl Type { Self::ProjCall { lhs, args, .. } => { 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::Not(t) => t.contains_type(target), Self::Ref(t) => t.contains_type(target), @@ -3029,7 +3034,7 @@ impl Type { Self::ProjCall { lhs, args, .. } => { 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::Not(t) => t.contains_tp(target), Self::Ref(t) => t.contains_tp(target), @@ -3063,7 +3068,7 @@ impl Type { Self::ProjCall { lhs, args, .. } => { 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::Not(t) => t.contains_value(target), Self::Ref(t) => t.contains_value(target), @@ -3107,7 +3112,7 @@ impl Type { Self::ProjCall { lhs, args, .. } => { 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::Not(t) => t.contains_type(self), Self::Ref(t) => t.contains_type(self), @@ -3178,7 +3183,7 @@ impl Type { Self::Inf => Str::ever("Inf"), Self::NegInf => Str::ever("NegInf"), Self::Mono(name) => name.clone(), - Self::And(_) => Str::ever("And"), + Self::And(_, _) => Str::ever("And"), Self::Not(_) => Str::ever("Not"), Self::Or(_) => Str::ever("Or"), Self::Ref(_) => Str::ever("Ref"), @@ -3270,7 +3275,7 @@ impl Type { match self { Self::FreeVar(fv) if fv.is_linked() => fv.crack().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, } } @@ -3321,11 +3326,35 @@ impl Type { .into_iter() .map(|t| t.quantify()) .collect(), - Type::And(tys) => tys.clone(), + Type::And(tys, _) => tys.clone(), _ => vec![self.clone()], } } + pub fn default_intersection_type(&self) -> Option { + 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 { match self { Self::FreeVar(fv) if fv.is_linked() => fv.crack().tvar_name(), @@ -3397,7 +3426,7 @@ impl Type { match self { Self::FreeVar(fv) if fv.is_unbound() => true, 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::Not(t) => t.is_totally_unbound(), _ => false, @@ -3509,7 +3538,7 @@ impl Type { sub.destructive_coerce(); self.destructive_link(&sub); } - Type::And(tys) => { + Type::And(tys, _) => { for t in tys { t.destructive_coerce(); } @@ -3570,7 +3599,7 @@ impl Type { sub.undoable_coerce(list); self.undoable_link(&sub, list); } - Type::And(tys) => { + Type::And(tys, _) => { for t in tys { t.undoable_coerce(list); } @@ -3637,7 +3666,7 @@ impl Type { .map(|t| t.qvars_inner()) .unwrap_or_else(|| set! {}), ), - Self::And(tys) => tys + Self::And(tys, _) => tys .iter() .fold(set! {}, |acc, t| acc.concat(t.qvars_inner())), Self::Or(tys) => tys @@ -3785,7 +3814,7 @@ impl Type { Self::Refinement(refine) => refine.t.typarams_len(), // REVIEW: 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::Not(_) => Some(1), Self::Subr(subr) => Some( @@ -3852,7 +3881,7 @@ impl Type { Self::FreeVar(_unbound) => vec![], Self::Refinement(refine) => refine.t.typarams(), 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::Not(t) => vec![TyParam::t(*t.clone())], Self::Subr(subr) => subr.typarams(), @@ -4074,7 +4103,9 @@ impl Type { let r = r.iter().map(|(k, v)| (k.clone(), v.derefine())).collect(); 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::Not(ty) => !ty.derefine(), Self::Proj { lhs, rhs } => lhs.derefine().proj(rhs.clone()), @@ -4148,7 +4179,7 @@ impl Type { }); self } - Self::And(tys) => Self::checked_and( + Self::And(tys, idx) => Self::checked_and( tys.into_iter() .filter_map(|t| { if t.addr_eq(target) { @@ -4158,6 +4189,7 @@ impl Type { } }) .collect(), + idx, ), Self::Or(tys) => Self::checked_or( tys.into_iter() @@ -4224,11 +4256,12 @@ impl Type { before: Box::new(before.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() .filter(|t| !t.addr_eq(target)) .map(|t| t.eliminate_recursion(target)) .collect(), + idx, ), Self::Or(tys) => Self::checked_or( tys.into_iter() @@ -4262,9 +4295,10 @@ impl Type { pub(crate) fn eliminate_and_or_recursion(self, target: &Type) -> Self { match self { - Self::And(tys) => { - Self::checked_and(tys.into_iter().filter(|t| !t.addr_eq(target)).collect()) - } + Self::And(tys, idx) => Self::checked_and( + tys.into_iter().filter(|t| !t.addr_eq(target)).collect(), + idx, + ), Self::Or(tys) => { 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)), 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::Not(ty) => !ty.map(f), Self::Proj { lhs, rhs } => lhs.map(f).proj(rhs), @@ -4494,9 +4530,10 @@ impl Type { before: Box::new(before._replace_tp(target, to)), after: after.map(|t| Box::new(t._replace_tp(target, to))), }, - Self::And(tys) => { - Self::checked_and(tys.into_iter().map(|t| t._replace_tp(target, to)).collect()) - } + Self::And(tys, idx) => Self::checked_and( + tys.into_iter().map(|t| t._replace_tp(target, to)).collect(), + idx, + ), Self::Or(tys) => { 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)), 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::Not(ty) => !ty.map_tp(f), Self::Proj { lhs, rhs } => lhs.map_tp(f).proj(rhs), @@ -4664,10 +4703,11 @@ impl Type { after, }) } - Self::And(tys) => Ok(Self::checked_and( + Self::And(tys, idx) => Ok(Self::checked_and( tys.into_iter() .map(|t| t.try_map_tp(f)) .collect::>()?, + idx, )), Self::Or(tys) => Ok(Self::checked_or( tys.into_iter() @@ -4706,10 +4746,11 @@ impl Type { *refine.t = refine.t.replace_param(target, to); Self::Refinement(refine) } - Self::And(tys) => Self::And( + Self::And(tys, idx) => Self::And( tys.into_iter() .map(|t| t.replace_param(target, to)) .collect(), + idx, ), Self::Guard(guard) => Self::Guard(guard.replace_param(target, to)), _ => self, @@ -4718,7 +4759,7 @@ impl Type { pub fn eliminate_and_or(&mut self) { match self { - Self::And(tys) if tys.len() == 1 => { + Self::And(tys, _) if tys.len() == 1 => { *self = tys.remove(0); } Self::Or(tys) if tys.len() == 1 => { @@ -4795,7 +4836,9 @@ impl Type { } 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::Not(ty) => !ty.normalize(), Self::Structural(ty) => ty.normalize().structuralize(), @@ -4828,8 +4871,8 @@ impl Type { free.get_sub().unwrap_or(self.clone()) } else { match self { - Self::And(tys) => { - Self::checked_and(tys.iter().map(|t| t.lower_bounded()).collect()) + Self::And(tys, idx) => { + 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::Not(ty) => !ty.lower_bounded(), @@ -4848,8 +4891,8 @@ impl Type { free.get_super().unwrap_or(self.clone()) } else { match self { - Self::And(tys) => { - Self::checked_and(tys.iter().map(|t| t.upper_bounded()).collect()) + Self::And(tys, idx) => { + 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::Not(ty) => !ty.upper_bounded(), @@ -5024,7 +5067,7 @@ impl Type { match self { Self::FreeVar(fv) if fv.is_linked() => fv.crack().ands(), Self::Refinement(refine) => refine.t.ands(), - Self::And(tys) => tys.clone(), + Self::And(tys, _) => tys.clone(), _ => vec![self.clone()], } } @@ -5082,7 +5125,7 @@ impl Type { Self::Callable { param_ts, .. } => { 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::Not(t) => t.contained_ts(), Self::Bounded { sub, sup } => sub.contained_ts().union(&sup.contained_ts()), @@ -5152,7 +5195,7 @@ impl Type { } return_t.dereference(); } - Self::And(tys) => { + Self::And(tys, _) => { *tys = std::mem::take(tys) .into_iter() .map(|mut t| { @@ -5283,7 +5326,7 @@ impl Type { set.extend(return_t.variables()); 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::Not(ty) => ty.variables(), Self::Bounded { sub, sup } => sub.variables().union(&sup.variables()), @@ -5397,7 +5440,7 @@ impl<'t> ReplaceTable<'t> { } } // FIXME: - (Type::And(tys), Type::And(tys2)) => { + (Type::And(tys, _), Type::And(tys2, _)) => { for (l, r) in tys.iter().zip(tys2.iter()) { self.iterate(l, r); } diff --git a/examples/use_unit.er b/examples/use_unit.er index 5410e79b3..5a87e87eb 100644 --- a/examples/use_unit.er +++ b/examples/use_unit.er @@ -11,3 +11,7 @@ j: Joule f _: Kg = None f kg f kg/m*m + +w = 2.0kg +assert w >= 1.0kg +assert int(w.value()) == 2