Skip to content

Commit

Permalink
add lien-set into subtyping to address sketchiness
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 16, 2024
1 parent 5465273 commit c89d907
Show file tree
Hide file tree
Showing 3 changed files with 70 additions and 18 deletions.
2 changes: 1 addition & 1 deletion src/type_system/lien_set.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use crate::{
};

judgment_fn! {
fn lien_set_from_chain(
pub fn lien_set_from_chain(
env: Env,
a: LienChain,
) => Set<Lien> {
Expand Down
63 changes: 56 additions & 7 deletions src/type_system/subtypes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ use crate::{
type_system::{
env::Env,
lien_chains::{lien_chains, ty_chains, Lien, LienChain, My, Our, TyChain},
lien_set::lien_set_from_chain,
quantifiers::fold_zipped,
},
};
Expand Down Expand Up @@ -162,14 +163,20 @@ judgment_fn! {

(
(if place_covered_by_place(&a, &b))
(lien_chain_covered_by(chain_a, chain_b) => ())
(lien_set_from_chain(&env, &chain_a) => lien_set_a)
(lien_set_from_chain(&env, &chain_b) => lien_set_b)
(lien_set_covered_by(&lien_set_a, lien_set_b) => ())
(lien_chain_covered_by(&chain_a, &chain_b) => ())
--------------------------- ("sh-sh")
(sub_lien_chains(env, Cons(Lien::Shared(a), chain_a), Cons(Lien::Shared(b), chain_b)) => &env)
)

(
(if place_covered_by_place(&a, &b))
(lien_chain_strictly_covered_by(chain_a, chain_b) => ())
(lien_set_from_chain(&env, &chain_a) => lien_set_a)
(lien_set_from_chain(&env, &chain_b) => lien_set_b)
(lien_set_covered_by(&lien_set_a, lien_set_b) => ())
(lien_chain_strictly_covered_by(&chain_a, &chain_b) => ())
--------------------------- ("l-l")
(sub_lien_chains(env, Cons(Lien::Leased(a), chain_a), Cons(Lien::Leased(b), chain_b)) => &env)
)
Expand All @@ -183,6 +190,28 @@ judgment_fn! {
}
}

judgment_fn! {
fn lien_set_covered_by(
a: Set<Lien>,
b: Set<Lien>,
) => () {
debug(a, b)

(
------------------------------- ("nil")
(lien_set_covered_by((), _b) => ())
)

(
(&b_s => b)
(lien_covered_by(&a, b) => ())
(lien_set_covered_by(&a_s, &b_s) => ())
------------------------------- ("cons")
(lien_set_covered_by(Cons(a, a_s), b_s) => ())
)
}
}

judgment_fn! {
fn lien_chain_covered_by(
a: LienChain,
Expand Down Expand Up @@ -216,18 +245,38 @@ judgment_fn! {
(lien_chain_strictly_covered_by(My(), My()) => ())
)

(
(lien_covered_by(lien_a, lien_b) => ())
(lien_chain_strictly_covered_by(&chain_a, &chain_b) => ())
------------------------------- ("lien-lien")
(lien_chain_strictly_covered_by(Cons(lien_a, chain_a), Cons(lien_b, chain_b)) => ())
)
}
}

judgment_fn! {
fn lien_covered_by(
a: Lien,
b: Lien,
) => () {
debug(a, b)

(
(if place_covered_by_place(&a, &b))
(lien_chain_strictly_covered_by(chain_a, chain_b) => ())
------------------------------- ("lease-lease")
(lien_chain_strictly_covered_by(Cons(Lien::Leased(a), chain_a), Cons(Lien::Leased(b), chain_b)) => ())
(lien_covered_by(Lien::Leased(a), Lien::Leased(b)) => ())
)

(
(if place_covered_by_place(&a, &b))
------------------------------- ("shared-shared")
(lien_covered_by(Lien::Shared(a), Lien::Shared(b)) => ())
)

(
(if a == b)
(lien_chain_strictly_covered_by(chain_a, chain_b) => ())
------------------------------- ("var-var")
(lien_chain_strictly_covered_by(Cons(Lien::Var(a), chain_a), Cons(Lien::Var(b), chain_b)) => ())
------------------------------- ("var")
(lien_covered_by(Lien::Var(a), Lien::Var(b)) => ())
)
}
}
Expand Down
23 changes: 13 additions & 10 deletions src/type_system/tests/subtyping.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -443,7 +443,6 @@ fn shared_from_P_d1_to_shared_from_P_d2() {
/// This type is actually semi uninhabitable.
#[test]
#[allow(non_snake_case)]
#[ignore = "FIXME: subtyping with non-implied items"]
fn shared_pair1_leased_pair2_to_shared_pair1() {
check_program(&term(
"
Expand All @@ -461,25 +460,29 @@ fn shared_pair1_leased_pair2_to_shared_pair1() {
",
))
.assert_err(expect_test::expect![[r#"
check program `class Pair { d1 : Data ; d2 : Data ; } class Data { } class Main { fn test (my self pair : Pair, data : our leased {pair} Data) -> our Data { data . give ; } }`
check program `class Pair { d1 : Data ; d2 : Data ; } class Data { } class Main { fn test (my self pair1 : Pair, pair2 : Pair, data : shared {pair1} leased {pair2} Data) -> shared {pair1} Data { data . give ; } }`
Caused by:
0: check class named `Main`
1: check method named `test`
2: check function body
3: judgment `can_type_expr_as { expr: { data . give ; }, as_ty: our Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased {pair} Data, pair: Pair}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
3: judgment `can_type_expr_as { expr: { data . give ; }, as_ty: shared {pair1} Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared {pair1} leased {pair2} Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "can_type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr_as { expr: { data . give ; }, as_ty: our Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased {pair} Data, pair: Pair}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
judgment `type_expr_as { expr: { data . give ; }, as_ty: shared {pair1} Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared {pair1} leased {pair2} Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "type_expr_as" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub { a: our leased {pair} Data, b: our Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased {pair} Data, pair: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
judgment `sub { a: shared {pair1} leased {pair2} Data, b: shared {pair1} Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared {pair1} leased {pair2} Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
judgment `sub_in_cx { chain_a: my, a: our leased {pair} Data, chain_b: my, b: our Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased {pair} Data, pair: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_in_cx { chain_a: my, a: shared {pair1} leased {pair2} Data, chain_b: my, b: shared {pair1} Data, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared {pair1} leased {pair2} Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sub" failed at step #2 (src/file.rs:LL:CC) because
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(our leased{pair}, Data)}, ty_liens_b: {NamedTy(our, Data)}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased {pair} Data, pair: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(shared{pair1} leased{pair2}, Data)}, ty_liens_b: {NamedTy(shared{pair1}, Data)}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared {pair1} leased {pair2} Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_ty_chains { ty_chain_a: NamedTy(our leased{pair}, Data), ty_chain_b: NamedTy(our, Data), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased {pair} Data, pair: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_ty_chains { ty_chain_a: NamedTy(shared{pair1} leased{pair2}, Data), ty_chain_b: NamedTy(shared{pair1}, Data), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared {pair1} leased {pair2} Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "named ty" failed at step #3 (src/file.rs:LL:CC) because
judgment had no applicable rules: `sub_lien_chains { a: our leased{pair}, b: our, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: our leased {pair} Data, pair: Pair}, assumptions: {}, fresh: 0 } }`"#]]);
judgment `sub_lien_chains { a: shared{pair1} leased{pair2}, b: shared{pair1}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: shared {pair1} leased {pair2} Data, pair1: Pair, pair2: Pair}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "sh-sh" failed at step #3 (src/file.rs:LL:CC) because
judgment `lien_set_covered_by { a: {leased{pair2}}, b: {} }` failed at the following rule(s):
the rule "cons" failed at step #0 (src/file.rs:LL:CC) because
expression evaluated to an empty collection: `&b_s`"#]]);
}
#[test]
#[allow(non_snake_case)]
Expand Down Expand Up @@ -723,6 +726,6 @@ fn leased_vec_my_Data_to_leased_vec_leased_Data() {
judgment `sub_ty_chains { ty_chain_a: NamedTy(leased{source}, Data), ty_chain_b: NamedTy(leased{source} leased{source}, Data), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "named ty" failed at step #3 (src/file.rs:LL:CC) because
judgment `sub_lien_chains { a: leased{source}, b: leased{source} leased{source}, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {source} Vec[my Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "l-l" failed at step #1 (src/file.rs:LL:CC) because
the rule "l-l" failed at step #4 (src/file.rs:LL:CC) because
judgment had no applicable rules: `lien_chain_strictly_covered_by { a: my, b: leased{source} }`"#]]);
}

0 comments on commit c89d907

Please sign in to comment.