rework red-terms to have a single red-ty

we don't need full generality of a set of
ty-chains. imp't for method resolution in real
dada.

src/type_system/liens.rs

@@ -5,7 +5,7 @@ use crate::{
     type_system::{
         env::Env,
         quantifiers::union,
-        red_terms::{red_term, Chain, Lien, RedTerm, RedTy, TyChain},
+        red_terms::{red_term, Chain, Lien, RedPerm, RedTerm, RedTy},
     },
 };
 
@@ -17,69 +17,55 @@ judgment_fn! {
         debug(a, env)
 
         (
-            (red_term(&env, a) => red_term)
-            (union(&red_term.ty_chains, &|ty_chain| liens_from_ty_chain(&env, ty_chain)) => liens)
+            (red_term(&env, a) => RedTerm { red_perm, red_ty })
+            (liens_from_red_perm(&env, red_perm) => liens_1)
+            (liens_from_red_ty(&env, &red_ty) => liens_2)
             ----------------------------------- ("my")
-            (liens(env, a) => liens)
+            (liens(env, a) => (&liens_1, liens_2))
         )
     }
 }
 
 judgment_fn! {
-    fn liens_from_red_term(
+    fn liens_from_red_ty(
         env: Env,
-        a: RedTerm,
+        a: RedTy,
     ) => Set<Lien> {
         debug(a, env)
 
         (
-            (union(ty_chains, &|ty_chain| liens_from_ty_chain(&env, ty_chain)) => liens)
-            ----------------------------------- ("rule")
-            (liens_from_red_term(env, RedTerm { ty_chains }) => liens)
+            ----------------------------------- ("none")
+            (liens_from_red_ty(_env, RedTy::None) => ())
         )
-    }
-}
 
-judgment_fn! {
-    fn liens_from_ty_chain(
-        env: Env,
-        a: TyChain,
-    ) => Set<Lien> {
-        debug(a, env)
+        (
+            ----------------------------------- ("var")
+            (liens_from_red_ty(_env, RedTy::Var(_var)) => ())
+        )
 
         (
-            (liens_from_red_ty(&env, ty) => liens_1)
-            (liens_from_chain(&env, &chain) => liens_2)
+            (union(parameters, &|parameter| liens(&env, parameter)) => liens)
             ----------------------------------- ("named")
-            (liens_from_ty_chain(_env, TyChain { chain, ty }) => (&liens_1, liens_2))
+            (liens_from_red_ty(_env, RedTy::NamedTy(NamedTy { name: _, parameters })) => liens)
         )
     }
 }
 
 judgment_fn! {
-    fn liens_from_red_ty(
+    fn liens_from_red_perm(
         env: Env,
-        a: RedTy,
+        a: RedPerm,
     ) => Set<Lien> {
         debug(a, env)
 
         (
+            (union(chains, &|chain| liens_from_chain(&env, chain)) => liens)
             ----------------------------------- ("none")
-            (liens_from_red_ty(_env, RedTy::None) => ())
-        )
-
-        (
-            ----------------------------------- ("var")
-            (liens_from_red_ty(_env, RedTy::Var(_var)) => ())
-        )
-
-        (
-            (union(parameters, &|parameter| liens(&env, parameter)) => liens)
-            ----------------------------------- ("named")
-            (liens_from_red_ty(_env, RedTy::NamedTy(NamedTy { name: _, parameters })) => liens)
+            (liens_from_red_perm(_env, RedPerm { chains }) => liens)
         )
     }
 }
+
 judgment_fn! {
     fn liens_from_chain(
         env: Env,

src/type_system/red_terms.rs

@@ -15,26 +15,24 @@ use super::{env::Env, predicates::MeetsPredicate};
 /// using [`RedTy::None`][].
 #[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
 pub struct RedTerm {
-    pub ty_chains: Set<TyChain>,
+    pub red_perm: RedPerm,
+    pub red_ty: RedTy,
 }
 
 cast_impl!(RedTerm);
 
-/// A typed chain (of custody) indicates where the value originates
-/// as well as the type of data it contains. Somewhat confusing a [`TyChain`][]
-/// can also be constructed from a permission, in which case the type is
-/// [`RedTy::None`].
-#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
-pub struct TyChain {
-    pub chain: Chain,
-    pub ty: RedTy,
-}
-
-cast_impl!(TyChain);
-
-impl TyChain {
-    pub fn is_copy(&self, env: &Env) -> Fallible<bool> {
-        Ok(self.chain.is_copy(env) || self.ty.is_copy(env)?)
+impl RedTerm {
+    /// Create a set of [`TyChain`][] values from the [`RedTerm`][].
+    /// Convenient for subtyping.
+    pub fn ty_chains(&self) -> Set<TyChain> {
+        self.red_perm
+            .chains
+            .iter()
+            .map(|chain| TyChain {
+                chain: chain.clone(),
+                ty: self.red_ty.clone(),
+            })
+            .collect()
     }
 }
 
@@ -92,11 +90,20 @@ impl RedTy {
 /// All red perms represent something in this matrix (modulo generics).
 #[derive(Clone, Debug, Default, PartialOrd, Ord, PartialEq, Eq, Hash)]
 pub struct RedPerm {
-    chains: Set<Chain>,
+    pub chains: Set<Chain>,
 }
 
 cast_impl!(RedPerm);
 
+/// A "ty chain" combines a permission [`Chain`][] with a [`RedTy`][].
+#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
+pub struct TyChain {
+    pub chain: Chain,
+    pub ty: RedTy,
+}
+
+cast_impl!(TyChain);
+
 /// A chain (of custody) indicates where the value originates.
 #[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
 pub struct Chain {
@@ -146,26 +153,19 @@ impl Chain {
         }
     }
 
-    pub fn concat_term(&self, env: &Env, other: impl Upcast<RedTerm>) -> Fallible<RedTerm> {
-        let other: RedTerm = other.upcast();
-        let mut ty_chains = Set::new();
-        for ty_chain in &other.ty_chains {
-            ty_chains.insert(self.concat_ty(&env, ty_chain)?);
-        }
-        Ok(RedTerm { ty_chains })
+    pub fn concat_perm(&self, env: &Env, other: impl Upcast<RedPerm>) -> Fallible<RedPerm> {
+        let RedPerm { chains } = other.upcast();
+        Ok(RedPerm {
+            chains: chains.into_iter().map(|c| self.concat(&env, c)).collect(),
+        })
     }
 
-    /// Create a new typed chain of custody `(self other)`.
-    pub fn concat_ty(&self, env: &Env, other: impl Upcast<TyChain>) -> Fallible<TyChain> {
-        let other: TyChain = other.upcast();
-        if other.is_copy(env)? {
-            Ok(other)
-        } else {
-            Ok(TyChain {
-                chain: self.concat(&env, &other.chain),
-                ty: other.ty,
-            })
-        }
+    pub fn concat_term(&self, env: &Env, other: impl Upcast<RedTerm>) -> Fallible<RedTerm> {
+        let RedTerm { red_perm, red_ty } = other.upcast();
+        Ok(RedTerm {
+            red_perm: self.concat_perm(&env, red_perm)?,
+            red_ty,
+        })
     }
 
     pub fn is_copy(&self, env: &Env) -> bool {
@@ -278,43 +278,41 @@ judgment_fn! {
         debug(a, env)
 
         (
-            (collect(ty_chain_of_custody(env, a)) => ty_chains)
+            (red_perm(&env, &a) => red_perm)
+            (red_ty(&env, &a) => red_ty)
             ----------------------------------- ("red term")
-            (red_term(env, a) => RedTerm { ty_chains })
+            (red_term(env, a) => RedTerm { red_perm: red_perm.clone(), red_ty })
         )
 
     }
 }
 
 judgment_fn! {
-    fn ty_chain_of_custody(
+    fn red_ty(
         env: Env,
         a: Parameter,
-    ) => TyChain {
+    ) => RedTy {
         debug(a, env)
 
         (
-            (chain_of_custody(&env, a) => chain)
             ----------------------------------- ("perm")
-            (ty_chain_of_custody(env, _a: Perm) => TyChain { chain, ty: RedTy::None })
+            (red_ty(_env, _a: Perm) => RedTy::None)
         )
 
         (
-            (chain_of_custody(&env, l) => chain_l)
-            (ty_chain_of_custody(&env, &*r) => chain_r)
-            (let chain_l_r = chain_l.concat_ty(&env, chain_r)?)
+            (red_ty(&env, &*r) => red_r)
             ----------------------------------- ("ty-apply")
-            (ty_chain_of_custody(env, Ty::ApplyPerm(l, r)) => chain_l_r)
+            (red_ty(env, Ty::ApplyPerm(_l, r)) => red_r)
         )
 
         (
             ----------------------------------- ("universal ty var")
-            (ty_chain_of_custody(_env, Ty::Var(Variable::UniversalVar(v))) => TyChain { chain: Chain::my(), ty: RedTy::Var(v) })
+            (red_ty(_env, Ty::Var(Variable::UniversalVar(v))) => RedTy::Var(v))
         )
 
         (
             ----------------------------------- ("named ty")
-            (ty_chain_of_custody(_env, Ty::NamedTy(n)) => TyChain { chain: Chain::my(), ty: RedTy::NamedTy(n) })
+            (red_ty(_env, Ty::NamedTy(n)) => RedTy::NamedTy(n))
         )
     }
 }

src/type_system/subtypes.rs

@@ -43,7 +43,9 @@ judgment_fn! {
         (
             (red_term_under(&env, &chain_a, &a) => red_term_a)
             (red_term_under(&env, &chain_b, &b) => red_term_b)
-            (for_all(&red_term_a.ty_chains, &|ty_chain_a| sub_some(&env, &live_after, ty_chain_a, &red_term_b.ty_chains)) => ())
+            (let ty_chains_a = red_term_a.ty_chains())
+            (let ty_chains_b = red_term_b.ty_chains())
+            (for_all(&ty_chains_a, &|ty_chain_a| sub_some(&env, &live_after, ty_chain_a, &ty_chains_b)) => ())
             ------------------------------- ("sub")
             (sub_under_perms(env, live_after, chain_a, a, chain_b, b) => ())
         )

src/type_system/tests/assignment.rs

@@ -46,7 +46,7 @@ fn assign_leased_to_field_of_lease_that_is_typed_as_my() {
                                            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 { 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
+                                                 the rule "sub" failed at step #4 (src/file.rs:LL:CC) because
                                                    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_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):

src/type_system/tests/cancellation.rs

@@ -78,7 +78,7 @@ fn shared_live_leased_to_our_leased() {
                                                        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_under_perms { chain_a: Chain { liens: [] }, a: shared [p] Data, chain_b: Chain { liens: [] }, 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
+                                                             the rule "sub" failed at step #4 (src/file.rs:LL:CC) because
                                                                judgment `sub_some { ty_chain_a: TyChain { chain: Chain { liens: [Shared(p), Leased(d)] }, ty: NamedTy(Data) }, ty_chains_b: {TyChain { chain: Chain { liens: [Our, Leased(d)] }, ty: NamedTy(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-some" failed at step #1 (src/file.rs:LL:CC) because
                                                                    judgment `sub_ty_chain { ty_chain_a: TyChain { chain: Chain { liens: [Shared(p), Leased(d)] }, ty: NamedTy(Data) }, ty_chain_b: TyChain { chain: Chain { liens: [Our, Leased(d)] }, ty: NamedTy(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):
@@ -185,7 +185,7 @@ fn leased_live_leased_to_leased() {
                                                        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_under_perms { chain_a: Chain { liens: [] }, a: leased [p] Data, chain_b: Chain { liens: [] }, 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
+                                                             the rule "sub" failed at step #4 (src/file.rs:LL:CC) because
                                                                judgment `sub_some { ty_chain_a: TyChain { chain: Chain { liens: [Leased(p), Leased(d)] }, ty: NamedTy(Data) }, ty_chains_b: {TyChain { chain: Chain { liens: [Leased(d)] }, ty: NamedTy(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-some" failed at step #1 (src/file.rs:LL:CC) because
                                                                    judgment `sub_ty_chain { ty_chain_a: TyChain { chain: Chain { liens: [Leased(p), Leased(d)] }, ty: NamedTy(Data) }, ty_chain_b: TyChain { chain: Chain { liens: [Leased(d)] }, ty: NamedTy(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):

src/type_system/tests/fn_calls.rs

@@ -471,7 +471,7 @@ fn pair_method__expect_leased_self_a__got_leased_self_b() {
                                                        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_under_perms { chain_a: Chain { liens: [] }, a: leased [@ fresh(0) . b] Data, chain_b: Chain { liens: [] }, 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
+                                                             the rule "sub" failed at step #4 (src/file.rs:LL:CC) because
                                                                judgment `sub_some { ty_chain_a: TyChain { chain: Chain { liens: [Leased(@ fresh(0) . b)] }, ty: NamedTy(Data) }, ty_chains_b: {TyChain { chain: Chain { liens: [Leased(@ fresh(0) . a)] }, ty: NamedTy(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-some" failed at step #1 (src/file.rs:LL:CC) because
                                                                    judgment `sub_ty_chain { ty_chain_a: TyChain { chain: Chain { liens: [Leased(@ fresh(0) . b)] }, ty: NamedTy(Data) }, ty_chain_b: TyChain { chain: Chain { liens: [Leased(@ fresh(0) . a)] }, ty: NamedTy(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):