Skip to content

Commit 403c98a

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

File tree

18 files changed

+204
-194
lines changed

18 files changed

+204
-194
lines changed

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

+1-3
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

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+

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

+1-1
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

+1-3
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

+82-1
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,23 @@ 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+
vals.iter()
26+
.zip(params.iter())
27+
.filter_map(|(a, b)| match a {
28+
ExhaustiveState::ExactMatch => None,
29+
ExhaustiveState::ConstCover(cs) => {
30+
let Parameter::Const(c) = b else {
31+
todo!();
32+
};
33+
Some(Predicate::Covers(cs.clone(), c.clone()))
34+
}
35+
})
36+
.upcasted()
37+
.collect()
38+
}
39+
2140
judgment_fn! {
2241
pub fn prove_wc(
2342
decls: Decls,
@@ -48,6 +67,50 @@ judgment_fn! {
4867
(prove_wc(decls, env, assumptions, WcData::PR(goal)) => c)
4968
)
5069

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

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

112193
(
113194
(prove_wf(decls, env, assumptions, p) => c)

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

+4
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

+13
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

+38-1
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

+1-1
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

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+

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

+5-1
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,11 @@ impl<'t> ParseError<'t> {
115115

116116
/// Offset of this error relative to the starting point `text`
117117
pub fn offset(&self, text: &str) -> usize {
118-
assert!(text.ends_with(self.text));
118+
assert!(
119+
text.ends_with(self.text),
120+
"text={text}, \nself.text={}",
121+
self.text
122+
);
119123
text.len() - self.text.len()
120124
}
121125

0 commit comments

Comments
 (0)