From 0ab0ceb81ea512a2faf2b25adbf3f8bf273b2fd7 Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sat, 17 Feb 2024 07:29:36 -0500 Subject: [PATCH] more cancellation tests, cleanup compatibile code The layout logic was too simplistic. Replace with a judgment so we can e.g. test predicates easily. --- TODO.md | 2 ++ src/type_system/lien_chains.rs | 27 ++------------- src/type_system/subtypes.rs | 50 +++++++++++++++++++++++---- src/type_system/tests/cancellation.rs | 21 +++++++++++ src/type_system/tests/subtyping.rs | 42 +++++++++++++++++----- 5 files changed, 102 insertions(+), 40 deletions(-) diff --git a/TODO.md b/TODO.md index d12b287..6cc11be 100644 --- a/TODO.md +++ b/TODO.md @@ -26,3 +26,5 @@ Notes to myself about possible next steps: - [ ] introduce environment consistency check and assert it at various points - [ ] type inference - [ ] `foo.give.share` -- does this even parse? +- [ ] boxed classes +- [ ] boxed type \ No newline at end of file diff --git a/src/type_system/lien_chains.rs b/src/type_system/lien_chains.rs index 07f01e0..51d52bd 100644 --- a/src/type_system/lien_chains.rs +++ b/src/type_system/lien_chains.rs @@ -51,22 +51,6 @@ pub struct My(); #[derive(Copy, Clone, PartialOrd, Ord, PartialEq, Eq, Debug, Hash)] pub struct Our(); -#[derive(Clone, PartialOrd, Ord, PartialEq, Eq, Debug, Hash)] -pub enum LiensLayout { - ByValue, - ByRef, - ByVar(UniversalVar), -} - -impl TyChain { - pub fn lien_chain(&self) -> &LienChain { - match self { - TyChain::Var(lien_chain, _) => lien_chain, - TyChain::NamedTy(lien_chain, _) => lien_chain, - } - } -} - impl LienChain { fn apply_all(&self, liens: LienChain) -> Self { let mut this = self.clone(); @@ -122,15 +106,8 @@ impl LienChain { self.apply_lien(Lien::Leased(place.upcast()), pending) } - pub fn layout(&self) -> LiensLayout { - match self.vec.first() { - Some(lien) => match lien { - Lien::Our | Lien::Shared(_) => LiensLayout::ByValue, - Lien::Leased(_) => LiensLayout::ByRef, - Lien::Var(v) => LiensLayout::ByVar(v.clone()), - }, - None => LiensLayout::ByValue, - } + pub fn is_not_my(&self) -> bool { + !self.vec.is_empty() } } diff --git a/src/type_system/subtypes.rs b/src/type_system/subtypes.rs index 86014be..bc94fe9 100644 --- a/src/type_system/subtypes.rs +++ b/src/type_system/subtypes.rs @@ -95,10 +95,8 @@ judgment_fn! { ( (if a == b)! - (sub_lien_chains(env, live_after, chain_a, chain_b) => env) - (let layout_a = ty_chain_a.lien_chain().layout()) - (let layout_b = ty_chain_b.lien_chain().layout()) - (if layout_a == layout_b) + (sub_lien_chains(env, live_after, &chain_a, &chain_b) => env) + (compatible_layout(env, &chain_a, &chain_b) => env) -------------------------------- ("var") (sub_ty_chains(env, live_after, TyChain::Var(chain_a, a), TyChain::Var(chain_b, b)) => env) ) @@ -111,15 +109,53 @@ judgment_fn! { (fold_zipped(env, ¶meters_a, ¶meters_b, &|env, parameter_a, parameter_b| { sub_generic_parameter(env, &live_after, &chain_a, parameter_a, &chain_b, parameter_b) }) => env) - (let layout_a = ty_chain_a.lien_chain().layout()) - (let layout_b = ty_chain_b.lien_chain().layout()) - (if layout_a == layout_b) // FIXME: should consider if these are boxed classes + (compatible_layout(env, &chain_a, &chain_b) => env) -------------------------------- ("named ty") (sub_ty_chains(env, live_after, TyChain::NamedTy(chain_a, a), TyChain::NamedTy(chain_b, b)) => env) ) } } +judgment_fn! { + fn compatible_layout( + env: Env, + chain_a: LienChain, + chain_b: LienChain, + ) => Env { + debug(chain_a, chain_b, env) + + trivial(chain_a == chain_b => env) + + ( + (lien_chain_is_shared(env, chain) => env) + ------------------------------- ("my-shared") + (compatible_layout(env, My(), chain) => env) + ) + + ( + (lien_chain_is_shared(env, chain) => env) + ------------------------------- ("shared-my") + (compatible_layout(env, chain, My()) => env) + ) + + ( + (if chain_a.is_not_my() && chain_b.is_not_my())! + (lien_chain_is_shared(env, chain_a) => env) + (lien_chain_is_shared(env, &chain_b) => env) + ------------------------------- ("shared-shared") + (compatible_layout(env, chain_a, chain_b) => env) + ) + + ( + (if chain_a.is_not_my() && chain_b.is_not_my())! + (lien_chain_is_leased(env, chain_a) => env) + (lien_chain_is_leased(env, &chain_b) => env) + ------------------------------- ("leased-leased") + (compatible_layout(env, chain_a, chain_b) => env) + ) + } +} + judgment_fn! { fn sub_generic_parameter( env: Env, diff --git a/src/type_system/tests/cancellation.rs b/src/type_system/tests/cancellation.rs index e4d8390..6770b01 100644 --- a/src/type_system/tests/cancellation.rs +++ b/src/type_system/tests/cancellation.rs @@ -282,3 +282,24 @@ fn return_leased_dead_leased_to_leased_and_use_while_leased() { &accessed_place = p &leased_place = p"#]]); } + +#[test] +#[allow(non_snake_case)] +fn forall_leased_P_leased_P_data_to_P_data() { + check_program(&term( + " + class Data { + } + class Main { + fn test[perm P](my self, data: P Data) -> P Data + where + leased(P), + { + let p: leased{data} Data = data.lease; + p.give; + } + } + ", + )) + .assert_ok(expect_test::expect!["()"]); +} diff --git a/src/type_system/tests/subtyping.rs b/src/type_system/tests/subtyping.rs index 9544cde..ecd85f0 100644 --- a/src/type_system/tests/subtyping.rs +++ b/src/type_system/tests/subtyping.rs @@ -705,10 +705,14 @@ fn leased_vec_my_Data_to_leased_vec_leased_Data() { judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(my, Data)}, ty_liens_b: {NamedTy(leased{source}, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, 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 "cons" failed at step #1 (src/file.rs:LL:CC) because judgment `sub_ty_chains { ty_chain_a: NamedTy(my, Data), ty_chain_b: NamedTy(leased{source}, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, 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 #7 (src/file.rs:LL:CC) because - condition evaluted to false: `layout_a == layout_b` - layout_a = ByValue - layout_b = ByRef"#]]); + the rule "named ty" failed at step #5 (src/file.rs:LL:CC) because + judgment `compatible_layout { chain_a: my, chain_b: 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 "my-shared" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `lien_chain_is_shared { chain: 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 } }` + the rule "shared_a" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `lien_chain_is_shared { chain: 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 } }` + the rule "shared_b" failed at step #0 (src/file.rs:LL:CC) because + judgment had no applicable rules: `lien_chain_is_shared { chain: 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 } }`"#]]); } #[test] @@ -824,10 +828,32 @@ fn forall_P_vec_my_Data_to_P_vec_P_Data() { judgment `sub_ty_chain_sets { ty_liens_a: {NamedTy(my, Data)}, ty_liens_b: {NamedTy(!perm_0, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, 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(my, Data), ty_chain_b: NamedTy(!perm_0, Data), live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): - the rule "named ty" failed at step #7 (src/file.rs:LL:CC) because - condition evaluted to false: `layout_a == layout_b` - layout_a = ByValue - layout_b = ByVar(!perm_0)"#]]); + the rule "named ty" failed at step #5 (src/file.rs:LL:CC) because + judgment `compatible_layout { chain_a: my, chain_b: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "my-shared" failed at step #0 (src/file.rs:LL:CC) because + judgment `lien_chain_is_shared { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "var" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_predicate { predicate: shared(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "shared" failed at step #0 (src/file.rs:LL:CC) because + judgment `is_shared { a: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "is_shared" failed at step #1 (src/file.rs:LL:CC) because + cyclic proof attempt: `lien_chain_is_shared { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` + the rule "shared_a" failed at step #0 (src/file.rs:LL:CC) because + judgment `lien_chain_is_shared { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "var" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_predicate { predicate: shared(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "shared" failed at step #0 (src/file.rs:LL:CC) because + judgment `is_shared { a: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "is_shared" failed at step #1 (src/file.rs:LL:CC) because + cyclic proof attempt: `lien_chain_is_shared { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` + the rule "shared_b" failed at step #0 (src/file.rs:LL:CC) because + judgment `lien_chain_is_shared { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "var" failed at step #0 (src/file.rs:LL:CC) because + judgment `prove_predicate { predicate: shared(!perm_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "shared" failed at step #0 (src/file.rs:LL:CC) because + judgment `is_shared { a: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s): + the rule "is_shared" failed at step #1 (src/file.rs:LL:CC) because + cyclic proof attempt: `lien_chain_is_shared { chain: !perm_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Vec[Data], source: my Vec[my Data]}, assumptions: {}, fresh: 0 } }`"#]]); } #[test]