Skip to content

Commit

Permalink
more cancellation tests, cleanup compatibile code
Browse files Browse the repository at this point in the history 
The layout logic was too simplistic. Replace
with a judgment so we can e.g. test predicates
easily.
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 17, 2024
1 parent 394ecc3 commit 0ab0ceb
Show file tree
Hide file tree
Showing 5 changed files with 102 additions and 40 deletions.
2 changes: 2 additions & 0 deletions TODO.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
27 changes: 2 additions & 25 deletions src/type_system/lien_chains.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -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()
}
}

Expand Down
50 changes: 43 additions & 7 deletions src/type_system/subtypes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)
)
Expand All @@ -111,15 +109,53 @@ judgment_fn! {
(fold_zipped(env, &parameters_a, &parameters_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,
Expand Down
21 changes: 21 additions & 0 deletions src/type_system/tests/cancellation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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!["()"]);
}
42 changes: 34 additions & 8 deletions src/type_system/tests/subtyping.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down Expand Up @@ -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]
Expand Down

0 comments on commit 0ab0ceb

Please sign in to comment.