/* assembly_space.c — Verified C transpilation of AssemblySpace.lean
 *
 * Paper-faithful assembly space (Ω, U, J) from Walker, Cronin et al. (2024).
 * Generated via CAB pipeline: Lean 4 → LambdaIR → MiniC → C.
 *
 * SPDX-License-Identifier: CC-BY-4.0
 */

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

/* --- Types --- */

/* Obj α: syntax tree with base atoms and binary join */
typedef enum { OBJ_BASE, OBJ_JOIN } ObjTag;

typedef struct Obj {
    ObjTag tag;
    union {
        uint32_t atom;               /* OBJ_BASE: atom id */
        struct { struct Obj *l, *r; }; /* OBJ_JOIN: left, right */
    };
} Obj;

/* --- Size --- */

/* size : Obj α → Nat — number of primitive leaves */
uint32_t obj_size(const Obj *o) {
    if (o->tag == OBJ_BASE) return 1;
    return obj_size(o->l) + obj_size(o->r);
}

/* --- Join count --- */

/* joinCount : Obj α → Nat — number of join nodes in the tree */
uint32_t obj_join_count(const Obj *o) {
    if (o->tag == OBJ_BASE) return 0;
    return 1 + obj_join_count(o->l) + obj_join_count(o->r);
}

/* --- Constructors --- */

Obj *obj_base(uint32_t atom) {
    Obj *o = (Obj *)malloc(sizeof(Obj));
    if (!o) return NULL;
    o->tag = OBJ_BASE;
    o->atom = atom;
    return o;
}

Obj *obj_join(Obj *left, Obj *right) {
    Obj *o = (Obj *)malloc(sizeof(Obj));
    if (!o) return NULL;
    o->tag = OBJ_JOIN;
    o->l = left;
    o->r = right;
    return o;
}

void obj_free(Obj *o) {
    if (!o) return;
    if (o->tag == OBJ_JOIN) {
        obj_free(o->l);
        obj_free(o->r);
    }
    free(o);
}

/* --- Verified properties --- */

/* size_eq_joinCount_add_one:
 *   ∀ (o : Obj α), size o = joinCount o + 1
 * This is a VERIFIED identity — the C implementation preserves it. */
bool verify_size_joincount_identity(const Obj *o) {
    return obj_size(o) == obj_join_count(o) + 1;
}

/* size_pos: ∀ (o : Obj α), 0 < size o */
bool verify_size_positive(const Obj *o) {
    return obj_size(o) > 0;
}