refactor predicate grammar

Extract VarianceKind to its own thing

src/grammar.rs

@@ -441,37 +441,19 @@ formality_core::id!(ValueId);
 formality_core::id!(FieldId);
 formality_core::id!(MethodId);
 
-#[term($kind($parameter))]
-pub struct Predicate {
-    pub kind: PredicateKind,
-    pub parameter: Parameter,
-}
+#[term]
+pub enum Predicate {
+    Shared(Parameter),
 
-impl Predicate {
-    pub fn shared(parameter: impl Upcast<Parameter>) -> Predicate {
-        Predicate {
-            kind: PredicateKind::Shared,
-            parameter: parameter.upcast(),
-        }
-    }
+    Leased(Parameter),
 
-    pub fn leased(parameter: impl Upcast<Parameter>) -> Predicate {
-        Predicate {
-            kind: PredicateKind::Leased,
-            parameter: parameter.upcast(),
-        }
-    }
+    #[grammar($v0($v1))]
+    Variance(VarianceKind, Parameter),
 }
 
 #[term]
 #[derive(Copy)]
-pub enum PredicateKind {
-    /// `shared(p)` is true for shared types (our, shared) that can be copied at will.
-    Shared,
-
-    /// `leased(p)` is true for leased types that are always passed by reference.
-    Leased,
-
+pub enum VarianceKind {
     /// `relative(p)` is used to express variance.
     /// Whenever a type `P T` appears in a struct
     /// and `P != my`, `Relative(T)` must hold.
@@ -486,11 +468,8 @@ pub enum PredicateKind {
     Atomic,
 }
 
-impl PredicateKind {
+impl VarianceKind {
     pub fn apply(self, parameter: impl Upcast<Parameter>) -> Predicate {
-        Predicate {
-            kind: self,
-            parameter: parameter.upcast(),
-        }
+        Predicate::variance(self, parameter)
     }
 }

src/type_system/classes.rs

@@ -4,7 +4,7 @@ use fn_error_context::context;
 use formality_core::Fallible;
 
 use crate::grammar::{
-    Atomic, ClassDecl, ClassDeclBoundData, FieldDecl, NamedTy, PredicateKind, Program, Var,
+    Atomic, ClassDecl, ClassDeclBoundData, FieldDecl, NamedTy, Program, Var, VarianceKind,
 };
 
 use super::{
@@ -65,7 +65,7 @@ fn check_field(class_ty: &NamedTy, env: &Env, decl: &FieldDecl) -> Fallible<()>
         Atomic::No => {}
 
         Atomic::Yes => {
-            prove_predicate(&*env, PredicateKind::Atomic.apply(ty)).check_proven()?;
+            prove_predicate(&*env, VarianceKind::Atomic.apply(ty)).check_proven()?;
         }
     }
 

src/type_system/in_flight.rs

@@ -184,11 +184,16 @@ impl InFlight for Place {
 
 impl InFlight for Predicate {
     fn with_places_transformed(&self, transform: Transform<'_>) -> Self {
-        let Predicate { kind, parameter } = self;
-        let parameter = parameter.with_places_transformed(transform);
-        Predicate {
-            kind: *kind,
-            parameter,
+        match self {
+            Predicate::Shared(parameter) => {
+                Predicate::Shared(parameter.with_places_transformed(transform))
+            }
+            Predicate::Leased(parameter) => {
+                Predicate::Leased(parameter.with_places_transformed(transform))
+            }
+            Predicate::Variance(kind, parameter) => {
+                Predicate::Variance(*kind, parameter.with_places_transformed(transform))
+            }
         }
     }
 }

src/type_system/methods.rs

@@ -2,8 +2,8 @@ use fn_error_context::context;
 use formality_core::{Fallible, Upcast};
 
 use crate::grammar::{
-    Block, LocalVariableDecl, MethodDecl, MethodDeclBoundData, NamedTy, Predicate, PredicateKind,
-    ThisDecl, Ty, Var::This,
+    Block, LocalVariableDecl, MethodDecl, MethodDeclBoundData, NamedTy, ThisDecl, Ty, Var::This,
+    VarianceKind,
 };
 
 use super::{
@@ -33,8 +33,8 @@ pub fn check_method(class_ty: &NamedTy, env: impl Upcast<Env>, decl: &MethodDecl
         vars.iter()
             .flat_map(|v| {
                 vec![
-                    Predicate::new(PredicateKind::Relative, &v),
-                    Predicate::new(PredicateKind::Atomic, &v),
+                    VarianceKind::Relative.apply(&v),
+                    VarianceKind::Atomic.apply(&v),
                 ]
             })
             .collect::<Vec<_>>(),

src/type_system/predicates.rs

@@ -1,7 +1,7 @@
 use super::{env::Env, types::check_parameter};
 use crate::{
     dada_lang::grammar::UniversalVar,
-    grammar::{NamedTy, Parameter, Perm, Place, Predicate, PredicateKind, Ty},
+    grammar::{NamedTy, Parameter, Perm, Place, Predicate, Ty, VarianceKind},
     type_system::{
         is_::{is_leased, is_shared},
         places::place_ty,
@@ -22,8 +22,11 @@ pub fn check_predicates(env: &Env, predicates: &[Predicate]) -> Fallible<()> {
 
 #[context("check predicate `{:?}`", predicate)]
 pub fn check_predicate(env: &Env, predicate: &Predicate) -> Fallible<()> {
-    let Predicate { kind: _, parameter } = predicate;
-    check_predicate_parameter(env, parameter)
+    match predicate {
+        Predicate::Shared(parameter) => check_predicate_parameter(env, parameter),
+        Predicate::Leased(parameter) => check_predicate_parameter(env, parameter),
+        Predicate::Variance(_kind, parameter) => check_predicate_parameter(env, parameter),
+    }
 }
 
 #[context("check check_predicate_parameter `{:?}`", parameter)]
@@ -69,53 +72,47 @@ judgment_fn! {
         (
             (is_shared(env, p) => ())
             ---------------------------- ("shared")
-            (prove_predicate(env, Predicate { kind: PredicateKind::Shared, parameter: p }) => ())
+            (prove_predicate(env, Predicate::Shared(p)) => ())
         )
 
         (
             (is_leased(env, p) => ())
             ---------------------------- ("leased")
-            (prove_predicate(env, Predicate { kind: PredicateKind::Leased, parameter: p }) => ())
-        )
-
-        (
-            (variance_predicate(env, PredicateKind::Relative, parameter) => ())
-            ---------------------------- ("relative")
-            (prove_predicate(env, Predicate { kind: PredicateKind::Relative, parameter }) => ())
+            (prove_predicate(env, Predicate::Leased(p)) => ())
         )
 
         (
-            (variance_predicate(env, PredicateKind::Atomic, parameter) => ())
-            ---------------------------- ("atomic")
-            (prove_predicate(env, Predicate { kind: PredicateKind::Atomic, parameter }) => ())
+            (variance_predicate(env, kind, parameter) => ())
+            ---------------------------- ("variance")
+            (prove_predicate(env, Predicate::Variance(kind, parameter)) => ())
         )
     }
 }
 
 judgment_fn! {
     fn variance_predicate(
         env: Env,
-        kind: PredicateKind,
+        kind: VarianceKind,
         parameter: Parameter,
     ) => () {
         debug(kind, parameter, env)
 
         (
-            (for_all(parameters, &|parameter| prove_predicate(&env, Predicate::new(kind, parameter))) => ())
+            (for_all(parameters, &|parameter| prove_predicate(&env, kind.apply(parameter))) => ())
             ----------------------------- ("ty-named")
             (variance_predicate(env, kind, NamedTy { name: _, parameters }) => ())
         )
 
         (
-            (prove_predicate(&env, Predicate::new(kind, &*ty1)) => ())
-            (prove_predicate(&env, Predicate::new(kind, &*ty2)) => ())
+            (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, Predicate::new(kind, perm)) => ())
-            (prove_predicate(&env, Predicate::new(kind, &*ty)) => ())
+            (prove_predicate(&env, kind.apply(perm)) => ())
+            (prove_predicate(&env, kind.apply(&*ty)) => ())
             ----------------------------- ("ty")
             (variance_predicate(env, kind, Ty::ApplyPerm(perm, ty)) => ())
         )
@@ -151,15 +148,15 @@ judgment_fn! {
         )
 
         (
-            (prove_predicate(&env, Predicate::new(kind, &*perm1)) => ())
-            (prove_predicate(&env, Predicate::new(kind, &*perm2)) => ())
+            (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, Predicate::new(kind, &*perm1)) => ())
-            (prove_predicate(&env, Predicate::new(kind, &*perm2)) => ())
+            (prove_predicate(&env, kind.apply(&*perm1)) => ())
+            (prove_predicate(&env, kind.apply(&*perm2)) => ())
             ----------------------------- ("perm-apply")
             (variance_predicate(env, kind, Perm::Apply(perm1, perm2)) => ())
         )
@@ -170,14 +167,14 @@ judgment_fn! {
 judgment_fn! {
     fn variance_predicate_place(
         env: Env,
-        kind: PredicateKind,
+        kind: VarianceKind,
         place: Place,
     ) => () {
         debug(kind, place, env)
 
         (
             (place_ty(&env, place) => ty)
-            (prove_predicate(&env, Predicate::new(kind, ty)) => ())
+            (prove_predicate(&env, kind.apply(ty)) => ())
             ----------------------------- ("perm")
             (variance_predicate_place(env, kind, place) => ())
         )

src/type_system/tests/class_defn_wf.rs

@@ -122,7 +122,7 @@ fn forall_P_T_PT_requires_relative() {
             1: check field named `field`
             2: check type `!perm_0 !ty_1`
             3: judgment `prove_predicate { predicate: relative(!ty_1), env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                 the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                 the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                    judgment had no applicable rules: `variance_predicate { kind: relative, parameter: !ty_1, env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }`"#]]);
 }
 
@@ -188,13 +188,13 @@ fn forall_P_T_f1_T_f2_P_leased_f1_err() {
             2: check type `!perm_0 leased {self . f1} Data`
             3: check_perm(!perm_0 leased {self . f1}
             4: judgment `prove_predicate { predicate: relative(leased {self . f1}), env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                 the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                 the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                    judgment `variance_predicate { kind: relative, parameter: leased {self . f1}, env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
                      the rule "leased" failed at step #0 (src/file.rs:LL:CC) because
                        judgment `variance_predicate_place { kind: relative, place: self . f1, env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
                          the rule "perm" failed at step #1 (src/file.rs:LL:CC) because
                            judgment `prove_predicate { predicate: relative(!ty_1), env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                             the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                             the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                                judgment had no applicable rules: `variance_predicate { kind: relative, parameter: !ty_1, env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }`"#]]);
 }
 
@@ -224,13 +224,13 @@ fn forall_P_T_f1_T_f2_P_given_f1_err() {
             2: check type `!perm_0 given {self . f1} Data`
             3: check_perm(!perm_0 given {self . f1}
             4: judgment `prove_predicate { predicate: relative(given {self . f1}), env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                 the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                 the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                    judgment `variance_predicate { kind: relative, parameter: given {self . f1}, env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
                      the rule "given" failed at step #0 (src/file.rs:LL:CC) because
                        judgment `variance_predicate_place { kind: relative, place: self . f1, env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
                          the rule "perm" failed at step #1 (src/file.rs:LL:CC) because
                            judgment `prove_predicate { predicate: relative(!ty_1), env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                             the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                             the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                                judgment had no applicable rules: `variance_predicate { kind: relative, parameter: !ty_1, env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }`"#]]);
 }
 
@@ -275,11 +275,11 @@ fn forall_P_T_P_Vec_T_err() {
             1: check field named `f1`
             2: check type `!perm_0 Vec[!ty_1]`
             3: judgment `prove_predicate { predicate: relative(Vec[!ty_1]), env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                 the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                 the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                    judgment `variance_predicate { kind: relative, parameter: Vec[!ty_1], env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
                      the rule "ty-named" failed at step #0 (src/file.rs:LL:CC) because
                        judgment `prove_predicate { predicate: relative(!ty_1), env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                         the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                         the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                            judgment had no applicable rules: `variance_predicate { kind: relative, parameter: !ty_1, env: Env { program: "...", universe: universe(2), in_scope_vars: [!perm_0, !ty_1], local_variables: {self: Ref[!perm_0, !ty_1]}, assumptions: {}, fresh: 0 } }`"#]]);
 }
 
@@ -307,7 +307,7 @@ fn Ref1_requires_rel_Ref2_does_not_err() {
             1: check field named `f1`
             2: check type `Ref1[our, !ty_0]`
             3: judgment `prove_predicate { predicate: relative(!ty_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!ty_0], local_variables: {self: Ref2[!ty_0]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                 the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                 the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                    judgment had no applicable rules: `variance_predicate { kind: relative, parameter: !ty_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!ty_0], local_variables: {self: Ref2[!ty_0]}, assumptions: {}, fresh: 0 } }`"#]]);
 }
 
@@ -332,7 +332,7 @@ fn sh_from_arena() {
             1: check field named `f1`
             2: check type `shared {self . arena} !ty_0`
             3: judgment `prove_predicate { predicate: relative(!ty_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!ty_0], local_variables: {self: Ref[!ty_0]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                 the rule "relative" failed at step #0 (src/file.rs:LL:CC) because
+                 the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                    judgment had no applicable rules: `variance_predicate { kind: relative, parameter: !ty_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!ty_0], local_variables: {self: Ref[!ty_0]}, assumptions: {}, fresh: 0 } }`"#]]);
 }
 
@@ -354,7 +354,7 @@ fn atomic_field_req_atomic_err() {
             0: check class named `Atomic`
             1: check field named `f1`
             2: judgment `prove_predicate { predicate: atomic(!ty_0), env: Env { program: "...", universe: universe(1), in_scope_vars: [!ty_0], local_variables: {self: Atomic[!ty_0]}, assumptions: {}, fresh: 0 } }` failed at the following rule(s):
-                 the rule "atomic" failed at step #0 (src/file.rs:LL:CC) because
+                 the rule "variance" failed at step #0 (src/file.rs:LL:CC) because
                    judgment had no applicable rules: `variance_predicate { kind: atomic, parameter: !ty_0, env: Env { program: "...", universe: universe(1), in_scope_vars: [!ty_0], local_variables: {self: Atomic[!ty_0]}, assumptions: {}, fresh: 0 } }`"#]]);
 }
 

src/type_system/types.rs

@@ -5,7 +5,7 @@ use formality_core::Fallible;
 use crate::{
     dada_lang::grammar::{Binder, BoundVar},
     grammar::{
-        Kind, NamedTy, Parameter, Perm, Place, Predicate, PredicateKind, Program, Ty, TypeName,
+        Kind, NamedTy, Parameter, Perm, Place, Predicate, Program, Ty, TypeName, VarianceKind,
     },
 };
 
@@ -50,7 +50,7 @@ pub fn check_type(env: &Env, ty: &Ty) -> Fallible<()> {
         Ty::ApplyPerm(perm, ty1) => {
             check_perm(env, perm)?;
             check_type(env, ty1)?;
-            prove_predicate(env, PredicateKind::Relative.apply(&**ty1)).check_proven()?;
+            prove_predicate(env, VarianceKind::Relative.apply(&**ty1)).check_proven()?;
         }
 
         Ty::Or(l, r) => {
@@ -89,7 +89,7 @@ fn check_perm(env: &Env, perm: &Perm) -> Fallible<()> {
         Perm::Apply(l, r) | Perm::Or(l, r) => {
             check_perm(env, l)?;
             check_perm(env, r)?;
-            prove_predicate(env, PredicateKind::Relative.apply(&**r)).check_proven()?;
+            prove_predicate(env, VarianceKind::Relative.apply(&**r)).check_proven()?;
         }
     }
     Ok(())