fix: refinement subtyping

This commit is contained in:
Shunsuke Shibayama 2023-08-23 12:12:55 +09:00
parent dc7e0a341d
commit b9c4357038
3 changed files with 14 additions and 1 deletions

View file

@ -630,7 +630,13 @@ impl Context {
let l = Type::Refinement(l.clone().into_refinement());
self.structural_supertype_of(&l, rhs)
}
// ({I: Int | True} :> Int) == true, ({N: Nat | ...} :> Int) == false, ({I: Int | I >= 0} :> Int) == false
// {1, 2, 3} :> {1} or {2, 3} == true
(Refinement(_refine), Or(l, r)) => {
self.supertype_of(lhs, l) && self.supertype_of(lhs, r)
}
// ({I: Int | True} :> Int) == true
// {N: Nat | ...} :> Int) == false
// ({I: Int | I >= 0} :> Int) == false
(Refinement(l), r) => {
if l.pred.mentions(&l.var) {
match l.pred.can_be_false() {

2
tests/should_ok/slice.er Normal file
View file

@ -0,0 +1,2 @@
_ = [1, 2, 3][1] + 1
_ = ["c"] + ["a", "b"][1..1000]

View file

@ -263,6 +263,11 @@ fn exec_self_type() -> Result<(), ()> {
expect_success("tests/should_ok/self_type.er", 0)
}
#[test]
fn exec_slice() -> Result<(), ()> {
expect_success("tests/should_ok/slice.er", 0)
}
#[test]
fn exec_structural_example() -> Result<(), ()> {
expect_success("examples/structural.er", 0)