@@ -985,14 +985,6 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
985
985
}
986
986
}
987
987
None => {
988
- if floundered {
989
- // The strand floundered when trying to select a subgoal.
990
- // This will always return a `RootSearchFail`, either because the
991
- // root table floundered or we yield with `QuantumExceeded`.
992
- return NoRemainingSubgoalsResult :: RootSearchFail (
993
- self . on_subgoal_selection_flounder ( ) ,
994
- ) ;
995
- }
996
988
debug ! ( "answer is not available (or not new)" ) ;
997
989
998
990
// This table ned nowhere of interest
@@ -1056,47 +1048,6 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
1056
1048
Some ( Forest :: canonicalize_strand ( self . context , strand) )
1057
1049
}
1058
1050
1059
- fn on_subgoal_selection_flounder ( & mut self ) -> RootSearchFail {
1060
- debug ! ( "all subgoals floundered" ) ;
1061
-
1062
- // We were unable to select a subgoal for this strand
1063
- // because all of them had floundered or because any one
1064
- // that we dependended on negatively floundered
1065
-
1066
- loop {
1067
- // This table is marked as floundered
1068
- let table = self . stack . top ( ) . table ;
1069
- debug ! (
1070
- "Marking table {:?} as floundered! (all subgoals floundered)" ,
1071
- table
1072
- ) ;
1073
- self . forest . tables [ table] . mark_floundered ( ) ;
1074
-
1075
- let mut strand = match self . stack . pop_and_take_caller_strand ( ) {
1076
- Some ( s) => s,
1077
- None => {
1078
- // That was the root table, so we are done.
1079
- return RootSearchFail :: QuantumExceeded ;
1080
- }
1081
- } ;
1082
-
1083
- if self . propagate_floundered_subgoal ( & mut strand) {
1084
- // This strand will never lead anywhere of interest.
1085
- // Drop it and continue around the loop.
1086
- drop ( strand) ;
1087
- } else {
1088
- // We want to maybe pursue this strand later
1089
- let table = self . stack . top ( ) . table ;
1090
- let canonical_strand = Forest :: canonicalize_strand ( self . context , strand) ;
1091
- self . forest . tables [ table] . enqueue_strand ( canonical_strand) ;
1092
-
1093
- // Now we yield with `QuantumExceeded`
1094
- self . unwind_stack ( ) ;
1095
- return RootSearchFail :: QuantumExceeded ;
1096
- }
1097
- }
1098
- }
1099
-
1100
1051
fn on_no_strands_left ( & mut self ) -> Result < ( ) , RootSearchFail > {
1101
1052
debug ! ( "no more strands available (or all cycles)" ) ;
1102
1053
0 commit comments