// core.el — the math floor, rewritten in El (first principles).
// The constructor, the state space, ordered roles — the same relatives
// the substrate was verified with, now expressed in the language itself.

// term: a structural value is an atom "0"|"1" or a list ["R", a, b]
fn atom0() -> [String] { return ["0"] }
fn atom1() -> [String] { return ["1"] }
fn is_atom(t: [String]) -> Bool { return str_eq(native_list_get(t, 0), "R") == false }
fn is_zero(t: [String]) -> Bool { return is_atom(t) && str_eq(native_list_get(t, 0), "0") }
fn is_unit(t: [String]) -> Bool { return is_atom(t) && str_eq(native_list_get(t, 0), "1") }

// constructor — REFUSES impossible terms (distinct operands only)
fn R(a: [String], b: [String]) -> [String] {
    if str_eq(native_list_get(a, 0), "0") && str_eq(native_list_get(b, 0), "0") { return ["ERROR"] }
    if str_eq(native_list_get(a, 0), "1") && str_eq(native_list_get(b, 0), "1") { return ["ERROR"] }
    let t: [String] = native_list_empty()
    let t = native_list_append(t, "R")
    let t = native_list_append(t, native_list_get(a, 0))
    let t = native_list_append(t, native_list_get(b, 0))
    return t
}

// term equality by serialization (canonical string of the structure)
fn term_str(t: [String]) -> String {
    let n: Int = native_list_len(t)
    if n == 1 { return native_list_get(t, 0) }
    let out: String = "R("
    let out = str_concat(out, str_concat(native_list_get(t, 1), ","))
    let out = str_concat(out, str_concat(native_list_get(t, 2), ")"))
    return out
}
fn term_eq(a: [String], b: [String]) -> Bool { return str_eq(term_str(a), term_str(b)) }

// ordered-role recovery (P-012): defined only on Im(R)
fn L(t: [String]) -> [String] {
    if is_atom(t) { return ["ERROR"] }
    return [native_list_get(t, 1)]
}
fn RR(t: [String]) -> [String] {
    if is_atom(t) { return ["ERROR"] }
    return [native_list_get(t, 2)]
}

fn main() -> Void {
    let z: [String] = atom0()
    let u: [String] = atom1()
    let r1: [String] = R(z, u)
    println(term_str(r1))
    println(term_str(L(r1)))
    println(term_str(RR(r1)))
    println(term_eq(L(r1), z))
}