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

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

/* Atom: identified by a natural number */
typedef struct { unsigned int id; } Atom;

/* AtomVar: either a concrete atom or a de Bruijn bound variable */
typedef enum { ATOMVAR_ATOM, ATOMVAR_BVAR } AtomVarTag;
typedef struct {
    AtomVarTag tag;
    union {
        Atom atom;
        unsigned int bvar;
    };
} AtomVar;

/* Goal: the goal language for the contextual kernel */
typedef enum { GOAL_ATOM, GOAL_IMP, GOAL_CONJ, GOAL_DISJ, GOAL_ALL } GoalTag;
typedef struct Goal {
    GoalTag tag;
    union {
        AtomVar atom;
        struct { struct Goal *lhs; struct Goal *rhs; } imp;
        struct { struct Goal *left; struct Goal *right; } conj;
        struct { struct Goal *left; struct Goal *right; } disj;
        struct Goal *body; /* all */
    };
} Goal;

/* Program: a list of goals */
typedef struct ProgramNode {
    Goal *head;
    struct ProgramNode *tail;
} ProgramNode;

typedef ProgramNode *Program;

/* substAtomVar: substitute bvar n with atom a */
AtomVar subst_atomvar(unsigned int n, Atom a, AtomVar v) {
    if (v.tag == ATOMVAR_BVAR && v.bvar == n) {
        return (AtomVar){ .tag = ATOMVAR_ATOM, .atom = a };
    }
    return v;
}

/* freshAtomForGoal: compute a fresh atom not in the program or goal */
static unsigned int max_atom_in_atomvar(AtomVar v) {
    return v.tag == ATOMVAR_ATOM ? v.atom.id : 0;
}

static unsigned int max_atom_in_goal(Goal *g) {
    if (!g) return 0;
    switch (g->tag) {
        case GOAL_ATOM: return max_atom_in_atomvar(g->atom);
        case GOAL_IMP: {
            unsigned int l = max_atom_in_goal(g->imp.lhs);
            unsigned int r = max_atom_in_goal(g->imp.rhs);
            return l > r ? l : r;
        }
        case GOAL_CONJ: case GOAL_DISJ: {
            unsigned int l = max_atom_in_goal(g->conj.left);
            unsigned int r = max_atom_in_goal(g->conj.right);
            return l > r ? l : r;
        }
        case GOAL_ALL: return max_atom_in_goal(g->body);
    }
    return 0;
}

static unsigned int max_atom_in_program(Program P) {
    unsigned int m = 0;
    for (ProgramNode *n = P; n; n = n->tail) {
        unsigned int v = max_atom_in_goal(n->head);
        if (v > m) m = v;
    }
    return m;
}

Atom fresh_atom_for_goal(Program P, Goal *g) {
    unsigned int mp = max_atom_in_program(P);
    unsigned int mg = max_atom_in_goal(g);
    return (Atom){ .id = (mp > mg ? mp : mg) + 1 };
}