From 014dcfee7bca01cc4cbb5ca7113dc634bc3ac6ea Mon Sep 17 00:00:00 2001 From: Cassie Jones Date: Mon, 17 Feb 2020 15:23:35 +0100 Subject: [PATCH] Allow goals to yield to other goals while working Previously we searched over streams of states, that provided solutions to the searched sub-goals. This meant though, that if you attempted to search in a goal which couldn't make progress like the "unproductive" rule below, it would block forever with no way to yield back to the rest of the search without producing a wrong result. unproductive(X) :- unproductive(X). The new search works via iterators over Step instead of over State, where a Step::Working represents a goal which was unable to produce a result, and instead decided to yield, and a Step::Soln(State) is a solution like before. Currently the only goal which will introduce new Working states into the stream is the delay constructor, before forcing, since recursive goals are the only non-terminating goals that are in the core. --- README.md | 9 ++-- src/bin/readme_examples.rs | 10 ++-- src/lib.rs | 98 ++++++++++++++++++++++++++++++-------- src/main.rs | 34 ++++++++++--- 4 files changed, 116 insertions(+), 35 deletions(-) diff --git a/README.md b/README.md index 536437f..4ba7949 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ extension points are: . ## Usage: You build up goals with goal constructors, and then execute them with the -`search` method of `Goal`, running that on an initial state. One of the +`solve` method of `Goal`, running that on an initial state. One of the simplest possible programs you could write is: ```rust @@ -25,7 +25,7 @@ use mukan::{Goal, call_fresh, State, eq}; fn main() { let goal = call_fresh(|x| eq(413, x)); - for soln in goal.search(State::new()) { + for soln in goal.solve(State::new()) { println!("{}", soln); } } @@ -66,7 +66,7 @@ let goal = fresh!((c) => all! { eq((a, b), c), eq((b, 8), c), }); -for soln in goal.search(state) { +for soln in goal.solve(state) { println!("{:?}", reify_vars(&vars, soln)); } ``` @@ -89,11 +89,12 @@ fn peano(n: impl Into) -> impl Goal { We need the `delay()` in order to prevent the goal from being constructed forever without being searched at all. If you try to solve `peano` with a variable, then you'd get an infinite stream of assignments that satisfy it. +Here we just take the first 10: ```rust let (vars, state) = State::with_vars(1); let goal = peano(vars[0]); -for soln in goal.search(state).take(10) { +for soln in goal.solve(state).take(10) { println!("{:?}", reify_vars(&vars, soln)); } ``` diff --git a/src/bin/readme_examples.rs b/src/bin/readme_examples.rs index 7e0642f..875a029 100644 --- a/src/bin/readme_examples.rs +++ b/src/bin/readme_examples.rs @@ -2,12 +2,12 @@ use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify_vars, Goal, State, fn main() { let goal = call_fresh(|x| eq(413, x)); - for soln in goal.search(State::new()) { + for soln in goal.solve(State::new()) { println!("{}", soln); } let goal = call_fresh(|x| or(eq(612, x), eq(1025, x))); - for soln in goal.search(State::new()) { + for soln in goal.solve(State::new()) { println!("{}", soln); } @@ -15,7 +15,7 @@ fn main() { eq((a, b), c), eq((b, 8), c), }); - for soln in goal.search(State::new()) { + for soln in goal.solve(State::new()) { println!("{}", soln); } @@ -25,7 +25,7 @@ fn main() { eq((a, b), c), eq((b, 8), c), }); - for soln in goal.search(state) { + for soln in goal.solve(state) { println!("{:?}", reify_vars(&vars, soln)); } @@ -42,7 +42,7 @@ fn main() { let (vars, state) = State::with_vars(1); let goal = peano(vars[0]); - for soln in goal.search(state).take(10) { + for soln in goal.solve(state).take(10) { println!("{:?}", reify_vars(&vars, soln)); } } diff --git a/src/lib.rs b/src/lib.rs index bd9b49d..dd6d474 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -11,25 +11,37 @@ pub struct State { subst: Subst, } +#[derive(Debug, Clone)] +pub enum Step { + Working, + Soln(State), +} + +impl From for Step { + fn from(state: State) -> Step { + Step::Soln(state) + } +} + pub fn delay(thunk: impl Clone + Fn() -> G + 'static) -> BoxedGoal { BoxedGoal::new(move |state: State| thunk().search(state)) } #[derive(Clone)] pub struct BoxedGoal { - inner: Box>>>, + inner: Box>>>, } impl BoxedGoal { fn new(goal: impl Goal + Clone + 'static) -> Self { BoxedGoal { - inner: Box::new(BoxGoalInner(goal)), + inner: Box::new(BoxGoalInner(goal)) as Box>, } } } impl Goal for BoxedGoal { - type Stream = Box>; + type Stream = Box>; fn search(&self, state: State) -> Self::Stream { self.inner.search(state) } @@ -39,22 +51,62 @@ impl Goal for BoxedGoal { struct BoxGoalInner(G); impl Goal for BoxGoalInner +where + G: Goal + Clone + 'static, +{ + type Stream = Box>; + fn search(&self, state: State) -> Self::Stream { + Box::new(BoxedGoalIter { + first: true, + state: Some(state), + goal: self.0.clone(), + iter: None, + }) + } +} + +struct BoxedGoalIter { + first: bool, + state: Option, + goal: G, + iter: Option, +} + +impl Iterator for BoxedGoalIter where G: Goal + Clone, G::Stream: 'static, { - type Stream = Box>; - fn search(&self, state: State) -> Self::Stream { - Box::new(self.0.search(state)) + type Item = Step; + fn next(&mut self) -> Option { + if self.first { + self.first = false; + return Some(Step::Working); + } + match &mut self.iter { + Some(iter) => iter.next(), + None => { + let mut iter = self.goal.search(self.state.take().unwrap()); + let result = iter.next(); + self.iter = Some(iter); + result + } + } } } pub trait Goal: DynClone { - type Stream: Iterator; + type Stream: Iterator; fn search(&self, state: State) -> Self::Stream; + fn solve(&self, state: State) -> std::iter::FilterMap Option> { + self.search(state).filter_map(|step| match step { + Step::Working => None, + Step::Soln(state) => Some(state), + }) + } } -dyn_clone::clone_trait_object!(Goal>>); +dyn_clone::clone_trait_object!(Goal>>); pub fn call_fresh(block: impl Clone + Fn(Var) -> G) -> impl Goal + Clone { move |mut state: State| { @@ -202,14 +254,15 @@ pub fn reify_vars(vars: &[Var], state: State) -> HashMap { result } -impl Goal for F +impl Goal for F where F: Clone + Fn(State) -> S, - S: Iterator, + S: Iterator, + St: Into, { - type Stream = S; - fn search(&self, state: State) -> S { - self(state) + type Stream = std::iter::Map Step>; + fn search(&self, state: State) -> Self::Stream { + self(state).map(Into::into) } } @@ -231,7 +284,6 @@ impl Iterator for Plus where S: Iterator, R: Iterator, - T: fmt::Display, { type Item = T; fn next(&mut self) -> Option { @@ -275,7 +327,7 @@ where } } -struct Bind, R: Goal> { +struct Bind where S::Item: Into { a: S, b: R, current: Option, @@ -284,10 +336,11 @@ struct Bind, R: Goal> { impl Iterator for Bind where - S: Iterator, + S: Iterator, R: Goal, + S::Item: Into, { - type Item = State; + type Item = Step; fn next(&mut self) -> Option { if self.done { @@ -295,9 +348,14 @@ where } match &mut self.current { None => { - if let Some(state) = self.a.next() { - self.current = Some(self.b.search(state)); - self.next() + 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 diff --git a/src/main.rs b/src/main.rs index 2a99a91..dc421fc 100644 --- a/src/main.rs +++ b/src/main.rs @@ -4,7 +4,7 @@ use std::io::Write; fn main() { println!("Part 1"); let term = call_fresh(|a| call_fresh(move |b| or(and(eq(a, b), eq(a, 1)), eq(b, 2)))); - for soln in term.search(State::new()) { + for soln in term.solve(State::new()) { println!("{:?}", reify(soln)); } @@ -17,13 +17,13 @@ fn main() { eq(d, 413), } }); - for soln in term.search(State::new()) { + for soln in term.solve(State::new()) { println!("{:?}", reify(soln)); } println!("Part 3"); let term = fresh!((a, b) => eq(a, b)); - for soln in term.search(State::new()) { + for soln in term.solve(State::new()) { println!("{:?}", reify(soln)); } @@ -36,7 +36,7 @@ fn main() { ) } let term = fresh!((n) => peano(n)); - for soln in term.search(State::new()).take(5) { + for soln in term.solve(State::new()).take(5) { println!("{:?}", reify(soln)); } @@ -99,15 +99,37 @@ fn main() { println!("Peano addition!"); let (vars, state) = State::with_vars(2); - let sum = 100; + let sum = 10; let term = sums_to(vars[0], vars[1], make_nat(sum)); print!("= "); - for soln in term.search(state) { + for soln in term.solve(state) { let n = term_to_nat(&soln.eval_var(vars[0])).unwrap(); let m = term_to_nat(&soln.eval_var(vars[1])).unwrap(); print!("{} + {} = ", n, m); std::io::stdout().flush().unwrap(); } println!("{}", sum); + + println!("Infinite data!"); + let term = fresh!((x, y, z) => all! { + eq(x, (1, x)), + eq(x, (1, (1, x))), + eq(x, (1, (y, (1, x)))), + eq(x, (1, z)), + }); + for soln in term.solve(State::new()) { + println!("= {}", soln); + } + + fn unproductive(x: impl Into) -> impl Goal + Clone { + let x = x.into(); + delay(move || unproductive(x.clone())) + } + + println!("Or Unproductive"); + let (vars, state) = State::with_vars(2); + let goal = or(peano(vars[0]), unproductive(vars[0])); + for soln in goal.solve(state).take(5) { + println!("peano {}", term_to_nat(&soln.eval_var(vars[0])).unwrap()); } } -- 2.43.2