Merge pull request #178 from shua/nopr

inline PR into WcData
rust-lang · Jul 1, 2024 · 3523b85 · 3523b85
2 parents 915661b + 45c754f
commit 3523b85
Show file tree

Hide file tree

Showing 6 changed files with 30 additions and 50 deletions.
diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs
@@ -2,7 +2,7 @@ use formality_core::{set, Set, Upcast};
 use formality_macros::term;
 use formality_types::grammar::{
     AdtId, AliasName, AliasTy, Binder, Parameter, Predicate, Relation, TraitId, TraitRef, Ty, Wc,
-    Wcs, PR,
+    Wcs,
 };
 
 #[term]
@@ -175,13 +175,14 @@ impl TraitDecl {
 
         fn is_supertrait(self_var: &Parameter, wc: &Wc) -> bool {
             match wc.data() {
-                formality_types::grammar::WcData::PR(PR::Predicate(Predicate::IsImplemented(
+                formality_types::grammar::WcData::Predicate(Predicate::IsImplemented(
                     trait_ref,
-                ))) => trait_ref.parameters[0] == *self_var,
-                formality_types::grammar::WcData::PR(PR::Relation(Relation::Outlives(a, _))) => {
+                )) => trait_ref.parameters[0] == *self_var,
+                formality_types::grammar::WcData::Relation(Relation::Outlives(a, _)) => {
                     *a == *self_var
                 }
-                formality_types::grammar::WcData::PR(_) => false,
+                formality_types::grammar::WcData::Predicate(_) => false,
+                formality_types::grammar::WcData::Relation(_) => false,
                 formality_types::grammar::WcData::ForAll(binder) => {
                     is_supertrait(self_var, binder.peek())
                 }

diff --git a/crates/formality-prove/src/prove/prove_via.rs b/crates/formality-prove/src/prove/prove_via.rs
@@ -1,5 +1,5 @@
 use formality_core::judgment_fn;
-use formality_types::grammar::{WcData, Wcs, PR};
+use formality_types::grammar::{WcData, Wcs};
 
 use crate::{
     decls::Decls,
@@ -12,26 +12,26 @@ judgment_fn! {
         env: Env,
         assumptions: Wcs,
         via: WcData,
-        goal: PR,
+        goal: WcData,
     ) => Constraints {
         debug(goal, via, assumptions, env, decls)
 
         (
-            (let (skel_c, parameters_c) = predicate.debone())
-            (let (skel_g, parameters_g) = goal.debone())
+            (let (skel_c, parameters_c) = pred_1.debone())
+            (let (skel_g, parameters_g) = pred_2.debone())
             (if skel_c == skel_g)!
             (prove(decls, env, assumptions, Wcs::all_eq(parameters_c, parameters_g)) => c)
             ----------------------------- ("predicate-congruence-axiom")
-            (prove_via(decls, env, assumptions, PR::Predicate(predicate), goal) => c)
+            (prove_via(decls, env, assumptions, WcData::Predicate(pred_1), WcData::Predicate(pred_2)) => c)
         )
 
         (
-            (let (skel_c, parameters_c) = relation.debone())
-            (let (skel_g, parameters_g) = goal.debone())
+            (let (skel_c, parameters_c) = rel_1.debone())
+            (let (skel_g, parameters_g) = rel_2.debone())
             (if skel_c == skel_g)
             (if parameters_c == parameters_g)! // for relations, we require 100% match
             ----------------------------- ("relation-axiom")
-            (prove_via(_decls, env, _assumptions, PR::Relation(relation), goal) => Constraints::none(env))
+            (prove_via(_decls, env, _assumptions, WcData::Relation(rel_1), WcData::Relation(rel_2)) => Constraints::none(env))
         )
 
         (

diff --git a/crates/formality-prove/src/prove/prove_wc.rs b/crates/formality-prove/src/prove/prove_wc.rs
@@ -43,7 +43,13 @@ judgment_fn! {
             (&assumptions => a)!
             (prove_via(&decls, &env, &assumptions, a, &goal) => c)
             ----------------------------- ("assumption")
-            (prove_wc(decls, env, assumptions, WcData::PR(goal)) => c)
+            (prove_wc(decls, env, assumptions, WcData::Predicate(goal)) => c)
+        )
+        (
+            (&assumptions => a)!
+            (prove_via(&decls, &env, &assumptions, a, &goal) => c)
+            ----------------------------- ("assumption")
+            (prove_wc(decls, env, assumptions, WcData::Relation(goal)) => c)
         )
 
         (

diff --git a/crates/formality-rust/src/prove.rs b/crates/formality-rust/src/prove.rs
@@ -7,7 +7,7 @@ use crate::grammar::{
 use formality_core::{seq, Set, To, Upcast, Upcasted};
 use formality_prove as prove;
 use formality_types::grammar::{
-    AdtId, AliasTy, Binder, BoundVar, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs, PR,
+    AdtId, AliasTy, Binder, BoundVar, ParameterKind, Predicate, Relation, TraitId, Ty, Wc, Wcs,
 };
 
 impl Program {
@@ -357,7 +357,6 @@ macro_rules! upcast_to_wcs {
 upcast_to_wcs! {
     Wc,
     Wcs,
-    PR,
     Predicate,
     Relation,
 }

diff --git a/crates/formality-types/src/grammar/formulas.rs b/crates/formality-types/src/grammar/formulas.rs
@@ -1,6 +1,5 @@
 use formality_core::term;
 
-use formality_core::cast_impl;
 use formality_core::To;
 use formality_core::Upcast;
 
@@ -210,26 +209,6 @@ impl TraitId {
     }
 }
 
-/// "PR" == Predicate or Relation
-///
-/// We need a better name for this lol.
-#[term]
-pub enum PR {
-    #[cast]
-    Relation(Relation),
-    #[cast]
-    Predicate(Predicate),
-}
-
-impl PR {
-    pub fn debone(&self) -> (Skeleton, Vec<Parameter>) {
-        match self {
-            PR::Predicate(v) => v.debone(),
-            PR::Relation(v) => v.debone(),
-        }
-    }
-}
-
 pub trait Debone {
     fn debone(&self) -> (Skeleton, Vec<Parameter>);
 }
@@ -244,10 +223,5 @@ macro_rules! debone_impl {
     };
 }
 
-debone_impl!(PR);
 debone_impl!(Predicate);
 debone_impl!(Relation);
-
-// Transitive casting impls:
-
-cast_impl!((TraitRef) <: (Predicate) <: (PR));
diff --git a/crates/formality-types/src/grammar/wc.rs b/crates/formality-types/src/grammar/wc.rs
@@ -4,8 +4,6 @@ use formality_core::{
     cast_impl, set, term, Cons, DowncastFrom, DowncastTo, Set, Upcast, UpcastFrom, Upcasted,
 };
 
-use crate::grammar::PR;
-
 use super::{Binder, BoundVar, Parameter, Predicate, Relation, TraitRef};
 
 #[term($set)]
@@ -124,7 +122,10 @@ impl Wc {
 #[term]
 pub enum WcData {
     #[cast]
-    PR(PR),
+    Relation(Relation),
+
+    #[cast]
+    Predicate(Predicate),
 
     #[grammar(for $v0)]
     ForAll(Binder<Wc>),
@@ -155,10 +156,10 @@ impl DowncastFrom<Wc> for WcData {
 
 // ---
 
-cast_impl!((PR) <: (WcData) <: (Wc));
-cast_impl!((Relation) <: (PR) <: (Wc));
-cast_impl!((Predicate) <: (PR) <: (Wc));
-cast_impl!((TraitRef) <: (PR) <: (Wc));
+cast_impl!((TraitRef) <: (Predicate) <: (WcData));
+cast_impl!((Relation) <: (WcData) <: (Wc));
+cast_impl!((Predicate) <: (WcData) <: (Wc));
+cast_impl!((TraitRef) <: (WcData) <: (Wc));
 
 impl UpcastFrom<Wc> for Wcs {
     fn upcast_from(term: Wc) -> Self {
@@ -176,7 +177,6 @@ impl DowncastTo<Wc> for Wcs {
     }
 }
 
-cast_impl!((PR) <: (Wc) <: (Wcs));
 cast_impl!((Relation) <: (Wc) <: (Wcs));
 cast_impl!((Predicate) <: (Wc) <: (Wcs));
 cast_impl!((TraitRef) <: (Wc) <: (Wcs));