From 4651a383aee50d94f442920b5ebabd541b03bb6f Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Fri, 20 Sep 2024 16:56:22 +0900 Subject: [PATCH 1/3] feat: add `Dimension` and `unit` module --- crates/erg_compiler/codegen.rs | 6 +- crates/erg_compiler/context/compare.rs | 8 + .../context/initialize/classes.rs | 156 ++++++++++++++++++ crates/erg_compiler/context/initialize/mod.rs | 2 + crates/erg_compiler/context/inquire.rs | 2 + crates/erg_compiler/context/unify.rs | 45 ++++- .../erg_compiler/lib/core/_erg_std_prelude.py | 34 ++++ crates/erg_compiler/lib/core/_erg_type.py | 2 + crates/erg_compiler/lib/std/exception.er | 1 - crates/erg_compiler/lib/std/unit.er | 96 +++++++++++ crates/erg_compiler/transpile.rs | 2 +- crates/erg_compiler/ty/mod.rs | 12 +- crates/erg_compiler/ty/value.rs | 1 + examples/use_unit.er | 13 ++ tests/should_err/use_unit.er | 12 ++ tests/test.rs | 10 ++ 16 files changed, 392 insertions(+), 10 deletions(-) create mode 100644 crates/erg_compiler/lib/std/unit.er create mode 100644 examples/use_unit.er create mode 100644 tests/should_err/use_unit.er diff --git a/crates/erg_compiler/codegen.rs b/crates/erg_compiler/codegen.rs index 248481b54..fe48695b1 100644 --- a/crates/erg_compiler/codegen.rs +++ b/crates/erg_compiler/codegen.rs @@ -2716,7 +2716,7 @@ impl PyCodeGenerator { Expr::Accessor(Accessor::Ident(ident)) if ident.vis().is_private() => { self.emit_call_local(ident, call.args) } - other if other.ref_t().is_poly_type_meta() => { + other if other.ref_t().is_poly_meta_type() => { self.emit_expr(other); self.emit_index_args(call.args); } @@ -2754,7 +2754,7 @@ impl PyCodeGenerator { self.emit_load_name_instr(Identifier::private("#sum")); self.emit_args_311(args, Name); } - other if local.ref_t().is_poly_type_meta() && other != "classof" => { + other if local.ref_t().is_poly_meta_type() && other != "classof" => { if self.py_version.minor <= Some(9) { self.load_fake_generic(); self.emit_load_name_instr(Identifier::private("#FakeGenericAlias")); @@ -2798,7 +2798,7 @@ impl PyCodeGenerator { if let Some(func_name) = debind(&method_name) { return self.emit_call_fake_method(obj, func_name, method_name, args); } - let is_type = method_name.ref_t().is_poly_type_meta(); + let is_type = method_name.ref_t().is_poly_meta_type(); let kind = if self.py_version.minor >= Some(11) || method_name.vi.t.is_method() { BoundAttr } else { diff --git a/crates/erg_compiler/context/compare.rs b/crates/erg_compiler/context/compare.rs index f6125066d..c2b816dfe 100644 --- a/crates/erg_compiler/context/compare.rs +++ b/crates/erg_compiler/context/compare.rs @@ -1154,12 +1154,15 @@ impl Context { Type::Obj } }; + /* if variance == Variance::Contravariant { self.subtype_of(&fv_t, &sub_t) } else { // REVIEW: covariant, invariant self.supertype_of(&fv_t, &sub_t) } + */ + self.subtype_of(&sub_t, &fv_t) || self.supertype_of(&sub_t, &fv_t) } (_, TyParam::FreeVar(fv)) if fv.is_unbound() => { let Some(fv_t) = fv.get_type() else { @@ -1172,14 +1175,18 @@ impl Context { Type::Obj } }; + /* if variance == Variance::Contravariant { self.subtype_of(&sup_t, &fv_t) } else { // REVIEW: covariant, invariant self.supertype_of(&sup_t, &fv_t) } + */ + self.subtype_of(&sup_t, &fv_t) || self.supertype_of(&sup_t, &fv_t) } (TyParam::Value(sup), _) => { + // Value([Value(1)]) => TyParam([Value(1)]) if let Ok(sup) = Self::convert_value_into_tp(sup.clone()) { self.supertype_of_tp(&sup, sub_p, variance) } else { @@ -1408,6 +1415,7 @@ impl Context { /// union(?T(<: Str), ?U(<: Int)) == ?T or ?U /// union(List(Int, 2), List(Str, 2)) == List(Int or Str, 2) /// union(List(Int, 2), List(Str, 3)) == List(Int, 2) or List(Int, 3) + /// union(List(Int, 2), List(Int, ?N)) == List(Int, ?N) /// union({ .a = Int }, { .a = Str }) == { .a = Int or Str } /// union({ .a = Int }, { .a = Int; .b = Int }) == { .a = Int } or { .a = Int; .b = Int } # not to lost `b` information /// union((A and B) or C) == (A or C) and (B or C) diff --git a/crates/erg_compiler/context/initialize/classes.rs b/crates/erg_compiler/context/initialize/classes.rs index 2e36976ce..84204f23a 100644 --- a/crates/erg_compiler/context/initialize/classes.rs +++ b/crates/erg_compiler/context/initialize/classes.rs @@ -4055,6 +4055,161 @@ impl Context { Immutable, Visibility::BUILTIN_PRIVATE, ); + // TODO: non-builtin + /* Dimension */ + let Ty = type_q("Ty"); + let M = mono_q_tp("M", instanceof(Int)); + let L = mono_q_tp("L", instanceof(Int)); + let Time = mono_q_tp("T", instanceof(Int)); + let I = mono_q_tp("I", instanceof(Int)); + let Temp = mono_q_tp("Θ", instanceof(Int)); + let N = mono_q_tp("N", instanceof(Int)); + let J = mono_q_tp("J", instanceof(Int)); + let M2 = mono_q_tp("M2", instanceof(Int)); + let L2 = mono_q_tp("L2", instanceof(Int)); + let Time2 = mono_q_tp("T2", instanceof(Int)); + let I2 = mono_q_tp("I2", instanceof(Int)); + let Temp2 = mono_q_tp("Θ2", instanceof(Int)); + let N2 = mono_q_tp("N2", instanceof(Int)); + let J2 = mono_q_tp("J2", instanceof(Int)); + let dimension_t = poly( + DIMENSION, + vec![ + ty_tp(Ty.clone()), + M.clone(), + L.clone(), + Time.clone(), + I.clone(), + Temp.clone(), + N.clone(), + J.clone(), + ], + ); + let dimension2_t = poly( + DIMENSION, + vec![ + ty_tp(Ty.clone()), + M2.clone(), + L2.clone(), + Time2.clone(), + I2.clone(), + Temp2.clone(), + N2.clone(), + J2.clone(), + ], + ); + let params = vec![ + PS::t_nd("Ty"), + PS::named_nd("M", Int), + PS::named_nd("L", Int), + PS::named_nd("T", Int), + PS::named_nd("I", Int), + PS::named_nd("Θ", Int), + PS::named_nd("N", Int), + PS::named_nd("J", Int), + ]; + let mut dimension = Self::builtin_poly_class(DIMENSION, params, 10); + dimension + .register_trait(self, poly(OUTPUT, vec![ty_tp(Ty.clone())])) + .unwrap(); + let value_t = fn0_met(dimension_t.clone(), Ty.clone()).quantify(); + dimension.register_builtin_erg_impl( + FUNC_VALUE, + value_t, + Immutable, + Visibility::BUILTIN_PUBLIC, + ); + let mut dimension_add = + Self::builtin_methods(Some(poly(ADD, vec![ty_tp(dimension_t.clone())])), 2); + let t = fn1_met( + dimension_t.clone(), + dimension_t.clone(), + dimension_t.clone(), + ) + .quantify(); + dimension_add.register_builtin_erg_impl(OP_ADD, t, Immutable, Visibility::BUILTIN_PUBLIC); + let out_t = dimension_t.clone(); + dimension_add.register_builtin_const( + OUTPUT, + Visibility::BUILTIN_PUBLIC, + None, + ValueObj::builtin_class(out_t.clone()), + ); + dimension.register_trait_methods(dimension_t.clone(), dimension_add); + let mut dimension_sub = + Self::builtin_methods(Some(poly(SUB, vec![ty_tp(dimension_t.clone())])), 2); + let t = fn1_met( + dimension_t.clone(), + dimension_t.clone(), + dimension_t.clone(), + ) + .quantify(); + dimension_sub.register_builtin_erg_impl(OP_SUB, t, Immutable, Visibility::BUILTIN_PUBLIC); + dimension_sub.register_builtin_const( + OUTPUT, + Visibility::BUILTIN_PUBLIC, + None, + ValueObj::builtin_class(out_t), + ); + dimension.register_trait_methods(dimension_t.clone(), dimension_sub); + let mut dimension_mul = + Self::builtin_methods(Some(poly(MUL, vec![ty_tp(dimension2_t.clone())])), 2); + let dimension_added_t = poly( + DIMENSION, + vec![ + ty_tp(Ty.clone()), + M.clone() + M2.clone(), + L.clone() + L2.clone(), + Time.clone() + Time2.clone(), + I.clone() + I2.clone(), + Temp.clone() + Temp2.clone(), + N.clone() + N2.clone(), + J.clone() + J2.clone(), + ], + ); + let t = fn1_met( + dimension_t.clone(), + dimension2_t.clone(), + dimension_added_t.clone(), + ) + .quantify(); + dimension_mul.register_builtin_erg_impl(OP_MUL, t, Immutable, Visibility::BUILTIN_PUBLIC); + dimension_mul.register_builtin_const( + OUTPUT, + Visibility::BUILTIN_PUBLIC, + None, + ValueObj::builtin_class(dimension_added_t), + ); + dimension.register_trait_methods(dimension_t.clone(), dimension_mul); + let mut dimension_div = + Self::builtin_methods(Some(poly(DIV, vec![ty_tp(dimension2_t.clone())])), 2); + let dimension_subtracted_t = poly( + DIMENSION, + vec![ + ty_tp(Ty.clone()), + M.clone() - M2.clone(), + L.clone() - L2.clone(), + Time.clone() - Time2.clone(), + I.clone() - I2.clone(), + Temp.clone() - Temp2.clone(), + N.clone() - N2.clone(), + J.clone() - J2.clone(), + ], + ); + let t = fn1_met( + dimension_t.clone(), + dimension2_t.clone(), + dimension_subtracted_t.clone(), + ) + .quantify(); + dimension_div.register_builtin_erg_impl(OP_DIV, t, Immutable, Visibility::BUILTIN_PUBLIC); + dimension_div.register_builtin_const( + OUTPUT, + Visibility::BUILTIN_PUBLIC, + None, + ValueObj::builtin_class(dimension_subtracted_t), + ); + dimension.register_trait_methods(dimension_t.clone(), dimension_div); let mut base_exception = Self::builtin_mono_class(BASE_EXCEPTION, 2); base_exception.register_superclass(Obj, &obj); base_exception.register_builtin_erg_impl( @@ -4472,6 +4627,7 @@ impl Context { Const, Some(GENERATOR), ); + self.register_builtin_type(dimension_t, dimension, vis.clone(), Const, Some(DIMENSION)); self.register_builtin_type( mono(BASE_EXCEPTION), base_exception, diff --git a/crates/erg_compiler/context/initialize/mod.rs b/crates/erg_compiler/context/initialize/mod.rs index c7c3aa075..51dcb4f02 100644 --- a/crates/erg_compiler/context/initialize/mod.rs +++ b/crates/erg_compiler/context/initialize/mod.rs @@ -403,6 +403,8 @@ const FUNC_TO_LIST: &str = "to_list"; const FILE: &str = "File"; const CALLABLE: &str = "Callable"; const GENERATOR: &str = "Generator"; +const DIMENSION: &str = "Dimension"; +const FUNC_VALUE: &str = "value"; const BASE_EXCEPTION: &str = "BaseException"; const ATTR_ARGS: &str = "args"; const FUNC_WITH_TRACEBACK: &str = "with_traceback"; diff --git a/crates/erg_compiler/context/inquire.rs b/crates/erg_compiler/context/inquire.rs index 30be2cfc8..143388f73 100644 --- a/crates/erg_compiler/context/inquire.rs +++ b/crates/erg_compiler/context/inquire.rs @@ -2689,6 +2689,7 @@ impl Context { fmt_slice(pos_args), fmt_slice(kw_args) ); + debug_assert!(instance.has_no_qvar(), "{instance} has qvar"); let instance = match self .substitute_call( obj, @@ -2717,6 +2718,7 @@ impl Context { "{instance} is quantified subr" ); log!(info "Substituted:\ninstance: {instance}"); + debug_assert!(instance.has_no_qvar(), "{instance} has qvar"); let res = self .eval_t_params(instance, self.level, obj) .map_err(|(t, errs)| { diff --git a/crates/erg_compiler/context/unify.rs b/crates/erg_compiler/context/unify.rs index fea7e0dcc..cbefbfa1d 100644 --- a/crates/erg_compiler/context/unify.rs +++ b/crates/erg_compiler/context/unify.rs @@ -12,6 +12,7 @@ use erg_common::Str; use erg_common::{fmt_vec, fn_name, log}; use crate::context::eval::Substituter; +use crate::context::instantiate::TyVarCache; use crate::ty::constructors::*; use crate::ty::free::{Constraint, FreeKind, HasLevel, GENERIC_LEVEL}; use crate::ty::typaram::{OpKind, TyParam}; @@ -1377,6 +1378,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { // * sub_unify({0}, ?T(:> {1}, <: Nat)): (?T(:> {0, 1}, <: Nat)) // * sub_unify(Bool, ?T(<: Bool or Y)): (?T == Bool) // * sub_unify(Float, ?T(<: Structural{ .imag = ?U })) ==> ?U == Float + // * sub_unify(K(Int, 1), ?T(:> K(?A, ?N))) ==> ?A(:> Int), ?N == 1 if let Type::Refinement(refine) = maybe_sub { if refine.t.addr_eq(maybe_sup) { return Ok(()); @@ -1386,7 +1388,18 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { if sup.is_structural() || !sup.is_recursive() { self.sub_unify(maybe_sub, &sup)?; } - let new_sub = self.ctx.union(maybe_sub, &sub); + let mut new_sub = self.ctx.union(maybe_sub, &sub); + if maybe_sub.qual_name() == sub.qual_name() && new_sub.has_unbound_var() { + let list = UndoableLinkedList::new(); + if self + .ctx + .undoable_sub_unify(maybe_sub, &sub, &(), &list, None) + .is_ok() + { + drop(list); + self.sub_unify(maybe_sub, &sub)?; + } + } // Expanding to an Or-type is prohibited by default // This increases the quality of error reporting // (Try commenting out this part and run tests/should_err/subtyping.er to see the error report changes on lines 29-30) @@ -1397,6 +1410,7 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { let unified = self.unify(&l, &r); if let Some(unified) = unified { log!("unify({l}, {r}) == {unified}"); + new_sub = unified; } else { let maybe_sub = self.ctx.readable_type(maybe_sub.clone()); let new_sub = self.ctx.readable_type(new_sub); @@ -1987,6 +2001,8 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { /// unify(Eq, Int) == None /// unify(Int or Str, Int) == Some(Int or Str) /// unify(Int or Str, NoneType) == None + /// unify(K(1), K(2)) == None + /// unify(Int, ?U(<: Int) and ?T(<: Int)) == Some(?U and ?T) /// ``` fn unify(&self, lhs: &Type, rhs: &Type) -> Option { match (lhs, rhs) { @@ -2006,6 +2022,19 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { return None; } } + (And(tys), other) | (other, And(tys)) => { + let mut unified = Obj; + for ty in tys { + if let Some(t) = self.unify(ty, other) { + unified = self.ctx.intersection(&unified, &t); + } + } + if unified != Obj && unified != Never { + return Some(unified); + } else { + return None; + } + } (FreeVar(fv), _) if fv.is_linked() => return self.unify(&fv.crack(), rhs), (_, FreeVar(fv)) if fv.is_linked() => return self.unify(lhs, &fv.crack()), // TODO: unify(?T, ?U) ? @@ -2035,6 +2064,20 @@ impl<'c, 'l, 'u, L: Locational> Unifier<'c, 'l, 'u, L> { if r_sup == Obj || self.ctx.is_trait(&r_sup) { continue; } + let Ok(l_substituter) = Substituter::substitute_typarams(self.ctx, &l_sup, lhs) + else { + continue; + }; + let mut tv_cache = TyVarCache::new(self.ctx.level, self.ctx); + let l_sup = self.ctx.detach(l_sup.clone(), &mut tv_cache); + drop(l_substituter); + let Ok(r_substituter) = Substituter::substitute_typarams(self.ctx, &r_sup, rhs) + else { + continue; + }; + let mut tv_cache = TyVarCache::new(self.ctx.level, self.ctx); + let r_sup = self.ctx.detach(r_sup.clone(), &mut tv_cache); + drop(r_substituter); if let Some(t) = self.ctx.max(&l_sup, &r_sup).either() { return Some(t.clone()); } diff --git a/crates/erg_compiler/lib/core/_erg_std_prelude.py b/crates/erg_compiler/lib/core/_erg_std_prelude.py index 58befaa6e..f36927e23 100644 --- a/crates/erg_compiler/lib/core/_erg_std_prelude.py +++ b/crates/erg_compiler/lib/core/_erg_std_prelude.py @@ -24,3 +24,37 @@ class Never: pass + +from typing import Generic, TypeVar + +Ty = TypeVar('Ty') +M = TypeVar('M', bound=int) +L = TypeVar("L", bound=int) +T = TypeVar("T", bound=int) +I = TypeVar("I", bound=int) +Θ = 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) + def __str__(self): + return f"Dimension({float(self)})" + def __add__(self, other): + return Dimension(float(self) + other) + def __sub__(self, other): + return Dimension(float(self) - other) + def __mul__(self, other): + return Dimension(float(self) * other) + def __rmul__(self, other): + return Dimension(other * float(self)) + def __truediv__(self, other): + return Dimension(float(self) / other) + def __floordiv__(self, other): + return Dimension(float(self) // other) + def __rtruediv__(self, other): + return Dimension(other / float(self)) + def __rfloordiv__(self, other): + return Dimension(other // float(self)) + def type_check(self, t: type) -> bool: + return t.__name__ == "Dimension" diff --git a/crates/erg_compiler/lib/core/_erg_type.py b/crates/erg_compiler/lib/core/_erg_type.py index cc2373844..5d9a6c271 100644 --- a/crates/erg_compiler/lib/core/_erg_type.py +++ b/crates/erg_compiler/lib/core/_erg_type.py @@ -25,10 +25,12 @@ def __repr__(self): class FakeGenericAlias: + __name__: str __origin__: type __args__: list # list[type] def __init__(self, origin, *args): + self.__name__ = origin.__name__ self.__origin__ = origin self.__args__ = args diff --git a/crates/erg_compiler/lib/std/exception.er b/crates/erg_compiler/lib/std/exception.er index 6d0bb34e5..0f3a54a4c 100644 --- a/crates/erg_compiler/lib/std/exception.er +++ b/crates/erg_compiler/lib/std/exception.er @@ -1,6 +1,5 @@ unsound = import "unsound" -# TODO: exception: Exception unsound.pyexec(""" def try_(p, exc=lambda _: None, els=lambda: None, fin=lambda: None): __result = None diff --git a/crates/erg_compiler/lib/std/unit.er b/crates/erg_compiler/lib/std/unit.er new file mode 100644 index 000000000..7f6790e5f --- /dev/null +++ b/crates/erg_compiler/lib/std/unit.er @@ -0,0 +1,96 @@ +unsound = import "unsound" + +unsound.pyexec(""" +kg = Dimension(1) +m = Dimension(1) +s = Dimension(1) +a = Dimension(1) +k = Dimension(1) +mol = Dimension(1) +cd = Dimension(1) +""") +.kg = unsound.pyeval("kg") +.m = unsound.pyeval("m") +.s = unsound.pyeval("s") +.a = unsound.pyeval("a") +.k = unsound.pyeval("k") +.mol = unsound.pyeval("mol") +.cd = unsound.pyeval("cd") + +assert .kg in Dimension(Int, 1, 0, 0, 0, 0, 0, 0) +assert .m in Dimension(Int, 0, 1, 0, 0, 0, 0, 0) +assert .s in Dimension(Int, 0, 0, 1, 0, 0, 0, 0) +assert .a in Dimension(Int, 0, 0, 0, 1, 0, 0, 0) +assert .k in Dimension(Int, 0, 0, 0, 0, 1, 0, 0) +assert .mol in Dimension(Int, 0, 0, 0, 0, 0, 1, 0) +assert .cd in Dimension(Int, 0, 0, 0, 0, 0, 0, 1) + +# Base unit types +''' +Kilogram +''' +.Kg = Dimension(Int, 1, 0, 0, 0, 0, 0, 0) +''' +Meter +''' +.M = Dimension(Int, 0, 1, 0, 0, 0, 0, 0) +''' +Second +''' +.S = Dimension(Int, 0, 0, 1, 0, 0, 0, 0) +''' +Ampere +''' +.A = Dimension(Int, 0, 0, 0, 1, 0, 0, 0) +''' +Kelvin +''' +.K = Dimension(Int, 0, 0, 0, 0, 1, 0, 0) +.Mol = Dimension(Int, 0, 0, 0, 0, 0, 1, 0) +''' +Candela +''' +.Cd = Dimension(Int, 0, 0, 0, 0, 0, 0, 1) +# Derived unit types +.Hz = Dimension(Int, 0, 0, -1, 0, 0, 0, 0) +.J = Dimension(Int, 1, 2, -2, 0, 0, 0, 0) +.N = Dimension(Int, 1, 1, -2, 0, 0, 0, 0) +.Pa = Dimension(Int, 1, -1, -2, 0, 0, 0, 0) +.W = Dimension(Int, 1, 2, -3, 0, 0, 0, 0) +.C = Dimension(Int, 0, 0, 1, 1, 0, 0, 0) +.V = Dimension(Int, 1, 2, -3, -1, 0, 0, 0) +.F = Dimension(Int, -1, -2, 4, 2, 0, 0, 0) +.Ohm = Dimension(Int, 1, 2, -3, -2, 0, 0, 0) +.Siemens = Dimension(Int, -1, -2, 3, 2, 0, 0, 0) +.Wb = Dimension(Int, 1, 2, -2, -1, 0, 0, 0) +.Tesla = Dimension(Int, 1, 0, -2, -1, 0, 0, 0) +.Henry = Dimension(Int, 1, 2, -2, -2, 0, 0, 0) +.Bq = Dimension(Int, 0, 0, -1, 0, 0, 0, 0) +.Gy = Dimension(Int, 2, 0, -2, 0, 0, 0, 0) +.Sv = Dimension(Int, 2, 0, -2, 0, 0, 0, 0) +.Kat = Dimension(Int, 0, 0, -1, 0, 0, 1, 0) + +.quecto = 1e-30 +.ronto = 1e-27 +.yocto = 1e-24 +.zepto = 1e-21 +.atto = 1e-18 +.femto = 1e-15 +.pico = 1e-12 +.nano = 1e-9 +.micro = 1e-6 +.milli = 1e-3 +.centi = 1e-2 +.deci = 1e-1 +.deca = 1e+1 +.hecto = 1e+2 +.kilo = 1e+3 +.mega = 1e+6 +.giga = 1e+9 +.tera = 1e+12 +.peta = 1e+15 +.exa = 1e+18 +.zetta = 1e+21 +.yotta = 1e+24 +.ronna = 1e+27 +.quetta = 1e+30 diff --git a/crates/erg_compiler/transpile.rs b/crates/erg_compiler/transpile.rs index 987a1c5d5..c7b577ec9 100644 --- a/crates/erg_compiler/transpile.rs +++ b/crates/erg_compiler/transpile.rs @@ -988,7 +988,7 @@ impl PyScriptGenerator { } fn transpile_simple_call(&mut self, call: Call) -> String { - let enc = if call.obj.ref_t().is_poly_type_meta() { + let enc = if call.obj.ref_t().is_poly_meta_type() { Enclosure::Bracket } else { Enclosure::Paren diff --git a/crates/erg_compiler/ty/mod.rs b/crates/erg_compiler/ty/mod.rs index 32f782779..4022b17f2 100644 --- a/crates/erg_compiler/ty/mod.rs +++ b/crates/erg_compiler/ty/mod.rs @@ -2853,11 +2853,11 @@ impl Type { } } - pub fn is_poly_type_meta(&self) -> bool { + pub fn is_poly_meta_type(&self) -> bool { match self { - Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_poly_type_meta(), - Self::Refinement(refine) => refine.t.is_poly_type_meta(), - Self::Quantified(q) => q.is_poly_type_meta(), + Self::FreeVar(fv) if fv.is_linked() => fv.crack().is_poly_meta_type(), + Self::Refinement(refine) => refine.t.is_poly_meta_type(), + Self::Quantified(q) => q.is_poly_meta_type(), Self::Subr(subr) => subr.return_t.is_type(), _ => false, } @@ -3415,6 +3415,10 @@ impl Type { || (self.has_no_qvar() && self.has_no_unbound_var()) } + pub fn is_polymorphic(&self) -> bool { + matches!(self.typarams_len(), Some(1..)) + } + /// TODO: /// ```erg /// Nat == {x: Int | x >= 0} diff --git a/crates/erg_compiler/ty/value.rs b/crates/erg_compiler/ty/value.rs index 994040acc..39cd0d882 100644 --- a/crates/erg_compiler/ty/value.rs +++ b/crates/erg_compiler/ty/value.rs @@ -975,6 +975,7 @@ impl PartialEq for ValueObj { match (self, other) { (Self::Int(i1), Self::Int(i2)) => i1 == i2, (Self::Nat(n1), Self::Nat(n2)) => n1 == n2, + (Self::Int(i), Self::Nat(n)) | (Self::Nat(n), Self::Int(i)) => *i as u64 == *n, (Self::Float(f1), Self::Float(f2)) => f1 == f2, (Self::Str(s1), Self::Str(s2)) => s1 == s2, (Self::Bool(b1), Self::Bool(b2)) => b1 == b2, diff --git a/examples/use_unit.er b/examples/use_unit.er new file mode 100644 index 000000000..5410e79b3 --- /dev/null +++ b/examples/use_unit.er @@ -0,0 +1,13 @@ +{m; s; kg; Kg} = import "unit" + +print! kg + kg +j = kg*m*m/(s*s) +v = j/kg*s/m +print! m/s + v + +Joule = Dimension(Int, 1, 2, -2, 0, 0, 0, 0) +j: Joule + +f _: Kg = None +f kg +f kg/m*m diff --git a/tests/should_err/use_unit.er b/tests/should_err/use_unit.er new file mode 100644 index 000000000..da70e9507 --- /dev/null +++ b/tests/should_err/use_unit.er @@ -0,0 +1,12 @@ +{m; s; kg; Kg} = import "unit" + +print! kg + m # ERR +j = kg*m*m/(s*s) +v = j/kg*s/m +print! m/s + v*m # ERR + +Joule = Dimension(Int, 1, 2, -2, 0, 0, 0, 0) +m: Joule # ERR + +f _: Kg = None +f kg/m # ERR diff --git a/tests/test.rs b/tests/test.rs index 4ed20fb92..4bf731aeb 100644 --- a/tests/test.rs +++ b/tests/test.rs @@ -467,6 +467,11 @@ fn exec_tuple_test() -> Result<(), ()> { expect_success("tests/should_ok/tuple.er", 0) } +#[test] +fn exec_use_unit() -> Result<(), ()> { + expect_success("examples/use_unit.er", 0) +} + #[test] fn exec_unit_test() -> Result<(), ()> { expect_success("examples/unit_test.er", 0) @@ -769,6 +774,11 @@ fn exec_refinement_class_err() -> Result<(), ()> { expect_failure("tests/should_err/refinement_class.er", 0, 2) } +#[test] +fn exec_use_unit_err() -> Result<(), ()> { + expect_failure("tests/should_err/use_unit.er", 0, 4) +} + #[test] fn exec_var_args_err() -> Result<(), ()> { expect_failure("tests/should_err/var_args.er", 0, 4) From ff53af0cb643157df4b34c38d5546fa90839aa48 Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Fri, 20 Sep 2024 20:31:03 +0900 Subject: [PATCH 2/3] 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 From b3a7a6a4deb27a74da00ba7689d458620255a83b Mon Sep 17 00:00:00 2001 From: Shunsuke Shibayama Date: Fri, 20 Sep 2024 21:15:40 +0900 Subject: [PATCH 3/3] doc: change example code --- README.md | 4 ++-- README_JA.md | 4 ++-- README_zh-CN.md | 4 ++-- README_zh-TW.md | 4 ++-- crates/erg_compiler/lib/std/unit.er | 28 ++++++++++++++++++++++++++++ 5 files changed, 36 insertions(+), 8 deletions(-) diff --git a/README.md b/README.md index fb81d3ecc..69b3f0fd0 100644 --- a/README.md +++ b/README.md @@ -53,11 +53,11 @@ print! "hello, ", end := "" # TypeError: `.times!` is a method of `Nat` (0 or more Int), not `Int` - {Meter; Sec; meter; yard; sec} = import "unit" + {Meter; Sec; meter; kg; sec} = import "unit" velocity x: Meter, t: Sec = x / t - v = velocity 3yard, 2sec # TypeError: the type of `x` was mismatched: expect `Meter`, found `Yard` + v = velocity 3kg, 2sec # TypeError: the type of `x` was mismatched: expect `Meter`, found `Kg` v = velocity 3meter, 2sec # v == 1.5 m/s ``` diff --git a/README_JA.md b/README_JA.md index 7ac177895..2b847cd81 100644 --- a/README_JA.md +++ b/README_JA.md @@ -54,11 +54,11 @@ print! "hello,", end := "" # TypeError: `.times!`は`Nat`(0以上のInt)のメソッドです、`Int`ではありません - {Meter; Sec; meter; yard; sec} = import "unit" + {Meter; Sec; Kg; meter; sec} = import "unit" velocity x: Meter, t: Sec = x / t - v = velocity 3yard, 2sec # TypeError: `x`の型が適合しません。`Meter`を予期しましたが、`Yard`が渡されました + v = velocity 3kg, 2sec # TypeError: `x`の型が適合しません。`Meter`を予期しましたが、`Kg`が渡されました v = velocity 3meter, 2sec # v == 1.5 m/s ``` diff --git a/README_zh-CN.md b/README_zh-CN.md index e1d2856f7..3a4386e44 100644 --- a/README_zh-CN.md +++ b/README_zh-CN.md @@ -53,11 +53,11 @@ print! "hello, ", end := "" # 类型错误: `.times!`是`Nat`(0或更大整数)的方法，不是`Int`的 - {Meter; Sec; meter; yard; sec} = import "unit" + {Meter; Sec; meter; kg; sec} = import "unit" velocity x: Meter, t: Sec = x / t - v = velocity 3yard, 2sec # 类型错误: `x`的类型不匹配: 预期为`Meter`，找到`Yard'` + v = velocity 3kg, 2sec # 类型错误: `x`的类型不匹配: 预期为`Meter`，找到`Kg` v = velocity 3meter, 2sec # v == 1.5 m/s ``` diff --git a/README_zh-TW.md b/README_zh-TW.md index f7de12d33..cc769e7ff 100644 --- a/README_zh-TW.md +++ b/README_zh-TW.md @@ -53,11 +53,11 @@ print! "hello, ", end := "" # 類型錯誤: `.times!`是`Nat`(0或更大整數)的方法，不是`Int`的 - {Meter; Sec; meter; yard; sec} = import "unit" + {Meter; Sec; meter; kg; sec} = import "unit" velocity x: Meter, t: Sec = x / t - v = velocity 3yard, 2sec # 類型錯誤: `x`的類型不匹配: 預期為`Meter`，找到`Yard'` + v = velocity 3kg, 2sec # 類型錯誤: `x`的類型不匹配: 預期為`Meter`，找到`Kg` v = velocity 3meter, 2sec # v == 1.5 m/s ``` diff --git a/crates/erg_compiler/lib/std/unit.er b/crates/erg_compiler/lib/std/unit.er index 7f6790e5f..4b9179e05 100644 --- a/crates/erg_compiler/lib/std/unit.er +++ b/crates/erg_compiler/lib/std/unit.er @@ -16,6 +16,11 @@ cd = Dimension(1) .k = unsound.pyeval("k") .mol = unsound.pyeval("mol") .cd = unsound.pyeval("cd") +.meter = .m +.sec = .s +.ampere = .a +.kelvin = .k +.candela = .cd assert .kg in Dimension(Int, 1, 0, 0, 0, 0, 0, 0) assert .m in Dimension(Int, 0, 1, 0, 0, 0, 0, 0) @@ -24,6 +29,11 @@ assert .a in Dimension(Int, 0, 0, 0, 1, 0, 0, 0) assert .k in Dimension(Int, 0, 0, 0, 0, 1, 0, 0) assert .mol in Dimension(Int, 0, 0, 0, 0, 0, 1, 0) assert .cd in Dimension(Int, 0, 0, 0, 0, 0, 0, 1) +assert .meter in Dimension(Int, 0, 1, 0, 0, 0, 0, 0) +assert .sec in Dimension(Int, 0, 0, 1, 0, 0, 0, 0) +assert .ampere in Dimension(Int, 0, 0, 0, 1, 0, 0, 0) +assert .kelvin in Dimension(Int, 0, 0, 0, 0, 1, 0, 0) +assert .candela in Dimension(Int, 0, 0, 0, 0, 0, 0, 1) # Base unit types ''' @@ -34,41 +44,59 @@ Kilogram Meter ''' .M = Dimension(Int, 0, 1, 0, 0, 0, 0, 0) +.Meter = .M ''' Second ''' .S = Dimension(Int, 0, 0, 1, 0, 0, 0, 0) +.Sec = .S ''' Ampere ''' .A = Dimension(Int, 0, 0, 0, 1, 0, 0, 0) +.Ampere = .A ''' Kelvin ''' .K = Dimension(Int, 0, 0, 0, 0, 1, 0, 0) +.Kelvin = .K .Mol = Dimension(Int, 0, 0, 0, 0, 0, 1, 0) ''' Candela ''' .Cd = Dimension(Int, 0, 0, 0, 0, 0, 0, 1) +.Candela = .Cd # Derived unit types .Hz = Dimension(Int, 0, 0, -1, 0, 0, 0, 0) +.Hertz = .Hz .J = Dimension(Int, 1, 2, -2, 0, 0, 0, 0) +.Joule = .J .N = Dimension(Int, 1, 1, -2, 0, 0, 0, 0) +.Newton = .N .Pa = Dimension(Int, 1, -1, -2, 0, 0, 0, 0) +.Pascal = .Pa .W = Dimension(Int, 1, 2, -3, 0, 0, 0, 0) +.Watt = .W .C = Dimension(Int, 0, 0, 1, 1, 0, 0, 0) +.Coulomb = .C .V = Dimension(Int, 1, 2, -3, -1, 0, 0, 0) +.Volt = .V .F = Dimension(Int, -1, -2, 4, 2, 0, 0, 0) +.Farad = .F .Ohm = Dimension(Int, 1, 2, -3, -2, 0, 0, 0) .Siemens = Dimension(Int, -1, -2, 3, 2, 0, 0, 0) .Wb = Dimension(Int, 1, 2, -2, -1, 0, 0, 0) +.Weber = .Wb .Tesla = Dimension(Int, 1, 0, -2, -1, 0, 0, 0) .Henry = Dimension(Int, 1, 2, -2, -2, 0, 0, 0) .Bq = Dimension(Int, 0, 0, -1, 0, 0, 0, 0) +.Becquerel = .Bq .Gy = Dimension(Int, 2, 0, -2, 0, 0, 0, 0) +.Gray = .Gy .Sv = Dimension(Int, 2, 0, -2, 0, 0, 0, 0) +.Sievert = .Sv .Kat = Dimension(Int, 0, 0, -1, 0, 0, 1, 0) +.Katal = .Kat .quecto = 1e-30 .ronto = 1e-27