From: Cassie Jones Date: Mon, 17 Feb 2020 16:52:12 +0000 (+0100) Subject: Make the Bind iterator for AND goals fair X-Git-Url: https://git.witchoflight.com/mukan/commitdiff_plain 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 20c3961..43aba0c 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -150,10 +150,10 @@ pub fn eq(u: impl Into, v: impl Into) -> 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 where S::Item: Into, { - a: S, + a: std::iter::Fuse, b: R, - current: Option, - done: bool, + streams: Vec, + index: usize, } impl Iterator for Bind @@ -346,31 +346,30 @@ where type Item = Step; fn next(&mut self) -> Option { - 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 dc421fc..3b18c3e 100644 --- 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); + } }