simplify SubGoalSelection variants

Author: adamrk

chalk-engine/src/logic.rs

@@ -53,12 +53,9 @@ enum SubGoalSelection {
     /// coinductive, or create a cycle.
     Selected,
 
-    /// This strand has no remaining subgoals.
-    NoRemainingSubgoals,
-
-    /// This strand has floundered. Either all the positive subgoals
-    /// have floundered or a single negative subgoal has floundered.
-    Floundered,
+    /// This strand has no remaining subgoals, but there may still be
+    /// floundered subgoals.
+    NotSelected,
 }
 
 /// This is returned `on_no_remaining_subgoals`
@@ -506,12 +503,8 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
                             self.on_subgoal_selected(strand)?;
                             continue;
                         }
-                        selection @ SubGoalSelection::NoRemainingSubgoals
-                        | selection @ SubGoalSelection::Floundered => {
-                            match self.on_no_remaining_subgoals(
-                                strand,
-                                selection == SubGoalSelection::Floundered,
-                            ) {
+                        SubGoalSelection::NotSelected => {
+                            match self.on_no_remaining_subgoals(strand) {
                                 NoRemainingSubgoalsResult::RootAnswerAvailable => return Ok(()),
                                 NoRemainingSubgoalsResult::RootSearchFail(e) => return Err(e),
                                 NoRemainingSubgoalsResult::Success => {}
@@ -895,11 +888,8 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
         Ok(())
     }
 
-    fn on_no_remaining_subgoals(
-        &mut self,
-        strand: Strand<I, C>,
-        floundered: bool,
-    ) -> NoRemainingSubgoalsResult {
+    fn on_no_remaining_subgoals(&mut self, strand: Strand<I, C>) -> NoRemainingSubgoalsResult {
+        let floundered = strand.ex_clause.floundered_subgoals.len() > 0;
         let possible_answer = if !floundered {
             debug!("no remaining subgoals for the table");
             self.pursue_answer(strand)
@@ -1231,14 +1221,14 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
             while strand.selected_subgoal.is_none() {
                 if strand.ex_clause.subgoals.len() == 0 {
                     if strand.ex_clause.floundered_subgoals.is_empty() {
-                        return SubGoalSelection::NoRemainingSubgoals;
+                        return SubGoalSelection::NotSelected;
                     }
 
                     self.reconsider_floundered_subgoals(&mut strand.ex_clause);
 
                     if strand.ex_clause.subgoals.is_empty() {
                         assert!(!strand.ex_clause.floundered_subgoals.is_empty());
-                        return SubGoalSelection::Floundered;
+                        return SubGoalSelection::NotSelected;
                     }
 
                     continue;
@@ -1274,7 +1264,7 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
             if self.forest.tables[selected_subgoal_table].is_floundered() {
                 if self.propagate_floundered_subgoal(strand) {
                     // This strand will never lead anywhere of interest.
-                    return SubGoalSelection::Floundered;
+                    return SubGoalSelection::NotSelected;
                 } else {
                     // This subgoal has floundered and has been marked.
                     // We previously would immediately mark the table as
@@ -1329,7 +1319,7 @@ impl<'forest, I: Interner, C: Context<I> + 'forest, CO: ContextOps<I, C> + 'fore
         let is_trivial_answer = self
             .context
             .is_trivial_substitution(&self.forest.tables[table].table_goal, &answer.subst)
-            && C::empty_constraints(&answer.subst);
+            && answer.subst.value.constraints.is_empty();
 
         if is_trivial_answer {
             None