Skip to content

Commit fcf3935

Browse files
nikomatsakisnikomatsakis
committed
add ability to define match commit point
use this to filter out the transitive rule unless there is at least one base case
1 parent b520dc0 commit fcf3935

File tree

3 files changed

+115
-74
lines changed

3 files changed

+115
-74
lines changed

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

Lines changed: 113 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,40 @@ mod test_reachable;
1010

1111
pub type JudgmentStack<J, O> = RefCell<FixedPointStack<J, Set<O>>>;
1212

13+
/// `judgment_fn!` allows construction of inference rules using a more logic-like notation.
14+
///
15+
/// The macro input looks like so:
16+
///
17+
/// ```ignore
18+
/// (
19+
/// ( /* condition 1 */) // each condition is a parenthesized group
20+
/// ( /* condition 2 */)
21+
/// ( /* condition 3 */)! // `!` is optional and indicates match commit point, see below
22+
/// -------------------- // 3 or more `-` separate the condition from the conclusion
23+
/// ( /* conclusion */) // as is the conclusion
24+
/// )
25+
/// ```
26+
///
27+
/// The conditions can be the following
28+
///
29+
/// * `(<expr> => <binding>)` -- used to apply judgments, but really `<expr>` can be anything with an `into_iter` method.
30+
/// * `(if <expr>)`
31+
/// * `(if let <pat> = <expr>)`
32+
/// * `(let <binding> = <expr>)`
33+
///
34+
/// The conclusions can be the following
35+
///
36+
/// * `(<pat> => <binding>)
37+
///
38+
/// ## Failure reporting and match commit points
39+
///
40+
/// When we fail to prove a judgment, we'll produce a failure that includes
41+
/// all rules that partially matched. By default this lits includes every
42+
/// rule that matches the patterns in its conclusion.
43+
/// Sometimes this is annoyingly verbose.
44+
/// You can place a `!` after a condition to mark it as a "match commit point".
45+
/// Rules that fail before reaching the match commit point will not be included
46+
/// in the failure result.
1347
#[macro_export]
1448
macro_rules! judgment_fn {
1549
(
@@ -111,30 +145,6 @@ macro_rules! judgment_fn {
111145
}
112146
}
113147

114-
/// push_rules! allows construction of inference rules using a more logic-like notation.
115-
///
116-
/// The macro input looks like: `push_rules!(builder, (...) (...) (...))` where each
117-
/// parenthesized group `(...)` is an inference rule. Inference rules are written like so:
118-
///
119-
/// ```ignore
120-
/// (
121-
/// ( /* condition 1 */) // each condition is a parenthesized group
122-
/// ( /* condition 2 */)
123-
/// -------------------- // 3 or more `-` separate the condition from the conclusion
124-
/// ( /* conclusion */) // as is the conclusion
125-
/// )
126-
/// ```
127-
///
128-
/// The conditions can be the following
129-
///
130-
/// * `(<expr> => <binding>)` -- used to apply judgments, but really `<expr>` can be anything with an `into_iter` method.
131-
/// * `(if <expr>)`
132-
/// * `(if let <pat> = <expr>)`
133-
/// * `(let <binding> = <expr>)`
134-
///
135-
/// The conclusions can be the following
136-
///
137-
/// * `(<pat> => <binding>)
138148
#[macro_export]
139149
macro_rules! push_rules {
140150
($judgment_name:ident, $input_value:expr, $output:expr, $failed_rules:expr, $input_names:tt => $output_ty:ty, $($rule:tt)*) => {
@@ -144,21 +154,27 @@ macro_rules! push_rules {
144154
// `@rule (builder) rule` phase: invoked for each rule, emits `push_rule` call
145155

146156
(@rule ($judgment_name:ident, $input_value:expr, $output:expr, $failed_rules:expr, $input_names:tt => $output_ty:ty) ($($m:tt)*)) => {
157+
// Start accumulating.
147158
$crate::push_rules!(@accum
148159
args($judgment_name, $input_value, $output, $failed_rules, $input_names => $output_ty)
149-
accum()
150-
$($m)*
160+
accum((1-1); 0;)
161+
input($($m)*)
151162
);
152163
};
153164

154-
// `@accum (conditions)` phase: accumulates the contents of a given rule,
165+
// `@accum ($match_index; $current_index; conditions)` phase: accumulates the contents of a given rule,
155166
// pushing tokens into `conditions` until the `-----` and conclusion are found.
167+
//
168+
// The `$match_index` stores the location where `!` was found. It is expected to start
169+
// at 0. The `current_index` is also expected to start as the expression `0`.
156170

157171
(@accum
158172
args($judgment_name:ident, $input_value:expr, $output:expr, $failed_rules:expr, ($($input_names:ident),*) => $output_ty:ty)
159-
accum($($m:tt)*)
160-
---$(-)* ($n:literal)
161-
($conclusion_name:ident($($patterns:tt)*) => $v:expr)
173+
accum($match_index:expr; $current_index:expr; $($m:tt)*)
174+
input(
175+
---$(-)* ($n:literal)
176+
($conclusion_name:ident($($patterns:tt)*) => $v:expr)
177+
)
162178
) => {
163179
// Found the conclusion.
164180
{
@@ -173,23 +189,53 @@ macro_rules! push_rules {
173189
};
174190

175191
if let Some(__JudgmentStruct($($input_names),*)) = Some($input_value) {
176-
$crate::push_rules!(@match inputs($($input_names)*) patterns($($patterns)*,) args(@body ($judgment_name; $n; $v; $output); ($failed_rules, ($($input_names),*), $n); $($m)*));
192+
$crate::push_rules!(@match
193+
inputs($($input_names)*)
194+
patterns($($patterns)*,)
195+
args(@body
196+
($judgment_name; $n; $v; $output);
197+
($failed_rules, $match_index, ($($input_names),*), $n);
198+
$($m)*
199+
)
200+
);
177201
}
178202
}
179203
};
180204

181-
(@accum args $args:tt accum($($m:tt)*) ($($n:tt)*) $($o:tt)*) => {
182-
// Push the condition into the list `$m`.
183-
$crate::push_rules!(@accum args $args accum($($m)* ($($n)*)) $($o)*)
205+
(@accum
206+
args $args:tt
207+
accum($match_index:expr; $current_index:expr; $($m:tt)*)
208+
input(! $($o:tt)*)
209+
) => {
210+
// If we see a `!` in the list, that represents a "match commit point".
211+
// Overwrite `$match_index` with `$current_index` and proceed.
212+
$crate::push_rules!(@accum
213+
args $args
214+
accum($current_index; $current_index; $($m)*)
215+
input($($o)*)
216+
)
217+
};
218+
219+
(@accum
220+
args $args:tt
221+
accum($match_index:expr; $current_index:expr; $($m:tt)*)
222+
input(($($n:tt)*) $($o:tt)*)
223+
) => {
224+
// Move one parenthesized condition `($n*)` onto the list after `$m`.
225+
$crate::push_rules!(@accum
226+
args $args
227+
accum($match_index; $current_index+1; $($m)* ($($n)*))
228+
input($($o)*)
229+
)
184230
};
185231

186232
// Matching phase: peel off the patterns one by one and match them against the values
187233
// extracted from the input. For anything that is not an identity pattern, invoke `downcast`.
188234

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)*)) => {
235+
(@match inputs() patterns() args(@body ($judgment_name:ident; $n:literal; $v:expr; $output:expr); $inputs:tt; $($m:tt)*)) => {
190236
tracing::trace_span!("matched rule", rule = $n, judgment = stringify!($judgment_name)).in_scope(|| {
191237
let mut step_index = 0;
192-
$crate::push_rules!(@body ($judgment_name, $n, $v, $output); ($failed_rules, $inputs, $rule_name); step_index; $($m)*);
238+
$crate::push_rules!(@body ($judgment_name, $n, $v, $output); $inputs; step_index; $($m)*);
193239
});
194240
};
195241

@@ -302,24 +348,36 @@ macro_rules! push_rules {
302348

303349
//
304350

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-
);
351+
(@record_failure ($failed_rules:expr, $match_index:expr, $inputs:tt, $rule_name:literal); $step_index:ident; $cause:expr) => {
352+
if $step_index >= $match_index {
353+
tracing::debug!(
354+
"rule {rn} failed at step {s} because {cause} ({file}:{line}:{column})",
355+
rn = $rule_name,
356+
s = $step_index,
357+
cause = $cause,
358+
file = file!(),
359+
line = line!(),
360+
column = column!(),
361+
);
362+
$failed_rules.insert(
363+
$crate::judgment::FailedRule {
364+
rule_name_index: Some(($rule_name.to_string(), $step_index)),
365+
file: file!().to_string(),
366+
line: line!(),
367+
column: column!(),
368+
cause: $cause,
369+
}
370+
);
371+
} else {
372+
tracing::trace!(
373+
"rule {rn} failed at step {s} because {cause} ({file}:{line}:{column})",
374+
rn = $rule_name,
375+
s = $step_index,
376+
cause = $cause,
377+
file = file!(),
378+
line = line!(),
379+
column = column!(),
380+
);
381+
}
324382
}
325383
}

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

Lines changed: 1 addition & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ judgment_fn!(
3333
)
3434

3535
(
36-
(transitive_reachable(&graph, a) => b)
36+
(transitive_reachable(&graph, a) => b)!
3737
(transitive_reachable(&graph, b) => c)
3838
(if c % 2 == 0)
3939
--------------------------------------- ("transitive")
@@ -66,23 +66,6 @@ fn judgment() {
6666
expr: "b % 2 == 0",
6767
},
6868
},
69-
FailedRule {
70-
rule_name_index: Some(
71-
(
72-
"transitive",
73-
0,
74-
),
75-
),
76-
file: "crates/formality-core/src/judgment/test_filtered.rs",
77-
line: 24,
78-
column: 1,
79-
cause: FailedJudgment(
80-
FailedJudgment {
81-
judgment: "transitive_reachable { node: 0, g: Graph { edges: [(0, 1), (1, 2), (2, 4), (2, 3), (3, 6), (4, 8), (8, 10)] } }",
82-
failed_rules: {},
83-
},
84-
),
85-
},
8669
},
8770
}
8871
"#]]

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ judgment_fn! {
3434
)
3535

3636
(
37-
(transitive_reachable(&graph, a) => b)
37+
(transitive_reachable(&graph, a) => b)!
3838
(transitive_reachable(&graph, b) => c)
3939
--------------------------------------- ("transitive")
4040
(transitive_reachable(graph, a) => c)

0 commit comments

Comments
 (0)