Skip to content

Commit

Permalink
split class/value types in type chains
Browse files Browse the repository at this point in the history
  • Loading branch information
@nikomatsakis
nikomatsakis committed Feb 29, 2024
1 parent 5bad692 commit b61992c
Show file tree
Hide file tree
Showing 12 changed files with 91 additions and 79 deletions.
13 changes: 11 additions & 2 deletions src/type_system/lien_chains.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,8 @@ use crate::{
#[derive(Clone, PartialOrd, Ord, PartialEq, Eq, Debug, Hash)]
pub enum TyChain {
Var(LienChain, UniversalVar),
NamedTy(LienChain, NamedTy),
ClassTy(LienChain, NamedTy),
ValueTy(LienChain, NamedTy),
}

cast_impl!(TyChain);
Expand Down Expand Up @@ -235,9 +236,17 @@ judgment_fn! {
debug(chain, pending, a, env)

(
(if env.is_class_ty(&n.name))!
(let chain = chain.apply_all(&env, pending))
----------------------------------- ("named-ty")
(ty_chains_cx(env, chain, pending, n: NamedTy) => set![TyChain::NamedTy(chain, n)])
(ty_chains_cx(env, chain, pending, n: NamedTy) => set![TyChain::ClassTy(chain, n)])
)

(
(if env.is_value_ty(&n.name))!
(let chain = chain.apply_all(&env, pending))
----------------------------------- ("named-ty")
(ty_chains_cx(env, chain, pending, n: NamedTy) => set![TyChain::ValueTy(chain, n)])
)

(
Expand Down
5 changes: 4 additions & 1 deletion src/type_system/lien_set.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,10 @@ judgment_fn! {
(lien_set_from_ty_chains(&env, &liens1) => lien_set1)
(lien_set_from_parameters(&env, &parameters) => lien_set2)
----------------------------------- ("nil")
(lien_set_from_ty_chains(env, Cons(TyChain::NamedTy(liens, NamedTy { name: _, parameters }), liens1)) => (&lien_set0, &lien_set1, lien_set2))
(lien_set_from_ty_chains(env, Cons(
TyChain::ClassTy(liens, NamedTy { name: _, parameters }) | TyChain::ValueTy(liens, NamedTy { name: _, parameters }),
liens1,
)) => (&lien_set0, &lien_set1, lien_set2))
)
}
}
Expand Down
12 changes: 6 additions & 6 deletions src/type_system/subtypes.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -104,8 +104,8 @@ judgment_fn! {
(
(let NamedTy { name: name_a, parameters: parameters_a } = a)
(let NamedTy { name: name_b, parameters: parameters_b } = b)
(if name_a == name_b) // FIXME: subtyping between classes
(if env.is_class_ty(&name_a))!
(assert env.is_class_ty(&name_a))
(if name_a == name_b)! // FIXME: subtyping between classes
(sub_lien_chains(env, &live_after, &chain_a, &chain_b) => env)
(let variances = env.variances(&name_a)?)
(if parameters_a.len() == variances.len())
Expand All @@ -115,19 +115,19 @@ judgment_fn! {
}) => env)
(compatible_layout(env, &chain_a, &chain_b) => env)
-------------------------------- ("class ty")
(sub_ty_chains(env, live_after, TyChain::NamedTy(chain_a, a), TyChain::NamedTy(chain_b, b)) => env)
(sub_ty_chains(env, live_after, TyChain::ClassTy(chain_a, a), TyChain::ClassTy(chain_b, b)) => env)
)

(
(let NamedTy { name: name_a, parameters: parameters_a } = a)
(let NamedTy { name: name_b, parameters: parameters_b } = b)
(if name_a == name_b)
(if env.is_value_ty(&name_a))!
(assert env.is_value_ty(&name_a))
(if name_a == name_b)!
(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)
}) => env)
-------------------------------- ("value ty")
(sub_ty_chains(env, live_after, TyChain::NamedTy(chain_a, a), TyChain::NamedTy(chain_b, b)) => env)
(sub_ty_chains(env, live_after, TyChain::ValueTy(chain_a, a), TyChain::ValueTy(chain_b, b)) => env)
)
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/type_system/tests/assignment.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,9 +46,9 @@ fn assign_leased_to_field_of_lease_that_is_typed_as_my() {
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
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), 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_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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_ty_chain_sets { ty_liens_a: {ClassTy(!perm_0, Data)}, ty_liens_b: {ClassTy(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), relative(!perm_0), atomic(!perm_0)}, 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(!perm_0, Data), ty_chain_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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
judgment `sub_ty_chains { ty_chain_a: ClassTy(!perm_0, Data), ty_chain_b: ClassTy(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), relative(!perm_0), atomic(!perm_0)}, fresh: 0 } }` failed at the following rule(s):
the rule "class ty" failed at step #4 (src/file.rs:LL:CC) because
judgment had no applicable rules: `sub_lien_chains { a: !perm_0, b: my, 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 } }`"#]]);
}
Expand Down
8 changes: 4 additions & 4 deletions src/type_system/tests/cancellation.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,9 +79,9 @@ fn shared_live_leased_to_our_leased() {
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
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):
judgment `sub_ty_chain_sets { ty_liens_a: {ClassTy(shared{p} leased{d}, Data)}, ty_liens_b: {ClassTy(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
judgment `sub_ty_chains { ty_chain_a: NamedTy(shared{p} leased{d}, Data), ty_chain_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):
judgment `sub_ty_chains { ty_chain_a: ClassTy(shared{p} leased{d}, Data), ty_chain_b: ClassTy(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 "class ty" failed at step #4 (src/file.rs:LL:CC) because
judgment `sub_lien_chains { a: shared{p} leased{d}, b: our leased{d}, 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 "cancel shared" failed at step #1 (src/file.rs:LL:CC) because
Expand Down Expand Up @@ -170,9 +170,9 @@ fn leased_live_leased_to_leased() {
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
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):
judgment `sub_ty_chain_sets { ty_liens_a: {ClassTy(leased{p} leased{d}, Data)}, ty_liens_b: {ClassTy(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
judgment `sub_ty_chains { ty_chain_a: NamedTy(leased{p} leased{d}, Data), ty_chain_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):
judgment `sub_ty_chains { ty_chain_a: ClassTy(leased{p} leased{d}, Data), ty_chain_b: ClassTy(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 "class ty" failed at step #4 (src/file.rs:LL:CC) because
judgment `sub_lien_chains { a: leased{p} leased{d}, b: leased{d}, 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 "cancel leased" failed at step #1 (src/file.rs:LL:CC) because
Expand Down
4 changes: 2 additions & 2 deletions src/type_system/tests/fn_calls.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -465,9 +465,9 @@ fn pair_method__expect_leased_self_a__got_leased_self_b() {
the rule "sub" failed at step #0 (src/file.rs:LL:CC) because
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):
judgment `sub_ty_chain_sets { ty_liens_a: {ClassTy(leased{@ fresh(0) . b}, Data)}, ty_liens_b: {ClassTy(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
judgment `sub_ty_chains { ty_chain_a: NamedTy(leased{@ fresh(0) . b}, Data), ty_chain_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):
judgment `sub_ty_chains { ty_chain_a: ClassTy(leased{@ fresh(0) . b}, Data), ty_chain_b: ClassTy(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 "class ty" failed at step #4 (src/file.rs:LL:CC) because
judgment `sub_lien_chains { a: leased{@ fresh(0) . b}, b: leased{@ fresh(0) . a}, 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 "matched starts" failed at step #0 (src/file.rs:LL:CC) because
Expand Down
Loading

0 comments on commit b61992c

Please sign in to comment.