From 6928f8cf8a6384e310de34e470bcd266d8ce29d7 Mon Sep 17 00:00:00 2001
From: Cassie Jones <code@witchoflight.com>
Date: Mon, 17 Feb 2020 13:03:23 +0100
Subject: [PATCH] Evaluate larger peano for performance evaluation

This is mostly just changing the output format for it so that it doesn't
take up the entire screen even when running for the ways to sum to 100.
---
 src/lib.rs  |  5 +++++
 src/main.rs | 28 +++++++++++++++++++++++++---
 2 files changed, 30 insertions(+), 3 deletions(-)

diff --git a/src/lib.rs b/src/lib.rs
index fa56b55..bd9b49d 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -136,6 +136,11 @@ impl State {
         })
     }
 
+    pub fn eval_var(&self, var: Var) -> Term {
+        let var = Term::Var(var);
+        self.eval(&var)
+    }
+
     pub fn eval(&self, term: &Term) -> Term {
         match self.subst.walk(&term) {
             Term::Pair(u, v) => Term::from((self.eval(&*u), self.eval(&*v))),
diff --git a/src/main.rs b/src/main.rs
index 190cb77..2a99a91 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,4 +1,5 @@
-use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify, reify_vars, Goal, State, Term};
+use mukan::{all, and, call_fresh, delay, eq, fresh, or, reify, Goal, State, Term};
+use std::io::Write;
 
 fn main() {
     println!("Part 1");
@@ -47,6 +48,20 @@ fn main() {
         }
     }
 
+    fn term_to_nat(mut n: &Term) -> Option<u32> {
+        let mut res = 0;
+        loop {
+            match n {
+                Term::Pair(s, k) if &**s == &Term::Lit(1) => {
+                    res += 1;
+                    n = k;
+                }
+                Term::Lit(0) => return Some(res),
+                _ => return None,
+            }
+        }
+    }
+
     fn less(n: impl Into<Term>, m: impl Into<Term>) -> impl Goal + Clone {
         let n = n.into();
         let m = m.into();
@@ -84,8 +99,15 @@ fn main() {
 
     println!("Peano addition!");
     let (vars, state) = State::with_vars(2);
-    let term = sums_to(vars[0], vars[1], make_nat(10));
+    let sum = 100;
+    let term = sums_to(vars[0], vars[1], make_nat(sum));
+    print!("= ");
     for soln in term.search(state) {
-        println!("= {:?}", reify_vars(&vars, soln));
+        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);
     }
 }
-- 
2.43.2