From 3b3fb775ecfcfe49965577af42b29bb25b1fc6dc Mon Sep 17 00:00:00 2001 From: Niko Matsakis Date: Sun, 9 Feb 2025 20:46:05 -0500 Subject: [PATCH] remove Or types/perms --- src/grammar.rs | 7 -- src/type_system/expressions.rs | 6 +- src/type_system/in_flight.rs | 8 -- src/type_system/places.rs | 1 - src/type_system/predicates.rs | 16 ---- src/type_system/red_terms.rs | 129 +-------------------------------- src/type_system/types.rs | 7 +- 7 files changed, 5 insertions(+), 169 deletions(-) diff --git a/src/grammar.rs b/src/grammar.rs index 2b25b1d..e0dd8c9 100644 --- a/src/grammar.rs +++ b/src/grammar.rs @@ -245,9 +245,6 @@ pub enum Ty { #[grammar($v0 $v1)] ApplyPerm(Perm, Arc), - - #[grammar($v0 | $v1)] - Or(Arc, Arc), } 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, Arc), - - #[grammar($v0 | $v1)] - Or(Arc, Arc), } mod perm_impls; diff --git a/src/type_system/expressions.rs b/src/type_system/expressions.rs index 05277f4..f869c7d 100644 --- 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 index c7d5908..39e1c03 100644 --- 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 index 46568af..c59472f 100644 --- 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 index 7d09987..58f90ae 100644 --- 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 index 109360d..0343bb4 100644 --- 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 { - 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>) -> RedPerm { - let places: Set = 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>) -> RedPerm { - let places: Set = 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), -} - 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 index 381c342..430c6c5 100644 --- 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()?;