Skip to content

Commit

Permalink
handle context/leased-invariance better
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 17, 2024
1 parent f20aea5 commit 54a01c6
Show file tree
Hide file tree
Showing 8 changed files with 150 additions and 52 deletions.
16 changes: 8 additions & 8 deletions src/type_system/lien_chains.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -230,15 +230,15 @@ pub fn collapse(pairs: Set<(LienChain, LienChain)>) -> Set<LienChain> {
judgment_fn! {
pub fn ty_chains(
env: Env,
liens: LienChain,
cx: LienChain,
a: Ty,
) => Set<TyChain> {
debug(liens, a, env)
debug(cx, a, env)

(
(ty_chains_cx(&env, liens, My(), a) => ty_liens)
(ty_chains_cx(&env, My(), cx, a) => ty_liens)
----------------------------------- ("restrictions")
(ty_chains(env, liens, a) => ty_liens)
(ty_chains(env, cx, a) => ty_liens)
)
}
}
Expand Down Expand Up @@ -305,15 +305,15 @@ judgment_fn! {
judgment_fn! {
pub fn lien_chains(
env: Env,
liens: LienChain,
cx: LienChain,
a: Parameter,
) => Set<LienChain> {
debug(liens, a, env)
debug(cx, a, env)

(
(lien_chain_pairs(&env, liens, My(), a) => pairs)
(lien_chain_pairs(&env, My(), cx, a) => pairs)
----------------------------------- ("restrictions")
(lien_chains(env, liens, a) => collapse(pairs))
(lien_chains(env, cx, a) => collapse(pairs))
)
}
}
Expand Down
58 changes: 47 additions & 11 deletions src/type_system/subtypes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,27 +34,27 @@ judgment_fn! {
fn sub_in_cx(
env: Env,
live_after: LivePlaces,
chain_a: LienChain,
cx_a: LienChain,
a: Parameter,
chain_b: LienChain,
cx_b: LienChain,
b: Parameter,
) => Env {
debug(chain_a, a, chain_b, b, live_after, env)
debug(cx_a, a, cx_b, b, live_after, env)

(
(ty_chains(&env, liens_a, a) => ty_liens_a)
(ty_chains(&env, &liens_b, &b) => ty_liens_b)
(ty_chains(&env, cx_a, a) => ty_liens_a)
(ty_chains(&env, &cx_b, &b) => ty_liens_b)
(sub_ty_chain_sets(&env, &live_after, &ty_liens_a, ty_liens_b) => env)
------------------------------- ("sub")
(sub_in_cx(env, live_after, liens_a, a: Ty, liens_b, b: Ty) => env)
(sub_in_cx(env, live_after, cx_a, a: Ty, cx_b, b: Ty) => env)
)

(
(lien_chains(&env, liens_a, a) => liens_a)
(lien_chains(&env, &liens_b, &b) => liens_b)
(sub_lien_chain_sets(&env, &live_after, &liens_a, liens_b) => env)
(lien_chains(&env, cx_a, a) => chain_a)
(lien_chains(&env, &cx_b, &b) => chain_b)
(sub_lien_chain_sets(&env, &live_after, &chain_a, chain_b) => env)
------------------------------- ("sub")
(sub_in_cx(env, live_after, liens_a, a: Perm, liens_b, b: Perm) => env)
(sub_in_cx(env, live_after, cx_a, a: Perm, cx_b, b: Perm) => env)
)
}
}
Expand Down Expand Up @@ -108,7 +108,7 @@ judgment_fn! {
(if name_a == name_b)! // FIXME: subtyping between classes
(sub_lien_chains(env, &live_after, &chain_a, &chain_b) => env)
(fold_zipped(env, &parameters_a, &parameters_b, &|env, parameter_a, parameter_b| {
sub_in_cx(env, &live_after, &chain_a, parameter_a, &chain_b, 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())
Expand All @@ -119,6 +119,42 @@ judgment_fn! {
}
}

judgment_fn! {
fn sub_generic_parameter(
env: Env,
live_after: LivePlaces,
cx_a: LienChain,
a: Parameter,
cx_b: LienChain,
b: Parameter,
) => Env {
debug(cx_a, a, cx_b, b, live_after, env)

// For a leased type, the generics have to be exactly the same on both sides
// and we don't inherit context. Consider `leased Vec[T]` -- when the lease is up,
// it's going to go back to a `my Vec[T]`, so we don't treat it as a `leased Vec[leased T]`.
(
(if cx_a.is_leased(&env))!
(assert cx_b.is_leased(&env))
(sub_in_cx(env, &live_after, My(), &a, My(), &b) => env)
(sub_in_cx(env, &live_after, My(), &b, My(), &a) => env)
------------------------------- ("invariant")
(sub_generic_parameter(env, live_after, cx_a, a, cx_b, b) => env)
)

// For non-leased types, the generics can inherit context, since they are read only
// and hence covariant. For example `shared Vec[T]` is basically the same as a
// `shared Vec[shared T]`.
(
(if !cx_a.is_leased(&env))!
(assert !cx_b.is_leased(&env))
(sub_in_cx(env, live_after, cx_a, a, cx_b, b) => env)
------------------------------- ("covariant")
(sub_generic_parameter(env, live_after, cx_a, a, cx_b, b) => env)
)
}
}

judgment_fn! {
/// Provable if every chain in `chains_a` is a subchain of some chain in `chains_b`.
fn sub_lien_chain_sets(
Expand Down
2 changes: 1 addition & 1 deletion src/type_system/tests/assignment.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@ fn assign_leased_to_field_of_lease_that_is_typed_as_my() {
the rule "type_expr_as" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub { a: !perm_0 Data, b: Data, live_after: LivePlaces { accessed: {}, traversed: {pair} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Data, pair: !perm_0 Pair}, assumptions: {leased(!perm_0)}, 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: !perm_0 Data, chain_b: my, b: Data, live_after: LivePlaces { accessed: {}, traversed: {pair} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Data, pair: !perm_0 Pair}, assumptions: {leased(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_in_cx { cx_a: my, a: !perm_0 Data, cx_b: my, b: Data, live_after: LivePlaces { accessed: {}, traversed: {pair} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Data, pair: !perm_0 Pair}, assumptions: {leased(!perm_0)}, 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(!perm_0, Data)}, ty_liens_b: {NamedTy(my, Data)}, live_after: LivePlaces { accessed: {}, traversed: {pair} }, env: Env { program: "...", universe: universe(1), in_scope_vars: [!perm_0], local_variables: {self: my Main, data: !perm_0 Data, pair: !perm_0 Pair}, assumptions: {leased(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
Expand Down
4 changes: 2 additions & 2 deletions src/type_system/tests/cancellation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ fn shared_live_leased_to_our_leased() {
the rule "type_expr_as" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub { a: shared {p} Data, b: our leased {d} Data, live_after: LivePlaces { accessed: {p}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, d: Data, p: leased {d} Data, q: shared {p} Data}, 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: shared {p} Data, chain_b: my, b: our leased {d} Data, live_after: LivePlaces { accessed: {p}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, d: Data, p: leased {d} Data, q: shared {p} Data}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_in_cx { cx_a: my, a: shared {p} Data, cx_b: my, b: our leased {d} Data, live_after: LivePlaces { accessed: {p}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, d: Data, p: leased {d} Data, q: shared {p} Data}, 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(shared{p} leased{d}, Data)}, ty_liens_b: {NamedTy(our leased{d}, Data)}, live_after: LivePlaces { accessed: {p}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, d: Data, p: leased {d} Data, q: shared {p} Data}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
Expand Down Expand Up @@ -168,7 +168,7 @@ fn leased_live_leased_to_leased() {
the rule "type_expr_as" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub { a: leased {p} Data, b: leased {d} Data, live_after: LivePlaces { accessed: {p}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, d: Data, p: leased {d} Data, q: leased {p} Data}, 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: leased {p} Data, chain_b: my, b: leased {d} Data, live_after: LivePlaces { accessed: {p}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, d: Data, p: leased {d} Data, q: leased {p} Data}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_in_cx { cx_a: my, a: leased {p} Data, cx_b: my, b: leased {d} Data, live_after: LivePlaces { accessed: {p}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, d: Data, p: leased {d} Data, q: leased {p} Data}, 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(leased{p} leased{d}, Data)}, ty_liens_b: {NamedTy(leased{d}, Data)}, live_after: LivePlaces { accessed: {p}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, d: Data, p: leased {d} Data, q: leased {p} Data}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
Expand Down
2 changes: 1 addition & 1 deletion src/type_system/tests/fn_calls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -463,7 +463,7 @@ fn pair_method__expect_leased_self_a__got_leased_self_b() {
the rule "cons" failed at step #5 (src/file.rs:LL:CC) because
judgment `sub { a: leased {@ fresh(0) . b} Data, b: leased {@ fresh(0) . a} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Pair, @ fresh(1): leased {@ fresh(0) . b} Data, data: leased {@ fresh(0) . b} Data, pair: Pair}, assumptions: {}, fresh: 2 } }` 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: leased {@ fresh(0) . b} Data, chain_b: my, b: leased {@ fresh(0) . a} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Pair, @ fresh(1): leased {@ fresh(0) . b} Data, data: leased {@ fresh(0) . b} Data, pair: Pair}, assumptions: {}, fresh: 2 } }` failed at the following rule(s):
judgment `sub_in_cx { cx_a: my, a: leased {@ fresh(0) . b} Data, cx_b: my, b: leased {@ fresh(0) . a} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Pair, @ fresh(1): leased {@ fresh(0) . b} Data, data: leased {@ fresh(0) . b} Data, pair: Pair}, assumptions: {}, fresh: 2 } }` 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(leased{@ fresh(0) . b}, Data)}, ty_liens_b: {NamedTy(leased{@ fresh(0) . a}, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Pair, @ fresh(1): leased {@ fresh(0) . b} Data, data: leased {@ fresh(0) . b} Data, pair: Pair}, assumptions: {}, fresh: 2 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
Expand Down
2 changes: 1 addition & 1 deletion src/type_system/tests/new_with_self_references.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ fn choice_with_non_self_ref() {
the rule "cons" failed at step #6 (src/file.rs:LL:CC) because
judgment `sub { a: shared {d3} Data, b: shared {@ fresh(0) . pair} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): Choice, d1: Data, d2: Data, d3: Data, pair: Pair, r: shared {d3} Data}, assumptions: {}, fresh: 1 } }` 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: shared {d3} Data, chain_b: my, b: shared {@ fresh(0) . pair} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): Choice, d1: Data, d2: Data, d3: Data, pair: Pair, r: shared {d3} Data}, assumptions: {}, fresh: 1 } }` failed at the following rule(s):
judgment `sub_in_cx { cx_a: my, a: shared {d3} Data, cx_b: my, b: shared {@ fresh(0) . pair} Data, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): Choice, d1: Data, d2: Data, d3: Data, pair: Pair, r: shared {d3} Data}, assumptions: {}, fresh: 1 } }` 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(shared{d3}, Data)}, ty_liens_b: {NamedTy(shared{@ fresh(0) . pair}, Data)}, live_after: LivePlaces { accessed: {}, traversed: {} }, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): Choice, d1: Data, d2: Data, d3: Data, pair: Pair, r: shared {d3} Data}, assumptions: {}, fresh: 1 } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
Expand Down
Loading

0 comments on commit 54a01c6

Please sign in to comment.