From 45c754fc9a7eb52d6a6ed384663abb3409027c05 Mon Sep 17 00:00:00 2001 From: shua Date: Sun, 30 Jun 2024 22:12:23 +0200 Subject: [PATCH] inline PR into WcData This change inlines the `PR` enum into the `WcData` enum. The comment on `PR` "we need to come up with a better name for this" indicates this type is not encoding some deeper logical idea. This change passing all tests indicates that the type is also not necessary. --- crates/formality-prove/src/decls.rs | 11 ++++---- crates/formality-prove/src/prove/prove_via.rs | 16 ++++++------ crates/formality-prove/src/prove/prove_wc.rs | 8 +++++- crates/formality-rust/src/prove.rs | 3 +-- .../formality-types/src/grammar/formulas.rs | 26 ------------------- crates/formality-types/src/grammar/wc.rs | 16 ++++++------ 6 files changed, 30 insertions(+), 50 deletions(-) diff --git a/crates/formality-prove/src/decls.rs b/crates/formality-prove/src/decls.rs index 95b8767d..00bd5222 100644 --- 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 index a6e0bb59..3ff339c5 100644 --- 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 index 47e6bca2..586f5db2 100644 --- 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 index 424a64b0..e62cbd4d 100644 --- 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 index a750f806..d9522c21 100644 --- 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) { - match self { - PR::Predicate(v) => v.debone(), - PR::Relation(v) => v.debone(), - } - } -} - pub trait Debone { fn debone(&self) -> (Skeleton, Vec); } @@ -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 index ef31a4da..eae2a680 100644 --- 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), @@ -155,10 +156,10 @@ impl DowncastFrom 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 for Wcs { fn upcast_from(term: Wc) -> Self { @@ -176,7 +177,6 @@ impl DowncastTo for Wcs { } } -cast_impl!((PR) <: (Wc) <: (Wcs)); cast_impl!((Relation) <: (Wc) <: (Wcs)); cast_impl!((Predicate) <: (Wc) <: (Wcs)); cast_impl!((TraitRef) <: (Wc) <: (Wcs));