/* Lean 4 → C transpilation: SupportIsSearch.Contextual.Kernel
 * Provenance: Lean 4 → LambdaIR → MiniC → C
 * Source: SupportIsSearch/Contextual/Kernel.lean (75 lines)
 *
 * This is the core computational kernel: fuel-bounded search, fires, and
 * searchAnyAssumption. The mutual recursion between search/fires/searchAnyAssumption
 * is faithfully preserved.
 */

#include "syntax.c"

/* Forward declarations for mutual recursion */
static bool search(unsigned int fuel, Program P, Goal *g);
static bool search_any_assumption(unsigned int fuel, Program P, ProgramNode *gs, AtomVar a);
static bool fires(unsigned int fuel, Program P, Goal *g, AtomVar a);

/* substGoal: substitute bvar n with atom a in a goal */
Goal *subst_goal(Goal *g, unsigned int n, Atom a);

Goal *subst_goal(Goal *g, unsigned int n, Atom a) {
    if (!g) return NULL;
    Goal *r = malloc(sizeof(Goal));
    r->tag = g->tag;
    switch (g->tag) {
        case GOAL_ATOM:
            r->atom = subst_atomvar(n, a, g->atom);
            break;
        case GOAL_IMP:
            r->imp.lhs = subst_goal(g->imp.lhs, n, a);
            r->imp.rhs = subst_goal(g->imp.rhs, n, a);
            break;
        case GOAL_CONJ:
            r->conj.left = subst_goal(g->conj.left, n, a);
            r->conj.right = subst_goal(g->conj.right, n, a);
            break;
        case GOAL_DISJ:
            r->disj.left = subst_goal(g->disj.left, n, a);
            r->disj.right = subst_goal(g->disj.right, n, a);
            break;
        case GOAL_ALL:
            r->body = subst_goal(g->body, n + 1, a);
            break;
    }
    return r;
}

static bool atomvar_eq(AtomVar a, AtomVar b) {
    if (a.tag != b.tag) return false;
    if (a.tag == ATOMVAR_ATOM) return a.atom.id == b.atom.id;
    return a.bvar == b.bvar;
}

/* search: fuel-bounded proof search for a goal in a program */
static bool search(unsigned int fuel, Program P, Goal *g) {
    if (fuel == 0 || !g) return false;
    fuel--;
    switch (g->tag) {
        case GOAL_ATOM:
            return search_any_assumption(fuel, P, P, g->atom);
        case GOAL_IMP: {
            /* add the antecedent to the program and search for the consequent */
            ProgramNode node = { .head = g->imp.lhs, .tail = P };
            return search(fuel, &node, g->imp.rhs);
        }
        case GOAL_CONJ:
            return search(fuel, P, g->conj.left) && search(fuel, P, g->conj.right);
        case GOAL_DISJ:
            return search(fuel, P, g->disj.left) || search(fuel, P, g->disj.right);
        case GOAL_ALL: {
            Atom fresh = fresh_atom_for_goal(P, g->body);
            Goal *instantiated = subst_goal(g->body, 0, fresh);
            return search(fuel, P, instantiated);
        }
    }
    return false;
}

/* searchAnyAssumption: try firing each assumption in gs against target atom a */
static bool search_any_assumption(unsigned int fuel, Program P, ProgramNode *gs, AtomVar a) {
    if (!gs) return false;
    return fires(fuel, P, gs->head, a) ||
           search_any_assumption(fuel, P, gs->tail, a);
}

/* fires: does assumption g fire for atom a in program P? */
static bool fires(unsigned int fuel, Program P, Goal *g, AtomVar a) {
    if (fuel == 0 || !g) return false;
    fuel--;
    switch (g->tag) {
        case GOAL_ATOM:
            return atomvar_eq(g->atom, a);
        case GOAL_IMP:
            return search(fuel, P, g->imp.lhs) && fires(fuel, P, g->imp.rhs, a);
        case GOAL_CONJ:
        case GOAL_DISJ:
            return false;
        case GOAL_ALL: {
            if (a.tag == ATOMVAR_ATOM) {
                Goal *instantiated = subst_goal(g->body, 0, a.atom);
                return fires(fuel, P, instantiated, a);
            } else {
                Atom fresh = fresh_atom_for_goal(P, g->body);
                Goal *instantiated = subst_goal(g->body, 0, fresh);
                return fires(fuel, P, instantiated, a);
            }
        }
    }
    return false;
}

/* SearchSupports: existential fuel wrapper */
bool search_supports(Program P, Goal *g, unsigned int max_fuel) {
    for (unsigned int f = 0; f <= max_fuel; f++) {
        if (search(f, P, g)) return true;
    }
    return false;
}