Skip to content

Commit

Permalink
introduce helper function for common combo
Browse files Browse the repository at this point in the history 
I have mixed feelings here. The code is shorter
but the push/pop pairs are no longer as evident.
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 6, 2024
1 parent 8802d20 commit a57a94f
Show file tree
Hide file tree
Showing 5 changed files with 20 additions and 18 deletions.
6 changes: 6 additions & 0 deletions src/type_system/env.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,12 @@ impl Env {
Ok(())
}

pub fn with_in_flight_stored_to_fresh_variable(&self, ty: impl Upcast<Ty>) -> (Self, Var) {
let (mut env, var) = self.push_fresh_variable(ty);
env = env.with_in_flight_stored_to(&var);
(env, var)
}

pub fn push_fresh_variable(&self, ty: impl Upcast<Ty>) -> (Env, Var) {
let mut env = self.clone();
let fresh = env.fresh;
Expand Down
6 changes: 2 additions & 4 deletions src/type_system/expressions.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,8 +131,7 @@ judgment_fn! {
(
// Start by typing the `this` expression, store into `@temp(0)`
(type_expr(env, flow, live_after.before(&exprs), &*receiver) => (env, flow, receiver_ty))
(let (env, this_var) = env.push_fresh_variable(&receiver_ty))
(let env = env.with_in_flight_stored_to(&this_var))
(let (env, this_var) = env.with_in_flight_stored_to_fresh_variable(&receiver_ty))

// Use receiver type to look up the method
(resolve_method(&env, &receiver_ty, &method_name, &parameters) => (this_input_ty, inputs, output, predicates))
Expand Down Expand Up @@ -309,8 +308,7 @@ judgment_fn! {
(
// Type the expression and then move `@in_flight` to `@input_temp`
(type_expr(env, flow, live_after.before(&exprs), expr) => (env, flow, expr_ty))
(let (env, input_temp) = env.push_fresh_variable(&expr_ty))
(let env = env.with_in_flight_stored_to(&input_temp))
(let (env, input_temp) = env.with_in_flight_stored_to_fresh_variable(&expr_ty))
(let () = tracing::debug!("type_method_arguments_as: expr_ty = {:?} input_temp = {:?} env = {:?}", expr_ty, input_temp, env))

// The expression type must be a subtype of the field type
Expand Down
6 changes: 2 additions & 4 deletions src/type_system/statements.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,7 @@ judgment_fn! {

(
(type_expr(env, flow, &live_after, expr) => (env, flow, ty))
(let (env, temp) = env.push_fresh_variable(&ty))
(let env = env.with_in_flight_stored_to(&temp))
(let (env, temp) = env.with_in_flight_stored_to_fresh_variable(&ty))
(env_permits_access(env, flow, &live_after, Access::Drop, &temp) => (env, flow))
(parameter_permits_access(env, flow, &ty, Access::Drop, &temp) => (env, flow))
(let env = env.pop_fresh_variable(&temp))
Expand Down Expand Up @@ -91,8 +90,7 @@ judgment_fn! {
// FIXME: should be live_after.without(place) -- or at least if place is just a variable
(place_ty(&env, &place) => ty)
(type_expr_as(&env, &flow, &live_after, &expr, &ty) => (env, flow))
(let (env, temp) = env.push_fresh_variable(&ty))
(let env = env.with_in_flight_stored_to(&temp))
(let (env, temp) = env.with_in_flight_stored_to_fresh_variable(&ty))
(env_permits_access(env, flow, &live_after, Access::Lease, &place) => (env, flow))
(let flow = flow.assign_place(&place))
(let env = env.with_var_stored_to(&temp, &place))
Expand Down
14 changes: 7 additions & 7 deletions src/type_system/tests/fn_calls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ fn send_same_message_twice() {
judgment `type_statement { statement: channel . lease . send [leased {channel}] (bar . give) ;, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, bar: Bar, channel: Channel[Bar]}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {bar} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
the rule "expr" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: channel . lease . send [leased {channel}] (bar . give), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, bar: Bar, channel: Channel[Bar]}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {bar} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
the rule "call" failed at step #8 (src/file.rs:LL:CC) because
the rule "call" failed at step #7 (src/file.rs:LL:CC) because
judgment `type_method_arguments_as { exprs: [bar . give], input_names: [msg], input_tys: [Bar], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): leased {channel} Channel[Bar], bar: Bar, channel: Channel[Bar]}, assumptions: {}, fresh: 1 }, flow: Flow { moved_places: {bar} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
the rule "cons" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: bar . give, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): leased {channel} Channel[Bar], bar: Bar, channel: Channel[Bar]}, assumptions: {}, fresh: 1 }, flow: Flow { moved_places: {bar} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
Expand Down Expand Up @@ -151,7 +151,7 @@ fn needs_leased_got_shared_self() {
judgment `type_statement { statement: channel . share . send [shared {channel}] (bar . give) ;, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, bar: Bar, channel: Channel[Bar]}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
the rule "expr" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: channel . share . send [shared {channel}] (bar . give), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, bar: Bar, channel: Channel[Bar]}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
the rule "call" failed at step #9 (src/file.rs:LL:CC) because
the rule "call" failed at step #8 (src/file.rs:LL:CC) because
judgment `prove_predicates { predicate: [leased(shared {channel})], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): shared {channel} Channel[Bar], @ fresh(1): Bar, bar: Bar, channel: Channel[Bar]}, assumptions: {}, fresh: 2 } }` failed at the following rule(s):
the rule "prove_predicates" failed at step #0 (src/file.rs:LL:CC) because
judgment `prove_predicate { predicate: leased(shared {channel}), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): shared {channel} Channel[Bar], @ fresh(1): Bar, bar: Bar, channel: Channel[Bar]}, assumptions: {}, fresh: 2 } }` failed at the following rule(s):
Expand Down Expand Up @@ -279,7 +279,7 @@ fn take_pair_and_data__give_pair_share_data_share_later() {
judgment `type_statement { statement: self . give . take_pair_and_data [my] (pair . give, data . share) ;, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, data: shared {pair . a} Data, pair: Pair}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {} }, live_after: LiveVars { vars: {data} } }` failed at the following rule(s):
the rule "expr" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: self . give . take_pair_and_data [my] (pair . give, data . share), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, data: shared {pair . a} Data, pair: Pair}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {} }, live_after: LiveVars { vars: {data} } }` failed at the following rule(s):
the rule "call" failed at step #10 (src/file.rs:LL:CC) because
the rule "call" failed at step #9 (src/file.rs:LL:CC) because
judgment `accesses_permitted { access: drop, places: [@ fresh(0), @ fresh(1), @ fresh(2)], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): my TheClass, @ fresh(1): Pair, @ fresh(2): shared {data} shared {@ fresh(1) . a} Data, data: shared {@ fresh(1) . a} Data, pair: Pair}, assumptions: {}, fresh: 3 }, flow: Flow { moved_places: {self, pair} }, live_after: LiveVars { vars: {data} } }` failed at the following rule(s):
the rule "accesses_permitted" failed at step #0 (src/file.rs:LL:CC) because
judgment `"flat_map"` failed at the following rule(s):
Expand Down Expand Up @@ -355,7 +355,7 @@ fn take_pair_and_data__give_pair_give_data_give_later() {
judgment `type_statement { statement: self . give . take_pair_and_data [my] (pair . give, data . give) ;, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, data: shared {pair . a} Data, pair: Pair}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {} }, live_after: LiveVars { vars: {data} } }` failed at the following rule(s):
the rule "expr" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: self . give . take_pair_and_data [my] (pair . give, data . give), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, data: shared {pair . a} Data, pair: Pair}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {} }, live_after: LiveVars { vars: {data} } }` failed at the following rule(s):
the rule "call" failed at step #10 (src/file.rs:LL:CC) because
the rule "call" failed at step #9 (src/file.rs:LL:CC) because
judgment `accesses_permitted { access: drop, places: [@ fresh(0), @ fresh(1), @ fresh(2)], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): my TheClass, @ fresh(1): Pair, @ fresh(2): shared {@ fresh(1) . a} Data, data: shared {@ fresh(1) . a} Data, pair: Pair}, assumptions: {}, fresh: 3 }, flow: Flow { moved_places: {self, data, pair} }, live_after: LiveVars { vars: {data} } }` failed at the following rule(s):
the rule "accesses_permitted" failed at step #0 (src/file.rs:LL:CC) because
judgment `"flat_map"` failed at the following rule(s):
Expand All @@ -375,7 +375,7 @@ fn take_pair_and_data__give_pair_give_data_give_later() {
condition evaluted to false: `place_disjoint_from(&accessed_place, &shared_place)`
&accessed_place = @ fresh(1)
&shared_place = @ fresh(1) . a
the rule "call" failed at step #10 (src/file.rs:LL:CC) because
the rule "call" failed at step #9 (src/file.rs:LL:CC) because
judgment `accesses_permitted { access: drop, places: [@ fresh(0), @ fresh(1), @ fresh(2)], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my TheClass, @ fresh(0): my TheClass, @ fresh(1): Pair, @ fresh(2): shared {@ fresh(1) . a} Data, data: shared {@ fresh(1) . a} Data, pair: Pair}, assumptions: {}, fresh: 3 }, flow: Flow { moved_places: {self, pair} }, live_after: LiveVars { vars: {data} } }` failed at the following rule(s):
the rule "accesses_permitted" failed at step #0 (src/file.rs:LL:CC) because
judgment `"flat_map"` failed at the following rule(s):
Expand Down Expand Up @@ -480,9 +480,9 @@ fn pair_method__expect_leased_self_a__got_leased_self_b() {
judgment `type_statement { statement: pair . give . method (data . give) ;, env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {pair . b} Data, pair: Pair}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
the rule "expr" failed at step #0 (src/file.rs:LL:CC) because
judgment `type_expr { expr: pair . give . method (data . give), env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, data: leased {pair . b} Data, pair: Pair}, assumptions: {}, fresh: 0 }, flow: Flow { moved_places: {} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
the rule "call" failed at step #8 (src/file.rs:LL:CC) because
the rule "call" failed at step #7 (src/file.rs:LL:CC) because
judgment `type_method_arguments_as { exprs: [data . give], input_names: [data], input_tys: [leased {@ fresh(0) . a} Data], env: Env { program: "...", universe: universe(0), in_scope_vars: [], local_variables: {self: my Main, @ fresh(0): Pair, data: leased {@ fresh(0) . b} Data, pair: Pair}, assumptions: {}, fresh: 1 }, flow: Flow { moved_places: {pair} }, live_after: LiveVars { vars: {} } }` failed at the following rule(s):
the rule "cons" failed at step #5 (src/file.rs:LL:CC) because
the rule "cons" failed at step #4 (src/file.rs:LL:CC) because
judgment `sub { a: leased {@ fresh(0) . b} Data, b: leased {@ fresh(0) . a} Data, 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 }, flow: Flow { moved_places: {data, pair} } }` failed at the following rule(s):
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
judgment `sub_in { terms_a: Terms { unique: true, shared: false, leased: false, vars: {}, named_tys: {}, shared_places: {}, leased_places: {} }, a: leased {@ fresh(0) . b} Data, terms_b: Terms { unique: true, shared: false, leased: false, vars: {}, named_tys: {}, shared_places: {}, leased_places: {} }, b: leased {@ fresh(0) . a} Data, 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 }, flow: Flow { moved_places: {data, pair} } }` failed at the following rule(s):
Expand Down
Loading

0 comments on commit a57a94f

Please sign in to comment.