diff --git a/src/type_system/tests/assignment.rs b/src/type_system/tests/assignment.rs index 0d5a787..6662f70 100644 --- a/src/type_system/tests/assignment.rs +++ b/src/type_system/tests/assignment.rs @@ -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; (); @@ -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, @@ -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; (); diff --git a/src/type_system/tests/cancellation.rs b/src/type_system/tests/cancellation.rs index 245262a..8a8e324 100644 --- a/src/type_system/tests/cancellation.rs +++ b/src/type_system/tests/cancellation.rs @@ -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; @@ -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; @@ -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; @@ -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; diff --git a/src/type_system/tests/fn_calls.rs b/src/type_system/tests/fn_calls.rs index 0a07179..ff4a3e9 100644 --- a/src/type_system/tests/fn_calls.rs +++ b/src/type_system/tests/fn_calls.rs @@ -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), { } } @@ -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), { } } @@ -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), { } } diff --git a/src/type_system/tests/subtyping.rs b/src/type_system/tests/subtyping.rs index 50a86b0..952756c 100644 --- a/src/type_system/tests/subtyping.rs +++ b/src/type_system/tests/subtyping.rs @@ -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; diff --git a/src/type_system/tests/subtyping/liskov.rs b/src/type_system/tests/subtyping/liskov.rs index e53d4f3..7968b01 100644 --- a/src/type_system/tests/subtyping/liskov.rs +++ b/src/type_system/tests/subtyping/liskov.rs @@ -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;",