Skip to content

Commit 0de138c

Browse files
nikomatsakisnikomatsakis
authored
Merge pull request #161 from nikomatsakis/upcast-arc-and-more
More usability improvements
2 parents a2d8b3d + f913710 commit 0de138c

26 files changed

+269
-83
lines changed

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

Lines changed: 38 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -70,13 +70,37 @@ impl<T: Ord + Clone> VecExt<T> for Vec<T> {
7070
}
7171

7272
pub trait SetExt<T>: Sized {
73-
fn split_first(self) -> Option<(T, Self)>;
73+
fn split_first(self) -> Option<(T, Set<T>)>;
7474

75-
fn union_with(self, other: Self) -> Self;
75+
fn union_with(self, other: impl Upcast<Set<T>>) -> Set<T>;
7676

77-
fn plus(self, other: T) -> Self;
77+
fn with_element(self, other: impl Upcast<T>) -> Set<T>;
7878

79-
fn split_nth(&self, i: usize) -> Option<(T, Self)>;
79+
fn without_element(self, other: impl Upcast<T>) -> Set<T>;
80+
81+
fn split_nth(&self, i: usize) -> Option<(T, Set<T>)>;
82+
}
83+
84+
impl<T: Ord + Clone> SetExt<T> for &Set<T> {
85+
fn split_first(self) -> Option<(T, Set<T>)> {
86+
self.clone().split_first()
87+
}
88+
89+
fn union_with(self, other: impl Upcast<Set<T>>) -> Set<T> {
90+
self.clone().union_with(other)
91+
}
92+
93+
fn with_element(self, other: impl Upcast<T>) -> Set<T> {
94+
self.clone().with_element(other)
95+
}
96+
97+
fn without_element(self, other: impl Upcast<T>) -> Set<T> {
98+
self.clone().without_element(other)
99+
}
100+
101+
fn split_nth(&self, i: usize) -> Option<(T, Set<T>)> {
102+
<Set<T>>::split_nth(self, i)
103+
}
80104
}
81105

82106
impl<T: Ord + Clone> SetExt<T> for Set<T> {
@@ -87,22 +111,28 @@ impl<T: Ord + Clone> SetExt<T> for Set<T> {
87111
Some((e, c))
88112
}
89113

90-
fn split_nth(&self, i: usize) -> Option<(T, Self)> {
114+
fn split_nth(&self, i: usize) -> Option<(T, Set<T>)> {
91115
let mut s = self.clone();
92116
let item = self.iter().skip(i).next()?;
93117
let item = s.take(item).unwrap();
94118
Some((item, s))
95119
}
96120

97-
fn union_with(mut self, other: Self) -> Self {
121+
fn union_with(mut self, other: impl Upcast<Set<T>>) -> Set<T> {
122+
let other: Set<T> = other.upcast();
98123
for item in other {
99124
self.insert(item);
100125
}
101126
self
102127
}
103128

104-
fn plus(mut self, other: T) -> Self {
105-
self.insert(other);
129+
fn with_element(mut self, other: impl Upcast<T>) -> Set<T> {
130+
self.insert(other.upcast());
131+
self
132+
}
133+
134+
fn without_element(mut self, other: impl Upcast<T>) -> Set<T> {
135+
self.remove(&other.upcast());
106136
self
107137
}
108138
}

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

Lines changed: 97 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -178,15 +178,20 @@ macro_rules! push_rules {
178178
) => {
179179
// Found the conclusion.
180180
{
181-
// give the user a type error if the name they gave
182-
// in the conclusion is not the same as the name of the
183-
// function
184-
#[allow(dead_code)]
185-
struct WrongJudgmentNameInConclusion;
186-
const _: WrongJudgmentNameInConclusion = {
187-
let $judgment_name = WrongJudgmentNameInConclusion;
181+
$crate::respan!(
188182
$conclusion_name
189-
};
183+
(
184+
// give the user a type error if the name they gave
185+
// in the conclusion is not the same as the name of the
186+
// function
187+
#[allow(dead_code)]
188+
struct WrongJudgmentNameInConclusion;
189+
const _: WrongJudgmentNameInConclusion = {
190+
let $judgment_name = WrongJudgmentNameInConclusion;
191+
$conclusion_name
192+
};
193+
)
194+
);
190195

191196
if let Some(__JudgmentStruct($($input_names),*)) = Some($input_value) {
192197
$crate::push_rules!(@match
@@ -283,33 +288,104 @@ macro_rules! push_rules {
283288
// expression `v` is carried in from the conclusion and forms the final
284289
// output of this rule, once all the conditions are evaluated.
285290

286-
(@body $args:tt; $inputs:tt; $step_index:expr; (if $c:expr) $($m:tt)*) => {
287-
if $c {
291+
(@body $args:tt; $inputs:tt; $step_index:expr; (if let $p:pat = $e:expr) $($m:tt)*) => {
292+
let value = &$e;
293+
if let $p = Clone::clone(value) {
288294
$crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
289295
} else {
290-
$crate::push_rules!(@record_failure $inputs; $step_index, $c; $crate::judgment::RuleFailureCause::IfFalse {
291-
expr: stringify!($c).to_string(),
296+
$crate::push_rules!(@record_failure $inputs; $step_index, $e; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
297+
pattern: stringify!($p).to_string(),
298+
value: format!("{:?}", value),
292299
});
293300
}
294301
};
295302

296-
(@body $args:tt; $inputs:tt; $step_index:expr; (assert $c:expr) $($m:tt)*) => {
297-
assert!($c);
298-
$crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
303+
// For `(if ...)`, we have special treatment to try and extract the arguments so we can give better information
304+
// about why the expression evaluated to false.
305+
(@body $args:tt; $inputs:tt; $step_index:expr; (if $($c:tt)*) $($m:tt)*) => {
306+
$crate::push_rules!(@body_if $args; $inputs; $step_index; $($c)*; $($c)*; $($m)*)
299307
};
300308

301-
(@body $args:tt; $inputs:tt; $step_index:expr; (if let $p:pat = $e:expr) $($m:tt)*) => {
302-
let value = &$e;
303-
if let $p = Clone::clone(value) {
309+
(@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( ); $origcond:expr; $($m:tt)*) => {
310+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); arg0.$method(); $origcond; $($m)*)
311+
};
312+
313+
(@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( ); $origcond:expr; $($m:tt)*) => {
314+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); !arg0.$method(); $origcond; $($m)*)
315+
};
316+
317+
(@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
318+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0.$method(arg1); $origcond; $($m)*)
319+
};
320+
321+
(@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
322+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); !arg0.$method(arg1); $origcond; $($m)*)
323+
};
324+
325+
(@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident . $method:ident ( $arg1:expr, $arg2:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
326+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1, arg2 = $arg2); arg0.$method(arg1, arg2); $origcond; $($m)*)
327+
};
328+
329+
(@body_if $args:tt; $inputs:tt; $step_index:expr; ! $arg0:ident . $method:ident ( $arg1:expr, $arg2:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
330+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1, arg2 = $arg2); !arg0.$method(arg1, arg2); $origcond; $($m)*)
331+
};
332+
333+
(@body_if $args:tt; $inputs:tt; $step_index:expr; $func:ident ( $arg0:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
334+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); $func(arg0); $origcond; $($m)*)
335+
};
336+
337+
(@body_if $args:tt; $inputs:tt; $step_index:expr; ! $func:ident ( $arg0:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
338+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0); !$func(arg0); $origcond; $($m)*)
339+
};
340+
341+
(@body_if $args:tt; $inputs:tt; $step_index:expr; $func:ident ( $arg0:expr, $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
342+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); $func(arg0, arg1); $origcond; $($m)*)
343+
};
344+
345+
(@body_if $args:tt; $inputs:tt; $step_index:expr; ! $func:ident ( $arg0:expr, $arg1:expr $(,)? ); $origcond:expr; $($m:tt)*) => {
346+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); ! $func(arg0, arg1); $origcond; $($m)*)
347+
};
348+
349+
(@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident == $arg1:ident; $origcond:expr; $($m:tt)*) => {
350+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0 == arg1; $origcond; $($m)*)
351+
};
352+
353+
(@body_if $args:tt; $inputs:tt; $step_index:expr; $arg0:ident != $arg1:ident; $origcond:expr; $($m:tt)*) => {
354+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (arg0 = $arg0, arg1 = $arg1); arg0 != arg1; $origcond; $($m)*)
355+
};
356+
357+
(@body_if $args:tt; $inputs:tt; $step_index:expr; $e:expr; $origcond:expr; $($m:tt)*) => {
358+
$crate::push_rules!(@structured_if $args; $inputs; $step_index; (); $e; $origcond; $($m)*)
359+
};
360+
361+
(@structured_if $args:tt; $inputs:tt; $step_index:expr; ($($argn:ident = $arge:expr),*); $cond:expr; $origcond:expr; $($m:tt)*) => {
362+
$(
363+
let $argn = &$arge;
364+
)*
365+
if {
366+
$(
367+
let $argn = Clone::clone($argn);
368+
)*
369+
$cond
370+
} {
304371
$crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
305372
} else {
306-
$crate::push_rules!(@record_failure $inputs; $step_index, $e; $crate::judgment::RuleFailureCause::IfLetDidNotMatch {
307-
pattern: stringify!($p).to_string(),
308-
value: format!("{:?}", value),
373+
$crate::push_rules!(@record_failure $inputs; $step_index, $origcond; $crate::judgment::RuleFailureCause::IfFalse {
374+
expr: stringify!($origcond).to_string(),
375+
args: vec![
376+
$(
377+
(stringify!($arge).to_string(), format!("{:?}", $argn)),
378+
)*
379+
],
309380
});
310381
}
311382
};
312383

384+
(@body $args:tt; $inputs:tt; $step_index:expr; (assert $c:expr) $($m:tt)*) => {
385+
assert!($c);
386+
$crate::push_rules!(@body $args; $inputs; $step_index + 1; $($m)*);
387+
};
388+
313389
(@body $args:tt; $inputs:tt; $step_index:expr; ($i:expr => $p:pat) $($m:tt)*) => {
314390
// Explicitly calling `into_iter` silences some annoying lints
315391
// in the case where `$i` is an `Option` or a `Result`

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

Lines changed: 27 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
use crate::{set, Set, SetExt};
1+
use crate::{set, Set};
22
use std::{
33
fmt::Debug,
44
hash::{Hash, Hasher},
@@ -316,11 +316,12 @@ impl FailedJudgment {
316316
// This will return a boolean indicating if all the failed rules
317317
// ultimately failed because of a cycle.
318318

319+
let mut stack1 = stack.clone();
320+
stack1.insert(&judgment.judgment);
321+
319322
let judgment_has_non_cycle;
320-
(judgment.failed_rules, judgment_has_non_cycle) = Self::strip_cycles(
321-
stack.clone().plus(&judgment.judgment),
322-
judgment.failed_rules,
323-
);
323+
(judgment.failed_rules, judgment_has_non_cycle) =
324+
Self::strip_cycles(stack1, judgment.failed_rules);
324325
failed_rule.cause = RuleFailureCause::FailedJudgment(judgment);
325326

326327
if judgment_has_non_cycle.0 {
@@ -384,7 +385,14 @@ impl FailedRule {
384385
#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug)]
385386
pub enum RuleFailureCause {
386387
/// The rule did not succeed because an `(if X)` condition evaluated to false.
387-
IfFalse { expr: String },
388+
IfFalse {
389+
/// The stringified form of the expression.
390+
expr: String,
391+
392+
/// A set of pairs with the stringified form of arguments within the expression plus the debug representation of its value.
393+
/// This is a best effort extraction via the macro.
394+
args: Vec<(String, String)>,
395+
},
388396

389397
/// The rule did not succeed because an `(if let)` pattern failed to match.
390398
IfLetDidNotMatch { pattern: String, value: String },
@@ -426,8 +434,8 @@ impl std::fmt::Display for FailedJudgment {
426434
if failed_rules.is_empty() {
427435
write!(f, "judgment had no applicable rules: `{judgment}` ",)
428436
} else {
429-
let rules: String = failed_rules.iter().map(|r| r.to_string()).collect();
430-
let rules = indent(rules);
437+
let rules: Vec<String> = failed_rules.iter().map(|r| r.to_string()).collect();
438+
let rules = indent(rules.join("\n"));
431439
write!(
432440
f,
433441
"judgment `{judgment}` failed at the following rule(s):\n{rules}"
@@ -465,8 +473,12 @@ impl std::fmt::Display for FailedRule {
465473
impl std::fmt::Display for RuleFailureCause {
466474
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
467475
match self {
468-
RuleFailureCause::IfFalse { expr } => {
469-
write!(f, "condition evaluted to false: `{expr}`")
476+
RuleFailureCause::IfFalse { expr, args } => {
477+
write!(f, "condition evaluted to false: `{expr}`")?;
478+
for (arg_expr, arg_value) in args {
479+
write!(f, "\n {arg_expr} = {arg_value}")?;
480+
}
481+
Ok(())
470482
}
471483
RuleFailureCause::IfLetDidNotMatch { pattern, value } => {
472484
write!(f, "pattern `{pattern}` did not match value `{value}`")
@@ -492,7 +504,7 @@ impl<T: Debug> std::fmt::Display for ProvenSet<T> {
492504
Data::Success(set) => {
493505
write!(f, "{{\n")?;
494506
for item in set {
495-
write!(f, "{}", indent(format!("{item:?},\n")))?;
507+
write!(f, "{},\n", indent(format!("{item:?}")))?;
496508
}
497509
write!(f, "}}\n")?;
498510
Ok(())
@@ -503,14 +515,12 @@ impl<T: Debug> std::fmt::Display for ProvenSet<T> {
503515

504516
fn indent(s: impl std::fmt::Display) -> String {
505517
let s = s.to_string();
506-
s.lines()
518+
let lines: Vec<String> = s
519+
.lines()
507520
.map(|l| format!(" {l}"))
508521
.map(|l| l.trim_end().to_string())
509-
.map(|mut l| {
510-
l.push_str("\n");
511-
l
512-
})
513-
.collect()
522+
.collect();
523+
lines.join("\n")
514524
}
515525

516526
/// This trait is used for the `(foo => bar)` patterns.

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -51,8 +51,7 @@ fn judgment() {
5151
transitive_reachable(&graph, 0).assert_err(expect_test::expect![[r#"
5252
judgment `transitive_reachable { node: 0, g: Graph { edges: [(0, 1), (1, 2), (2, 4), (2, 3), (3, 6), (4, 8), (8, 10)] } }` failed at the following rule(s):
5353
the rule "base" failed at step #1 (src/file.rs:LL:CC) because
54-
condition evaluted to false: `b % 2 == 0`
55-
"#]]);
54+
condition evaluted to false: `b % 2 == 0`"#]]);
5655

5756
transitive_reachable(&graph, 2).assert_ok(expect_test::expect![[r#"
5857
{

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,7 @@ where
6060
T: Debug,
6161
E: Debug,
6262
{
63+
#[track_caller]
6364
fn assert_ok(self, expect: expect_test::Expect) {
6465
match self {
6566
Ok(v) => {
@@ -71,11 +72,12 @@ where
7172
}
7273
}
7374

75+
#[track_caller]
7476
fn assert_err(self, expect: expect_test::Expect) {
7577
match self {
7678
Ok(v) => panic!("expected `Err`, got `Ok`: {v:?}"),
7779
Err(e) => {
78-
expect.assert_eq(&format!("{e:?}"));
80+
expect.assert_eq(&normalize_paths(format!("{e:?}")));
7981
}
8082
}
8183
}

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,5 @@ fn not_well_formed_adt() {
6363
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
6464
judgment `prove_wc { goal: Foo(u64), assumptions: {}, env: Env { variables: [], coherence_mode: false }, decls: decls(222, [trait Foo <ty> ], [impl Foo(u32)], [], [], [], [adt X <ty> where {Foo(^ty0_0)}], {}, {}) }` failed at the following rule(s):
6565
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
66-
expression evaluated to an empty collection: `decls.trait_invariants()`
67-
"#]]);
66+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]);
6867
}

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -192,8 +192,7 @@ fn test_normalize_assoc_ty_existential0() {
192192
the rule "existential-universal" failed at step #0 (src/file.rs:LL:CC) because
193193
condition evaluted to false: `env.universe(p) < env.universe(v)`
194194
the rule "normalize-via-impl" failed at step #0 (src/file.rs:LL:CC) because
195-
expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`
196-
"#]]);
195+
expression evaluated to an empty collection: `decls.alias_eq_decls(&a.name)`"#]]);
197196
}
198197

199198
#[test]

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,8 +54,7 @@ fn not_partial_eq_implies_eq() {
5454
the rule "assumption" failed at step #1 (src/file.rs:LL:CC) because
5555
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(!ty_1), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
5656
the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because
57-
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
58-
"#]]);
57+
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {PartialEq(!ty_1)}, env: Env { variables: [!ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
5958
}
6059

6160
#[test]
@@ -102,6 +101,5 @@ fn universals_not_eq() {
102101
the rule "symmetric" failed at step #0 (src/file.rs:LL:CC) because
103102
cyclic proof attempt: `prove_eq { a: !ty_0, b: !ty_1, assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
104103
the rule "trait implied bound" failed at step #3 (src/file.rs:LL:CC) because
105-
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`
106-
"#]]);
104+
judgment had no applicable rules: `prove_via { goal: Eq(!ty_1), via: PartialEq(?ty_2), assumptions: {Eq(!ty_0)}, env: Env { variables: [!ty_0, !ty_1, ?ty_2], coherence_mode: false }, decls: decls(222, [trait Eq <ty> where {PartialEq(^ty0_0)}, trait PartialEq <ty> ], [], [], [], [], [], {}, {}) }`"#]]);
107105
}

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,8 @@ fn test_forall_not_local() {
2222
judgment `is_local_trait_ref { goal: Debug(!ty_1), assumptions: {}, env: Env { variables: [!ty_1], coherence_mode: true }, decls: decls(222, [], [], [], [], [], [], {}, {}) }` failed at the following rule(s):
2323
the rule "local trait" failed at step #0 (src/file.rs:LL:CC) because
2424
condition evaluted to false: `decls.is_local_trait_id(&goal.trait_id)`
25-
"#]]);
25+
decls = decls(222, [], [], [], [], [], [], {}, {})
26+
&goal.trait_id = Debug"#]]);
2627
}
2728

2829
#[test]

0 commit comments

Comments
 (0)