more name simplification

Author: nikomatsakis

crates/formality-prove/src/prove.rs

@@ -2,8 +2,8 @@ mod constraints;
 mod env;
 mod minimize;
 mod prove_after;
-mod prove_apr;
-mod prove_apr_via;
+mod prove_pr;
+mod prove_pr_via;
 mod prove_eq;
 mod prove_normalize;
 mod prove_wc;

crates/formality-prove/src/prove/prove_apr.rs renamed to crates/formality-prove/src/prove/prove_pr.rs

@@ -9,15 +9,15 @@ use crate::{
         env::Env,
         prove,
         prove_after::prove_after,
-        prove_apr_via::prove_apr_via,
         prove_eq::{all_eq, prove_ty_eq},
+        prove_pr_via::prove_pr_via,
     },
 };
 
 use super::constraints::Constraints;
 
 judgment_fn! {
-    pub fn prove_apr(
+    pub fn prove_pr(
         decls: Decls,
         env: Env,
         assumptions: Wcs,
@@ -27,9 +27,9 @@ judgment_fn! {
 
         (
             (&assumptions => a)
-            (prove_apr_via(&decls, &env, &assumptions, a, &goal) => c)
+            (prove_pr_via(&decls, &env, &assumptions, a, &goal) => c)
             ----------------------------- ("assumption")
-            (prove_apr(decls, env, assumptions, goal) => c)
+            (prove_pr(decls, env, assumptions, goal) => c)
         )
 
         (
@@ -42,23 +42,23 @@ judgment_fn! {
             (prove_after(&decls, c, &co_assumptions, &i.where_clause) => c)
             (prove_after(&decls, c, &assumptions, &t.where_clause) => c)
             ----------------------------- ("impl")
-            (prove_apr(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
+            (prove_pr(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
         )
 
         (
             (decls.trait_invariants() => ti)
             (let (env, subst) = env.existential_substitution(&ti.binder))
             (let ti = ti.binder.instantiate_with(&subst).unwrap())
-            (prove_apr_via(&decls, env, &assumptions, &ti.where_clause, &trait_ref) => c)
+            (prove_pr_via(&decls, env, &assumptions, &ti.where_clause, &trait_ref) => c)
             (prove_after(&decls, c, &assumptions, &ti.trait_ref) => c)
             ----------------------------- ("trait implied bound")
-            (prove_apr(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
+            (prove_pr(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
         )
 
         (
             (prove_ty_eq(decls, env, assumptions, a, b) => c)
             ----------------------------- ("eq")
-            (prove_apr(decls, env, assumptions, Relation::Equals(Parameter::Ty(a), Parameter::Ty(b))) => c)
+            (prove_pr(decls, env, assumptions, Relation::Equals(Parameter::Ty(a), Parameter::Ty(b))) => c)
         )
     }
 }

crates/formality-prove/src/prove/prove_apr_via.rs renamed to crates/formality-prove/src/prove/prove_pr_via.rs

@@ -11,7 +11,7 @@ use crate::{
 };
 
 judgment_fn! {
-    pub fn prove_apr_via(
+    pub fn prove_pr_via(
         decls: Decls,
         env: Env,
         assumptions: Wcs,
@@ -26,7 +26,7 @@ judgment_fn! {
             (if skel_c == skel_g)
             (prove(decls, env, assumptions, all_eq(parameters_c, parameters_g)) => c)
             ----------------------------- ("predicate-congruence-axiom")
-            (prove_apr_via(decls, env, assumptions, PR::Predicate(predicate), goal) => c)
+            (prove_pr_via(decls, env, assumptions, PR::Predicate(predicate), goal) => c)
         )
 
         (
@@ -35,22 +35,22 @@ judgment_fn! {
             (if skel_c == skel_g)
             (if parameters_c == parameters_g) // for relations, we require 100% match
             ----------------------------- ("relation-axiom")
-            (prove_apr_via(_decls, env, _assumptions, PR::Relation(relation), goal) => Constraints::none(env))
+            (prove_pr_via(_decls, env, _assumptions, PR::Relation(relation), goal) => Constraints::none(env))
         )
 
         (
             (let (env, subst) = env.existential_substitution(&binder))
             (let via1 = binder.instantiate_with(&subst).unwrap())
-            (prove_apr_via(decls, env, assumptions, via1, goal) => c)
+            (prove_pr_via(decls, env, assumptions, via1, goal) => c)
             ----------------------------- ("forall")
-            (prove_apr_via(decls, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst))
+            (prove_pr_via(decls, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst))
         )
 
         (
-            (prove_apr_via(&decls, env, &assumptions, wc_consequence, goal) => c)
+            (prove_pr_via(&decls, env, &assumptions, wc_consequence, goal) => c)
             (prove_after(&decls, c, &assumptions, &wc_condition) => c)
             ----------------------------- ("implies")
-            (prove_apr_via(decls, env, assumptions, WcData::Implies(wc_condition, wc_consequence), goal) => c)
+            (prove_pr_via(decls, env, assumptions, WcData::Implies(wc_condition, wc_consequence), goal) => c)
         )
     }
 }

crates/formality-prove/src/prove/prove_wc.rs

@@ -5,7 +5,7 @@ use formality_types::{
 
 use crate::{
     decls::Decls,
-    prove::{env::Env, prove_apr::prove_apr},
+    prove::{env::Env, prove_pr::prove_pr},
 };
 
 use super::constraints::Constraints;
@@ -20,9 +20,9 @@ judgment_fn! {
         debug(goal, assumptions, env, decls)
 
         (
-            (prove_apr(decls, env, assumptions, a) => c)
+            (prove_pr(decls, env, assumptions, a) => c)
             --- ("atomic")
-            (prove_wc(decls, env, assumptions, WcData::Atomic(a)) => c)
+            (prove_wc(decls, env, assumptions, WcData::PR(a)) => c)
         )
 
         (

crates/formality-types/src/grammar/wc.rs

@@ -119,7 +119,7 @@ impl Wc {
 #[term]
 pub enum WcData {
     #[cast]
-    Atomic(PR),
+    PR(PR),
 
     #[grammar(for $v0)]
     ForAll(Binder<Wc>),