Skip to content

Commit b520dc0

Browse files
nikomatsakisnikomatsakis
committed
track causes of judgment failures
1 parent 70cf56e commit b520dc0

File tree

12 files changed

+616
-74
lines changed

12 files changed

+616
-74
lines changed

‎Cargo.lock

Lines changed: 14 additions & 3 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎crates/formality-core/Cargo.toml

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,8 @@ formality-macros = { version = "0.1.0", path = "../formality-macros" }
2121
anyhow = "1.0.75"
2222
contracts = "0.6.3"
2323
final_fn = "0.1.0"
24+
itertools = "0.12.0"
25+
either = "1.9.0"
2426

2527
[dev-dependencies]
2628
expect-test = "1.4.1"

‎crates/formality-core/src/fixed_point.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ pub fn fixed_point<Input, Output>(
1111
storage: &'static LocalKey<RefCell<FixedPointStack<Input, Output>>>,
1212
args: Input,
1313
default_value: impl Fn(&Input) -> Output,
14-
next_value: impl Fn(Input) -> Output,
14+
next_value: impl FnMut(Input) -> Output,
1515
) -> Output
1616
where
1717
Input: Value,
@@ -48,10 +48,10 @@ where
4848
Input: Value,
4949
Output: Value,
5050
DefaultValue: Fn(&Input) -> Output,
51-
NextValue: Fn(Input) -> Output,
51+
NextValue: FnMut(Input) -> Output,
5252
TracingSpan: Fn(&Input) -> tracing::Span,
5353
{
54-
fn apply(&self, input: Input) -> Output {
54+
fn apply(&mut self, input: Input) -> Output {
5555
if let Some(r) = self.with_stack(|stack| stack.search(&input)) {
5656
tracing::debug!("recursive call to {:?}, yielding {:?}", input, r);
5757
return r;

‎crates/formality-core/src/judgment.rs

Lines changed: 89 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,14 @@
1-
use std::{cell::RefCell, collections::BTreeSet};
1+
use std::cell::RefCell;
22

3-
use crate::fixed_point::FixedPointStack;
3+
use crate::{fixed_point::FixedPointStack, Set};
4+
5+
mod proven_set;
6+
pub use proven_set::{FailedJudgment, FailedRule, ProvenSet, RuleFailureCause, TryIntoIter};
47

58
mod test_filtered;
69
mod test_reachable;
710

8-
pub type JudgmentStack<J, O> = RefCell<FixedPointStack<J, BTreeSet<O>>>;
11+
pub type JudgmentStack<J, O> = RefCell<FixedPointStack<J, Set<O>>>;
912

1013
#[macro_export]
1114
macro_rules! judgment_fn {
@@ -19,7 +22,7 @@ macro_rules! judgment_fn {
1922
}
2023
) => {
2124
$(#[$attr])*
22-
$v fn $name($($input_name : impl $crate::Upcast<$input_ty>),*) -> $crate::Set<$output> {
25+
$v fn $name($($input_name : impl $crate::Upcast<$input_ty>),*) -> $crate::ProvenSet<$output> {
2326
#[derive(Ord, PartialOrd, Eq, PartialEq, Hash, Clone)]
2427
struct __JudgmentStruct($($input_ty),*);
2528

@@ -30,7 +33,7 @@ macro_rules! judgment_fn {
3033
let mut f = fmt.debug_struct(stringify!($name));
3134
let __JudgmentStruct($($input_name),*) = self;
3235
$(
33-
f.field(stringify!($debug_input_name), $input_name);
36+
f.field(stringify!($debug_input_name), $debug_input_name);
3437
)*
3538
f.finish()
3639
}
@@ -47,11 +50,13 @@ macro_rules! judgment_fn {
4750
// Trivial cases are an (important) optimization that lets
4851
// you cut out all the normal rules.
4952
if $trivial_expr {
50-
return std::iter::once($trivial_result).collect();
53+
return $crate::ProvenSet::proven(std::iter::once($trivial_result).collect());
5154
}
5255
)*
5356

54-
$crate::fixed_point::fixed_point::<
57+
let mut failed_rules = $crate::set![];
58+
let input = __JudgmentStruct($($input_name),*);
59+
let output = $crate::fixed_point::fixed_point::<
5560
__JudgmentStruct,
5661
$crate::Set<$output>,
5762
>(
@@ -73,7 +78,7 @@ macro_rules! judgment_fn {
7378
},
7479

7580
// Input:
76-
__JudgmentStruct($($input_name),*),
81+
input.clone(),
7782

7883
// Default value:
7984
|_| Default::default(),
@@ -82,17 +87,26 @@ macro_rules! judgment_fn {
8287
|input: __JudgmentStruct| {
8388
let mut output = $crate::Set::new();
8489

90+
failed_rules.clear();
91+
8592
$crate::push_rules!(
8693
$name,
8794
&input,
8895
output,
96+
failed_rules,
8997
($($input_name),*) => $output,
9098
$(($($rule)*))*
9199
);
92100

93101
output
94102
},
95-
)
103+
);
104+
105+
if !output.is_empty() {
106+
$crate::ProvenSet::proven(output)
107+
} else {
108+
$crate::ProvenSet::failed_rules(&input, failed_rules)
109+
}
96110
}
97111
}
98112
}
@@ -123,15 +137,15 @@ macro_rules! judgment_fn {
123137
/// * `(<pat> => <binding>)
124138
#[macro_export]
125139
macro_rules! push_rules {
126-
($judgment_name:ident, $input_value:expr, $output:expr, $input_names:tt => $output_ty:ty, $($rule:tt)*) => {
127-
$($crate::push_rules!(@rule ($judgment_name, $input_value, $output, $input_names => $output_ty) $rule);)*
140+
($judgment_name:ident, $input_value:expr, $output:expr, $failed_rules:expr, $input_names:tt => $output_ty:ty, $($rule:tt)*) => {
141+
$($crate::push_rules!(@rule ($judgment_name, $input_value, $output, $failed_rules, $input_names => $output_ty) $rule);)*
128142
};
129143

130144
// `@rule (builder) rule` phase: invoked for each rule, emits `push_rule` call
131145

132-
(@rule ($judgment_name:ident, $input_value:expr, $output:expr, $input_names:tt => $output_ty:ty) ($($m:tt)*)) => {
146+
(@rule ($judgment_name:ident, $input_value:expr, $output:expr, $failed_rules:expr, $input_names:tt => $output_ty:ty) ($($m:tt)*)) => {
133147
$crate::push_rules!(@accum
134-
args($judgment_name, $input_value, $output, $input_names => $output_ty)
148+
args($judgment_name, $input_value, $output, $failed_rules, $input_names => $output_ty)
135149
accum()
136150
$($m)*
137151
);
@@ -141,7 +155,7 @@ macro_rules! push_rules {
141155
// pushing tokens into `conditions` until the `-----` and conclusion are found.
142156

143157
(@accum
144-
args($judgment_name:ident, $input_value:expr, $output:expr, ($($input_names:ident),*) => $output_ty:ty)
158+
args($judgment_name:ident, $input_value:expr, $output:expr, $failed_rules:expr, ($($input_names:ident),*) => $output_ty:ty)
145159
accum($($m:tt)*)
146160
---$(-)* ($n:literal)
147161
($conclusion_name:ident($($patterns:tt)*) => $v:expr)
@@ -159,7 +173,7 @@ macro_rules! push_rules {
159173
};
160174

161175
if let Some(__JudgmentStruct($($input_names),*)) = Some($input_value) {
162-
$crate::push_rules!(@match inputs($($input_names)*) patterns($($patterns)*,) args(@body ($judgment_name; $n; $v; $output); $($m)*));
176+
$crate::push_rules!(@match inputs($($input_names)*) patterns($($patterns)*,) args(@body ($judgment_name; $n; $v; $output); ($failed_rules, ($($input_names),*), $n); $($m)*));
163177
}
164178
}
165179
};
@@ -172,9 +186,10 @@ macro_rules! push_rules {
172186
// Matching phase: peel off the patterns one by one and match them against the values
173187
// extracted from the input. For anything that is not an identity pattern, invoke `downcast`.
174188

175-
(@match inputs() patterns() args(@body ($judgment_name:ident; $n:literal; $v:expr; $output:expr); $($m:tt)*)) => {
189+
(@match inputs() patterns() args(@body ($judgment_name:ident; $n:literal; $v:expr; $output:expr); ($failed_rules:expr, $inputs:tt, $rule_name:literal); $($m:tt)*)) => {
176190
tracing::trace_span!("matched rule", rule = $n, judgment = stringify!($judgment_name)).in_scope(|| {
177-
$crate::push_rules!(@body ($judgment_name, $n, $v, $output) $($m)*);
191+
let mut step_index = 0;
192+
$crate::push_rules!(@body ($judgment_name, $n, $v, $output); ($failed_rules, $inputs, $rule_name); step_index; $($m)*);
178193
});
179194
};
180195

@@ -222,47 +237,89 @@ macro_rules! push_rules {
222237
// expression `v` is carried in from the conclusion and forms the final
223238
// output of this rule, once all the conditions are evaluated.
224239

225-
(@body $args:tt (if $c:expr) $($m:tt)*) => {
240+
(@body $args:tt; $inputs:tt; $step_index:ident; (if $c:expr) $($m:tt)*) => {
226241
if $c {
227-
$crate::push_rules!(@body $args $($m)*);
242+
$step_index += 1;
243+
$crate::push_rules!(@body $args; $inputs; $step_index; $($m)*);
228244
} else {
229-
tracing::trace!("failed to match if condition {:?}", stringify!($c))
245+
$crate::push_rules!(@record_failure $inputs; $step_index; $crate::judgment::RuleFailureCause::IfFalse {
246+
expr: stringify!($c).to_string(),
247+
});
230248
}
231249
};
232250

233-
(@body $args:tt (assert $c:expr) $($m:tt)*) => {
251+
(@body $args:tt; $inputs:tt; $step_index:ident; (assert $c:expr) $($m:tt)*) => {
234252
assert!($c);
235-
$crate::push_rules!(@body $args $($m)*);
253+
$step_index += 1;
254+
$crate::push_rules!(@body $args; $inputs; $step_index; $($m)*);
236255
};
237256

238-
(@body $args:tt (if let $p:pat = $e:expr) $($m:tt)*) => {
239-
if let $p = $e {
240-
$crate::push_rules!(@body $args $($m)*);
257+
(@body $args:tt; $inputs:tt; $step_index:ident; (if let $p:pat = $e:expr) $($m:tt)*) => {
258+
let value = &$e;
259+
if let $p = Clone::clone(value) {
260+
$step_index += 1;
261+
$crate::push_rules!(@body $args; $inputs; $step_index; $($m)*);
241262
} else {
242-
tracing::trace!("failed to match pattern {:?}", stringify!($p))
263+
$crate::push_rules!(@record_failure $inputs; $step_index; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
264+
pattern: stringify!($p).to_string(),
265+
value: format!("{:?}", value),
266+
});
243267
}
244268
};
245269

246-
(@body $args:tt ($i:expr => $p:pat) $($m:tt)*) => {
270+
(@body $args:tt; $inputs:tt; $step_index:ident; ($i:expr => $p:pat) $($m:tt)*) => {
247271
// Explicitly calling `into_iter` silences some annoying lints
248272
// in the case where `$i` is an `Option` or a `Result`
249-
for $p in std::iter::IntoIterator::into_iter($i) {
250-
$crate::push_rules!(@body $args $($m)*);
273+
match $crate::judgment::TryIntoIter::try_into_iter($i, || stringify!($i).to_string()) {
274+
Ok(i) => {
275+
$step_index += 1;
276+
for $p in std::iter::IntoIterator::into_iter(i) {
277+
$crate::push_rules!(@body $args; $inputs; $step_index; $($m)*);
278+
}
279+
}
280+
Err(e) => {
281+
$crate::push_rules!(@record_failure $inputs; $step_index; e);
282+
}
251283
}
252284
};
253285

254-
(@body $args:tt (let $p:pat = $i:expr) $($m:tt)*) => {
286+
(@body $args:tt; $inputs:tt; $step_index:ident; (let $p:pat = $i:expr) $($m:tt)*) => {
255287
{
256288
let $p = $i;
257-
$crate::push_rules!(@body $args $($m)*);
289+
$step_index += 1;
290+
$crate::push_rules!(@body $args; $inputs; $step_index; $($m)*);
258291
}
259292
};
260293

261-
(@body ($judgment_name:ident, $rule_name:literal, $v:expr, $output:expr)) => {
294+
(@body ($judgment_name:ident, $rule_name:literal, $v:expr, $output:expr); $inputs:tt; $step_index:ident;) => {
262295
{
296+
let _ = $step_index; // suppress warnings about value not being read
263297
let result = $crate::Upcast::upcast($v);
264298
tracing::debug!("produced {:?} from rule {:?} in judgment {:?}", result, $rule_name, stringify!($judgment_name));
265299
$output.insert(result)
266300
}
267301
};
302+
303+
//
304+
305+
(@record_failure ($failed_rules:expr, $inputs:tt, $rule_name:literal); $step_index:ident; $cause:expr) => {
306+
tracing::trace!(
307+
"rule {rn} failed at step {s} because {cause} ({file}:{line}:{column})",
308+
rn = $rule_name,
309+
s = $step_index,
310+
cause = $cause,
311+
file = file!(),
312+
line = line!(),
313+
column = column!(),
314+
);
315+
$failed_rules.insert(
316+
$crate::judgment::FailedRule {
317+
rule_name_index: Some(($rule_name.to_string(), $step_index)),
318+
file: file!().to_string(),
319+
line: line!(),
320+
column: column!(),
321+
cause: $cause,
322+
}
323+
);
324+
}
268325
}

0 commit comments

Comments
 (0)