' Test suite for the lambda calculus engine

' Booleans
let true  = \a.\b.a;
let false = \a.\b.b;

' If-then-else
let if = \b.\x.\y.b x y;

' Test out if
if true 0 1;
if false 0 1;

' Test out the id function (id is built in)
id true;
id false;
id id;
id id id;
id (id id id);


' Test out endlessness
let apply_self = \x.x x;

apply_self;
id apply_self;
apply_self id;
apply_self apply_self;

' Test out lazy evaluation
(\x.3) (apply_self apply_self);


' Lets test a primative or two
succ 1;
to_church 5;
depth (to_church 5);

let five = to_church 5;
depth five;

' Check out partial evaluation (return a function)
(\x.\b.x b) 6;

' We should try the math primitives.
mul 7 6;
div 10 2;
add 6 9;
sub 10 2;
eq 7 6;
eq 7 7;


' Time to test recursion
' A fixpoint combinator
let fix = \f. (\x. f (x x))(\x. f (x x));

' Example of using fixpoint to define recursive functions, e.g factorial
let factorial = fix (\f . \n . id (eq n 0) 1 (mul n (f (sub n 1))));

' Factorial 5 = 120
factorial 5;

' Test ordered pairs (lists)
let pair = \x.\y.\b.b x y;
let hd = \p.p true;
let tl = \p.p false;

tl (pair 3 5);
hd (pair 3 5);

let list_a = pair 1 (pair 3 5);

hd list_a;
tl list_a;

hd (tl list_a);

pair 0 1;
pair 0 (pair 1 2);

primpair 0 1;
let list_b = primpair 0 (primpair 1 2);

primhd list_a;
primtl list_a;

let subtest =
  let a = 0 in
  let b = 1 in
  add a b;

subtest;