remove Or types/perms

dada-lang · Feb 10, 2025 · 3b3fb77 · 3b3fb77
1 parent 598a0c4
commit 3b3fb77
Show file tree

Hide file tree

Showing 7 changed files with 5 additions and 169 deletions.
diff --git a/src/grammar.rs b/src/grammar.rs
@@ -245,9 +245,6 @@ pub enum Ty {
 
     #[grammar($v0 $v1)]
     ApplyPerm(Perm, Arc<Ty>),
-
-    #[grammar($v0 | $v1)]
-    Or(Arc<Ty>, Arc<Ty>),
 }
 
 impl Ty {
@@ -280,7 +277,6 @@ impl Ty {
         match self {
             Ty::NamedTy(_) | Ty::Var(_) => self.clone(),
             Ty::ApplyPerm(_, ty) => ty.strip_perm(),
-            Ty::Or(ty1, ty2) => Ty::or(ty1.strip_perm(), ty2.strip_perm()),
         }
     }
 }
@@ -307,9 +303,6 @@ pub enum Perm {
 
     #[grammar($v0 $v1)]
     Apply(Arc<Perm>, Arc<Perm>),
-
-    #[grammar($v0 | $v1)]
-    Or(Arc<Perm>, Arc<Perm>),
 }
 mod perm_impls;
 

diff --git a/src/type_system/expressions.rs b/src/type_system/expressions.rs
@@ -165,10 +165,10 @@ judgment_fn! {
 
         (
             (type_expr_as(&env, live_after.before_all([&if_true, &if_false]), &*cond, TypeName::Int) => env)
-            (type_expr(&env, &live_after, &*if_true) => (env, if_true_ty))
-            (type_expr(&env, &live_after, &*if_false) => (env, if_false_ty))
+            (type_expr_as(env, &live_after, &*if_true, Ty::unit()) => env)
+            (type_expr_as(env, &live_after, &*if_false, Ty::unit()) => env)
             ----------------------------------- ("if")
-            (type_expr(env, live_after, Expr::If(cond, if_true, if_false)) => (&env, Ty::or(&if_true_ty, if_false_ty)))
+            (type_expr(env, live_after, Expr::If(cond, if_true, if_false)) => (env, Ty::unit()))
         )
     }
 }

diff --git a/src/type_system/in_flight.rs b/src/type_system/in_flight.rs
@@ -118,10 +118,6 @@ impl InFlight for Ty {
                 perm.with_places_transformed(transform),
                 ty.with_places_transformed(transform),
             ),
-            Ty::Or(l, r) => Ty::Or(
-                l.with_places_transformed(transform).into(),
-                r.with_places_transformed(transform).into(),
-            ),
         }
     }
 }
@@ -148,10 +144,6 @@ impl InFlight for Perm {
                 l.with_places_transformed(transform).into(),
                 r.with_places_transformed(transform).into(),
             ),
-            Perm::Or(l, r) => Perm::Or(
-                l.with_places_transformed(transform).into(),
-                r.with_places_transformed(transform).into(),
-            ),
         }
     }
 }

diff --git a/src/type_system/places.rs b/src/type_system/places.rs
@@ -109,7 +109,6 @@ impl Env {
                     .collect();
                 Ok(fields_with_perm)
             }
-            Ty::Or(..) => anyhow::bail!("or fields not implemented"),
         }
     }
 }
diff --git a/src/type_system/predicates.rs b/src/type_system/predicates.rs
@@ -159,13 +159,6 @@ judgment_fn! {
             (variance_predicate(env, kind, NamedTy { name: _, parameters }) => ())
         )
 
-        (
-            (prove_predicate(&env, kind.apply(&*ty1)) => ())
-            (prove_predicate(&env, kind.apply(&*ty2)) => ())
-            ----------------------------- ("ty-or")
-            (variance_predicate(env, kind, Ty::Or(ty1, ty2)) => ())
-        )
-
         (
             (prove_predicate(&env, kind.apply(perm)) => ())
             (prove_predicate(&env, kind.apply(&*ty)) => ())
@@ -203,13 +196,6 @@ judgment_fn! {
             (variance_predicate(env, kind, Perm::Given(places)) => ())
         )
 
-        (
-            (prove_predicate(&env, kind.apply(&*perm1)) => ())
-            (prove_predicate(&env, kind.apply(&*perm2)) => ())
-            ----------------------------- ("perm-or")
-            (variance_predicate(env, kind, Perm::Or(perm1, perm2)) => ())
-        )
-
         (
             (prove_predicate(&env, kind.apply(&*perm1)) => ())
             (prove_predicate(&env, kind.apply(&*perm2)) => ())
@@ -334,7 +320,6 @@ impl MeetsPredicate for Ty {
                 panic!("unexpected variable: {self:?}")
             }
             Ty::ApplyPerm(perm, ty) => Compose(perm, ty).meets_predicate(env, predicate),
-            Ty::Or(ty, ty1) => Many(&[ty, ty1]).meets_predicate(env, predicate),
         }
     }
 }
@@ -396,7 +381,6 @@ impl MeetsPredicate for Perm {
             crate::grammar::Perm::Apply(perm, perm1) => {
                 Compose(perm, perm1).meets_predicate(env, k)
             }
-            crate::grammar::Perm::Or(perm, perm1) => Many(&[perm, perm1]).meets_predicate(env, k),
         }
     }
 }

diff --git a/src/type_system/red_terms.rs b/src/type_system/red_terms.rs
@@ -1,6 +1,4 @@
-use formality_core::{
-    cast_impl, judgment_fn, set, Cons, Downcast, DowncastFrom, Fallible, Set, Upcast,
-};
+use formality_core::{cast_impl, judgment_fn, Cons, Downcast, DowncastFrom, Fallible, Set, Upcast};
 
 use crate::{
     grammar::{NamedTy, Parameter, ParameterPredicate, Perm, Place, Ty, UniversalVar, Variable},
@@ -99,79 +97,6 @@ pub struct RedPerm {
 
 cast_impl!(RedPerm);
 
-impl RedPerm {
-    pub fn union(&self, other: impl Upcast<RedPerm>) -> RedPerm {
-        let other: RedPerm = other.upcast();
-        RedPerm {
-            chains: self.chains.union(&other.chains).cloned().collect(),
-        }
-    }
-
-    /// Represents a `my` permission.
-    pub fn my() -> RedPerm {
-        RedPerm {
-            chains: set![Chain::my()],
-        }
-    }
-
-    /// Represents an `our` permission.
-    pub fn our() -> RedPerm {
-        RedPerm {
-            chains: set![Chain::our()],
-        }
-    }
-
-    /// Represents a permission shared from a set of places.
-    pub fn shared(places: impl Upcast<Set<Place>>) -> RedPerm {
-        let places: Set<Place> = places.upcast();
-        RedPerm {
-            chains: places
-                .into_iter()
-                .map(|place| Chain::shared(place))
-                .collect(),
-        }
-    }
-
-    /// Represents a permission leased from a set of places.
-    pub fn leased(places: impl Upcast<Set<Place>>) -> RedPerm {
-        let places: Set<Place> = places.upcast();
-        RedPerm {
-            chains: places
-                .into_iter()
-                .map(|place| Chain::leased(place))
-                .collect(),
-        }
-    }
-
-    /// True if this lien-set represents a *copyable* term.
-    ///
-    /// False means the value is not known to be copyable, not that it is not copyable.
-    pub fn is_copy(&self, env: &Env) -> bool {
-        self.chains.iter().any(|chain| chain.is_copy(env))
-    }
-
-    /// True if this lien-set represents a *copyable* term.
-    ///
-    /// False means the value is not known to be copyable, not that it is not copyable.
-    pub fn is_moved(&self, env: &Env) -> bool {
-        self.chains.iter().all(|chain| chain.is_moved(env))
-    }
-
-    /// True if this lien-set represents a *lent* term.
-    ///
-    /// False means the value is not known to be lent, not that it is not lent.
-    pub fn is_lent(&self, env: &Env) -> bool {
-        self.chains.iter().any(|chain| chain.is_lent(env))
-    }
-
-    /// True if this lien-set represents an *owned* term.
-    ///
-    /// False means the value is not known to be owned, not that it is not owned.
-    pub fn is_owned(&self, env: &Env) -> bool {
-        self.chains.iter().all(|chain| chain.is_owned(env))
-    }
-}
-
 /// A chain (of custody) indicates where the value originates.
 #[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
 pub struct Chain {
@@ -328,20 +253,6 @@ impl Lien {
     }
 }
 
-/// The *layout* of a [`Perms`] indicates what we memory layout types
-/// with these permissions will have.
-#[derive(Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
-pub enum Layout {
-    /// Known to be by-value
-    Value,
-
-    /// Known to be leased
-    Leased,
-
-    /// Could not determine layout due to these variables
-    Unknown(Set<UniversalVar>),
-}
-
 judgment_fn! {
     pub fn red_term_under(
         env: Env,
@@ -356,7 +267,6 @@ judgment_fn! {
             ----------------------------------- ("red term")
             (red_term_under(env, chain, a) => red_term)
         )
-
     }
 }
 
@@ -406,19 +316,6 @@ judgment_fn! {
             ----------------------------------- ("named ty")
             (ty_chain_of_custody(_env, Ty::NamedTy(n)) => TyChain { chain: Chain::my(), ty: RedTy::NamedTy(n) })
         )
-
-        (
-            (ty_chain_of_custody(&env, &*l) => chain_l)
-            ----------------------------------- ("ty or l")
-            (ty_chain_of_custody(env, Ty::Or(l, _r)) => chain_l)
-        )
-
-        (
-            (ty_chain_of_custody(&env, &*r) => chain_r)
-            ----------------------------------- ("ty or r")
-            (ty_chain_of_custody(env, Ty::Or(_l, r)) => chain_r)
-        )
-
     }
 }
 
@@ -502,29 +399,5 @@ judgment_fn! {
             ----------------------------------- ("named ty")
             (chain_of_custody(_env, Ty::NamedTy(_n)) => Chain::my())
         )
-
-        (
-            (chain_of_custody(&env, &*l) => chain_l)
-            ----------------------------------- ("ty or l")
-            (chain_of_custody(env, Ty::Or(l, _r)) => chain_l)
-        )
-
-        (
-            (chain_of_custody(&env, &*r) => chain_r)
-            ----------------------------------- ("ty or r")
-            (chain_of_custody(env, Ty::Or(_l, r)) => chain_r)
-        )
-
-        (
-            (chain_of_custody(&env, &*l) => chain_l)
-            ----------------------------------- ("perm or l")
-            (chain_of_custody(env, Perm::Or(l, _r)) => chain_l)
-        )
-
-        (
-            (chain_of_custody(&env, &*r) => chain_r)
-            ----------------------------------- ("perm or r")
-            (chain_of_custody(env, Perm::Or(_l, r)) => chain_r)
-        )
     }
 }
diff --git a/src/type_system/types.rs b/src/type_system/types.rs
@@ -52,11 +52,6 @@ pub fn check_type(env: &Env, ty: &Ty) -> Fallible<()> {
             check_type(env, ty1)?;
             prove_predicate(env, VarianceKind::Relative.apply(&**ty1)).check_proven()?;
         }
-
-        Ty::Or(l, r) => {
-            check_type(env, l)?;
-            check_type(env, r)?;
-        }
     }
     Ok(())
 }
@@ -86,7 +81,7 @@ fn check_perm(env: &Env, perm: &Perm) -> Fallible<()> {
             assert!(env.var_in_scope(*v));
         }
 
-        Perm::Apply(l, r) | Perm::Or(l, r) => {
+        Perm::Apply(l, r) => {
             check_perm(env, l)?;
             check_perm(env, r)?;
             prove_predicate(env, VarianceKind::Relative.apply(&**r)).check_proven()?;