Skip to content

Commit 0909bed

Browse files
JulianKnodtJulianKnodt
committed
Add new exhaustive covering predicate
& Add additional tests
1 parent bc4a135 commit 0909bed

File tree

17 files changed

+201
-194
lines changed

17 files changed

+201
-194
lines changed

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,7 @@ use formality_rust::{
33
grammar::{Fn, FnBoundData},
44
prove::ToWcs,
55
};
6-
use formality_types::{
7-
grammar::{Fallible, Wcs},
8-
};
6+
use formality_types::grammar::{Fallible, Wcs};
97

108
use crate::Check;
119

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
mod combinators;
12
mod constraints;
23
mod env;
34
mod is_local;
@@ -9,7 +10,6 @@ mod prove_via;
910
mod prove_wc;
1011
mod prove_wc_list;
1112
mod prove_wf;
12-
mod combinators;
1313

1414
pub use constraints::Constraints;
1515
use formality_types::{cast::Upcast, collections::Set, grammar::Wcs, set, visit::Visit};

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

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,7 @@ use formality_types::{
55

66
use crate::{
77
decls::Decls,
8-
prove::{
9-
constraints::Constraints, env::Env, prove, prove_after::prove_after,
10-
},
8+
prove::{constraints::Constraints, env::Env, prove, prove_after::prove_after},
119
};
1210

1311
judgment_fn! {

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

Lines changed: 83 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
use formality_types::{
2-
grammar::{Predicate, Relation, Wc, WcData, Wcs},
2+
cast::Upcasted,
3+
grammar::{Const, ExhaustiveState, Predicate, Relation, Scalar, Ty, Wc, WcData, Wcs},
34
judgment_fn,
45
};
56

67
use crate::{
78
decls::Decls,
9+
derive_links::Parameter,
810
prove::{
911
env::Env,
1012
is_local::{is_local_trait_ref, may_be_remote},
@@ -18,6 +20,24 @@ use crate::{
1820

1921
use super::constraints::Constraints;
2022

23+
pub fn is_covering(vals: &[ExhaustiveState], params: &[Parameter]) -> Wcs {
24+
assert_eq!(vals.len(), params.len());
25+
println!("vals={vals:?}, params={params:?}");
26+
vals.iter()
27+
.zip(params.iter())
28+
.filter_map(|(a, b)| match a {
29+
ExhaustiveState::ExactMatch => None,
30+
ExhaustiveState::ConstCover(cs) => {
31+
let Parameter::Const(c) = b else {
32+
todo!();
33+
};
34+
Some(Predicate::Covers(cs.clone(), c.clone()))
35+
}
36+
})
37+
.upcasted()
38+
.collect()
39+
}
40+
2141
judgment_fn! {
2242
pub fn prove_wc(
2343
decls: Decls,
@@ -48,6 +68,50 @@ judgment_fn! {
4868
(prove_wc(decls, env, assumptions, WcData::PR(goal)) => c)
4969
)
5070

71+
(
72+
(decls.impl_decls(&trait_ref.trait_id) => i)
73+
(let (env, subst) = env.existential_substitution(&i.binder))
74+
(let i = i.binder.instantiate_with(&subst).unwrap())
75+
(let co_assumptions = (&assumptions, &trait_ref))
76+
(prove(&decls, env, &co_assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => c)
77+
(let t = decls.trait_decl(&i.trait_ref.trait_id).binder.instantiate_with(&i.trait_ref.parameters).unwrap())
78+
(prove_after(&decls, c, &co_assumptions, &i.where_clause) => c)
79+
(prove_after(&decls, c, &assumptions, &t.where_clause) => c)
80+
----------------------------- ("positive impl")
81+
(prove_wc(decls, env, assumptions, Predicate::IsImplemented(trait_ref)) => c.pop_subst(&subst))
82+
)
83+
84+
(
85+
(let mut covering_consts = vec![ExhaustiveState::ExactMatch; trait_ref.parameters.len()])
86+
(let ass = &assumptions)
87+
(let d = &decls)
88+
(d.impl_decls(&trait_ref.trait_id).flat_map(|i| {
89+
90+
let (env, subst) = env.clone().existential_substitution(&i.binder);
91+
let i = i.binder.instantiate_with(&subst).unwrap();
92+
let co_assumptions = (ass, &trait_ref);
93+
let cs = prove(
94+
&decls, env, &co_assumptions,
95+
Wcs::eq_or_cover(
96+
&i.trait_ref.parameters, &trait_ref.parameters, &mut covering_consts
97+
)
98+
).into_iter().collect::<Vec<_>>();
99+
let cs = cs.into_iter().flat_map(move |c| {
100+
prove_after(d, c, &co_assumptions, &i.where_clause)
101+
.into_iter()
102+
}).into_iter().collect::<Vec<_>>();
103+
let cs :Vec<Constraints> = cs.into_iter().flat_map(move |c| {
104+
let t = d.trait_decl(&i.trait_ref.trait_id)
105+
.binder.instantiate_with(&i.trait_ref.parameters).unwrap();
106+
prove_after(d, c, ass, &t.where_clause).into_iter()
107+
}).collect::<Vec<_>>();
108+
cs
109+
}).collect::<Vec<_>>().into_iter() => c)
110+
(prove_after(d, c, ass, is_covering(&covering_consts, &trait_ref.parameters)) => _c)
111+
----------------------------- ("exhaustive positive impl")
112+
(prove_wc(_d, env, _ass, Predicate::IsImplemented(trait_ref)) => Constraints::none(env.clone()))
113+
)
114+
51115
(
52116
(decls.impl_decls(&trait_ref.trait_id) => i)
53117
(let (env, subst) = env.existential_substitution(&i.binder))
@@ -108,6 +172,24 @@ judgment_fn! {
108172
(prove_wc(decls, env, assumptions, Predicate::IsLocal(trait_ref)) => c)
109173
)
110174

175+
(
176+
(let () = vals.sort_unstable())
177+
(prove(&decls, env, &assumptions, Predicate::ConstHasType(var, Ty::bool())) => c)
178+
(vals.iter().cloned() => v)
179+
(prove_after(&decls, &c, &assumptions, Predicate::ConstHasType(v, Ty::bool())) => c)
180+
(if vals.len() == 2)
181+
(vals.iter()
182+
.enumerate()
183+
.flat_map(|(i,v)|
184+
prove_after(
185+
&decls, &c, &assumptions,
186+
Relation::eq(Const::valtree(Scalar::new(i as u128), Ty::bool()), v)
187+
)
188+
).collect::<Vec<_>>().into_iter() => c)
189+
----------------------------- ("exhausttive bool values cover variable")
190+
(prove_wc(decls, env, assumptions, Predicate::Covers(mut vals, var)) => c)
191+
)
192+
111193

112194
(
113195
(prove_wf(decls, env, assumptions, p) => c)

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,10 @@ impl Const {
2626
Self::new(ConstData::Value(vt.upcast(), ty.upcast()))
2727
}
2828

29+
pub fn is_variable(&self) -> bool {
30+
matches!(self.data(), ConstData::Variable(_))
31+
}
32+
2933
pub fn as_variable(&self) -> Option<Variable> {
3034
match self.data() {
3135
ConstData::Value(_, _) => None,

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,9 @@ pub enum Predicate {
3131

3232
#[grammar(@ConstHasType($v0, $v1))]
3333
ConstHasType(Const, Ty),
34+
35+
#[grammar(@CoveringSet($v0, $v1))]
36+
Covers(Vec<Const>, Const),
3437
}
3538

3639
/// A coinductive predicate is one that can be proven via a cycle.
@@ -88,6 +91,7 @@ pub enum Skeleton {
8891
Equals,
8992
Sub,
9093
Outlives,
94+
Covered,
9195
}
9296

9397
impl Predicate {
@@ -125,6 +129,15 @@ impl Predicate {
125129
Skeleton::ConstHasType,
126130
vec![ct.clone().upcast(), ty.clone().upcast()],
127131
),
132+
Predicate::Covers(consts, c) => (
133+
Skeleton::Covered,
134+
consts
135+
.iter()
136+
.cloned()
137+
.chain(std::iter::once(c.clone()))
138+
.map(|c| Parameter::Const(c))
139+
.collect::<Vec<_>>(),
140+
),
128141
}
129142
}
130143
}

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

Lines changed: 38 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,13 +10,19 @@ use crate::{
1010
set,
1111
};
1212

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

1515
#[term($set)]
1616
pub struct Wcs {
1717
set: Set<Wc>,
1818
}
1919

20+
#[derive(Debug, Clone, PartialEq)]
21+
pub enum ExhaustiveState {
22+
ExactMatch,
23+
ConstCover(Vec<Const>),
24+
}
25+
2026
impl Wcs {
2127
pub fn t() -> Self {
2228
set![].upcast()
@@ -33,6 +39,37 @@ impl Wcs {
3339
.upcasted()
3440
.collect()
3541
}
42+
/// Goal(s) to prove `a` and `b` are equal (they must have equal length)
43+
pub fn eq_or_cover(
44+
candidate: impl Upcast<Vec<Parameter>>,
45+
trait_impl: impl Upcast<Vec<Parameter>>,
46+
covering_items: &mut Vec<ExhaustiveState>,
47+
) -> Wcs {
48+
let a: Vec<Parameter> = candidate.upcast();
49+
let b: Vec<Parameter> = trait_impl.upcast();
50+
assert_eq!(a.len(), b.len());
51+
a.into_iter()
52+
.zip(b)
53+
.enumerate()
54+
.filter_map(|(i, (a, b))| match (&a, &b) {
55+
(Parameter::Const(ct), Parameter::Const(param)) if param.is_variable() => {
56+
if covering_items[i] == ExhaustiveState::ExactMatch {
57+
covering_items[i] = ExhaustiveState::ConstCover(vec![]);
58+
}
59+
let ExhaustiveState::ConstCover(ref mut c) = &mut covering_items[i] else {
60+
panic!();
61+
};
62+
c.push(ct.clone());
63+
None
64+
}
65+
_ => {
66+
assert!(matches!(covering_items[i], ExhaustiveState::ExactMatch));
67+
Some(Relation::eq(a, b))
68+
}
69+
})
70+
.upcasted()
71+
.collect()
72+
}
3673
}
3774

3875
impl<'w> IntoIterator for &'w Wcs {

‎crates/formality-types/src/judgment/test_filtered.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ use std::sync::Arc;
44

55
use formality_macros::{term, test};
66

7-
use crate::{judgment_fn};
7+
use crate::judgment_fn;
88

99
#[term($edges)]
1010
struct Graph {

‎crates/formality-types/src/matcher.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+

0 commit comments

Comments
 (0)