Skip to content

Commit 056cda2

Browse files
matthewwmattheww
committed
Update expected test output following prove_wc() changes
The missing_dependent_where_clause test now passes
1 parent 7adc59d commit 056cda2

File tree

2 files changed

+41
-17
lines changed

2 files changed

+41
-17
lines changed

‎src/test/mod.rs

Lines changed: 20 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -52,14 +52,16 @@ fn hello_world_fail() {
5252
judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Bar(!ty_0, !ty_1))}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
5353
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
5454
judgment `prove_wc { goal: @ WellFormedTraitRef(Bar(!ty_0, !ty_1)), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
55-
the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because
56-
judgment `prove { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty, ty> where {Bar(^ty0_1, ^ty0_0)}, trait Bar <ty, ty> where {Baz(^ty0_1)}, trait Baz <ty> ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s):
57-
failed at (src/file.rs:LL:CC) because
58-
judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
59-
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
60-
judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
61-
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
62-
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
55+
the rule "trait well formed" failed at step #3 (src/file.rs:LL:CC) because
56+
judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)} }` failed at the following rule(s):
57+
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
58+
judgment `prove { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness }, decls: decls(222, [trait Foo <ty, ty> where {Bar(^ty0_1, ^ty0_0)}, trait Bar <ty, ty> where {Baz(^ty0_1)}, trait Baz <ty> ], [], [], [], [], [], {Bar, Baz, Foo}, {}) }` failed at the following rule(s):
59+
failed at (src/file.rs:LL:CC) because
60+
judgment `prove_wc_list { goal: {Baz(!ty_1)}, assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
61+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
62+
judgment `prove_wc { goal: Baz(!ty_1), assumptions: {Bar(!ty_0, !ty_1)}, env: Env { variables: [!ty_1, !ty_0], bias: Soundness } }` failed at the following rule(s):
63+
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
64+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
6365
)
6466
}
6567

@@ -133,14 +135,16 @@ fn basic_where_clauses_fail() {
133135
judgment `prove_wc { goal: for <ty> @ WellFormedTraitRef(A(u32, ^ty0_0)), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [], bias: Soundness } }` failed at the following rule(s):
134136
the rule "forall" failed at step #2 (src/file.rs:LL:CC) because
135137
judgment `prove_wc { goal: @ WellFormedTraitRef(A(u32, !ty_1)), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_1], bias: Soundness } }` failed at the following rule(s):
136-
the rule "trait well formed" failed at step #2 (src/file.rs:LL:CC) because
137-
judgment `prove { goal: {B(!ty_0)}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s):
138-
failed at (src/file.rs:LL:CC) because
139-
judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
140-
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
141-
judgment `prove_wc { goal: B(!ty_0), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
142-
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
143-
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
138+
the rule "trait well formed" failed at step #3 (src/file.rs:LL:CC) because
139+
judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_1], bias: Soundness }, known_true: true, substitution: {} }, goal: {B(!ty_1)}, assumptions: {for <ty> A(u32, ^ty0_0)} }` failed at the following rule(s):
140+
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
141+
judgment `prove { goal: {B(!ty_0)}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait A <ty, ty> where {B(^ty0_1)}, trait B <ty> , trait WellFormed <ty> where {for <ty> A(u32, ^ty0_0)}], [], [], [], [], [], {A, B, WellFormed}, {}) }` failed at the following rule(s):
142+
failed at (src/file.rs:LL:CC) because
143+
judgment `prove_wc_list { goal: {B(!ty_0)}, assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
144+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
145+
judgment `prove_wc { goal: B(!ty_0), assumptions: {for <ty> A(u32, ^ty0_0)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
146+
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
147+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
144148
)
145149
}
146150

‎src/test/well_formed_trait_ref.rs

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,26 @@ fn missing_dependent_where_clause() {
4545

4646
[ /* TODO */ ]
4747

48-
expect_test::expect![[r#"..."#]]
48+
expect_test::expect![[r#"
49+
prove_where_clauses_well_formed([S1<!ty_1> : Trait2])
50+
51+
Caused by:
52+
judgment `prove { goal: {@ WellFormedTraitRef(Trait2(S1<!ty_0>))}, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Trait1 <ty> , trait Trait2 <ty> ], [], [], [], [], [adt S1 <ty> where {Trait1(^ty0_0)}, adt S2 <ty> where {Trait2(S1<^ty0_0>)}], {Trait1, Trait2}, {S1, S2}) }` failed at the following rule(s):
53+
failed at (src/file.rs:LL:CC) because
54+
judgment `prove_wc_list { goal: {@ WellFormedTraitRef(Trait2(S1<!ty_0>))}, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
55+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
56+
judgment `prove_wc { goal: @ WellFormedTraitRef(Trait2(S1<!ty_0>)), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
57+
the rule "trait well formed" failed at step #0 (src/file.rs:LL:CC) because
58+
judgment `prove_wf { goal: S1<!ty_0>, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
59+
the rule "ADT" failed at step #3 (src/file.rs:LL:CC) because
60+
judgment `prove_after { constraints: Constraints { env: Env { variables: [!ty_0], bias: Soundness }, known_true: true, substitution: {} }, goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1<!ty_0>)} }` failed at the following rule(s):
61+
the rule "prove_after" failed at step #1 (src/file.rs:LL:CC) because
62+
judgment `prove { goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness }, decls: decls(222, [trait Trait1 <ty> , trait Trait2 <ty> ], [], [], [], [], [adt S1 <ty> where {Trait1(^ty0_0)}, adt S2 <ty> where {Trait2(S1<^ty0_0>)}], {Trait1, Trait2}, {S1, S2}) }` failed at the following rule(s):
63+
failed at (src/file.rs:LL:CC) because
64+
judgment `prove_wc_list { goal: {Trait1(!ty_0)}, assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
65+
the rule "some" failed at step #0 (src/file.rs:LL:CC) because
66+
judgment `prove_wc { goal: Trait1(!ty_0), assumptions: {Trait2(S1<!ty_0>)}, env: Env { variables: [!ty_0], bias: Soundness } }` failed at the following rule(s):
67+
the rule "trait implied bound" failed at step #0 (src/file.rs:LL:CC) because
68+
expression evaluated to an empty collection: `decls.trait_invariants()`"#]]
4969
)
5070
}

0 commit comments

Comments
 (0)