Skip to content

Commit 121f69f

Browse files
nikomatsakisnikomatsakis
committed
introduce rust layer, conversion to prove
rename program in prove layer to decls
1 parent 6c2b93f commit 121f69f

39 files changed

+498
-618
lines changed

‎Cargo.lock

Lines changed: 1 addition & 2 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎crates/formality-prove/src/program.rs renamed to ‎crates/formality-prove/src/decls.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,15 +5,15 @@ use formality_types::{
55
};
66

77
#[term]
8-
pub struct Program {
8+
pub struct Decls {
99
pub max_size: usize,
1010
pub trait_decls: Vec<TraitDecl>,
1111
pub impl_decls: Vec<ImplDecl>,
1212
pub alias_eq_decls: Vec<AliasEqDecl>,
1313
pub alias_bound_decls: Vec<AliasBoundDecl>,
1414
}
1515

16-
impl Program {
16+
impl Decls {
1717
/// Max size used in unit tests that are not stress testing maximum size.
1818
pub const DEFAULT_MAX_SIZE: usize = 222;
1919

@@ -58,7 +58,7 @@ impl Program {
5858

5959
pub fn empty() -> Self {
6060
Self {
61-
max_size: Program::DEFAULT_MAX_SIZE,
61+
max_size: Decls::DEFAULT_MAX_SIZE,
6262
trait_decls: vec![],
6363
impl_decls: vec![],
6464
alias_eq_decls: vec![],

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,12 @@
11
use formality_types::derive_links;
22

33
mod db;
4-
mod program;
4+
mod decls;
55
mod prove;
66

7+
pub use decls::*;
8+
pub use prove::prove;
9+
pub use prove::Env;
10+
711
#[cfg(test)]
812
mod test;

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

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,41 +14,41 @@ pub use constraints::Constraints;
1414
use formality_types::{cast::Upcast, collections::Set, grammar::Wcs, set, visit::Visit};
1515
use tracing::Level;
1616

17-
use crate::program::Program;
17+
use crate::decls::Decls;
1818

1919
pub use self::env::Env;
2020
use self::prove_wc_list::prove_wc_list;
2121

2222
/// Top-level entry point for proving things; other rules recurse to this one.
2323
pub fn prove(
24-
program: impl Upcast<Program>,
24+
decls: impl Upcast<Decls>,
2525
env: impl Upcast<Env>,
2626
assumptions: impl Upcast<Wcs>,
2727
goal: impl Upcast<Wcs>,
2828
) -> Set<Constraints> {
29-
let program: Program = program.upcast();
29+
let decls: Decls = decls.upcast();
3030
let env: Env = env.upcast();
3131
let assumptions: Wcs = assumptions.upcast();
3232
let goal: Wcs = goal.upcast();
3333

3434
let (env, (assumptions, goal), min) = minimize::minimize(env, (assumptions, goal));
3535

36-
let span = tracing::span!(Level::DEBUG, "prove", ?goal, ?assumptions, ?env, ?program);
36+
let span = tracing::span!(Level::DEBUG, "prove", ?goal, ?assumptions, ?env, ?decls);
3737
let _guard = span.enter();
3838

3939
let term_in = (&assumptions, &goal);
40-
if term_in.size() > program.max_size {
40+
if term_in.size() > decls.max_size {
4141
tracing::debug!(
4242
"term has size {} which exceeds max size of {}",
4343
term_in.size(),
44-
program.max_size
44+
decls.max_size
4545
);
4646
return set![Constraints::none(env).ambiguous()];
4747
}
4848

4949
assert!(env.encloses(term_in));
5050

51-
let result_set = prove_wc_list(program, &env, assumptions, goal);
51+
let result_set = prove_wc_list(decls, &env, assumptions, goal);
5252

5353
result_set.iter().for_each(|constraints1| {
5454
assert!(constraints1.is_valid_extension_of(&env));

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,23 +1,23 @@
11
use formality_types::{grammar::Wcs, judgment_fn};
22

3-
use crate::{program::Program, prove::prove};
3+
use crate::{decls::Decls, prove::prove};
44

55
use super::constraints::Constraints;
66

77
judgment_fn! {
88
pub fn prove_after(
9-
program: Program,
9+
decls: Decls,
1010
constraints: Constraints,
1111
assumptions: Wcs,
1212
goal: Wcs,
1313
) => Constraints {
14-
debug(constraints, goal, assumptions, program)
14+
debug(constraints, goal, assumptions, decls)
1515

1616
(
1717
(let (assumptions, goal) = c1.substitution().apply(&(assumptions, goal)))
18-
(prove(program, c1.env(), assumptions, goal) => c2)
18+
(prove(decls, c1.env(), assumptions, goal) => c2)
1919
--- ("prove_after")
20-
(prove_after(program, c1, assumptions, goal) => c1.seq(c2))
20+
(prove_after(decls, c1, assumptions, goal) => c1.seq(c2))
2121
)
2222
}
2323
}

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

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use formality_types::{
44
};
55

66
use crate::{
7-
program::Program,
7+
decls::Decls,
88
prove::{
99
env::Env,
1010
prove,
@@ -18,47 +18,47 @@ use super::constraints::Constraints;
1818

1919
judgment_fn! {
2020
pub fn prove_apr(
21-
program: Program,
21+
decls: Decls,
2222
env: Env,
2323
assumptions: Wcs,
2424
goal: APR,
2525
) => Constraints {
26-
debug(goal, assumptions, env, program)
26+
debug(goal, assumptions, env, decls)
2727

2828
(
2929
(&assumptions => a)
30-
(prove_apr_via(&program, &env, &assumptions, a, &goal) => c)
30+
(prove_apr_via(&decls, &env, &assumptions, a, &goal) => c)
3131
----------------------------- ("assumption")
32-
(prove_apr(program, env, assumptions, goal) => c)
32+
(prove_apr(decls, env, assumptions, goal) => c)
3333
)
3434

3535
(
36-
(program.impl_decls(&trait_ref.trait_id) => i)
36+
(decls.impl_decls(&trait_ref.trait_id) => i)
3737
(let (env, subst) = env.existential_substitution(&i.binder))
3838
(let i = i.binder.instantiate_with(&subst).unwrap())
39-
(let t = program.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
39+
(let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
4040
(let co_assumptions = (&assumptions, &trait_ref))
41-
(prove(&program, env, &co_assumptions, all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
42-
(prove_after(&program, c, &co_assumptions, &i.where_clause) => c)
43-
(prove_after(&program, c, &assumptions, &t.where_clause) => c)
41+
(prove(&decls, env, &co_assumptions, all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
42+
(prove_after(&decls, c, &co_assumptions, &i.where_clause) => c)
43+
(prove_after(&decls, c, &assumptions, &t.where_clause) => c)
4444
----------------------------- ("impl")
45-
(prove_apr(program, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
45+
(prove_apr(decls, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
4646
)
4747

4848
(
49-
(program.trait_invariants() => ti)
49+
(decls.trait_invariants() => ti)
5050
(let (env, subst) = env.existential_substitution(&ti.binder))
5151
(let ti = ti.binder.instantiate_with(&subst).unwrap())
52-
(prove_apr_via(&program, env, &assumptions, &ti.where_clause, &trait_ref) => c)
53-
(prove_after(&program, c, &assumptions, &ti.trait_ref) => c)
52+
(prove_apr_via(&decls, env, &assumptions, &ti.where_clause, &trait_ref) => c)
53+
(prove_after(&decls, c, &assumptions, &ti.trait_ref) => c)
5454
----------------------------- ("trait implied bound")
55-
(prove_apr(program, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
55+
(prove_apr(decls, env, assumptions, AtomicPredicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
5656
)
5757

5858
(
59-
(prove_ty_eq(program, env, assumptions, a, b) => c)
59+
(prove_ty_eq(decls, env, assumptions, a, b) => c)
6060
----------------------------- ("eq")
61-
(prove_apr(program, env, assumptions, AtomicRelation::Equals(Parameter::Ty(a), Parameter::Ty(b))) => c)
61+
(prove_apr(decls, env, assumptions, AtomicRelation::Equals(Parameter::Ty(a), Parameter::Ty(b))) => c)
6262
)
6363
}
6464
}

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -4,29 +4,29 @@ use formality_types::{
44
};
55

66
use crate::{
7-
program::Program,
7+
decls::Decls,
88
prove::{
99
constraints::Constraints, env::Env, prove, prove_after::prove_after, prove_eq::all_eq,
1010
},
1111
};
1212

1313
judgment_fn! {
1414
pub fn prove_apr_via(
15-
program: Program,
15+
decls: Decls,
1616
env: Env,
1717
assumptions: Wcs,
1818
via: WcData,
1919
goal: APR,
2020
) => Constraints {
21-
debug(goal, via, assumptions, env, program)
21+
debug(goal, via, assumptions, env, decls)
2222

2323
(
2424
(let (skel_c, parameters_c) = predicate.debone())
2525
(let (skel_g, parameters_g) = goal.debone())
2626
(if skel_c == skel_g)
27-
(prove(program, env, assumptions, all_eq(parameters_c, parameters_g)) => c)
27+
(prove(decls, env, assumptions, all_eq(parameters_c, parameters_g)) => c)
2828
----------------------------- ("predicate-congruence-axiom")
29-
(prove_apr_via(program, env, assumptions, APR::AtomicPredicate(predicate), goal) => c)
29+
(prove_apr_via(decls, env, assumptions, APR::AtomicPredicate(predicate), goal) => c)
3030
)
3131

3232
(
@@ -35,22 +35,22 @@ 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(_program, env, _assumptions, APR::AtomicRelation(relation), goal) => Constraints::none(env))
38+
(prove_apr_via(_decls, env, _assumptions, APR::AtomicRelation(relation), goal) => Constraints::none(env))
3939
)
4040

4141
(
4242
(let (env, subst) = env.existential_substitution(&binder))
4343
(let via1 = binder.instantiate_with(&subst).unwrap())
44-
(prove_apr_via(program, env, assumptions, via1, goal) => c)
44+
(prove_apr_via(decls, env, assumptions, via1, goal) => c)
4545
----------------------------- ("forall")
46-
(prove_apr_via(program, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst))
46+
(prove_apr_via(decls, env, assumptions, WcData::ForAll(binder), goal) => c.pop_subst(&subst))
4747
)
4848

4949
(
50-
(prove_apr_via(&program, env, &assumptions, wc_consequence, goal) => c)
51-
(prove_after(&program, c, &assumptions, &wc_condition) => c)
50+
(prove_apr_via(&decls, env, &assumptions, wc_consequence, goal) => c)
51+
(prove_after(&decls, c, &assumptions, &wc_condition) => c)
5252
----------------------------- ("implies")
53-
(prove_apr_via(program, env, assumptions, WcData::Implies(wc_condition, wc_consequence), goal) => c)
53+
(prove_apr_via(decls, env, assumptions, WcData::Implies(wc_condition, wc_consequence), goal) => c)
5454
)
5555
}
5656
}

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

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ use formality_types::{
1010
};
1111

1212
use crate::{
13-
program::Program,
13+
decls::Decls,
1414
prove::{
1515
constraints::occurs_in, prove, prove_after::prove_after, prove_normalize::prove_normalize,
1616
},
@@ -37,89 +37,89 @@ pub fn eq(a: impl Upcast<Parameter>, b: impl Upcast<Parameter>) -> AtomicRelatio
3737

3838
judgment_fn! {
3939
pub fn prove_ty_eq(
40-
program: Program,
40+
decls: Decls,
4141
env: Env,
4242
assumptions: Wcs,
4343
a: Ty,
4444
b: Ty,
4545
) => Constraints {
46-
debug(a, b, assumptions, env, program)
46+
debug(a, b, assumptions, env, decls)
4747

4848
trivial(a == b => Constraints::none(env))
4949

5050
(
51-
(prove_ty_eq(program, env, assumptions, r, l) => env_c)
51+
(prove_ty_eq(decls, env, assumptions, r, l) => env_c)
5252
----------------------------- ("symmetric")
53-
(prove_ty_eq(program, env, assumptions, l, r) => env_c)
53+
(prove_ty_eq(decls, env, assumptions, l, r) => env_c)
5454
)
5555

5656
(
5757
(let RigidTy { name: a_name, parameters: a_parameters } = a)
5858
(let RigidTy { name: b_name, parameters: b_parameters } = b)
5959
(if a_name == b_name)
60-
(prove(program, env, assumptions, all_eq(a_parameters, b_parameters)) => c)
60+
(prove(decls, env, assumptions, all_eq(a_parameters, b_parameters)) => c)
6161
----------------------------- ("rigid")
62-
(prove_ty_eq(program, env, assumptions, TyData::RigidTy(a), TyData::RigidTy(b)) => c)
62+
(prove_ty_eq(decls, env, assumptions, TyData::RigidTy(a), TyData::RigidTy(b)) => c)
6363
)
6464

6565
(
6666
(let AliasTy { name: a_name, parameters: a_parameters } = a)
6767
(let AliasTy { name: b_name, parameters: b_parameters } = b)
6868
(if a_name == b_name)
69-
(prove(program, env, assumptions, all_eq(a_parameters, b_parameters)) => env_c)
69+
(prove(decls, env, assumptions, all_eq(a_parameters, b_parameters)) => env_c)
7070
----------------------------- ("alias")
71-
(prove_ty_eq(program, env, assumptions, TyData::AliasTy(a), TyData::AliasTy(b)) => env_c)
71+
(prove_ty_eq(decls, env, assumptions, TyData::AliasTy(a), TyData::AliasTy(b)) => env_c)
7272
)
7373

7474
(
75-
(prove_existential_var_eq(program, env, assumptions, v, r) => c)
75+
(prove_existential_var_eq(decls, env, assumptions, v, r) => c)
7676
----------------------------- ("existential-nonvar")
77-
(prove_ty_eq(program, env, assumptions, Variable::InferenceVar(v), r) => c)
77+
(prove_ty_eq(decls, env, assumptions, Variable::InferenceVar(v), r) => c)
7878
)
7979

8080
(
81-
(prove_normalize(&program, env, &assumptions, &x) => (c, y))
82-
(prove_after(&program, c, &assumptions, eq(y, &z)) => c)
81+
(prove_normalize(&decls, env, &assumptions, &x) => (c, y))
82+
(prove_after(&decls, c, &assumptions, eq(y, &z)) => c)
8383
----------------------------- ("normalize-l")
84-
(prove_ty_eq(program, env, assumptions, x, z) => c)
84+
(prove_ty_eq(decls, env, assumptions, x, z) => c)
8585
)
8686
}
8787
}
8888

8989
judgment_fn! {
9090
pub fn prove_existential_var_eq(
91-
program: Program,
91+
decls: Decls,
9292
env: Env,
9393
assumptions: Wcs,
9494
v: InferenceVar,
9595
b: Parameter,
9696
) => Constraints {
97-
debug(v, b, assumptions, env, program)
97+
debug(v, b, assumptions, env, decls)
9898

9999
(
100100
(if let None = t.downcast::<Variable>())
101-
(equate_variable(program, env, assumptions, v, t) => c)
101+
(equate_variable(decls, env, assumptions, v, t) => c)
102102
----------------------------- ("existential-nonvar")
103-
(prove_existential_var_eq(program, env, assumptions, v, t) => c)
103+
(prove_existential_var_eq(decls, env, assumptions, v, t) => c)
104104
)
105105

106106
(
107107
// Map the higher rank variable to the lower rank one.
108108
(let (a, b) = env.order_by_universe(l, r))
109109
----------------------------- ("existential-existential")
110-
(prove_existential_var_eq(_program, env, _assumptions, l, Variable::InferenceVar(r)) => (env, (b, a)))
110+
(prove_existential_var_eq(_decls, env, _assumptions, l, Variable::InferenceVar(r)) => (env, (b, a)))
111111
)
112112

113113
(
114114
(if env.universe(p) < env.universe(v))
115115
----------------------------- ("existential-placeholder")
116-
(prove_existential_var_eq(_program, env, _assumptions, v, Variable::PlaceholderVar(p)) => (env, (v, p)))
116+
(prove_existential_var_eq(_decls, env, _assumptions, v, Variable::PlaceholderVar(p)) => (env, (v, p)))
117117
)
118118
}
119119
}
120120

121121
fn equate_variable(
122-
program: Program,
122+
decls: Decls,
123123
mut env: Env,
124124
assumptions: Wcs,
125125
x: InferenceVar,
@@ -188,5 +188,5 @@ fn equate_variable(
188188

189189
tracing::debug!("equated: constraints={:?}, goals={:?}", constraints, goals);
190190

191-
prove_after(program, constraints, assumptions, goals)
191+
prove_after(decls, constraints, assumptions, goals)
192192
}

0 commit comments

Comments
 (0)