#include <stdio.h>
#include <stdlib.h>
#include <string.h>

// AST; variable, application, lambda.
typedef enum { VAR, APP, LAM } Tag;

typedef struct Term {
    Tag tag;
    const char* name;   // For VAR.
    struct Term *f, *a; // For APP: function and argument.
    const char* param;  // For LAM: bound variable name.
    struct Term* body;  // For LAM: body expression.
} Term;

static Term* var(const char* n) {
    Term* t = malloc(sizeof *t);
    t->tag = VAR;
    t->name = n;
    return t;
}

static Term* app(Term* f, Term* a) {
    Term* t = malloc(sizeof *t);
    t->tag = APP;
    t->f = f;
    t->a = a;
    return t;
}

static Term* lam(const char* p, Term* b) {
    Term* t = malloc(sizeof *t);
    t->tag = LAM;
    t->param = p;
    t->body = b;
    return t;
}

static Term* elim(Term* t);

// [v]t → SKI
static Term* bracket(const char* v, Term* t) {
    if (t->tag == VAR)
        return strcmp(v, t->name) == 0
                   ? var("I")
                   : app(var("K"), t); // [v]v = I, [v]x = K x
    if (t->tag == APP)
        return app(
            app(var("S"), bracket(v, t->f)), bracket(v, t->a)
        ); // [v](p q) = S ([v]p) ([v]q)
    fprintf(stderr, "tf did you just do\n");
    exit(1);
}

// Eliminate the λs.
static Term* elim(Term* t) {
    switch (t->tag) {
        case VAR: return t;
        case APP: return app(elim(t->f), elim(t->a));
        case LAM: return bracket(t->param, elim(t->body));
    }
    return NULL;
}

// Man I love how C provides such a rich standard library for strings.
typedef struct {
    char* buf;
    size_t len, cap;
} Str;

static void sb_init(Str* s) {
    s->buf = NULL;
    s->len = s->cap = 0;
}

static void sb_putc(Str* s, char c) {
    if (s->len + 1 >= s->cap) {
        s->cap = s->cap ? s->cap * 2 : 256;
        s->buf = realloc(s->buf, s->cap);
    }
    s->buf[s->len++] = c;
    s->buf[s->len] = 0;
}

static void sb_puts(Str* s, const char* p) {
    while (*p) sb_putc(s, *p++);
}

static void spit_out(Str* s, Term* t) {
    switch (t->tag) {
        case VAR: sb_puts(s, t->name); return;
        case APP:
            sb_puts(s, "{call ");
            spit_out(s, t->f);
            sb_putc(s, ' ');
            spit_out(s, t->a);
            sb_putc(s, '}');
            return;
        default: fprintf(stderr, "Tried to spit out a lambda D:\n"); exit(1);
    }
}

int main(void) {
    // First we construct the z combinator in SKI...
    Term* z =
        lam("f",
            app(lam("x", app(var("f"),
                             lam("v", app(app(var("x"), var("x")), var("v"))))),
                lam("x", app(var("f"), lam("v", app(app(var("x"), var("x")),
                                                    var("v")))))));
    Term* z_ski = elim(z);
    Str z_txt;
    sb_init(&z_txt);
    spit_out(&z_txt, z_ski);

    // Then print the factorial function using it.
    printf(
        "{with {I {fun {x} x}} "
        "{with {K {fun {x} {fun {y} x}}} "
        "{with {S {fun {f} {fun {g} {fun {x} {call {call f x} {call g x}}}}}} "
        "{with {Z %s} " // <<<< Z combinator goes here.
        "{with {fact {call Z {fun {f} {fun {n} {if0 n 1 {* n {call f {- n "
        "1}}}}}}}} "
        "{call fact 5}}}}}}\n",
        z_txt.buf
    );

    free(z_txt.buf);
    return 0;
}