language-servers/erg
1
0
Fork 0
mirror of https://github.com/erg-lang/erg.git synced 2025-08-04 10:49:54 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: subtyping bugs

Browse source
This commit is contained in:
Shunsuke Shibayama 2023-03-19 23:21:11 +09:00
parent 988f9f6c99
commit b40666d618
7 changed files with 45 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

2
crates/erg_compiler/context/compare.rs
View file

@ -925,6 +925,7 @@ impl Context {
self.union(&fv.crack(), other)
}
(Refinement(l), Refinement(r)) => Type::Refinement(self.union_refinement(l, r)),
(Structural(l), Structural(r)) => self.union(l, r).structuralize(),
(t, Type::Never) | (Type::Never, t) => t.clone(),
// Array({1, 2}, 2), Array({3, 4}, 2) ==> Array({1, 2, 3, 4}, 2)
(
@ -987,6 +988,7 @@ impl Context {
self.intersection(&fv.crack(), other)
}
(Refinement(l), Refinement(r)) => Type::Refinement(self.intersection_refinement(l, r)),
(Structural(l), Structural(r)) => self.intersection(l, r).structuralize(),
// {.i = Int} and {.s = Str} == {.i = Int; .s = Str}
(Record(l), Record(r)) => Type::Record(l.clone().concat(r.clone())),
// {i = Int; j = Int} and not {i = Int} == {j = Int}

14
crates/erg_compiler/context/initialize/classes.rs
View file

@ -560,6 +560,20 @@ impl Context {
ValueObj::builtin_class(Nat),
);
nat.register_trait(Nat, nat_add);
/*
Since `Int <: Sub(Int)`, the fact that `Nat <: Sub(Nat)` is not inherently necessary.
However, if there were a constraint `T <: Sub(T)`, we would not be able to let `T = Nat`, so we temporarily insert this trait implementation.
In the future, it will be implemented automatically by glue patch.
*/
let op_t_ = fn1_met(Nat, Nat, Int);
let mut nat_sub = Self::builtin_methods(Some(poly(SUB, vec![ty_tp(Nat)])), 2);
nat_sub.register_builtin_erg_impl(OP_SUB, op_t_, Const, Visibility::BUILTIN_PUBLIC);
nat_sub.register_builtin_const(
OUTPUT,
Visibility::BUILTIN_PUBLIC,
ValueObj::builtin_class(Int),
);
nat.register_trait(Nat, nat_sub);
let mut nat_mul = Self::builtin_methods(Some(poly(MUL, vec![ty_tp(Nat)])), 2);
nat_mul.register_builtin_erg_impl(OP_MUL, op_t.clone(), Const, Visibility::BUILTIN_PUBLIC);
nat_mul.register_builtin_const(

3
crates/erg_compiler/context/initialize/patches.rs
View file

@ -74,5 +74,8 @@ impl Context {
option_eq_impl.register_builtin_erg_impl("__eq__", op_t, Const, Visibility::BUILTIN_PUBLIC);
option_eq.register_trait(base, option_eq_impl);
self.register_builtin_patch("OptionEq", option_eq, Visibility::BUILTIN_PRIVATE, Const);
/* SuperSub (U <: T <: Sub(T) ==> U <: Sub(U)) */
// SuperSub|T <: Sub(T)| U <: T = Patch U
// SuperSub|U <: Sub(U)|
}
}

28
crates/erg_compiler/context/instantiate.rs
View file

@ -338,9 +338,6 @@ impl Context {
let t = self.instantiate_t_inner(*t, tmp_tv_cache, loc)?;
Ok(TyParam::t(t))
}
TyParam::FreeVar(fv) if fv.is_linked() => {
self.instantiate_tp(fv.crack().clone(), tmp_tv_cache, loc)
}
p @ (TyParam::Value(_)
| TyParam::Mono(_)
| TyParam::FreeVar(_)
@ -370,32 +367,10 @@ impl Context {
let (name, constr) = (fv.unbound_name().unwrap(), fv.constraint().unwrap());
if let Some(t) = tmp_tv_cache.get_tyvar(&name) {
let t = t.clone();
if let Type::FreeVar(fv) = &t {
if fv
.constraint()
.map(|cons| cons.is_uninited())
.unwrap_or(false)
{
let new_constr =
tmp_tv_cache.instantiate_constraint(constr, self, loc)?;
fv.update_constraint(new_constr, true);
}
}
Ok(t)
} else if let Some(tp) = tmp_tv_cache.get_typaram(&name) {
if let TyParam::Type(t) = tp {
let t = *t.clone();
if let Type::FreeVar(fv) = &t {
if fv
.constraint()
.map(|cons| cons.is_uninited())
.unwrap_or(false)
{
let new_constr =
tmp_tv_cache.instantiate_constraint(constr, self, loc)?;
fv.update_constraint(new_constr, true);
}
}
Ok(t)
} else {
todo!(
@ -508,9 +483,6 @@ impl Context {
let t = self.instantiate_t_inner(*t, tmp_tv_cache, loc)?;
Ok(t.structuralize())
}
FreeVar(fv) if fv.is_linked() => {
self.instantiate_t_inner(fv.crack().clone(), tmp_tv_cache, loc)
}
FreeVar(fv) => {
let (sub, sup) = fv.get_subsup().unwrap();
let sub = self.instantiate_t_inner(sub, tmp_tv_cache, loc)?;

28
crates/erg_compiler/context/unify.rs
View file

@ -619,21 +619,25 @@ impl Context {
// ?T(<: Add(?T))
// ?U(:> {1, 2}, <: Add(?U)) ==> {1, 2}
rfv.forced_undoable_link(&rsub);
for (lps, rps) in lsub.typarams().iter().zip(rsub.typarams().iter()) {
self.sub_unify_tp(lps, rps, None, loc, false)
.map_err(|errs| {
rfv.undo();
errs
})?;
if lsub.qual_name() == rsub.qual_name() {
for (lps, rps) in lsub.typarams().iter().zip(rsub.typarams().iter()) {
self.sub_unify_tp(lps, rps, None, loc, false)
.map_err(|errs| {
rfv.undo();
errs
})?;
}
}
// lsup: Add(?X(:> Int)), rsup: Add(?Y(:> Nat))
// => lsup: Add(?X(:> Int)), rsup: Add((?X(:> Int)))
for (lps, rps) in lsup.typarams().iter().zip(rsup.typarams().iter()) {
self.sub_unify_tp(lps, rps, None, loc, false)
.map_err(|errs| {
rfv.undo();
errs
})?;
if lsup.qual_name() == rsup.qual_name() {
for (lps, rps) in lsup.typarams().iter().zip(rsup.typarams().iter()) {
self.sub_unify_tp(lps, rps, None, loc, false)
.map_err(|errs| {
rfv.undo();
errs
})?;
}
}
rfv.undo();
let intersec = self.intersection(&lsup, &rsup);

9
tests/should_err/subtyping.er
View file

@ -47,3 +47,12 @@ g x =
g 1 # OK
g None # ERR
h x, y =
_ = x == y
_ = x - y
x + y
_ = h -1, -2 # OK
_ = h 1, 2 # OK
_ = h "a", "b" # ERR

2
tests/test.rs
View file

@ -283,7 +283,7 @@ fn exec_structural_err() -> Result<(), ()> {
#[test]
fn exec_subtyping_err() -> Result<(), ()> {
expect_failure("tests/should_err/subtyping.er", 8)
expect_failure("tests/should_err/subtyping.er", 10)
}
#[test]