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

   1 use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify, Goal, State, Term};
   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 }