Witch of Git - mukan/blob - src/main.rs

   1 use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify, reify_vars, Goal, State, Term};
   2
   3 fn main() {
   4     println!("Part 1");
   5     let term = call_fresh(|a| call_fresh(move |b| or(and(eq(a, b), eq(a, 1)), eq(b, 2))));
   6     for soln in term.search(State::new()) {
   7         println!("{:?}", reify(soln));
   8     }
   9
  10     println!("Part 2");
  11     let term = fresh!((p, a, b, c, d) => {
  12         all! {
  13             eq(p, (a, b)),
  14             eq((a, b), (c, d)),
  15             eq((a, b), (b, c)),
  16             eq(d, 413),
  17         }
  18     });
  19     for soln in term.search(State::new()) {
  20         println!("{:?}", reify(soln));
  21     }
  22
  23     println!("Part 3");
  24     let term = fresh!((a, b) => eq(a, b));
  25     for soln in term.search(State::new()) {
  26         println!("{:?}", reify(soln));
  27     }
  28
  29     println!("Peano");
  30     fn peano(n: impl Into<Term>) -> impl Goal + Clone {
  31         let n = n.into();
  32         or(
  33             eq(n.clone(), 0),
  34             fresh!((r) => and(eq(n.clone(), (1, r)), delay(move || peano(r)))),
  35         )
  36     }
  37     let term = fresh!((n) => peano(n));
  38     for soln in term.search(State::new()).take(5) {
  39         println!("{:?}", reify(soln));
  40     }
  41
  42     fn make_nat(n: u32) -> Term {
  43         if n == 0 {
  44             0.into()
  45         } else {
  46             (1, make_nat(n - 1)).into()
  47         }
  48     }
  49
  50     fn less(n: impl Into<Term>, m: impl Into<Term>) -> impl Goal + Clone {
  51         let n = n.into();
  52         let m = m.into();
  53         or(
  54             eq((1, n.clone()), m.clone()),
  55             fresh!((x) => all! {
  56                 eq(m.clone(), (1, x)),
  57                 {
  58                     let n = n.clone();
  59                     delay(move || less(n.clone(), x.clone()))
  60                 }
  61             }),
  62         )
  63     }
  64
  65     fn sums_to(n: impl Into<Term>, m: impl Into<Term>, s: impl Into<Term>) -> impl Goal + Clone {
  66         let n = n.into();
  67         let m = m.into();
  68         let s = s.into();
  69         or(
  70             and(eq(n.clone(), 0), eq(m.clone(), s.clone())),
  71             fresh!((x) => all! {
  72                  eq(n.clone(), (1, x)),
  73                  {
  74                      let m = m.clone();
  75                      let s = s.clone();
  76                      delay(move || all! {
  77                         less(m.clone(), s.clone()),
  78                         sums_to(x, (1, m.clone()), s.clone()),
  79                      })
  80                  }
  81             }),
  82         )
  83     }
  84
  85     println!("Peano addition!");
  86     let (vars, state) = State::with_vars(2);
  87     let term = sums_to(vars[0], vars[1], make_nat(10));
  88     for soln in term.search(state) {
  89         println!("= {:?}", reify_vars(&vars, soln));
  90     }
  91 }