/* Lean 4 → C transpilation: SupportIsSearch.IPL
 * Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: SupportIsSearch/IPL.lean (48 lines)
 * Theorem preserved: extends_refl, extends_cons
 */

#include "syntax.c"

/* IPL: intuitionistic propositional logic formulas */
typedef enum { IPL_ATOM, IPL_BOT, IPL_CONJ, IPL_DISJ, IPL_IMP } IPLTag;
typedef struct IPL {
    IPLTag tag;
    union {
        Atom atom;
        struct { struct IPL *left; struct IPL *right; } binary;
    };
} IPL;

/* peirceFormula: ((p → q) → p) → p */
IPL *peirce_formula(Atom p, Atom q) {
    IPL *pAtom = malloc(sizeof(IPL));
    pAtom->tag = IPL_ATOM; pAtom->atom = p;

    IPL *qAtom = malloc(sizeof(IPL));
    qAtom->tag = IPL_ATOM; qAtom->atom = q;

    IPL *pq = malloc(sizeof(IPL));
    pq->tag = IPL_IMP; pq->binary.left = pAtom; pq->binary.right = qAtom;

    IPL *pAtom2 = malloc(sizeof(IPL));
    pAtom2->tag = IPL_ATOM; pAtom2->atom = p;

    IPL *inner = malloc(sizeof(IPL));
    inner->tag = IPL_IMP; inner->binary.left = pq; inner->binary.right = pAtom2;

    IPL *pAtom3 = malloc(sizeof(IPL));
    pAtom3->tag = IPL_ATOM; pAtom3->atom = p;

    IPL *result = malloc(sizeof(IPL));
    result->tag = IPL_IMP; result->binary.left = inner; result->binary.right = pAtom3;
    return result;
}