Skip to content

Commit

Permalink
update expect
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 6, 2025
1 parent 8218458 commit 587ec6e
Show file tree
Hide file tree
Showing 5 changed files with 45 additions and 29 deletions.
46 changes: 29 additions & 17 deletions src/type_system/tests/assignment.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@ fn assign_leased_to_field_of_lease_that_is_typed_as_my() {
class Main {
fn test[perm P](my self, pair: P Pair, data: P Data) -> ()
where
leased(P),
move(P),
lent(P),
{
pair.d1 = data.give;
();
Expand All @@ -22,37 +23,47 @@ fn assign_leased_to_field_of_lease_that_is_typed_as_my() {
",
))
.assert_err(expect_test::expect![[r#"
check program `class Data { } class Pair { d1 : Data ; d2 : Data ; } class Main { fn test [perm] (my self pair : ^perm0_0 Pair, data : ^perm0_0 Data) -> () where leased(^perm0_0) { pair . d1 = data . give ; () ; } }`
check program `class Data { } class Pair { d1 : Data ; d2 : Data ; } class Main { fn test [perm] (my self pair : ^perm0_0 Pair, data : ^perm0_0 Data) -> () where move(^perm0_0), lent(^perm0_0) { pair . d1 = 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: { pair . d1 = data . give ; () ; }, as_ty: (), 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
3: judgment `can_type_expr_as { expr: { pair . d1 = data . give ; () ; }, as_ty: (), 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, 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: { pair . d1 = data . give ; () ; }, as_ty: (), 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
judgment `type_expr_as { expr: { pair . d1 = data . give ; () ; }, as_ty: (), 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "type_expr_as" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: { pair . d1 = data . give ; () ; }, 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
judgment `type_expr { expr: { pair . d1 = data . give ; () ; }, 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "block" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_block { block: { pair . d1 = data . give ; () ; }, 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
judgment `type_block { block: { pair . d1 = data . give ; () ; }, 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "place" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_statements_with_final_ty { statements: [pair . d1 = data . give ;, () ;], ty: (), 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
judgment `type_statements_with_final_ty { statements: [pair . d1 = data . give ;, () ;], ty: (), 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "cons" failed at step #1 (src/file.rs:LL:CC) because
judgment `type_statement { statement: pair . d1 = data . give ;, 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
judgment `type_statement { statement: pair . d1 = data . give ;, 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {} } }` failed at the following rule(s):
the rule "reassign" failed at step #1 (src/file.rs:LL:CC) because
judgment `type_expr_as { expr: data . give, as_ty: Data, 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
judgment `type_expr_as { expr: data . give, as_ty: Data, 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }, live_after: LivePlaces { accessed: {}, traversed: {pair} } }` failed at the following rule(s):
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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!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_under_perms { perms_a: RedPerms { copied: false, shared_from: {}, leased_from: {}, variables: {} }, a: !perm_0 Data, perms_b: RedPerms { copied: false, shared_from: {}, leased_from: {}, variables: {} }, 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_under_perms { chain_a: Chain { liens: [] }, a: !perm_0 Data, chain_b: Chain { liens: [] }, 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!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_some { lien_data_a: RedTerm { perms: RedPerms { copied: false, shared_from: {}, leased_from: {}, variables: {!perm_0} }, ty: NamedTy(Data) }, lien_datas_b: {RedTerm { perms: RedPerms { copied: false, shared_from: {}, leased_from: {}, variables: {} }, ty: NamedTy(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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_some { ty_chain_a: TyChain { chain: Chain { liens: [Variable(!perm_0)] }, ty: NamedTy(Data) }, ty_chains_b: {TyChain { chain: Chain { liens: [] }, ty: NamedTy(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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "sub-some" failed at step #1 (src/file.rs:LL:CC) because
judgment `sub_lien_data { lien_data_a: RedTerm { perms: RedPerms { copied: false, shared_from: {}, leased_from: {}, variables: {!perm_0} }, ty: NamedTy(Data) }, lien_data_b: RedTerm { perms: RedPerms { copied: false, shared_from: {}, leased_from: {}, variables: {} }, ty: NamedTy(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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_ty_chain { ty_chain_a: TyChain { chain: Chain { liens: [Variable(!perm_0)] }, ty: NamedTy(Data) }, ty_chain_b: TyChain { chain: Chain { liens: [] }, ty: NamedTy(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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "sub-named" failed at step #3 (src/file.rs:LL:CC) because
judgment `sub_perms { perms_a: RedPerms { copied: false, shared_from: {}, leased_from: {}, variables: {!perm_0} }, perms_b: RedPerms { copied: false, shared_from: {}, leased_from: {}, variables: {} }, 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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "sub-some" failed at step #1 (src/file.rs:LL:CC) because
condition evaluted to false: `perms_a.is_lent(&env).implies(perms_b.is_lent(&env))`"#]]);
judgment `sub_chains { chain_a: Chain { liens: [Variable(!perm_0)] }, chain_b: Chain { liens: [] }, 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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "my-sub-copy" failed at step #0 (src/file.rs:LL:CC) because
condition evaluted to false: `chain_a.is_owned(&env)`
chain_a = Chain { liens: [Variable(!perm_0)] }
&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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }
the rule "my-sub-owned" failed at step #0 (src/file.rs:LL:CC) because
condition evaluted to false: `chain_a.is_owned(&env)`
chain_a = Chain { liens: [Variable(!perm_0)] }
&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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }
the rule "our-sub-copy" failed at step #0 (src/file.rs:LL:CC) because
condition evaluted to false: `chain_a.is_owned(&env)`
chain_a = Chain { liens: [Variable(!perm_0)] }
&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: {move(!perm_0), lent(!perm_0), relative(!perm_0), atomic(!perm_0)}, fresh: 0 }"#]]);
}

/// Pair is leased from P, but when you assign to its fields,
Expand All @@ -67,7 +78,8 @@ fn assign_owned_to_field_of_lease_that_is_typed_as_my() {
class Main {
fn test[perm P](my self, pair: P Pair, data: my Data) -> ()
where
leased(P),
move(P),
lent(P),
{
pair.d1 = data.give;
();
Expand Down
12 changes: 8 additions & 4 deletions src/type_system/tests/cancellation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,8 @@ fn return_leased_dead_leased_to_leased() {
class Main {
fn test[perm P](my self, d: P Data) -> leased[d] Data
where
leased(P),
move(P),
lent(P),
{
let p: leased[d] Data = d.lease;
let q: leased[p] Data = p.lease;
Expand All @@ -253,7 +254,8 @@ fn return_leased_dead_leased_to_leased_and_use_while_leased() {
class Main {
fn test[perm P](my self, d: P Data) -> leased[d] Data
where
leased(P),
move(P),
lent(P),
{
let p: leased[d] Data = d.lease;
let q: leased[p] Data = p.lease;
Expand Down Expand Up @@ -319,7 +321,8 @@ fn forall_leased_P_leased_P_data_to_P_data() {
class Main {
fn test[perm P](my self, data: P Data) -> P Data
where
leased(P),
move(P),
lent(P),
{
let p: leased[data] Data = data.lease;
p.give;
Expand All @@ -340,7 +343,8 @@ fn forall_leased_P_shared_P_data_to_our_P_data() {
class Main {
fn test[perm P](my self, data: P Data) -> our P Data
where
leased(P),
move(P),
lent(P),
{
let p: shared[data] Data = data.share;
p.give;
Expand Down
9 changes: 6 additions & 3 deletions src/type_system/tests/fn_calls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,8 @@ fn send_two_different_messages() {
class Channel[ty M] {
fn send[perm P](P self, msg: M)
where
leased(P),
move(P),
lent(P),
{
}
}
Expand Down Expand Up @@ -47,7 +48,8 @@ fn send_same_message_twice() {
class Channel[ty M] {
fn send[perm P](P self, msg: M)
where
leased(P),
move(P),
lent(P),
{
}
}
Expand Down Expand Up @@ -116,7 +118,8 @@ fn needs_leased_got_shared_self() {
class Channel[ty M] {
fn send[perm P](P self, msg: M)
where
leased(P),
move(P),
lent(P),
{
}
}
Expand Down
3 changes: 2 additions & 1 deletion src/type_system/tests/subtyping.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -144,7 +144,8 @@ fn give_from_our_Data_to_leased_P() {
class Main {
fn test[perm P](my self) -> P Data
where
leased(P),
move(P),
lent(P),
{
let d: our Data = new Data();
d.give;
Expand Down
4 changes: 0 additions & 4 deletions src/type_system/tests/subtyping/liskov.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -228,10 +228,6 @@ fn liskov_from_pair_leased_with_pair_give() {
PAIR_LEASED,
&[
// In these tests, `pair` is live, and so leases from either `pair.{a,b}` cannot be canceled.

// NDM: bug seems to be that the type of `pair.a.lease` is being computed as
// `leased[pair.a] P my Data`, which then gets "double expanded". I think we want
// to strip the permissions from `pair.a` when we compute the type.
With(
"let d1: leased[pair.a] Data = pair.a.lease; \
let d2: leased[pair.b] Data = pair.b.lease;",
Expand Down

0 comments on commit 587ec6e

Please sign in to comment.