@@ -1338,8 +1338,18 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
1338
1338
selected_subgoal : _,
1339
1339
last_pursued_time : _,
1340
1340
} = strand;
1341
+ // If there are subgoals left, they should be followed
1341
1342
assert ! ( subgoals. is_empty( ) ) ;
1343
+ // We can still try to get an ambiguous answer if there are floundered subgoals
1342
1344
let floundered = !floundered_subgoals. is_empty ( ) ;
1345
+ // So let's make sure that it *really* is an ambiguous answer (this should be set previously)
1346
+ assert ! ( !floundered || ambiguous) ;
1347
+
1348
+ // FIXME: If there are floundered subgoals, we *could* potentially
1349
+ // actually check if the partial answers to any of these subgoals
1350
+ // conflict. But this requires that we think about whether they are
1351
+ // positive or negative subgoals. This duplicates some of the logic
1352
+ // in `merge_answer_into_strand`, so a bit of refactoring is needed.
1343
1353
1344
1354
// If the answer gets too large, mark the table as floundered.
1345
1355
// This is the *most conservative* course. There are a few alternatives:
@@ -1381,14 +1391,7 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
1381
1391
constraints,
1382
1392
filtered_delayed_subgoals,
1383
1393
) ;
1384
- if floundered {
1385
- debug ! (
1386
- "answer from floundered Strand: table={:?}, subst={:?}" ,
1387
- table, subst
1388
- ) ;
1389
- } else {
1390
- debug ! ( "answer: table={:?}, subst={:?}" , table, subst) ;
1391
- }
1394
+ debug ! ( "answer: table={:?}, subst={:?}, floundered={:?}" , table, subst, floundered) ;
1392
1395
1393
1396
let answer = Answer { subst, ambiguous } ;
1394
1397
0 commit comments