Make the Bind iterator for AND goals fair
[mukan] / src / main.rs
1 use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify, Goal, State, Term, Var};
2 use std::io::Write;
3
4 fn main() {
5 println!("Part 1");
6 let term = call_fresh(|a| call_fresh(move |b| or(and(eq(a, b), eq(a, 1)), eq(b, 2))));
7 for soln in term.solve(State::new()) {
8 println!("{:?}", reify(soln));
9 }
10
11 println!("Part 2");
12 let term = fresh!((p, a, b, c, d) => {
13 all! {
14 eq(p, (a, b)),
15 eq((a, b), (c, d)),
16 eq((a, b), (b, c)),
17 eq(d, 413),
18 }
19 });
20 for soln in term.solve(State::new()) {
21 println!("{:?}", reify(soln));
22 }
23
24 println!("Part 3");
25 let term = fresh!((a, b) => eq(a, b));
26 for soln in term.solve(State::new()) {
27 println!("{:?}", reify(soln));
28 }
29
30 println!("Peano");
31 fn peano(n: impl Into<Term>) -> impl Goal + Clone {
32 let n = n.into();
33 or(
34 eq(n.clone(), 0),
35 fresh!((r) => and(eq(n.clone(), (1, r)), delay(move || peano(r)))),
36 )
37 }
38 let term = fresh!((n) => peano(n));
39 for soln in term.solve(State::new()).take(5) {
40 println!("{:?}", reify(soln));
41 }
42
43 fn make_nat(n: u32) -> Term {
44 if n == 0 {
45 0.into()
46 } else {
47 (1, make_nat(n - 1)).into()
48 }
49 }
50
51 fn term_to_nat(mut n: &Term) -> Option<u32> {
52 let mut res = 0;
53 loop {
54 match n {
55 Term::Pair(s, k) if &**s == &Term::Lit(1) => {
56 res += 1;
57 n = k;
58 }
59 Term::Lit(0) => return Some(res),
60 _ => return None,
61 }
62 }
63 }
64
65 fn less(n: impl Into<Term>, m: impl Into<Term>) -> impl Goal + Clone {
66 let n = n.into();
67 let m = m.into();
68 or(
69 eq((1, n.clone()), m.clone()),
70 fresh!((x) => all! {
71 eq(m.clone(), (1, x)),
72 {
73 let n = n.clone();
74 delay(move || less(n.clone(), x.clone()))
75 }
76 }),
77 )
78 }
79
80 fn sums_to(n: impl Into<Term>, m: impl Into<Term>, s: impl Into<Term>) -> impl Goal + Clone {
81 let n = n.into();
82 let m = m.into();
83 let s = s.into();
84 or(
85 and(eq(n.clone(), 0), eq(m.clone(), s.clone())),
86 fresh!((x) => all! {
87 eq(n.clone(), (1, x)),
88 {
89 let m = m.clone();
90 let s = s.clone();
91 delay(move || all! {
92 less(m.clone(), s.clone()),
93 sums_to(x, (1, m.clone()), s.clone()),
94 })
95 }
96 }),
97 )
98 }
99
100 println!("Peano addition!");
101 let (vars, state) = State::with_vars(2);
102 let sum = 10;
103 let term = sums_to(vars[0], vars[1], make_nat(sum));
104 print!("= ");
105 for soln in term.solve(state) {
106 let n = term_to_nat(&soln.eval_var(vars[0])).unwrap();
107 let m = term_to_nat(&soln.eval_var(vars[1])).unwrap();
108 print!("{} + {} = ", n, m);
109 std::io::stdout().flush().unwrap();
110 }
111 println!("{}", sum);
112
113 println!("Infinite data!");
114 let term = fresh!((x, y, z) => all! {
115 eq(x, (1, x)),
116 eq(x, (1, (1, x))),
117 eq(x, (1, (y, (1, x)))),
118 eq(x, (1, z)),
119 });
120 for soln in term.solve(State::new()) {
121 println!("= {}", soln);
122 }
123
124 fn unproductive(x: impl Into<Term>) -> impl Goal + Clone {
125 let x = x.into();
126 delay(move || unproductive(x.clone()))
127 }
128
129 println!("Or Unproductive");
130 let (vars, state) = State::with_vars(2);
131 let goal = or(peano(vars[0]), unproductive(vars[0]));
132 for soln in goal.solve(state).take(5) {
133 println!("peano {}", term_to_nat(&soln.eval_var(vars[0])).unwrap());
134 }
135
136 fn infinite(x: Var) -> impl Goal + Clone {
137 or(eq(x, x), delay(move || infinite(x)))
138 }
139
140 println!("And Fairness");
141 let goal = fresh!((x) => all! {
142 peano(x),
143 infinite(x),
144 });
145 for soln in goal.solve(State::new()).take(5) {
146 println!("{}", soln);
147 }
148 }