From 4d6853a0efb1489b6a1083eab71622ba9bf660cd Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Thu, 30 Apr 2026 15:15:50 -0600 Subject: [PATCH] REL1 Inductive.lean + Rust dispatch + 9 new smoke tests (25/25 + 46/46) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Inductive.lean (new module): schema combinators (mkSchema, mkCtor, mkPath) and canonical schema instances: - Plain inductives: natSchema, boolSchema, listSchema - HITs: s1Schema, intervalSchema, propTruncSchema Plus type-level helpers (CType.natC, listC, s1C, …) and term-level ergonomic builders (zeroC, succC, nilC, consC, baseC, loopC, …, natLit, natElim, boolElim, listElim). Rust kernel (native/cubical/src/): · tags.rs — TY_IND, TERM_DIMEXPR/CTOR/INDELIM, VAL_VCTOR/VDIMEXPR, NEU_NINDELIM tag constants per docs/INDUCTIVE_TYPES.md §6. · value.rs — mk_vctor, mk_vdimexpr, mk_nindelim builders. · eval.rs — TERM_DIMEXPR / TERM_CTOR / TERM_INDELIM dispatch arms; full β-reduction on canonical vctor target (find matching branch by name, vapp chain over ctor args); stuck nIndElim build for vneu target; eval_term_list / eval_branches / find_branch_body helpers (recursive list walking). · readback.rs — VAL_VCTOR / VAL_VDIMEXPR readback arms; readback_val_list, map_readback_branches helpers; NEU_NINDELIM neutral readback; mk_term_dimexpr, mk_term_ctor, mk_term_indelim builders. Tests (CubicalTransport/FFITest.lean): nine new smoke arms exercising canonical-form eval (zero, succ-of-succ, false, cons-true-nil, base, loop@r), readback round-trip on succ zero, and indElim β on Bool with both branch directions. Result: 25/25 smoke + 46/46 properties = 71/71 passing. Existing tests untouched (constructor tags preserved per REL1 freeze). Rust ABI version is now de facto v2 (new tags); update the TOPOLEI_FFI_ABI_VERSION constant in a follow-up commit. Remaining REL1 work (per task list): - #4 HasType arms for ctor / indElim - #8 transport over .ind axioms - #9 composition over .ind axioms - Path-ctor boundary firing (REL1.1) - Recursive-arg IH wiring in indElim β (REL1.1) - Topolei migration (sibling repo) per docs/INDUCTIVE_TYPES.md §9.1 Co-Authored-By: Claude Opus 4.7 (1M context) --- CubicalTransport.lean | 1 + CubicalTransport/FFITest.lean | 36 ++++- CubicalTransport/Inductive.lean | 265 ++++++++++++++++++++++++++++++++ native/cubical/src/eval.rs | 125 +++++++++++++++ native/cubical/src/readback.rs | 112 ++++++++++++++ native/cubical/src/tags.rs | 29 ++-- native/cubical/src/value.rs | 38 +++++ 7 files changed, 594 insertions(+), 12 deletions(-) create mode 100644 CubicalTransport/Inductive.lean diff --git a/CubicalTransport.lean b/CubicalTransport.lean index 829fad9..fc59ac2 100644 --- a/CubicalTransport.lean +++ b/CubicalTransport.lean @@ -19,4 +19,5 @@ import CubicalTransport.TransportLaws import CubicalTransport.System import CubicalTransport.CompLaws import CubicalTransport.Soundness +import CubicalTransport.Inductive import CubicalTransport.PropertyTest diff --git a/CubicalTransport/FFITest.lean b/CubicalTransport/FFITest.lean index e01c19a..583e598 100644 --- a/CubicalTransport/FFITest.lean +++ b/CubicalTransport/FFITest.lean @@ -20,6 +20,10 @@ import CubicalTransport.Readback import CubicalTransport.FFI +import CubicalTransport.Inductive + +open CubicalTransport.Inductive +open CubicalTransport.Inductive.CTerm namespace CubicalTransportFFITest @@ -139,7 +143,37 @@ def tests : List (String × String × String) := cvalSummary (vPApp (.vPathTransp .nil ⟨"i"⟩ .univ (.var "a0") (.var "b0") .bot (.var "p")) (.var ⟨"r"⟩)), - "vneu ncompN") ] + "vneu ncompN"), + -- ── REL1 inductive-type smoke tests ───────────────────────────────────── + ("eval (zero : Nat) ⇓ vctor zero", + cvalSummary (eval .nil zeroC), + "vctor zero ..."), + ("eval (succ (succ zero) : Nat) ⇓ vctor succ", + cvalSummary (eval .nil (succC (succC zeroC))), + "vctor succ ..."), + ("eval (false : Bool) ⇓ vctor false", + cvalSummary (eval .nil falseC), + "vctor false ..."), + ("eval (cons true nil : List Bool) ⇓ vctor cons", + cvalSummary (eval .nil (consC CType.boolC trueC (nilC CType.boolC))), + "vctor cons ..."), + ("readback ∘ eval (succ zero : Nat) ≡ ctor succ", + ctermSummary (readback (eval .nil (succC zeroC))), + "ctor succ ..."), + ("eval (base : S¹) ⇓ vctor base", + cvalSummary (eval .nil baseC), + "vctor base ..."), + ("eval (loop @ r : S¹) ⇓ vctor loop", + cvalSummary (eval .nil (loopC (.var ⟨"r"⟩))), + "vctor loop ..."), + ("indElim Bool false-case (true → \"yes\") on true ⇓ \"yes\"", + cvalSummary (eval .nil + (boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") trueC)), + "vneu nvar yes"), + ("indElim Bool true-case on false ⇓ \"no\"", + cvalSummary (eval .nil + (boolElim (.lam "x" (.var "M")) (.var "no") (.var "yes") falseC)), + "vneu nvar no") ] /-- Run every smoke test, print its actual vs expected. Returns the number of failures. -/ diff --git a/CubicalTransport/Inductive.lean b/CubicalTransport/Inductive.lean new file mode 100644 index 0000000..0459dec --- /dev/null +++ b/CubicalTransport/Inductive.lean @@ -0,0 +1,265 @@ +/- + CubicalTransport.Inductive + ========================== + Helper combinators and canonical schema instances for the REL1 + schema-based inductive (and higher-inductive) type system. + + This module sits *on top of* `Syntax.lean` — it doesn't add new + primitives, only ergonomic builders. Every value here is a plain + CTypeSchema / CType / CTerm; nothing is opaque. Downstream + consumers should prefer these helpers over hand-spelling + CTypeSchema literals so the canonical encodings are maintained + in one place. + + ## Sections + + · §1 Argument-shape helpers + · §2 Schema constructors (mkSchema, mkCtor, mkPath) + · §3 Type-level helpers (CType.list, CType.nat, …, CType.s1, …) + · §4 Term-level helpers (zeroC, succC, nilC, consC, baseC, loopC, …) + · §5 Eliminator builders (natElim, listElim, …) + + ## Design notes + + · Boundary clauses inside HIT path constructors reference *dim args* + via `DimVar.mk "$d_k"` (zero-indexed among `.dim` args) and + *non-dim args* via `CTerm.var "$arg_k"` (zero-indexed in the full + arg list). See INDUCTIVE_TYPES.md §4 for the discipline. + + · The schemas here are concrete values, not `def`s under a + `noncomputable` veil — `Nat`, `Bool`, etc. are first-class data + that downstream code can pattern-match on or use as parameters. +-/ + +import CubicalTransport.Syntax + +namespace CubicalTransport.Inductive + +-- ── §1. Argument-shape helpers ───────────────────────────────────────────── + +/-- A non-recursive argument of a closed CType. -/ +@[inline] def argType (A : CType) : CTypeArg := .type A + +/-- A reference to the schema's `i`th type parameter. -/ +@[inline] def argParam (i : Nat) : CTypeArg := .param i + +/-- A recursive argument of the inductive being defined. -/ +@[inline] def argSelf : CTypeArg := .self + +/-- A dimension argument (path-constructor binder). -/ +@[inline] def argDim : CTypeArg := .dim + +-- ── §2. Schema constructors ──────────────────────────────────────────────── + +/-- A point constructor (no boundary system, empty boundary list). -/ +@[inline] def mkCtor (name : String) (args : List CTypeArg) : CtorSpec := + .mk name args [] + +/-- A path constructor: a constructor whose argument list contains at + least one `.dim` arg, and whose boundary system specifies the + canonical reduction on the corresponding cube faces. -/ +@[inline] def mkPath (name : String) (args : List CTypeArg) + (boundary : List (FaceFormula × CTerm)) : CtorSpec := + .mk name args boundary + +/-- Build a schema from name, parameter count, and constructor list. -/ +@[inline] def mkSchema (name : String) (numParams : Nat) + (ctors : List CtorSpec) : CTypeSchema := + .mk name numParams ctors + +-- ── §3. Canonical plain inductive schemas ────────────────────────────────── + +/-- The natural numbers as a schema. + + `Nat` has two point constructors: + - `zero : Nat` + - `succ : Nat → Nat` (recursive arg: `.self`) +-/ +def natSchema : CTypeSchema := + mkSchema "Nat" 0 + [ mkCtor "zero" [] + , mkCtor "succ" [.self] ] + +/-- The booleans as a schema. -/ +def boolSchema : CTypeSchema := + mkSchema "Bool" 0 + [ mkCtor "false" [] + , mkCtor "true" [] ] + +/-- Polymorphic lists as a schema, parameterised by the element type. -/ +def listSchema : CTypeSchema := + mkSchema "List" 1 + [ mkCtor "nil" [] + , mkCtor "cons" [.param 0, .self] ] + +-- ── §4. Canonical HIT schemas ────────────────────────────────────────────── + +/-- The circle `S¹` as a HIT. + + Constructors: + - `base : S¹` (point) + - `loop : (i : I) → S¹` (path: `loop @ 0 = base = loop @ 1`) + + Boundary: at `i=0` and `i=1`, `loop` returns `base`. + + The `loop` boundary references `base` via the schema's own + `.ctor` constructor at the same schema (recursive self-reference + inside the schema's body). We construct it inline here. -/ +def s1Schema : CTypeSchema := + -- Build a self-referential schema: `loop`'s boundary uses + -- `.ctor s1Schema "base" [] []` which in turn references `s1Schema`. + -- Since the recursion is structural through the schema's data + -- (not through a Lean-level fixpoint), we define `s1Schema` via + -- Lean's well-founded recursion through structural data; the + -- result is a finite, well-formed `CTypeSchema` value — but Lean + -- won't accept a literal self-recursive `def` like this. + -- + -- Workaround: take the schema *name* + a fresh local schema that + -- refers to itself via a placeholder. At construction time we + -- patch the placeholder. This is implemented as a small fix-up + -- below. + let baseAt (s : CTypeSchema) : CTerm := .ctor s "base" [] [] + -- We need `s1Schema = mkSchema "S¹" 0 [base, loop]` where + -- `loop` carries a boundary that references `s1Schema`. + -- Lean's `let rec` doesn't handle this for `CTypeSchema` the + -- way it would for a function — but we can use a `where`-style + -- two-step build: first build a "stub" schema, then build the + -- final `loop` referring to it. Both schemas have the same + -- structural shape, so `s1Schema` is well-defined. + let stub : CTypeSchema := + mkSchema "S¹" 0 + [ mkCtor "base" [] + , mkPath "loop" [.dim] [] ] + let d : DimVar := ⟨"$d_0"⟩ + mkSchema "S¹" 0 + [ mkCtor "base" [] + , mkPath "loop" [.dim] + [ (.eq0 d, baseAt stub) + , (.eq1 d, baseAt stub) ] ] + +/-- The interval as a HIT. + + Constructors: + - `zero : I` + - `one : I` + - `seg : (i : I) → I` with `seg @ 0 = zero`, `seg @ 1 = one`. -/ +def intervalSchema : CTypeSchema := + let stub : CTypeSchema := + mkSchema "I" 0 + [ mkCtor "zero" [] + , mkCtor "one" [] + , mkPath "seg" [.dim] [] ] + let zeroAt (s : CTypeSchema) : CTerm := .ctor s "zero" [] [] + let oneAt (s : CTypeSchema) : CTerm := .ctor s "one" [] [] + let d : DimVar := ⟨"$d_0"⟩ + mkSchema "I" 0 + [ mkCtor "zero" [] + , mkCtor "one" [] + , mkPath "seg" [.dim] + [ (.eq0 d, zeroAt stub) + , (.eq1 d, oneAt stub) ] ] + +/-- Propositional truncation `‖A‖₋₁` as a HIT. + + Constructors: + - `inT : A → ‖A‖₋₁` (point) + - `squash : (x y : ‖A‖₋₁) → (i : I) → ‖A‖₋₁` + with `squash x y @ 0 = x`, `squash x y @ 1 = y`. -/ +def propTruncSchema : CTypeSchema := + let d : DimVar := ⟨"$d_0"⟩ + -- arg index: 0 = first .self ("$arg_0"), 1 = second .self ("$arg_1"), + -- 2 = .dim ($d_0). Boundary references positional arg names. + mkSchema "‖_‖₋₁" 1 + [ mkCtor "inT" [.param 0] + , mkPath "squash" [.self, .self, .dim] + [ (.eq0 d, .var "$arg_0") + , (.eq1 d, .var "$arg_1") ] ] + +-- ── §5. Type-level helpers ───────────────────────────────────────────────── + +/-- The `CType` for natural numbers. -/ +@[inline] def CType.natC : CType := .ind natSchema [] + +/-- The `CType` for booleans. -/ +@[inline] def CType.boolC : CType := .ind boolSchema [] + +/-- The `CType` for lists with element type `A`. -/ +@[inline] def CType.listC (A : CType) : CType := .ind listSchema [A] + +/-- The `CType` for the circle. -/ +@[inline] def CType.s1C : CType := .ind s1Schema [] + +/-- The `CType` for the interval. -/ +@[inline] def CType.intervalC : CType := .ind intervalSchema [] + +/-- The `CType` for propositional truncation `‖A‖₋₁`. -/ +@[inline] def CType.propTruncC (A : CType) : CType := + .ind propTruncSchema [A] + +-- ── §6. Term-level helpers ───────────────────────────────────────────────── + +namespace CTerm + +/-- The `CTerm` `zero : Nat`. -/ +@[inline] def zeroC : CTerm := .ctor natSchema "zero" [] [] + +/-- The `CTerm` `succ n` for a given `n : Nat`. -/ +@[inline] def succC (n : CTerm) : CTerm := .ctor natSchema "succ" [] [n] + +/-- The `CTerm` `false : Bool`. -/ +@[inline] def falseC : CTerm := .ctor boolSchema "false" [] [] + +/-- The `CTerm` `true : Bool`. -/ +@[inline] def trueC : CTerm := .ctor boolSchema "true" [] [] + +/-- The `CTerm` `nil : List A`. Carries the element type as parameter. -/ +@[inline] def nilC (A : CType) : CTerm := .ctor listSchema "nil" [A] [] + +/-- The `CTerm` `cons x xs : List A`. -/ +@[inline] def consC (A : CType) (x xs : CTerm) : CTerm := + .ctor listSchema "cons" [A] [x, xs] + +/-- The `CTerm` `base : S¹`. -/ +@[inline] def baseC : CTerm := .ctor s1Schema "base" [] [] + +/-- The `CTerm` `loop @ r : S¹` where `r : DimExpr`. -/ +@[inline] def loopC (r : DimExpr) : CTerm := + .ctor s1Schema "loop" [] [.dimExpr r] + +/-- The `CTerm` `inT a : ‖A‖₋₁`. -/ +@[inline] def inTC (A : CType) (a : CTerm) : CTerm := + .ctor propTruncSchema "inT" [A] [a] + +/-- The `CTerm` `squash x y @ r : ‖A‖₋₁`. -/ +@[inline] def squashC (A : CType) (x y : CTerm) (r : DimExpr) : CTerm := + .ctor propTruncSchema "squash" [A] [x, y, .dimExpr r] + +/-- Build a Nat literal `n` as a tower of `succ`s on `zero`. -/ +def natLit : Nat → CTerm + | 0 => zeroC + | n + 1 => succC (natLit n) + +end CTerm + +-- ── §7. Eliminator builders ──────────────────────────────────────────────── + +/-- Build an `indElim` for `Nat`. `motive` is the result type-former, + `caseZero` the body for `zero`, `caseSucc` the body for `succ` + (curried as `λ pred ih. body`). `target` is the natural being + eliminated. -/ +def natElim (motive caseZero caseSucc target : CTerm) : CTerm := + .indElim natSchema [] motive + [("zero", caseZero), ("succ", caseSucc)] target + +/-- Build an `indElim` for `Bool`. -/ +def boolElim (motive caseFalse caseTrue target : CTerm) : CTerm := + .indElim boolSchema [] motive + [("false", caseFalse), ("true", caseTrue)] target + +/-- Build an `indElim` for `List A`. `caseCons` is curried as + `λ head tail ih. body`. -/ +def listElim (A : CType) (motive caseNil caseCons target : CTerm) : CTerm := + .indElim listSchema [A] motive + [("nil", caseNil), ("cons", caseCons)] target + +end CubicalTransport.Inductive diff --git a/native/cubical/src/eval.rs b/native/cubical/src/eval.rs index fca4f92..98b74a8 100644 --- a/native/cubical/src/eval.rs +++ b/native/cubical/src/eval.rs @@ -205,10 +205,135 @@ pub fn eval(env: LeanObj, t: LeanObj) -> LeanObjMut { } } } + TERM_DIMEXPR => { + // .dimExpr r — lift to .vdimExpr r. + let r = ctor_field(t, 0); + retain(r); + mk_vdimexpr(r) + } + TERM_CTOR => { + // .ctor S c params args — produce canonical .vctor with each + // arg evaluated. Path-ctor boundary firing is REL1.1 work. + let schema = ctor_field(t, 0); + let name = ctor_field(t, 1); + let params = ctor_field(t, 2); + let args_term = ctor_field(t, 3); + retain(schema); retain(name); retain(params); + let args_val = eval_term_list(env, args_term); + mk_vctor(schema, name, params, args_val as LeanObj) + } + TERM_INDELIM => { + // .indElim S params motive branches target — β-reduce on a + // canonical vctor target; otherwise build .nIndElim stuck. + let schema = ctor_field(t, 0); + let params = ctor_field(t, 1); + let motive = ctor_field(t, 2); + let branches = ctor_field(t, 3); + let target = ctor_field(t, 4); + let target_val = eval(env, target); + let target_tag = ctor_tag(target_val as LeanObj); + if target_tag == VAL_VCTOR { + // Canonical β: find branch matching the ctor's name, + // apply branch body to each ctor arg via vapp chain. + let ctor_name = ctor_field(target_val as LeanObj, 1); + let ctor_args = ctor_field(target_val as LeanObj, 3); + match find_branch_body(branches, ctor_name) { + Some(body) => { + retain(body); + let mut acc = eval(env, body); + let mut cur = ctor_args; + while ctor_tag(cur) == 1 { + let head = ctor_field(cur, 0); + retain(head); + acc = vapp(acc, head as LeanObjMut); + cur = ctor_field(cur, 1); + } + release(target_val as LeanObj); + acc + } + None => { + release(target_val as LeanObj); + stuck_marker(b"\0") + } + } + } else if target_tag == VAL_VNEU { + // Stuck: extract inner neutral, build .nIndElim with + // env-evaluated motive and branches. + let inner_neu = ctor_field(target_val as LeanObj, 0); + retain(inner_neu); + let motive_val = eval(env, motive); + let branches_val = eval_branches(env, branches); + retain(schema); retain(params); + release(target_val as LeanObj); + let nelim = mk_nindelim(schema, params, motive_val as LeanObj, + branches_val as LeanObj, inner_neu); + mk_vneu(nelim as LeanObj) + } else { + release(target_val as LeanObj); + stuck_marker(b"\0") + } + } _ => stuck_marker(b"\0"), } } +/// Walk a Lean `List CTerm`, eval each element, return a new +/// `List CVal`. Cons-list shape: tag 0 = nil, tag 1 = cons (head, tail). +fn eval_term_list(env: LeanObj, terms: LeanObj) -> LeanObjMut { + if ctor_tag(terms) == 0 { + retain(terms); + terms as LeanObjMut + } else { + let head = ctor_field(terms, 0); + let tail = ctor_field(terms, 1); + let head_val = eval(env, head); + let tail_vals = eval_term_list(env, tail); + let cons = alloc_ctor(1, 2); + ctor_set_field(cons, 0, head_val as LeanObj); + ctor_set_field(cons, 1, tail_vals as LeanObj); + cons + } +} + +/// Walk a Lean `List (String × CTerm)`, eval each body, return +/// `List (String × CVal)`. +fn eval_branches(env: LeanObj, brs: LeanObj) -> LeanObjMut { + if ctor_tag(brs) == 0 { + retain(brs); + brs as LeanObjMut + } else { + let head = ctor_field(brs, 0); + let tail = ctor_field(brs, 1); + let name = ctor_field(head, 0); + let body = ctor_field(head, 1); + let body_val = eval(env, body); + retain(name); + let new_pair = alloc_ctor(0, 2); // Prod.mk + ctor_set_field(new_pair, 0, name); + ctor_set_field(new_pair, 1, body_val as LeanObj); + let tail_vals = eval_branches(env, tail); + let cons = alloc_ctor(1, 2); + ctor_set_field(cons, 0, new_pair as LeanObj); + ctor_set_field(cons, 1, tail_vals as LeanObj); + cons + } +} + +/// Look up a branch body in a `List (String × CTerm)` by ctor name. +/// Returns the borrowed CTerm body if found. +fn find_branch_body(brs: LeanObj, target_name: LeanObj) -> Option { + let mut cur = brs; + while ctor_tag(cur) == 1 { + let head = ctor_field(cur, 0); + let name = ctor_field(head, 0); + if unsafe { lean_string_eq(name, target_name) } { + return Some(ctor_field(head, 1)); + } + cur = ctor_field(cur, 1); + } + None +} + // ── vApp ──────────────────────────────────────────────────────────────────── /// `vApp : CVal → CVal → CVal` — function application. diff --git a/native/cubical/src/readback.rs b/native/cubical/src/readback.rs index 428841d..6cdd909 100644 --- a/native/cubical/src/readback.rs +++ b/native/cubical/src/readback.rs @@ -196,6 +196,42 @@ pub(crate) fn mk_term_snd(inner: LeanObj) -> LeanObjMut { ctor } +/// `.dimExpr r` — REL1. +#[inline] +pub(crate) fn mk_term_dimexpr(r: LeanObj) -> LeanObjMut { + let ctor = alloc_ctor(TERM_DIMEXPR, 1); + ctor_set_field(ctor, 0, r); + ctor +} + +/// `.ctor S c params args` — REL1 schema constructor application. +#[inline] +pub(crate) fn mk_term_ctor( + schema: LeanObj, name: LeanObj, params: LeanObj, args: LeanObj, +) -> LeanObjMut { + let ctor = alloc_ctor(TERM_CTOR, 4); + ctor_set_field(ctor, 0, schema); + ctor_set_field(ctor, 1, name); + ctor_set_field(ctor, 2, params); + ctor_set_field(ctor, 3, args); + ctor +} + +/// `.indElim S params motive branches target` — REL1. +#[inline] +pub(crate) fn mk_term_indelim( + schema: LeanObj, params: LeanObj, motive: LeanObj, + branches: LeanObj, target: LeanObj, +) -> LeanObjMut { + let ctor = alloc_ctor(TERM_INDELIM, 5); + ctor_set_field(ctor, 0, schema); + ctor_set_field(ctor, 1, params); + ctor_set_field(ctor, 2, motive); + ctor_set_field(ctor, 3, branches); + ctor_set_field(ctor, 4, target); + ctor +} + /// CType `.univ` — nullary scalar. #[inline] pub(crate) fn mk_ty_univ() -> LeanObjMut { lean_box_mut(TY_UNIV as usize) } @@ -477,6 +513,21 @@ pub fn readback(v: LeanObj) -> LeanObjMut { let bt = readback(b); mk_term_pair(at as LeanObj, bt as LeanObj) } + VAL_VCTOR => { + // `.vctor S c params args` — readback each arg, rebuild .ctor. + let schema = ctor_field(v, 0); + let name = ctor_field(v, 1); + let params = ctor_field(v, 2); + let args_val = ctor_field(v, 3); + retain(schema); retain(name); retain(params); + let args_term = readback_val_list(args_val); + mk_term_ctor(schema, name, params, args_term as LeanObj) + } + VAL_VDIMEXPR => { + let r = ctor_field(v, 0); + retain(r); + mk_term_dimexpr(r) + } _ => { // Malformed — return a marker var. let msg = unsafe { @@ -582,6 +633,21 @@ pub fn readback_neu(n: LeanObj) -> LeanObjMut { let inner_term = readback_neu(inner); mk_term_snd(inner_term as LeanObj) } + NEU_NINDELIM => { + // .nIndElim S params motive branches target — readback to + // .indElim with each branch body read back. + let schema = ctor_field(n, 0); + let params = ctor_field(n, 1); + let motive = ctor_field(n, 2); + let branches = ctor_field(n, 3); + let target = ctor_field(n, 4); + retain(schema); retain(params); + let motive_term = readback(motive); + let branches_term = map_readback_branches(branches); + let target_term = readback_neu(target); + mk_term_indelim(schema, params, motive_term as LeanObj, + branches_term as LeanObj, target_term as LeanObj) + } _ => { let msg = unsafe { lean_mk_string(b"\0".as_ptr() as *const core::ffi::c_char) @@ -591,6 +657,52 @@ pub fn readback_neu(n: LeanObj) -> LeanObjMut { } } +/// Map `readback` over a `List CVal`, producing a `List CTerm` — +/// used to read back the args of a `.vctor`. +fn readback_val_list(vals: LeanObj) -> LeanObjMut { + match ctor_tag(vals) { + LIST_NIL => lean_box_mut(LIST_NIL as usize), + LIST_CONS => { + let head = ctor_field(vals, 0); + let tail = ctor_field(vals, 1); + let head_term = readback(head); + let tail_term = readback_val_list(tail); + let cons = alloc_ctor(LIST_CONS, 2); + ctor_set_field(cons, 0, head_term as LeanObj); + ctor_set_field(cons, 1, tail_term as LeanObj); + cons + } + _ => lean_box_mut(LIST_NIL as usize), + } +} + +/// Map `readback` over a `List (String × CVal)`, producing a +/// `List (String × CTerm)` — used by the `nIndElim` readback arm. +fn map_readback_branches(brs: LeanObj) -> LeanObjMut { + match ctor_tag(brs) { + LIST_NIL => lean_box_mut(LIST_NIL as usize), + LIST_CONS => { + let head = ctor_field(brs, 0); + let name = ctor_field(head, 0); + let body_val = ctor_field(head, 1); + let tail = ctor_field(brs, 1); + + retain(name); + let body_term = readback(body_val); + let new_pair = alloc_ctor(PROD_MK, 2); + ctor_set_field(new_pair, 0, name); + ctor_set_field(new_pair, 1, body_term as LeanObj); + + let new_tail = map_readback_branches(tail); + let new_cons = alloc_ctor(LIST_CONS, 2); + ctor_set_field(new_cons, 0, new_pair as LeanObj); + ctor_set_field(new_cons, 1, new_tail as LeanObj); + new_cons + } + _ => lean_box_mut(LIST_NIL as usize), + } +} + /// Map `readback` over a `List (FaceFormula × CVal)`, producing a /// `List (FaceFormula × CTerm)` for use in a `.compN`. fn map_readback_clauses(clauses: LeanObj) -> LeanObjMut { diff --git a/native/cubical/src/tags.rs b/native/cubical/src/tags.rs index 9d67838..c5903e3 100644 --- a/native/cubical/src/tags.rs +++ b/native/cubical/src/tags.rs @@ -31,6 +31,7 @@ pub const TY_PI: u32 = 1; pub const TY_PATH: u32 = 2; pub const TY_SIGMA: u32 = 3; pub const TY_GLUE: u32 = 4; +pub const TY_IND: u32 = 5; // REL1: schema-based inductive type // ── CTerm (Cubical/Syntax.lean) ──────────────────────────────────────────── @@ -47,6 +48,9 @@ pub const TERM_UNGLUE: u32 = 9; pub const TERM_PAIR: u32 = 10; pub const TERM_FST: u32 = 11; pub const TERM_SND: u32 = 12; +pub const TERM_DIMEXPR: u32 = 13; // REL1: dim expression lifted to CTerm +pub const TERM_CTOR: u32 = 14; // REL1: schema constructor application +pub const TERM_INDELIM: u32 = 15; // REL1: inductive eliminator // ── CEnv (Cubical/Value.lean) ────────────────────────────────────────────── @@ -64,17 +68,20 @@ pub const VAL_VTUBEAPP: u32 = 5; pub const VAL_VCOMPFUN: u32 = 6; pub const VAL_VPATHTRANSP: u32 = 7; pub const VAL_VPAIR: u32 = 8; +pub const VAL_VCTOR: u32 = 9; // REL1: canonical schema-ctor value +pub const VAL_VDIMEXPR: u32 = 10; // REL1: lifted dim-expression value // ── CNeu (Cubical/Value.lean) ────────────────────────────────────────────── -pub const NEU_NVAR: u32 = 0; -pub const NEU_NAPP: u32 = 1; -pub const NEU_NPAPP: u32 = 2; -pub const NEU_NTRANSP: u32 = 3; -pub const NEU_NCOMP: u32 = 4; -pub const NEU_NHCOMP: u32 = 5; -pub const NEU_NCOMPN: u32 = 6; -pub const NEU_NGLUEIN: u32 = 7; -pub const NEU_NUNGLUE: u32 = 8; -pub const NEU_NFST: u32 = 9; -pub const NEU_NSND: u32 = 10; +pub const NEU_NVAR: u32 = 0; +pub const NEU_NAPP: u32 = 1; +pub const NEU_NPAPP: u32 = 2; +pub const NEU_NTRANSP: u32 = 3; +pub const NEU_NCOMP: u32 = 4; +pub const NEU_NHCOMP: u32 = 5; +pub const NEU_NCOMPN: u32 = 6; +pub const NEU_NGLUEIN: u32 = 7; +pub const NEU_NUNGLUE: u32 = 8; +pub const NEU_NFST: u32 = 9; +pub const NEU_NSND: u32 = 10; +pub const NEU_NINDELIM: u32 = 11; // REL1: stuck inductive eliminator diff --git a/native/cubical/src/value.rs b/native/cubical/src/value.rs index 64fb037..b8ad02a 100644 --- a/native/cubical/src/value.rs +++ b/native/cubical/src/value.rs @@ -214,6 +214,44 @@ pub(crate) fn mk_nsnd(n: LeanObj) -> LeanObjMut { ctor } +/// `.vctor S c params args` — canonical schema-constructor value (REL1). +/// Takes ownership of all four field handles. +#[inline] +pub(crate) fn mk_vctor( + schema: LeanObj, name: LeanObj, params: LeanObj, args: LeanObj, +) -> LeanObjMut { + let ctor = alloc_ctor(VAL_VCTOR, 4); + ctor_set_field(ctor, 0, schema); + ctor_set_field(ctor, 1, name); + ctor_set_field(ctor, 2, params); + ctor_set_field(ctor, 3, args); + ctor +} + +/// `.vdimExpr r` — dim-expression lifted to the value level (REL1). +#[inline] +pub(crate) fn mk_vdimexpr(r: LeanObj) -> LeanObjMut { + let ctor = alloc_ctor(VAL_VDIMEXPR, 1); + ctor_set_field(ctor, 0, r); + ctor +} + +/// `.nIndElim S params motive branches target` — stuck eliminator +/// neutral. Five fields per the Lean definition. +#[inline] +pub(crate) fn mk_nindelim( + schema: LeanObj, params: LeanObj, motive: LeanObj, + branches: LeanObj, target: LeanObj, +) -> LeanObjMut { + let ctor = alloc_ctor(NEU_NINDELIM, 5); + ctor_set_field(ctor, 0, schema); + ctor_set_field(ctor, 1, params); + ctor_set_field(ctor, 2, motive); + ctor_set_field(ctor, 3, branches); + ctor_set_field(ctor, 4, target); + ctor +} + // ── Environment operations ───────────────────────────────────────────────── /// `CEnv.cons name val rest` — extend env with a new binding.