Make pursue_answer return an Option

chalk-engine/src/logic.rs

@@ -135,10 +135,12 @@ impl<C: Context> Forest<C> {
                             ex_clause,
                             selected_subgoal,
                         };
-                        self.pursue_answer(table, strand).unwrap()
+                        match self.pursue_answer(table, strand) {
+                            Some(()) => Ok(()),
+                            None => panic!("Unexpected non unique answer.")
+                        }
                     },
-                );
-                Ok(())
+                )
             }
 
             // Things involving cycles should be impossible since our
@@ -218,9 +220,7 @@ impl<C: Context> Forest<C> {
         if let Some(depth) = self.stack.is_active(table) {
             info!("ensure_answer: cycle detected at depth {:?}", depth);
 
-            let is_coinductive = self.top_of_stack_is_coinductive_from(depth);
-
-            if is_coinductive {
+            if self.top_of_stack_is_coinductive_from(depth) {
                 info!("ensure_answer: cycle is coinductive");
                 return Ok(EnsureSuccess::Coinductive(None));
             }
@@ -395,10 +395,6 @@ impl<C: Context> Forest<C> {
         depth: StackIndex,
         mut strand: Strand<C>,
     ) -> StrandResult<C, EnsureSuccess<C>> {
-        // One key assumption with this approach is that no new subgoals
-        // will be added while processing a coinductive subgoal
-        // (particularly when `allow_coinduction` is true).
-
         let mut allow_coinduction = false;
         loop {
             info_heading!(
@@ -428,6 +424,7 @@ impl<C: Context> Forest<C> {
                     // is unconditionally coinductive, then they will generate an answer.
                     // Otherwise, they will store the strand back into the table.
                     if allow_coinduction {
+                        assert!(strand.ex_clause.subgoals.is_empty());
                         let Strand {
                             mut infer,
                             ex_clause,
@@ -453,6 +450,7 @@ impl<C: Context> Forest<C> {
                     let table = self.stack[depth].table;
                     return self
                         .pursue_answer(table, strand)
+                        .ok_or(StrandFail::NoSolution)
                         .map(|_| EnsureSuccess::AnswerAvailable);
                 }
 
@@ -534,7 +532,7 @@ impl<C: Context> Forest<C> {
     ///   strand led nowhere of interest.
     /// - the strand may represent a new answer, in which case it is
     ///   added to the table and `Ok` is returned.
-    fn pursue_answer(&mut self, table: TableIndex, strand: Strand<C>) -> StrandResult<C, ()> {
+    fn pursue_answer(&mut self, table: TableIndex, strand: Strand<C>) -> Option<()> {
         let Strand {
             mut infer,
             ex_clause:
@@ -632,10 +630,10 @@ impl<C: Context> Forest<C> {
                 self.tables[table].take_strands();
             }
 
-            Ok(())
+            Some(())
         } else {
-            info!("answer: not a new answer, returning StrandFail::NoSolution");
-            Err(StrandFail::NoSolution)
+            info!("answer: not a new answer, returning None");
+            None
         }
     }