Skip to content

Commit 91c8fe6

Browse files
nikomatsakisnikomatsakis
committed
simplify more names
1 parent f817eff commit 91c8fe6

File tree

8 files changed

+60
-62
lines changed

8 files changed

+60
-62
lines changed

‎crates/formality-check/src/impls.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ use formality_rust::grammar::{
88
};
99
use formality_types::{
1010
cast::Downcasted,
11-
grammar::{AtomicRelation, Binder, Fallible, Substitution, Wcs},
11+
grammar::{Binder, Fallible, Relation, Substitution, Wcs},
1212
term::Term,
1313
visit::Visit,
1414
};
@@ -122,14 +122,14 @@ impl super::Check<'_> {
122122
self.prove_goal(
123123
&env,
124124
(impl_assumptions, &ii_where_clauses),
125-
AtomicRelation::sub(ti_input_ty, ii_input_ty),
125+
Relation::sub(ti_input_ty, ii_input_ty),
126126
)?;
127127
}
128128

129129
self.prove_goal(
130130
&env,
131131
(impl_assumptions, &ii_where_clauses),
132-
AtomicRelation::sub(ii_output_ty, ti_output_ty),
132+
Relation::sub(ii_output_ty, ti_output_ty),
133133
)?;
134134

135135
Ok(())

‎crates/formality-prove/src/prove/prove_apr.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
use formality_types::{
2-
grammar::{AtomicRelation, Parameter, Predicate, Wcs, APR},
2+
grammar::{Parameter, Predicate, Relation, Wcs, PR},
33
judgment_fn,
44
};
55

@@ -21,7 +21,7 @@ judgment_fn! {
2121
decls: Decls,
2222
env: Env,
2323
assumptions: Wcs,
24-
goal: APR,
24+
goal: PR,
2525
) => Constraints {
2626
debug(goal, assumptions, env, decls)
2727

@@ -58,7 +58,7 @@ judgment_fn! {
5858
(
5959
(prove_ty_eq(decls, env, assumptions, a, b) => c)
6060
----------------------------- ("eq")
61-
(prove_apr(decls, env, assumptions, AtomicRelation::Equals(Parameter::Ty(a), Parameter::Ty(b))) => c)
61+
(prove_apr(decls, env, assumptions, Relation::Equals(Parameter::Ty(a), Parameter::Ty(b))) => c)
6262
)
6363
}
6464
}

‎crates/formality-prove/src/prove/prove_apr_via.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
use formality_types::{
2-
grammar::{WcData, Wcs, APR},
2+
grammar::{WcData, Wcs, PR},
33
judgment_fn,
44
};
55

@@ -16,7 +16,7 @@ judgment_fn! {
1616
env: Env,
1717
assumptions: Wcs,
1818
via: WcData,
19-
goal: APR,
19+
goal: PR,
2020
) => Constraints {
2121
debug(goal, via, assumptions, env, decls)
2222

@@ -26,7 +26,7 @@ judgment_fn! {
2626
(if skel_c == skel_g)
2727
(prove(decls, env, assumptions, all_eq(parameters_c, parameters_g)) => c)
2828
----------------------------- ("predicate-congruence-axiom")
29-
(prove_apr_via(decls, env, assumptions, APR::AtomicPredicate(predicate), goal) => c)
29+
(prove_apr_via(decls, env, assumptions, PR::Predicate(predicate), goal) => c)
3030
)
3131

3232
(
@@ -35,7 +35,7 @@ judgment_fn! {
3535
(if skel_c == skel_g)
3636
(if parameters_c == parameters_g) // for relations, we require 100% match
3737
----------------------------- ("relation-axiom")
38-
(prove_apr_via(_decls, env, _assumptions, APR::AtomicRelation(relation), goal) => Constraints::none(env))
38+
(prove_apr_via(_decls, env, _assumptions, PR::Relation(relation), goal) => Constraints::none(env))
3939
)
4040

4141
(

‎crates/formality-prove/src/prove/prove_eq.rs

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ use formality_types::{
22
cast::{Downcast, Upcast, Upcasted},
33
collections::{Deduplicate, Set},
44
grammar::{
5-
AliasTy, AtomicRelation, InferenceVar, Parameter, PlaceholderVar, RigidTy, Substitution,
6-
Ty, TyData, Variable, Wcs,
5+
AliasTy, InferenceVar, Parameter, PlaceholderVar, Relation, RigidTy, Substitution, Ty,
6+
TyData, Variable, Wcs,
77
},
88
judgment_fn, set,
99
visit::Visit,
@@ -25,14 +25,14 @@ pub fn all_eq(a: impl Upcast<Vec<Parameter>>, b: impl Upcast<Vec<Parameter>>) ->
2525
assert_eq!(a.len(), b.len());
2626
a.into_iter()
2727
.zip(b)
28-
.map(|(a, b)| AtomicRelation::eq(a, b))
28+
.map(|(a, b)| Relation::eq(a, b))
2929
.upcasted()
3030
.collect()
3131
}
3232

3333
/// Goal(s) to prove `a` and `b` are equal
34-
pub fn eq(a: impl Upcast<Parameter>, b: impl Upcast<Parameter>) -> AtomicRelation {
35-
AtomicRelation::eq(a, b)
34+
pub fn eq(a: impl Upcast<Parameter>, b: impl Upcast<Parameter>) -> Relation {
35+
Relation::eq(a, b)
3636
}
3737

3838
judgment_fn! {

‎crates/formality-prove/src/prove/prove_normalize.rs

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,7 @@
11
use formality_types::{
22
cast::Downcast,
33
grammar::{
4-
AliasTy, AtomicRelation, InferenceVar, Parameter, RigidTy, TyData, Variable, Wc, WcData,
5-
Wcs,
4+
AliasTy, InferenceVar, Parameter, Relation, RigidTy, TyData, Variable, Wc, WcData, Wcs,
65
},
76
judgment_fn,
87
};
@@ -73,14 +72,14 @@ judgment_fn! {
7372
(if let Some(Variable::InferenceVar(v_a)) = a.downcast())
7473
(if v_goal == v_a)
7574
----------------------------- ("var-axiom-l")
76-
(prove_normalize_via(_decls, env, _assumptions, AtomicRelation::Equals(a, b), Variable::InferenceVar(v_goal)) => (Constraints::none(env), b))
75+
(prove_normalize_via(_decls, env, _assumptions, Relation::Equals(a, b), Variable::InferenceVar(v_goal)) => (Constraints::none(env), b))
7776
)
7877

7978
(
8079
(if let Some(Variable::InferenceVar(v_a)) = a.downcast())
8180
(if v_goal == v_a)
8281
----------------------------- ("var-axiom-r")
83-
(prove_normalize_via(_decls, env, _assumptions, AtomicRelation::Equals(b, a), Variable::InferenceVar(v_goal)) => (Constraints::none(env), b))
82+
(prove_normalize_via(_decls, env, _assumptions, Relation::Equals(b, a), Variable::InferenceVar(v_goal)) => (Constraints::none(env), b))
8483
)
8584

8685
// The following 2 rules handle normalization of a type `X` given an assumption `X = Y`.
@@ -97,7 +96,7 @@ judgment_fn! {
9796
(prove_syntactically_eq(decls, env, assumptions, a, goal) => c)
9897
(let b = c.substitution().apply(&b))
9998
----------------------------- ("axiom-l")
100-
(prove_normalize_via(decls, env, assumptions, AtomicRelation::Equals(a, b), goal) => (c, b))
99+
(prove_normalize_via(decls, env, assumptions, Relation::Equals(a, b), goal) => (c, b))
101100
)
102101

103102
(
@@ -106,7 +105,7 @@ judgment_fn! {
106105
(prove_syntactically_eq(decls, env, assumptions, a, goal) => c)
107106
(let b = c.substitution().apply(&b))
108107
----------------------------- ("axiom-r")
109-
(prove_normalize_via(decls, env, assumptions, AtomicRelation::Equals(b, a), goal) => (c, b))
108+
(prove_normalize_via(decls, env, assumptions, Relation::Equals(b, a), goal) => (c, b))
110109
)
111110

112111
// These rules handle the the ∀ and ⇒ cases.

‎crates/formality-rust/src/prove.rs

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,7 @@ use formality_prove as prove;
77
use formality_types::{
88
cast::{To, Upcast, Upcasted},
99
grammar::{
10-
fresh_bound_var, AliasTy, AtomicRelation, Binder, ParameterKind, Predicate, Ty, Wc, Wcs,
11-
APR,
10+
fresh_bound_var, AliasTy, Binder, ParameterKind, Predicate, Relation, Ty, Wc, Wcs, PR,
1211
},
1312
seq,
1413
};
@@ -257,9 +256,9 @@ macro_rules! upcast_to_wcs {
257256
upcast_to_wcs! {
258257
Wc,
259258
Wcs,
260-
APR,
259+
PR,
261260
Predicate,
262-
AtomicRelation,
261+
Relation,
263262
}
264263

265264
impl<A, B> ToWcs for (A, B)
@@ -293,7 +292,7 @@ impl ToWcs for WhereClause {
293292
WhereClauseData::IsImplemented(self_ty, trait_id, parameters) => {
294293
trait_id.with(self_ty, parameters).upcast()
295294
}
296-
WhereClauseData::Outlives(a, b) => AtomicRelation::outlives(a, b).upcast(),
295+
WhereClauseData::Outlives(a, b) => Relation::outlives(a, b).upcast(),
297296
WhereClauseData::ForAll(binder) => {
298297
let (vars, wc) = binder.open();
299298
wc.to_wcs()
@@ -313,7 +312,7 @@ impl WhereBound {
313312
WhereBoundData::IsImplemented(trait_id, parameters) => {
314313
trait_id.with(self_ty, parameters).upcast()
315314
}
316-
WhereBoundData::Outlives(lt) => AtomicRelation::outlives(self_ty, lt).upcast(),
315+
WhereBoundData::Outlives(lt) => Relation::outlives(self_ty, lt).upcast(),
317316
WhereBoundData::ForAll(binder) => {
318317
let (vars, bound) = binder.open();
319318
Wc::for_all(&vars, bound.to_wc(self_ty))

‎crates/formality-types/src/grammar/formulas.rs

Lines changed: 26 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -80,19 +80,19 @@ impl AliasTy {
8080
}
8181

8282
impl Ty {
83-
pub fn well_formed(&self) -> AtomicRelation {
84-
AtomicRelation::WellFormed(self.upcast())
83+
pub fn well_formed(&self) -> Relation {
84+
Relation::WellFormed(self.upcast())
8585
}
8686
}
8787

8888
impl Parameter {
8989
/// Well-formed goal for a parameter
90-
pub fn well_formed(&self) -> AtomicRelation {
91-
AtomicRelation::WellFormed(self.to())
90+
pub fn well_formed(&self) -> Relation {
91+
Relation::WellFormed(self.to())
9292
}
9393

94-
pub fn outlives(&self, b: impl Upcast<Parameter>) -> AtomicRelation {
95-
AtomicRelation::Outlives(self.clone(), b.upcast())
94+
pub fn outlives(&self, b: impl Upcast<Parameter>) -> Relation {
95+
Relation::Outlives(self.clone(), b.upcast())
9696
}
9797
}
9898

@@ -168,7 +168,7 @@ impl AdtId {
168168

169169
/// Relations are built-in goals which are implemented in custom Rust logic.
170170
#[term]
171-
pub enum AtomicRelation {
171+
pub enum Relation {
172172
#[grammar($v0 = $v1)]
173173
Equals(Parameter, Parameter),
174174

@@ -182,15 +182,15 @@ pub enum AtomicRelation {
182182
WellFormed(Parameter),
183183
}
184184

185-
impl AtomicRelation {
185+
impl Relation {
186186
/// Capture a few trivial cases; we screen these out to cleanup the results
187187
/// from queries.
188188
pub fn is_trivially_true(&self) -> bool {
189189
match self {
190-
AtomicRelation::Equals(a, b) => a == b,
191-
AtomicRelation::Sub(a, b) => a == b,
192-
AtomicRelation::Outlives(a, b) => a == b,
193-
AtomicRelation::WellFormed(_) => false,
190+
Relation::Equals(a, b) => a == b,
191+
Relation::Sub(a, b) => a == b,
192+
Relation::Outlives(a, b) => a == b,
193+
Relation::WellFormed(_) => false,
194194
}
195195
}
196196

@@ -208,10 +208,10 @@ impl AtomicRelation {
208208

209209
pub fn debone(&self) -> (Skeleton, Vec<Parameter>) {
210210
match self {
211-
AtomicRelation::Equals(a, b) => (Skeleton::Equals, vec![a.clone(), b.clone()]),
212-
AtomicRelation::Sub(a, b) => (Skeleton::Sub, vec![a.clone(), b.clone()]),
213-
AtomicRelation::Outlives(a, b) => (Skeleton::Outlives, vec![a.clone(), b.clone()]),
214-
AtomicRelation::WellFormed(p) => (Skeleton::WellFormed, vec![p.clone()]),
211+
Relation::Equals(a, b) => (Skeleton::Equals, vec![a.clone(), b.clone()]),
212+
Relation::Sub(a, b) => (Skeleton::Sub, vec![a.clone(), b.clone()]),
213+
Relation::Outlives(a, b) => (Skeleton::Outlives, vec![a.clone(), b.clone()]),
214+
Relation::WellFormed(p) => (Skeleton::WellFormed, vec![p.clone()]),
215215
}
216216
}
217217
}
@@ -243,22 +243,22 @@ impl TraitId {
243243
}
244244
}
245245

246-
/// "APR" == AtomicPredicateOrRelation
246+
/// "PR" == Predicate or Relation
247247
///
248248
/// We need a better name for this lol.
249249
#[term]
250-
pub enum APR {
250+
pub enum PR {
251251
#[cast]
252-
AtomicPredicate(Predicate),
252+
Predicate(Predicate),
253253
#[cast]
254-
AtomicRelation(AtomicRelation),
254+
Relation(Relation),
255255
}
256256

257-
impl APR {
257+
impl PR {
258258
pub fn debone(&self) -> (Skeleton, Vec<Parameter>) {
259259
match self {
260-
APR::AtomicPredicate(v) => v.debone(),
261-
APR::AtomicRelation(v) => v.debone(),
260+
PR::Predicate(v) => v.debone(),
261+
PR::Relation(v) => v.debone(),
262262
}
263263
}
264264
}
@@ -277,10 +277,10 @@ macro_rules! debone_impl {
277277
};
278278
}
279279

280-
debone_impl!(APR);
280+
debone_impl!(PR);
281281
debone_impl!(Predicate);
282-
debone_impl!(AtomicRelation);
282+
debone_impl!(Relation);
283283

284284
// Transitive casting impls:
285285

286-
cast_impl!((TraitRef) <: (Predicate) <: (APR));
286+
cast_impl!((TraitRef) <: (Predicate) <: (PR));

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

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,11 @@ use crate::{
66
cast::{DowncastFrom, DowncastTo, Upcast, UpcastFrom},
77
cast_impl,
88
collections::{Set, SetExt},
9-
grammar::APR,
9+
grammar::PR,
1010
set,
1111
};
1212

13-
use super::{AtomicRelation, Binder, BoundVar, Predicate, TraitRef};
13+
use super::{Binder, BoundVar, Predicate, Relation, TraitRef};
1414

1515
#[term($set)]
1616
pub struct Wcs {
@@ -119,7 +119,7 @@ impl Wc {
119119
#[term]
120120
pub enum WcData {
121121
#[cast]
122-
Atomic(APR),
122+
Atomic(PR),
123123

124124
#[grammar(for $v0)]
125125
ForAll(Binder<Wc>),
@@ -150,10 +150,10 @@ impl DowncastFrom<Wc> for WcData {
150150

151151
// ---
152152

153-
cast_impl!((APR) <: (WcData) <: (Wc));
154-
cast_impl!((AtomicRelation) <: (APR) <: (Wc));
155-
cast_impl!((Predicate) <: (APR) <: (Wc));
156-
cast_impl!((TraitRef) <: (APR) <: (Wc));
153+
cast_impl!((PR) <: (WcData) <: (Wc));
154+
cast_impl!((Relation) <: (PR) <: (Wc));
155+
cast_impl!((Predicate) <: (PR) <: (Wc));
156+
cast_impl!((TraitRef) <: (PR) <: (Wc));
157157

158158
impl UpcastFrom<Wc> for Wcs {
159159
fn upcast_from(term: Wc) -> Self {
@@ -171,7 +171,7 @@ impl DowncastTo<Wc> for Wcs {
171171
}
172172
}
173173

174-
cast_impl!((APR) <: (Wc) <: (Wcs));
175-
cast_impl!((AtomicRelation) <: (Wc) <: (Wcs));
174+
cast_impl!((PR) <: (Wc) <: (Wcs));
175+
cast_impl!((Relation) <: (Wc) <: (Wcs));
176176
cast_impl!((Predicate) <: (Wc) <: (Wcs));
177177
cast_impl!((TraitRef) <: (Wc) <: (Wcs));

0 commit comments

Comments
 (0)