/* Lean 4 → C transpilation: SupportIsSearch.Contextual.Encoding
 * Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: SupportIsSearch/Contextual/Encoding.lean (28 lines)
 *
 * CPS (continuation-passing style) encoding of IPL formulas as goals.
 * This is the key insight of the paper: reading semantic clauses in CPS
 * reveals that quantifiers are eigenvariables, not domain-ranging.
 */

#include "ipl.c"

/* Helper: create goals */
static Goal *mk_atom_goal(AtomVar v) {
    Goal *g = malloc(sizeof(Goal)); g->tag = GOAL_ATOM; g->atom = v; return g;
}
static Goal *mk_imp_goal(Goal *l, Goal *r) {
    Goal *g = malloc(sizeof(Goal)); g->tag = GOAL_IMP; g->imp.lhs = l; g->imp.rhs = r; return g;
}
static Goal *mk_all_goal(Goal *body) {
    Goal *g = malloc(sizeof(Goal)); g->tag = GOAL_ALL; g->body = body; return g;
}

/*
 * encode : IPL → Goal
 *
 * atom p       ↦  atom p
 * bot          ↦  ∀x. x                     (Church encoding of falsity)
 * conj φ ψ    ↦  ∀k. (⟦φ⟧ → ⟦ψ⟧ → k) → k  (CPS pair)
 * disj φ ψ    ↦  ∀k. (⟦φ⟧ → k) → (⟦ψ⟧ → k) → k  (CPS sum)
 * imp φ ψ     ↦  ⟦φ⟧ → ⟦ψ⟧                 (directly structural)
 */
Goal *encode(IPL *phi) {
    if (!phi) return NULL;
    switch (phi->tag) {
        case IPL_ATOM:
            return mk_atom_goal((AtomVar){ .tag = ATOMVAR_ATOM, .atom = phi->atom });
        case IPL_BOT:
            /* ∀x. x — i.e. forall (bvar 0) */
            return mk_all_goal(mk_atom_goal((AtomVar){ .tag = ATOMVAR_BVAR, .bvar = 0 }));
        case IPL_CONJ: {
            /* ∀k. (⟦φ⟧ → ⟦ψ⟧ → k) → k */
            Goal *k = mk_atom_goal((AtomVar){ .tag = ATOMVAR_BVAR, .bvar = 0 });
            Goal *ephi = encode(phi->binary.left);
            Goal *epsi = encode(phi->binary.right);
            Goal *inner = mk_imp_goal(ephi, mk_imp_goal(epsi, k));
            Goal *k2 = mk_atom_goal((AtomVar){ .tag = ATOMVAR_BVAR, .bvar = 0 });
            return mk_all_goal(mk_imp_goal(inner, k2));
        }
        case IPL_DISJ: {
            /* ∀k. (⟦φ⟧ → k) → (⟦ψ⟧ → k) → k */
            Goal *k = mk_atom_goal((AtomVar){ .tag = ATOMVAR_BVAR, .bvar = 0 });
            Goal *ephi = encode(phi->binary.left);
            Goal *epsi = encode(phi->binary.right);
            Goal *branch_l = mk_imp_goal(ephi, k);
            Goal *k2 = mk_atom_goal((AtomVar){ .tag = ATOMVAR_BVAR, .bvar = 0 });
            Goal *branch_r = mk_imp_goal(epsi, k2);
            Goal *k3 = mk_atom_goal((AtomVar){ .tag = ATOMVAR_BVAR, .bvar = 0 });
            return mk_all_goal(mk_imp_goal(branch_l, mk_imp_goal(branch_r, k3)));
        }
        case IPL_IMP:
            return mk_imp_goal(encode(phi->binary.left), encode(phi->binary.right));
    }
    return NULL;
}

/* encodeBase: encode an atomic base as a program of atom goals */
Program encode_base(Atom *atoms, size_t n) {
    if (n == 0) return NULL;
    ProgramNode *head = malloc(sizeof(ProgramNode));
    head->head = mk_atom_goal((AtomVar){ .tag = ATOMVAR_ATOM, .atom = atoms[n - 1] });
    head->tail = (n > 1) ? encode_base(atoms, n - 1) : NULL;
    return head;
}