From 052144cabb126efe925a96f8a0597a0f2005d206 Mon Sep 17 00:00:00 2001 From: lemon Date: Mon, 23 Feb 2026 20:36:05 +0100 Subject: add metalang99 testsuite (preprocessor stress testing) --- .../external/metalang99/examples/lambda_calculus.c | 209 +++++++++++++++++++++ 1 file changed, 209 insertions(+) create mode 100644 test/external/metalang99/examples/lambda_calculus.c (limited to 'test/external/metalang99/examples/lambda_calculus.c') diff --git a/test/external/metalang99/examples/lambda_calculus.c b/test/external/metalang99/examples/lambda_calculus.c new file mode 100644 index 0000000..e300304 --- /dev/null +++ b/test/external/metalang99/examples/lambda_calculus.c @@ -0,0 +1,209 @@ +/* + * An untyped lambda calculus [1] interpreter using De Bruijn indices [2] and normal order + * evaluation strategy [3]. + * + * [1] https://en.wikipedia.org/wiki/Lambda_calculus + * [2] https://en.wikipedia.org/wiki/De_Bruijn_index + * [3] https://en.wikipedia.org/wiki/Evaluation_strategy#Normal_order + */ + +#include + +// Syntactic terms { + +#define var(i) ML99_call(var, i) +#define appl(M, N) ML99_call(appl, M, N) +#define lam(M) ML99_call(lam, M) + +#define var_IMPL(i) v(VAR(i)) +#define appl_IMPL(M, N) v(APPL(M, N)) +#define lam_IMPL(M) v(LAM(M)) + +#define VAR(i) ML99_CHOICE(var, i) +#define APPL(M, N) ML99_CHOICE(appl, M, N) +#define LAM(M) ML99_CHOICE(lam, M) +// } (Syntactic terms) + +// Variable substitution: `M[1=x]` { + +#define subst(M, x) ML99_call(subst, M, x) + +#define subst_IMPL(M, x) substAux_IMPL(M, x, 1) +#define substAux_IMPL(M, x, depth) ML99_callUneval(ML99_matchWithArgs, M, substAux_, x, depth) + +#define substAux_var_IMPL(i, x, depth) \ + ML99_IF( \ + ML99_NAT_EQ(i, depth), \ + v(x), \ + ML99_call(ML99_if, ML99_callUneval(ML99_greater, i, depth), v(VAR(ML99_DEC(i)), VAR(i)))) +#define substAux_appl_IMPL(M, N, x, depth) \ + appl(substAux_IMPL(M, x, depth), substAux_IMPL(N, x, depth)) +#define substAux_lam_IMPL(M, x, depth) \ + lam(ML99_call(substAux, v(M), incFreeVars_IMPL(x), v(ML99_INC(depth)))) +// } (Variable substitution) + +// Increment free variables in `M` { + +#define incFreeVars(M) ML99_call(incFreeVars, M) + +#define incFreeVars_IMPL(M) incFreeVarsAux_IMPL(M, 1) +#define incFreeVarsAux_IMPL(M, depth) ML99_callUneval(ML99_matchWithArgs, M, incFreeVarsAux_, depth) + +#define incFreeVarsAux_var_IMPL(i, depth) \ + ML99_call(ML99_if, ML99_callUneval(ML99_greaterEq, i, depth), v(VAR(ML99_INC(i)), VAR(i))) +#define incFreeVarsAux_appl_IMPL(M, N, depth) \ + appl(incFreeVarsAux_IMPL(M, depth), incFreeVarsAux_IMPL(N, depth)) +#define incFreeVarsAux_lam_IMPL(M, depth) lam(incFreeVarsAux_IMPL(M, ML99_INC(depth))) +// } (Increment free variables) + +// Evaluation { + +#define eval(M) ML99_call(eval, M) + +#define eval_IMPL(M) ML99_callUneval(ML99_match, M, eval_) +#define eval_var_IMPL(i) v(VAR(i)) +#define eval_appl_IMPL(M, N) ML99_callUneval(ML99_matchWithArgs, M, eval_appl_, N) +#define eval_lam_IMPL(M) lam(eval_IMPL(M)) + +#define eval_appl_var_IMPL(i, N) appl(v(VAR(i)), eval_IMPL(N)) +#define eval_appl_appl_IMPL(M, N, N1) \ + ML99_call(ML99_matchWithArgs, eval(appl_IMPL(M, N)), v(eval_appl_appl_, N1)) +#define eval_appl_lam_IMPL(M, N) eval(subst_IMPL(M, N)) + +#define eval_appl_appl_var_IMPL eval_appl_var_IMPL +#define eval_appl_appl_appl_IMPL(M, N, N1) appl(appl_IMPL(M, N), eval_IMPL(N1)) +#define eval_appl_appl_lam_IMPL eval_appl_lam_IMPL +// } (Evaluation) + +// Syntactical equality { + +#define termEq(lhs, rhs) ML99_matchWithArgs(lhs, v(termEq_), rhs) +#define termEq_var_IMPL(i, rhs) termEqPropagate(var, rhs, i) +#define termEq_appl_IMPL(M, N, rhs) termEqPropagate(appl, rhs, M, N) +#define termEq_lam_IMPL(M, rhs) termEqPropagate(lam, rhs, M) + +#define termEqPropagate(term_kind, rhs, ...) \ + ML99_IF( \ + ML99_IDENT_EQ(TERM_, ML99_CHOICE_TAG(rhs), term_kind), \ + ML99_matchWithArgs(v(rhs), v(termEq_##term_kind##_), v(__VA_ARGS__)), \ + ML99_false()) + +#define termEq_var_var_IMPL(j, i) v(ML99_NAT_EQ(i, j)) +#define termEq_appl_appl_IMPL(M, N, M1, N1) ML99_and(termEq(v(M), v(M1)), termEq(v(N), v(N1))) +#define termEq_lam_lam_IMPL(M, M1) termEq(v(M), v(M1)) + +#define TERM_var_var () +#define TERM_appl_appl () +#define TERM_lam_lam () +// } (Syntactical equality) + +#define ASSERT_REDUCES_TO(lhs, rhs) \ + /* Use two interpreter passes: one for `eval(lhs)`, one for `termEq`. Thereby we achieve more \ + * Metalang99 reduction steps available. */ \ + ML99_ASSERT_UNEVAL(ML99_EVAL(termEq(v(ML99_EVAL(eval(v(lhs)))), v(ML99_EVAL(eval(v(rhs))))))) + +// The identity combinator { + +#define I LAM(VAR(1)) + +ASSERT_REDUCES_TO(APPL(I, VAR(5)), VAR(5)); +// } (The identity combinator) + +// The K, S combinators { + +#define K LAM(LAM(VAR(2))) +#define S LAM(LAM(LAM(APPL(APPL(VAR(3), VAR(1)), APPL(VAR(2), VAR(1)))))) + +ASSERT_REDUCES_TO(APPL(APPL(S, K), K), I); +ASSERT_REDUCES_TO(APPL(APPL(APPL(S, K), S), K), K); + +ASSERT_REDUCES_TO(APPL(APPL(APPL(S, K), VAR(5)), VAR(6)), VAR(6)); +ASSERT_REDUCES_TO(APPL(APPL(K, VAR(5)), VAR(6)), VAR(5)); +// } (The K, S combinators) + +// Church booleans { + +#define T LAM(LAM(VAR(2))) +#define F LAM(LAM(VAR(1))) + +#define NOT LAM(APPL(APPL(VAR(1), F), T)) +#define AND LAM(LAM(APPL(APPL(VAR(2), VAR(1)), VAR(2)))) +#define OR LAM(LAM(APPL(APPL(VAR(2), VAR(2)), VAR(1)))) +#define XOR LAM(LAM(APPL(APPL(VAR(2), APPL(NOT, VAR(1))), VAR(1)))) + +#define IF LAM(LAM(LAM(APPL(APPL(VAR(3), VAR(2)), VAR(1))))) + +ASSERT_REDUCES_TO(APPL(NOT, T), F); +ASSERT_REDUCES_TO(APPL(NOT, F), T); +ASSERT_REDUCES_TO(APPL(NOT, APPL(NOT, T)), T); +ASSERT_REDUCES_TO(APPL(NOT, APPL(NOT, F)), F); + +ASSERT_REDUCES_TO(APPL(APPL(AND, T), T), T); +ASSERT_REDUCES_TO(APPL(APPL(AND, T), F), F); +ASSERT_REDUCES_TO(APPL(APPL(AND, F), T), F); +ASSERT_REDUCES_TO(APPL(APPL(AND, F), F), F); + +ASSERT_REDUCES_TO(APPL(APPL(OR, T), T), T); +ASSERT_REDUCES_TO(APPL(APPL(OR, T), F), T); +ASSERT_REDUCES_TO(APPL(APPL(OR, F), T), T); +ASSERT_REDUCES_TO(APPL(APPL(OR, F), F), F); + +ASSERT_REDUCES_TO(APPL(APPL(XOR, T), T), F); +ASSERT_REDUCES_TO(APPL(APPL(XOR, T), F), T); +ASSERT_REDUCES_TO(APPL(APPL(XOR, F), T), T); +ASSERT_REDUCES_TO(APPL(APPL(XOR, F), F), F); + +ASSERT_REDUCES_TO(APPL(APPL(APPL(IF, T), VAR(5)), VAR(6)), VAR(5)); +ASSERT_REDUCES_TO(APPL(APPL(APPL(IF, F), VAR(5)), VAR(6)), VAR(6)); +// } (Church booleans) + +// Church numerals { + +#define ZERO LAM(LAM(VAR(1))) +#define SUCC LAM(LAM(LAM(APPL(VAR(2), APPL(APPL(VAR(3), VAR(2)), VAR(1)))))) + +#define ONE APPL(SUCC, ZERO) +#define TWO APPL(SUCC, ONE) +#define THREE APPL(SUCC, TWO) +#define FOUR APPL(SUCC, THREE) + +#define ADD LAM(LAM(LAM(LAM(APPL(APPL(VAR(4), VAR(2)), APPL(APPL(VAR(3), VAR(2)), VAR(1))))))) +#define MUL LAM(LAM(LAM(LAM(APPL(APPL(VAR(4), APPL(VAR(3), VAR(2))), VAR(1)))))) + +ASSERT_REDUCES_TO(APPL(APPL(ADD, ZERO), ZERO), ZERO); +ASSERT_REDUCES_TO(APPL(APPL(ADD, ZERO), ONE), ONE); +ASSERT_REDUCES_TO(APPL(APPL(ADD, ONE), ZERO), ONE); +ASSERT_REDUCES_TO(APPL(APPL(ADD, ONE), TWO), THREE); + +ASSERT_REDUCES_TO(APPL(APPL(MUL, ZERO), ZERO), ZERO); +ASSERT_REDUCES_TO(APPL(APPL(MUL, ZERO), ONE), ZERO); +ASSERT_REDUCES_TO(APPL(APPL(MUL, ONE), ZERO), ZERO); +ASSERT_REDUCES_TO(APPL(APPL(MUL, TWO), TWO), FOUR); +// } (Church numerals) + +// Church pairs { + +#define PAIR LAM(LAM(LAM(APPL(APPL(VAR(1), VAR(3)), VAR(2))))) +#define FST LAM(APPL(VAR(1), T)) +#define SND LAM(APPL(VAR(1), F)) + +ASSERT_REDUCES_TO(APPL(FST, APPL(APPL(PAIR, VAR(5)), VAR(6))), VAR(5)); +ASSERT_REDUCES_TO(APPL(SND, APPL(APPL(PAIR, VAR(5)), VAR(6))), VAR(6)); +// } (Church pairs) + +// Church lists { + +#define NIL F +#define CONS PAIR +#define IS_NIL LAM(APPL(APPL(VAR(1), LAM(LAM(LAM(F)))), T)) + +#define LIST_1_2_3 APPL(APPL(CONS, VAR(1)), APPL(APPL(CONS, VAR(2)), APPL(APPL(CONS, VAR(3)), NIL))) + +ASSERT_REDUCES_TO(APPL(IS_NIL, NIL), T); +ASSERT_REDUCES_TO(APPL(IS_NIL, LIST_1_2_3), F); +// } (Church lists) + +// Recursion via self-application (or the Y combinator) is perfectly expressible, though when +// executed, it exhausts the Metalang99 recursion engine limit. + +int main(void) {} -- cgit v1.2.3