Make the Bind iterator for AND goals fair

Given and(goal_a, goal_b), previously if goal_b could produce an
infinite number of solutions, then goal_a wouldn't get a chance to move
on the to previous. It was doing a sort of dependent Cartesian product
where it would take one step on goal_a in order to find the context for
goal_b, and then completely exhaust goal_b in that context.

Now, we do a diagonal search, keeping a vector of searches in goal_b,
and asking goal_a for a new context each time we loop back around to the
beginning. If goal_a is exhausted, we stop adding new searches, and if
any of the searches in goal_b is exhausted, we remove it from the list
of searches to iterate over.

Some specific things to note: we respect yields in goal_a, so that a
diverging goal_a doesn't get stuck and instead will repeatedly yield,
letting the rest of the program continue its search, interleaved
elsewhere.

This changes performance, making the large Peano addition slower.

diff --git a/src/lib.rs b/src/lib.rs
index 20c39610f0778c07bda34c030851ac74833308c6..43aba0caebb179b7c455945acc606a2d1398921e 100644 (file)
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -150,10 +150,10 @@ pub fn eq(u: impl Into<Term>, v: impl Into<Term>) -> impl Goal + Clone {
 
 pub fn and(u: impl Goal + Clone, v: impl Goal + Clone) -> impl Goal + Clone {
     move |state: State| Bind {
-        a: u.search(state),
+        a: u.search(state).fuse(),
         b: v.clone(),
-        current: None,
-        done: false,
+        streams: Vec::new(),
+        index: 0,
     }
 }
 
@@ -331,10 +331,10 @@ struct Bind<S: Iterator, R: Goal>
 where
     S::Item: Into<Step>,
 {
-    a: S,
+    a: std::iter::Fuse<S>,
     b: R,
-    current: Option<R::Stream>,
-    done: bool,
+    streams: Vec<R::Stream>,
+    index: usize,
 }
 
 impl<S, R> Iterator for Bind<S, R>
@@ -346,31 +346,30 @@ where
     type Item = Step;
 
     fn next(&mut self) -> Option<Self::Item> {
-        if self.done {
-            return None;
+        if self.index == 0 {
+            match self.a.next().map(Into::into) {
+                Some(Step::Working) => return Some(Step::Working),
+                Some(Step::Soln(state)) => self.streams.push(self.b.search(state)),
+                None => (),
+            }
         }
-        match &mut self.current {
-            None => {
-                if let Some(step) = self.a.next() {
-                    match step.into() {
-                        Step::Soln(state) => {
-                            self.current = Some(self.b.search(state));
-                            self.next()
-                        }
-                        Step::Working => Some(Step::Working),
-                    }
-                } else {
-                    self.done = true;
-                    None
-                }
+
+        loop {
+            self.index += 1;
+            if self.streams.is_empty() {
+                return None;
+            } else if self.index >= self.streams.len() {
+                self.index = 0;
             }
-            Some(stream) => match stream.next() {
+
+            match self.streams[self.index].next() {
                 None => {
-                    self.current = None;
-                    self.next()
+                    self.streams.swap_remove(self.index);
                 }
-                item => item,
-            },
+                step => {
+                    return step;
+                }
+            }
         }
     }
 }

diff --git a/src/main.rs b/src/main.rs
index dc421fcabdc81c6e38ea80871c845c168079953d..3b18c3e08562ecd874252a9b5e3678005be36772 100644 (file)
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,4 +1,4 @@
-use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify, Goal, State, Term};
+use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify, Goal, State, Term, Var};
 use std::io::Write;
 
 fn main() {
@@ -132,4 +132,17 @@ fn main() {
     for soln in goal.solve(state).take(5) {
         println!("peano {}", term_to_nat(&soln.eval_var(vars[0])).unwrap());
     }
+
+    fn infinite(x: Var) -> impl Goal + Clone {
+        or(eq(x, x), delay(move || infinite(x)))
+    }
+
+    println!("And Fairness");
+    let goal = fresh!((x) => all! {
+        peano(x),
+        infinite(x),
+    });
+    for soln in goal.solve(State::new()).take(5) {
+        println!("{}", soln);
+    }
 }