]> Witch of Git - mukan/blob - src/bin/readme_examples.rs
Make the Bind iterator for AND goals fair
[mukan] / src / bin / readme_examples.rs
1 use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify_vars, Goal, State, Term};
2
3 fn main() {
4 let goal = call_fresh(|x| eq(413, x));
5 for soln in goal.solve(State::new()) {
6 println!("{}", soln);
7 }
8
9 let goal = call_fresh(|x| or(eq(612, x), eq(1025, x)));
10 for soln in goal.solve(State::new()) {
11 println!("{}", soln);
12 }
13
14 let goal = fresh!((a, b, c) => all! {
15 eq((a, b), c),
16 eq((b, 8), c),
17 });
18 for soln in goal.solve(State::new()) {
19 println!("{}", soln);
20 }
21
22 let (vars, state) = State::with_vars(2);
23 let (a, b) = (vars[0], vars[1]);
24 let goal = fresh!((c) => all! {
25 eq((a, b), c),
26 eq((b, 8), c),
27 });
28 for soln in goal.solve(state) {
29 println!("{:?}", reify_vars(&vars, soln));
30 }
31
32 fn peano(n: impl Into<Term>) -> impl Goal {
33 let n = n.into();
34 or(
35 eq(n.clone(), 0),
36 fresh!((x) => and(
37 eq(n.clone(), (1, x)),
38 delay(move || peano(x)),
39 )),
40 )
41 }
42
43 let (vars, state) = State::with_vars(1);
44 let goal = peano(vars[0]);
45 for soln in goal.solve(state).take(10) {
46 println!("{:?}", reify_vars(&vars, soln));
47 }
48 }