/* Turing Completeness: Lambda Calculus Foundations */
/* Demonstrates: Church encodings, combinators, functional completeness */

..out "=== Lambda Calculus Foundations Test ===";

/* Test 1: Church Numerals (encoding numbers as functions) */
/* Church 0: f -> x -> x */
church_zero : f x -> x;

/* Church 1: f -> x -> f x */
church_one : f x -> f x;

/* Church 2: f -> x -> f (f x) */  
church_two : f x -> f (f x);

/* Successor function: n -> f -> x -> f (n f x) */
church_succ : n f x -> f (n f x);

/* Test successor */
church_three : church_succ church_two;

/* Convert church numeral to integer for testing */
inc : x -> x + 1;
three_as_int : church_three @inc 0;

..assert three_as_int = 3;
..out "1. Church numerals: PASS";

/* Test 2: Church Booleans */
church_true : x y -> x;
church_false : x y -> y;

/* Church conditional: p -> x -> y -> p x y */
church_if : p x y -> p x y;

/* Test boolean logic */
bool_test1 : church_if @church_true "yes" "no";
bool_test2 : church_if @church_false "yes" "no"; 

..assert bool_test1 = "yes";
..assert bool_test2 = "no";
..out "2. Church booleans: PASS";

/* Test 3: Combinators (S, K, I) */
/* S combinator: f -> g -> x -> f x (g x) */
s_combinator : f g x -> f x (g x);

/* K combinator: x -> y -> x */  
k_combinator : x y -> x;

/* I combinator: x -> x (can be derived as S K K) */
i_combinator : @s_combinator @k_combinator @k_combinator;

/* Test I combinator */
identity_test : i_combinator 42;

..assert identity_test = 42;
..out "3. SKI combinators: PASS";

/* Test 4: Y Combinator (fixed point for recursion) */
/* Simplified recursive implementation without nested lambdas */
y_helper : f x -> f (x x);
y_inner : f x -> y_helper f x;
y_comb : f -> y_helper f @y_inner;

/* Factorial using Y combinator */
fact_func : f n -> when n is 0 then 1 _ then n * (f (n - 1));
y_factorial : @y_comb @fact_func;

factorial_result : y_factorial 5;

..assert factorial_result = 120;
..out "4. Y combinator recursion: PASS";

/* Test 5: Currying and partial application */
curry : f x y -> f x y;
add_func : x y -> x + y;
add_curry : curry @add_func;
add_five : add_curry 5;

curried_result : add_five 10;

..assert curried_result = 15;
..out "5. Currying: PASS";

..out "✅ All lambda calculus tests passed";
..out "Demonstrates: Functional completeness, Church encodings, combinatorial logic";