feat: construct test functions

src/experiments.rs

@@ -6,15 +6,12 @@ use clap::error::Result;
 use futures::{stream::FuturesUnordered, StreamExt};
 use lambda_calculus::{
     abs, app,
-    combinators::{Y, Z},
-    data::{
-        boolean::{fls, tru},
-        num::church::{add, eq, sub},
-    },
+    combinators::Z,
+    data::num::church::{add, eq, sub},
     parse,
     term::Notation::Classic,
     IntoChurchNum,
-    Term::{self, Abs, Var},
+    Term::{self, Var},
 };
 use plotters::prelude::*;
 
@@ -25,6 +22,61 @@ use crate::{
     read_inputs,
 };
 
+pub fn test_add(a: usize, b: usize) -> Term {
+    let mut test = parse(r"\eq. \a. \b. \ab. \f. (eq (f a b) ab)", Classic).unwrap();
+    test = app!(
+        test,
+        eq(),
+        a.into_church(),
+        b.into_church(),
+        (a + b).into_church()
+    );
+    // `test` has type (church -> church -> church) -> bool
+    test.reduce(lambda_calculus::HAP, 0);
+    println!("add test: {:?}", test);
+    test
+}
+
+pub fn test_succ(a: usize) -> Term {
+    let mut test = parse(r"\eq. \a. \asucc. \f. (eq (f a) asucc)", Classic).unwrap();
+    test = app!(test, eq(), a.into_church(), (a + 1).into_church());
+    // `test` has type (church -> church) -> bool
+    test.reduce(lambda_calculus::HAP, 0);
+    println!("successor test: {:?}", test);
+    test
+}
+
+pub fn test_sub(a: usize, b: usize) -> Term {
+    let mut test = parse(r"\eq. \a. \b. \ab. \f. (eq (f a b) ab)", Classic).unwrap();
+    test = app!(
+        test,
+        eq(),
+        a.into_church(),
+        b.into_church(),
+        (a - b).into_church()
+    );
+    // `test` has type (church -> church -> church) -> bool
+    test.reduce(lambda_calculus::HAP, 0);
+    println!("subtraction test: {:?}", test);
+    test
+}
+
+pub fn test_pred(a: usize) -> Term {
+    let mut test = parse(r"\eq. \a. \apred. \f. (eq (f a) apred)", Classic).unwrap();
+    test = app!(test, eq(), a.into_church(), (a - 1).into_church());
+    // `test` has type (church -> church) -> bool
+    test.reduce(lambda_calculus::HAP, 0);
+    println!("pred test: {:?}", test);
+    test
+}
+
+pub fn test_add_reduction() -> Term {
+    let mut comp = app!(test_add(1, 2), add());
+    comp.reduce(lambda_calculus::HAP, 0);
+    println!("add reduction: {:?}", comp);
+    comp
+}
+
 pub async fn look_for_magic() {
     let mut futures = FuturesUnordered::new();
     let run_length = 1000000;

src/main.rs

@@ -37,6 +37,7 @@ pub enum Experiment {
     SampleSimulate,
     SampleScan,
     MagicTestFunction,
+    MagicTestConstruct,
 }
 
 #[derive(Parser, Debug)]
@@ -196,6 +197,13 @@ fn main() -> std::io::Result<()> {
             Experiment::SampleSimulate => {
                 block_on(experiments::simulate_sample());
             }
+            Experiment::MagicTestConstruct => {
+                experiments::test_succ(0);
+                experiments::test_add(1, 2);
+                experiments::test_pred(1);
+                experiments::test_sub(1, 1);
+                experiments::test_add_reduction();
+            }
         }
         return Ok(());
     }