Skip to content

Commit 5768375

Browse files
nikomatsakisflodiebold
authored andcommitted
ensure all tests run for recursive solve
1 parent 8fcad2f commit 5768375

File tree

2 files changed

+28
-7
lines changed

2 files changed

+28
-7
lines changed

tests/test/coinduction.rs

Lines changed: 24 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -210,7 +210,15 @@ fn coinductive_unsound1() {
210210

211211
goal {
212212
forall<X> { X: C1orC2 }
213-
} yields_all[SolverChoice::slg(3, None)] {
213+
} yields[SolverChoice::slg(3, None)] {
214+
"No possible solution"
215+
}
216+
217+
goal {
218+
forall<X> { X: C1orC2 }
219+
} yields[SolverChoice::recursive()] {
220+
// FIXME -- recursive solver doesn't handle coinduction correctly
221+
"Unique; substitution [], lifetime constraints []"
214222
}
215223
}
216224
}
@@ -251,7 +259,8 @@ fn coinductive_unsound2() {
251259

252260
goal {
253261
forall<X> { X: C1orC2 }
254-
} yields_all[SolverChoice::slg(3, None)] {
262+
} yields {
263+
"No possible solution"
255264
}
256265
}
257266
}
@@ -298,8 +307,8 @@ fn coinductive_multicycle1() {
298307

299308
goal {
300309
forall<X> { X: Any }
301-
} yields_all[SolverChoice::slg(3, None)] {
302-
"substitution [], lifetime constraints []"
310+
} yields {
311+
"Unique; substitution [], lifetime constraints []"
303312
}
304313
}
305314
}
@@ -338,8 +347,8 @@ fn coinductive_multicycle2() {
338347

339348
goal {
340349
forall<X> { X: Any }
341-
} yields_all[SolverChoice::slg(3, None)] {
342-
"substitution [], lifetime constraints []"
350+
} yields {
351+
"Unique; substitution [], lifetime constraints []"
343352
}
344353
}
345354
}
@@ -388,7 +397,8 @@ fn coinductive_multicycle3() {
388397

389398
goal {
390399
forall<X> { X: Any }
391-
} yields_all[SolverChoice::slg(3, None)] {
400+
} yields {
401+
"No possible solution"
392402
}
393403
}
394404
}
@@ -439,5 +449,12 @@ fn coinductive_multicycle4() {
439449
forall<X> { X: Any }
440450
} yields_all[SolverChoice::slg(3, None)] {
441451
}
452+
453+
goal {
454+
forall<X> { X: Any }
455+
} yields[SolverChoice::recursive()] {
456+
// FIXME -- recursive solver doesn't have coinduction correctly
457+
"Unique; substitution [], lifetime constraints []"
458+
}
442459
}
443460
}

tests/test/misc.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,8 @@ fn only_draw_so_many() {
129129
exists<T> { T: Sized }
130130
} yields[SolverChoice::slg(10, Some(2))] {
131131
"Ambiguous; no inference guidance"
132+
} yields[SolverChoice::recursive()] {
133+
"Ambiguous; no inference guidance"
132134
}
133135
}
134136
}
@@ -155,6 +157,8 @@ fn only_draw_so_many_blow_up() {
155157
exists<T> { T: Foo }
156158
} yields[SolverChoice::slg(10, Some(2))] {
157159
"Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"
160+
} yields[SolverChoice::recursive()] {
161+
"Ambiguous; definite substitution for<?U0> { [?0 := Vec<^0.0>] }"
158162
}
159163
}
160164
}

0 commit comments

Comments
 (0)