feat: add Dimension and unit module

This commit is contained in:
Shunsuke Shibayama 2024-09-20 16:56:22 +09:00
parent 82848c10d6
commit 4651a383ae
16 changed files with 392 additions and 10 deletions

View file

@ -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 {

View file

@ -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)

View file

@ -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,

View file

@ -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";

View file

@ -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)| {

View file

@ -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<Type> {
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());
}

View file

@ -24,3 +24,37 @@ Record = tuple
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"

View file

@ -25,10 +25,12 @@ class UnionType:
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

View file

@ -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

View file

@ -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

View file

@ -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

View file

@ -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}

View file

@ -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,