diff --git a/native/cubical/include/cubical_transport.h b/native/cubical/include/cubical_transport.h index 0c5c29b..375ff81 100644 --- a/native/cubical/include/cubical_transport.h +++ b/native/cubical/include/cubical_transport.h @@ -9,43 +9,6 @@ // 2 — REL1: schema-based inductive types (CType.ind, CTerm.{dimExpr, // ctor, indElim}, CVal.vctor / vdimExpr, CNeu.nIndElim). // 3 — REL2: cubical interval primitive (CType.interval, tag 6). -// 6 — Modal cascade Phase 2 (cohesive triple ♭ ⊣ ♯ ⊣ ʃ). Adds: -// CType.flat / .sharp / .shape (tags 9 / 10 / 11) -// CTerm.{flat,sharp,shape}Intro (tags 17 / 18 / 19) -// CTerm.{flat,sharp,shape}Elim (tags 20 / 21 / 22) -// CVal.v{Flat,Sharp,Shape}Intro (tags 12 / 13 / 14) -// CNeu.n{flat,sharp,shape}Elim (tags 12 / 13 / 14) -// Layouts (Lean keeps implicit `{ℓ}` at runtime — same v4 rule): -// CType.flat {ℓ} A : 2 fields — [ℓ, A] -// CType.sharp {ℓ} A : 2 fields — [ℓ, A] -// CType.shape {ℓ} A : 2 fields — [ℓ, A] -// CTerm.flatIntro a : 1 field — [a] (no implicit ℓ) -// CTerm.sharpIntro a : 1 field — [a] -// CTerm.shapeIntro a : 1 field — [a] -// CTerm.flatElim f m : 2 fields — [f, m] -// CTerm.sharpElim f m : 2 fields — [f, m] -// CTerm.shapeElim f m : 2 fields — [f, m] -// CVal.vFlatIntro v : 1 field — [v] (CVal payload) -// CVal.vSharpIntro v : 1 field — [v] -// CVal.vShapeIntro v : 1 field — [v] -// CNeu.nflatElim f n : 2 fields — [f, n] (eliminator -// value, stuck CNeu) -// CNeu.nsharpElim f n : 2 fields — [f, n] -// CNeu.nshapeElim f n : 2 fields — [f, n] -// Reductions (mirror Cubical/Eval.lean exactly): -// eval env (.flatIntro a) -// = .vFlatIntro (eval env a) (similarly sharp/shape) -// eval env (.flatElim f m) = -// match eval env m with -// | .vFlatIntro a → vApp (eval env f) a (β) -// | .vneu n → .vneu (.nflatElim (eval env f) n) -// | _ → marker neutral (.nvar "<...>") -// Modal-type-driven transport / composition reductions are -// intentionally absent: a `transp i {flat A} φ t` falls through -// to the existing stuck-neutral path (transport.rs / composition.rs -// only have explicit arms for TY_PI; everything else stucks via -// ntransp / nhcomp / ncomp). Modal cohesion-driven reductions -// (`flat`-transport, `shape`-shape law) land in Phase 3. // 5 — CType.El (decoder) and CTerm.code (encoder) constructors for // universe-coding. Adds CVal.vcode value form. Layouts: // CType.El {ℓ} P : 2 fields — [ℓ, P] @@ -54,6 +17,86 @@ // Lean keeps implicit `{ℓ}` parameters at runtime (verified via // probeLayout in the v4 cascade); these constructors follow the // same convention. +// 6 — Modal cascade Phase 2 (cohesive triple ♭ ⊣ ♯ ⊣ ʃ) — original +// per-modality variant. SUPERSEDED by v7 (modal tag unification). +// The v6 layout used 15 ad-hoc per-modality tags: +// CType.flat / .sharp / .shape (tags 9 / 10 / 11) +// CTerm.{flat,sharp,shape}Intro (tags 17 / 18 / 19) +// CTerm.{flat,sharp,shape}Elim (tags 20 / 21 / 22) +// CVal.v{Flat,Sharp,Shape}Intro (tags 12 / 13 / 14) +// CNeu.n{flat,sharp,shape}Elim (tags 12 / 13 / 14) +// Field shapes (no `k` slot): CType.flat = [ℓ, A] etc., 1-field +// intros, 2-field elims, 1-field vIntros, 2-field nElims. +// 7 — Modal tag unification (Refactor Phase 4, 2026-05-06). The 15 +// per-modality v6 tags collapse into 5 ModalityKind-parameterised +// tags, mirroring the Lean-side `inductive ModalityKind | flat | +// sharp | shape` enum (Syntax.lean Phase 2, Eval.lean Phase 3). +// +// New tags (final assignments, reusing the smallest v6 tag id +// per namespace): +// CType.modal (tag 9 — was TY_FLAT) +// CTerm.modalIntro (tag 17 — was TERM_FLAT_INTRO) +// CTerm.modalElim (tag 18 — was TERM_SHARP_INTRO; chosen so +// modalElim immediately follows modalIntro +// in tag order, matching Lean's declaration +// order in Syntax.lean) +// CVal.vModalIntro (tag 12 — was VAL_VFLAT_INTRO) +// CNeu.nModalElim (tag 12 — was NEU_NFLAT_ELIM) +// +// Reserved (RESERVED FOR FUTURE ABI v8+ EXTENSIONS — DO NOT +// REASSIGN IN THIS COMMIT. Gaps from the v6→v7 collapse): +// TERM tag-space: 19, 20, 21, 22 +// CType tag-space: 10, 11 +// VAL tag-space: 13, 14 +// NEU tag-space: 13, 14 +// +// ModalityKind discriminant: a non-erased Lean inductive with +// three nullary constructors (`flat | sharp | shape`). At +// runtime the value is a boxed scalar `lean_box(0/1/2)`; we +// inspect it with the standard `lean_obj_tag` accessor and +// compare against: +// MODKIND_FLAT = 0 +// MODKIND_SHARP = 1 +// MODKIND_SHAPE = 2 +// (declared `u32` in Rust to match the existing tag-namespace +// convention; `lean_obj_tag` returns `u32` already, so widening +// is unnecessary.) +// +// Layouts: +// CType.modal {ℓ} k A : 3 fields — [ℓ, k, A] +// CTerm.modalIntro k a : 2 fields — [k, a] (no implicit ℓ) +// CTerm.modalElim k f m : 3 fields — [k, f, m] +// CVal.vModalIntro k v : 2 fields — [k, v] (CVal payload) +// CNeu.nModalElim k f n : 3 fields — [k, f, n] +// (kind, eliminator value, +// stuck scrutinee) +// +// Reductions (mirror Cubical/Eval.lean's `eval (.modalElim k f m)` +// arm exactly — engine-layer axioms eval_modalIntro, +// eval_modalElim_beta, eval_modalElim_stuck): +// eval env (.modalIntro k a) +// = .vModalIntro k (eval env a) +// eval env (.modalElim k f m) = +// match eval env m with +// | .vModalIntro k' a → +// if k = k' then vApp (eval env f) a (β-rule) +// else marker "" +// | .vneu n → .vneu (.nModalElim k (eval env f) n) +// | _ → marker "" +// +// Kind comparison is by constructor index (read via +// `lean_obj_tag`). Mismatched-kind intros — which a well-typed +// source cannot produce but a bypassed typechecker conceivably +// could — are kept stuck via the `` +// marker neutral, matching Lean's behaviour. +// +// Modal-type-driven transport / composition reductions remain +// intentionally absent (same as v6): a `transp i {modal k A} φ t` +// falls through to the existing stuck-neutral path +// (transport.rs / composition.rs only have explicit arms for +// TY_PI; everything else stucks via ntransp / nhcomp / ncomp). +// Modal cohesion-driven reductions (`flat`-transport, `shape`- +// shape law) land in a future Phase. // 4 — Layer 0 §0.1 universe-stratification cascade: // · CType is now `CType : ULevel → Type` (level lives in the // index). @@ -94,21 +137,14 @@ // CType.El {ℓ} P → 2 slots: [ℓ, P] (v5) // CTerm.code {ℓ} A → 2 slots: [ℓ, A] (v5) // CVal.vcode {ℓ} A → 2 slots: [ℓ, A] (v5) -// CType.flat {ℓ} A → 2 slots: [ℓ, A] (v6) -// CType.sharp {ℓ} A → 2 slots: [ℓ, A] (v6) -// CType.shape {ℓ} A → 2 slots: [ℓ, A] (v6) -// CTerm.flatIntro a → 1 slot: [a] (v6) -// CTerm.sharpIntro a → 1 slot: [a] (v6) -// CTerm.shapeIntro a → 1 slot: [a] (v6) -// CTerm.flatElim f m → 2 slots: [f, m] (v6) -// CTerm.sharpElim f m → 2 slots: [f, m] (v6) -// CTerm.shapeElim f m → 2 slots: [f, m] (v6) -// CVal.vFlatIntro v → 1 slot: [v] (v6) -// CVal.vSharpIntro v → 1 slot: [v] (v6) -// CVal.vShapeIntro v → 1 slot: [v] (v6) -// CNeu.nflatElim f n → 2 slots: [f, n] (v6) -// CNeu.nsharpElim f n → 2 slots: [f, n] (v6) -// CNeu.nshapeElim f n → 2 slots: [f, n] (v6) +// CType.modal {ℓ} k A → 3 slots: [ℓ, k, A] (v7) +// CTerm.modalIntro k a → 2 slots: [k, a] (v7) +// CTerm.modalElim k f m → 3 slots: [k, f, m] (v7) +// CVal.vModalIntro k v → 2 slots: [k, v] (v7) +// CNeu.nModalElim k f n → 3 slots: [k, f, n] (v7) +// ModalityKind → 0 slots (boxed scalar +// index — flat=0, +// sharp=1, shape=2) // CTerm.transp i {ℓ} A φ t → 5 slots: [i, ℓ, A, φ, t] // CTerm.comp i {ℓ} A φ u t → 6 slots: [i, ℓ, A, φ, u, t] // CTerm.compN i {ℓ} A clauses t → 5 slots: [i, ℓ, A, clauses, t] @@ -128,7 +164,7 @@ #pragma once #include -#define CUBICAL_TRANSPORT_ABI_VERSION 6 +#define CUBICAL_TRANSPORT_ABI_VERSION 7 #ifdef __cplusplus extern "C" { diff --git a/native/cubical/src/dim_absent.rs b/native/cubical/src/dim_absent.rs index cfb61d7..aeaeb61 100644 --- a/native/cubical/src/dim_absent.rs +++ b/native/cubical/src/dim_absent.rs @@ -124,19 +124,20 @@ pub(crate) fn cterm_absent(i: LeanObj, t: LeanObj) -> bool { // ABI v5: universe-code encoder. Same approximation as // transp/comp — A (the CType payload) is not recursed into. TERM_CODE => true, - // ABI v6: modal introductions — dim-absence preserved through - // the wrapper. Layout: [a]. Mirrors Lean CTerm.dimAbsent arms - // for .flatIntro / .sharpIntro / .shapeIntro. - TERM_FLAT_INTRO | TERM_SHARP_INTRO | TERM_SHAPE_INTRO => { - let a = ctor_field(t, 0); + // ABI v7: unified modal introduction — dim-absence preserved + // through the wrapper. Layout: [k, a]. The kind field is a + // ModalityKind (no dim binders inside). Mirrors Lean's + // CTerm.dimAbsent arm for `.modalIntro k a`. + TERM_MODAL_INTRO => { + let a = ctor_field(t, 1); cterm_absent(i, a) } - // ABI v6: modal eliminations — check both eliminator and - // scrutinee. Layout: [f, m]. Mirrors Lean CTerm.dimAbsent - // arms for .flatElim / .sharpElim / .shapeElim. - TERM_FLAT_ELIM | TERM_SHARP_ELIM | TERM_SHAPE_ELIM => { - let f = ctor_field(t, 0); - let m = ctor_field(t, 1); + // ABI v7: unified modal elimination — check both the + // eliminator and the scrutinee. Layout: [k, f, m]. Mirrors + // Lean's CTerm.dimAbsent arm for `.modalElim k f m`. + TERM_MODAL_ELIM => { + let f = ctor_field(t, 1); + let m = ctor_field(t, 2); cterm_absent(i, f) && cterm_absent(i, m) } _ => true, @@ -232,11 +233,12 @@ pub(crate) fn ctype_absent(i: LeanObj, a: LeanObj) -> bool { let p = ctor_field(a, 1); cterm_absent(i, p) } - // ABI v6: cohesive modalities — recurse into the wrapped CType. - // Layout: [ℓ, A]. Mirrors Lean CType.dimAbsent arms for - // .flat / .sharp / .shape. - TY_FLAT | TY_SHARP | TY_SHAPE => { - let inner = ctor_field(a, 1); + // ABI v7: unified cohesive-modality former — recurse into the + // wrapped CType. Layout: [ℓ, k, A]. The ModalityKind field + // (index 1) carries no dim binders. Mirrors Lean + // CType.dimAbsent arm for `.modal k A`. + TY_MODAL => { + let inner = ctor_field(a, 2); ctype_absent(i, inner) } _ => true, diff --git a/native/cubical/src/eval.rs b/native/cubical/src/eval.rs index b97b2d5..d21767b 100644 --- a/native/cubical/src/eval.rs +++ b/native/cubical/src/eval.rs @@ -238,114 +238,75 @@ pub fn eval(env: LeanObj, t: LeanObj) -> LeanObjMut { retain(l); retain(a); mk_vcode(l, a) } - TERM_FLAT_INTRO => { - // .flatIntro a — ABI v6: η_♭ intro. Layout: [a] (1 field, no ℓ). - // eval env (.flatIntro a) = .vFlatIntro (eval env a) - // (mirror Cubical/Eval.lean axiom eval_flatIntro). - let a = ctor_field(t, 0); + TERM_MODAL_INTRO => { + // .modalIntro k a — ABI v7: unified η-intro for the cohesive + // triple. Layout: [k, a] (2 fields, no implicit ℓ — the + // ULevel lives on the surrounding CType.modal, not here). + // eval env (.modalIntro k a) = .vModalIntro k (eval env a) + // Mirror of Cubical/Eval.lean axiom eval_modalIntro. + let k = ctor_field(t, 0); + let a = ctor_field(t, 1); + retain(k); let va = eval(env, a); - mk_vflat_intro(va as LeanObj) + mk_vmodal_intro(k, va as LeanObj) } - TERM_SHARP_INTRO => { - let a = ctor_field(t, 0); - let va = eval(env, a); - mk_vsharp_intro(va as LeanObj) - } - TERM_SHAPE_INTRO => { - let a = ctor_field(t, 0); - let va = eval(env, a); - mk_vshape_intro(va as LeanObj) - } - TERM_FLAT_ELIM => { - // .flatElim f m — ABI v6: ♭.rec. Layout: [f, m] (2 fields). - // eval env (.flatElim f m) = + TERM_MODAL_ELIM => { + // .modalElim k f m — ABI v7: unified modal eliminator. + // Layout: [k, f, m] (3 fields). + // eval env (.modalElim k f m) = // match eval env m with - // | .vFlatIntro a → vApp (eval env f) a (β-rule) - // | .vneu n → .vneu (.nflatElim (eval env f) n) - // | _ → marker neutral - // (mirror Cubical/Eval.lean axioms eval_flatElim_beta / - // eval_flatElim_stuck.) - let f = ctor_field(t, 0); - let m = ctor_field(t, 1); + // | .vModalIntro k' a → + // if k = k' then vApp (eval env f) a (β-rule) + // else marker "" + // | .vneu n → .vneu (.nModalElim k (eval env f) n) + // | _ → marker "" + // Mirror of Cubical/Eval.lean's `eval (.modalElim k f m)` arm + // and the engine-layer axioms eval_modalElim_beta / + // eval_modalElim_stuck. + let k = ctor_field(t, 0); + let f = ctor_field(t, 1); + let m = ctor_field(t, 2); let vm = eval(env, m); let vm_ro = vm as LeanObj; match ctor_tag(vm_ro) { - VAL_VFLAT_INTRO => { - // β-reduce: extract the wrapped value, drop the - // outer .vFlatIntro, and apply f to it. - let inner = ctor_field(vm_ro, 0); - retain(inner); - release(vm_ro); - let vf = eval(env, f); - vapp(vf, inner as LeanObjMut) + VAL_VMODAL_INTRO => { + // Inspect the intro-value's kind (field 0) and + // compare against the eliminator's expected kind + // (field 0 of the .modalElim term). Both are + // `ModalityKind` objects; their constructor index + // (read via ctor_tag) is the discriminant. + let k_intro = ctor_field(vm_ro, 0); + if ctor_tag(k) == ctor_tag(k_intro) { + // β-reduce on matching kind. + let inner = ctor_field(vm_ro, 1); + retain(inner); + release(vm_ro); + let vf = eval(env, f); + vapp(vf, inner as LeanObjMut) + } else { + // Kind mismatch — preserved as a marker neutral + // matching Lean's ``. + // A well-typed source cannot produce this shape; + // a bypassed typechecker conceivably could. + release(vm_ro); + stuck_marker(b"\0") + } } VAL_VNEU => { - // Stuck: extract the inner CNeu, build .nflatElim - // with the evaluated eliminator function. + // Stuck: extract inner CNeu; build .nModalElim + // preserving the kind, the evaluated eliminator, + // and the stuck scrutinee neutral. let inner_neu = ctor_field(vm_ro, 0); retain(inner_neu); release(vm_ro); + retain(k); let vf = eval(env, f); - let nelim = mk_nflat_elim(vf as LeanObj, inner_neu); + let nelim = mk_nmodal_elim(k, vf as LeanObj, inner_neu); mk_vneu(nelim as LeanObj) } _ => { release(vm_ro); - stuck_marker(b"\0") - } - } - } - TERM_SHARP_ELIM => { - let f = ctor_field(t, 0); - let m = ctor_field(t, 1); - let vm = eval(env, m); - let vm_ro = vm as LeanObj; - match ctor_tag(vm_ro) { - VAL_VSHARP_INTRO => { - let inner = ctor_field(vm_ro, 0); - retain(inner); - release(vm_ro); - let vf = eval(env, f); - vapp(vf, inner as LeanObjMut) - } - VAL_VNEU => { - let inner_neu = ctor_field(vm_ro, 0); - retain(inner_neu); - release(vm_ro); - let vf = eval(env, f); - let nelim = mk_nsharp_elim(vf as LeanObj, inner_neu); - mk_vneu(nelim as LeanObj) - } - _ => { - release(vm_ro); - stuck_marker(b"\0") - } - } - } - TERM_SHAPE_ELIM => { - let f = ctor_field(t, 0); - let m = ctor_field(t, 1); - let vm = eval(env, m); - let vm_ro = vm as LeanObj; - match ctor_tag(vm_ro) { - VAL_VSHAPE_INTRO => { - let inner = ctor_field(vm_ro, 0); - retain(inner); - release(vm_ro); - let vf = eval(env, f); - vapp(vf, inner as LeanObjMut) - } - VAL_VNEU => { - let inner_neu = ctor_field(vm_ro, 0); - retain(inner_neu); - release(vm_ro); - let vf = eval(env, f); - let nelim = mk_nshape_elim(vf as LeanObj, inner_neu); - mk_vneu(nelim as LeanObj) - } - _ => { - release(vm_ro); - stuck_marker(b"\0") + stuck_marker(b"\0") } } } @@ -514,11 +475,13 @@ pub fn vapp(f: LeanObjMut, a: LeanObjMut) -> LeanObjMut { result } VAL_VPLAM | VAL_VTUBEAPP | VAL_VPATHTRANSP | VAL_VPAIR | VAL_VCODE - | VAL_VFLAT_INTRO | VAL_VSHARP_INTRO | VAL_VSHAPE_INTRO => { + | VAL_VMODAL_INTRO => { // Ill-typed application; marker neutral per FFI_DESIGN §6. - // ABI v6: modal intros are not functions either — they - // mirror the Lean `eval`'s explicit arm for vFlat/Sharp/ - // ShapeIntro applied as a function. + // ABI v7: the unified .vModalIntro is not a function either + // — mirror Lean `eval`'s explicit arm for `vModalIntro _ _` + // applied as a function (returns `` in the Lean source; we coalesce all + // non-function applications into one marker for FFI brevity). release(f_ro); release(a as LeanObj); stuck_marker(b"\0") diff --git a/native/cubical/src/readback.rs b/native/cubical/src/readback.rs index 064f419..44db388 100644 --- a/native/cubical/src/readback.rs +++ b/native/cubical/src/readback.rs @@ -583,28 +583,17 @@ pub fn readback(v: LeanObj) -> LeanObjMut { retain(l); retain(a); mk_term_code(l, a) } - // ABI v6: modal-introduction values. Layout: [v] (1 field). - // Mirrors Cubical/Readback.lean axioms readback_vFlatIntro etc. - VAL_VFLAT_INTRO => { - // readback (.vFlatIntro a) = .flatIntro (readback a) - let inner = ctor_field(v, 0); + // ABI v7: unified modal-introduction value. Layout: [k, v] + // (2 fields). Mirrors Cubical/Readback.lean's axiom for + // `.vModalIntro k v ↦ .modalIntro k (readback v)`. + VAL_VMODAL_INTRO => { + let k = ctor_field(v, 0); + let inner = ctor_field(v, 1); + retain(k); let inner_term = readback(inner); - let ctor = alloc_ctor(TERM_FLAT_INTRO, 1); - ctor_set_field(ctor, 0, inner_term as LeanObj); - ctor - } - VAL_VSHARP_INTRO => { - let inner = ctor_field(v, 0); - let inner_term = readback(inner); - let ctor = alloc_ctor(TERM_SHARP_INTRO, 1); - ctor_set_field(ctor, 0, inner_term as LeanObj); - ctor - } - VAL_VSHAPE_INTRO => { - let inner = ctor_field(v, 0); - let inner_term = readback(inner); - let ctor = alloc_ctor(TERM_SHAPE_INTRO, 1); - ctor_set_field(ctor, 0, inner_term as LeanObj); + let ctor = alloc_ctor(TERM_MODAL_INTRO, 2); + ctor_set_field(ctor, 0, k); + ctor_set_field(ctor, 1, inner_term as LeanObj); ctor } _ => { @@ -736,39 +725,23 @@ pub fn readback_neu(n: LeanObj) -> LeanObjMut { mk_term_indelim(schema, params, motive_term as LeanObj, branches_term as LeanObj, target_term as LeanObj) } - // ABI v6: modal-elimination stuck neutrals. Layout: [f, n] — - // field 0 is the evaluated eliminator function (a CVal), - // field 1 is the stuck scrutinee (a CNeu). Mirrors - // Cubical/Readback.lean readbackNeu_nflatElim etc. - NEU_NFLAT_ELIM => { - // readbackNeu (.nflatElim f n) = .flatElim (readback f) (readbackNeu n) - let f = ctor_field(n, 0); - let inner_neu = ctor_field(n, 1); + // ABI v7: unified modal-elimination stuck neutral. Layout: + // [k, f, n] — field 0 is the `ModalityKind`, field 1 is the + // evaluated eliminator function (a CVal), field 2 is the stuck + // scrutinee (a CNeu). Mirrors Cubical/Readback.lean's axiom + // for `.nModalElim k f n ↦ .modalElim k (readback f) + // (readbackNeu n)`. + NEU_NMODAL_ELIM => { + let k = ctor_field(n, 0); + let f = ctor_field(n, 1); + let inner_neu = ctor_field(n, 2); + retain(k); let f_term = readback(f); let inner_term = readback_neu(inner_neu); - let ctor = alloc_ctor(TERM_FLAT_ELIM, 2); - ctor_set_field(ctor, 0, f_term as LeanObj); - ctor_set_field(ctor, 1, inner_term as LeanObj); - ctor - } - NEU_NSHARP_ELIM => { - let f = ctor_field(n, 0); - let inner_neu = ctor_field(n, 1); - let f_term = readback(f); - let inner_term = readback_neu(inner_neu); - let ctor = alloc_ctor(TERM_SHARP_ELIM, 2); - ctor_set_field(ctor, 0, f_term as LeanObj); - ctor_set_field(ctor, 1, inner_term as LeanObj); - ctor - } - NEU_NSHAPE_ELIM => { - let f = ctor_field(n, 0); - let inner_neu = ctor_field(n, 1); - let f_term = readback(f); - let inner_term = readback_neu(inner_neu); - let ctor = alloc_ctor(TERM_SHAPE_ELIM, 2); - ctor_set_field(ctor, 0, f_term as LeanObj); - ctor_set_field(ctor, 1, inner_term as LeanObj); + let ctor = alloc_ctor(TERM_MODAL_ELIM, 3); + ctor_set_field(ctor, 0, k); + ctor_set_field(ctor, 1, f_term as LeanObj); + ctor_set_field(ctor, 2, inner_term as LeanObj); ctor } _ => { diff --git a/native/cubical/src/subst.rs b/native/cubical/src/subst.rs index 20ab8c1..e0f6e01 100644 --- a/native/cubical/src/subst.rs +++ b/native/cubical/src/subst.rs @@ -552,59 +552,34 @@ pub(crate) fn cterm_subst_dim(i: LeanObj, r: LeanObj, t: LeanObj) -> LeanObjMut retain(t); t as LeanObjMut } - // ABI v6: modal introductions — recurse into the wrapped CTerm. - // Layout: [a] (1 field, no implicit ℓ). - TERM_FLAT_INTRO => { - let a = ctor_field(t, 0); + // ABI v7: unified modal introduction — recurse into the wrapped + // CTerm, preserving the modality kind. Layout: [k, a] (2 fields, + // no implicit ℓ). Mirrors Lean's CTerm.substDim arm for + // `.modalIntro k a`. + TERM_MODAL_INTRO => { + let k = ctor_field(t, 0); + let a = ctor_field(t, 1); + retain(k); let na = cterm_subst_dim(i, r, a); - let ctor = alloc_ctor(TERM_FLAT_INTRO, 1); - ctor_set_field(ctor, 0, na as LeanObj); + let ctor = alloc_ctor(TERM_MODAL_INTRO, 2); + ctor_set_field(ctor, 0, k); + ctor_set_field(ctor, 1, na as LeanObj); ctor } - TERM_SHARP_INTRO => { - let a = ctor_field(t, 0); - let na = cterm_subst_dim(i, r, a); - let ctor = alloc_ctor(TERM_SHARP_INTRO, 1); - ctor_set_field(ctor, 0, na as LeanObj); - ctor - } - TERM_SHAPE_INTRO => { - let a = ctor_field(t, 0); - let na = cterm_subst_dim(i, r, a); - let ctor = alloc_ctor(TERM_SHAPE_INTRO, 1); - ctor_set_field(ctor, 0, na as LeanObj); - ctor - } - // ABI v6: modal eliminations — recurse into both subterms. - // Layout: [f, m] (2 fields). - TERM_FLAT_ELIM => { - let f = ctor_field(t, 0); - let m = ctor_field(t, 1); + // ABI v7: unified modal elimination — recurse into both subterms, + // preserving the modality kind. Layout: [k, f, m] (3 fields). + // Mirrors Lean's CTerm.substDim arm for `.modalElim k f m`. + TERM_MODAL_ELIM => { + let k = ctor_field(t, 0); + let f = ctor_field(t, 1); + let m = ctor_field(t, 2); + retain(k); let nf = cterm_subst_dim(i, r, f); let nm = cterm_subst_dim(i, r, m); - let ctor = alloc_ctor(TERM_FLAT_ELIM, 2); - ctor_set_field(ctor, 0, nf as LeanObj); - ctor_set_field(ctor, 1, nm as LeanObj); - ctor - } - TERM_SHARP_ELIM => { - let f = ctor_field(t, 0); - let m = ctor_field(t, 1); - let nf = cterm_subst_dim(i, r, f); - let nm = cterm_subst_dim(i, r, m); - let ctor = alloc_ctor(TERM_SHARP_ELIM, 2); - ctor_set_field(ctor, 0, nf as LeanObj); - ctor_set_field(ctor, 1, nm as LeanObj); - ctor - } - TERM_SHAPE_ELIM => { - let f = ctor_field(t, 0); - let m = ctor_field(t, 1); - let nf = cterm_subst_dim(i, r, f); - let nm = cterm_subst_dim(i, r, m); - let ctor = alloc_ctor(TERM_SHAPE_ELIM, 2); - ctor_set_field(ctor, 0, nf as LeanObj); - ctor_set_field(ctor, 1, nm as LeanObj); + let ctor = alloc_ctor(TERM_MODAL_ELIM, 3); + ctor_set_field(ctor, 0, k); + ctor_set_field(ctor, 1, nf as LeanObj); + ctor_set_field(ctor, 2, nm as LeanObj); ctor } _ => { @@ -786,30 +761,18 @@ fn mk_ty_el(l: LeanObj, p: LeanObj) -> LeanObjMut { ctor } -/// `.flat {ℓ} A` — ABI v6 cohesive-modality (♭). Layout: [ℓ, A]. +/// `.modal {ℓ} k A` — ABI v7 unified cohesive-modality former. +/// Layout: [ℓ, k, A] (3 fields). Replaces the v6 trio +/// `mk_ty_flat`/`mk_ty_sharp`/`mk_ty_shape`. `k` is a `ModalityKind` +/// runtime object (boxed-scalar for the nullary `flat`/`sharp`/`shape` +/// constructors); the field is consume-slot — caller must pass an +/// owned reference. #[inline] -fn mk_ty_flat(l: LeanObj, a: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(TY_FLAT, 2); +fn mk_ty_modal(l: LeanObj, k: LeanObj, a: LeanObj) -> LeanObjMut { + let ctor = alloc_ctor(TY_MODAL, 3); ctor_set_field(ctor, 0, l); - ctor_set_field(ctor, 1, a); - ctor -} - -/// `.sharp {ℓ} A` — ABI v6 cohesive-modality (♯). Layout: [ℓ, A]. -#[inline] -fn mk_ty_sharp(l: LeanObj, a: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(TY_SHARP, 2); - ctor_set_field(ctor, 0, l); - ctor_set_field(ctor, 1, a); - ctor -} - -/// `.shape {ℓ} A` — ABI v6 cohesive-modality (ʃ). Layout: [ℓ, A]. -#[inline] -fn mk_ty_shape(l: LeanObj, a: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(TY_SHAPE, 2); - ctor_set_field(ctor, 0, l); - ctor_set_field(ctor, 1, a); + ctor_set_field(ctor, 1, k); + ctor_set_field(ctor, 2, a); ctor } @@ -950,29 +913,17 @@ pub(crate) fn ctype_subst_dim_bool(i: LeanObj, b: bool, a: LeanObj) -> LeanObjMu let new_p = cterm_subst_dim_bool(i, b, p); mk_ty_el(l, new_p as LeanObj) } - // ABI v6: cohesive modalities — recurse into the wrapped CType. - // Layout: [ℓ, A]. Mirrors Lean's CType.substDim arms for - // .flat / .sharp / .shape. - TY_FLAT => { + // ABI v7: unified cohesive-modality former — recurse into the + // wrapped CType, preserving the modality kind. Layout: + // [ℓ, k, A]. Mirrors Lean's CType.substDim arm for `.modal k A` + // (which is structural in `A`, leaving the kind alone). + TY_MODAL => { let l = ctor_field(a, 0); - let inner = ctor_field(a, 1); - retain(l); + let k = ctor_field(a, 1); + let inner = ctor_field(a, 2); + retain(l); retain(k); let new_inner = ctype_subst_dim_bool(i, b, inner); - mk_ty_flat(l, new_inner as LeanObj) - } - TY_SHARP => { - let l = ctor_field(a, 0); - let inner = ctor_field(a, 1); - retain(l); - let new_inner = ctype_subst_dim_bool(i, b, inner); - mk_ty_sharp(l, new_inner as LeanObj) - } - TY_SHAPE => { - let l = ctor_field(a, 0); - let inner = ctor_field(a, 1); - retain(l); - let new_inner = ctype_subst_dim_bool(i, b, inner); - mk_ty_shape(l, new_inner as LeanObj) + mk_ty_modal(l, k, new_inner as LeanObj) } _ => { // Synthetic fallback at level zero. @@ -1114,28 +1065,17 @@ pub(crate) fn ctype_subst_dim_expr(i: LeanObj, r: LeanObj, a: LeanObj) -> LeanOb let new_p = cterm_subst_dim(i, r, p); mk_ty_el(l, new_p as LeanObj) } - // ABI v6: cohesive modalities — recurse into the wrapped CType. - // Layout: [ℓ, A]. Mirrors Lean's CType.substDimExpr arms. - TY_FLAT => { + // ABI v7: unified cohesive-modality former — recurse into the + // wrapped CType, preserving the modality kind. Layout: + // [ℓ, k, A]. Mirrors Lean's CType.substDimExpr arm for + // `.modal k A`. + TY_MODAL => { let l = ctor_field(a, 0); - let inner = ctor_field(a, 1); - retain(l); + let k = ctor_field(a, 1); + let inner = ctor_field(a, 2); + retain(l); retain(k); let new_inner = ctype_subst_dim_expr(i, r, inner); - mk_ty_flat(l, new_inner as LeanObj) - } - TY_SHARP => { - let l = ctor_field(a, 0); - let inner = ctor_field(a, 1); - retain(l); - let new_inner = ctype_subst_dim_expr(i, r, inner); - mk_ty_sharp(l, new_inner as LeanObj) - } - TY_SHAPE => { - let l = ctor_field(a, 0); - let inner = ctor_field(a, 1); - retain(l); - let new_inner = ctype_subst_dim_expr(i, r, inner); - mk_ty_shape(l, new_inner as LeanObj) + mk_ty_modal(l, k, new_inner as LeanObj) } _ => { mk_ty_univ(lean_box_mut(0) as LeanObj) diff --git a/native/cubical/src/tags.rs b/native/cubical/src/tags.rs index a6ce43b..1398c62 100644 --- a/native/cubical/src/tags.rs +++ b/native/cubical/src/tags.rs @@ -24,6 +24,29 @@ pub const FACE_EQ1: u32 = 3; pub const FACE_MEET: u32 = 4; pub const FACE_JOIN: u32 = 5; +// ── ModalityKind (Cubical/Syntax.lean — Refactor Phase 2, ABI v7) ───────── +// +// Level-erased enum tagging which arm of the cohesive triple `ʃ ⊣ ♭ ⊣ ♯` +// a unified modal constructor talks about. Replaces the v6 set of nine +// ad-hoc per-modality constructors. +// +// Lean inductive (zero-field arms — represented at runtime as boxed +// scalars `lean_box()`): +// +// inductive ModalityKind | flat | sharp | shape +// +// `lean_obj_tag` returns the constructor index uniformly for both scalar +// and heap objects, so we read the kind by `ctor_tag(k)` and compare +// against the constants below — exactly the existing pattern used for +// `FACE_TOP`, `DIM_ZERO`, etc. These are `u32` (matching every other +// tag-namespace constant in this module) rather than `u8`: the runtime +// API surface is `ctor_tag(o) -> u32`, and no current call site benefits +// from a narrower type. + +pub const MODKIND_FLAT: u32 = 0; +pub const MODKIND_SHARP: u32 = 1; +pub const MODKIND_SHAPE: u32 = 2; + // ── CType (Cubical/Syntax.lean) ──────────────────────────────────────────── // // Universe-stratified order (Layer 0 §0.1, ABI v4): @@ -36,6 +59,8 @@ pub const FACE_JOIN: u32 = 5; // 5 ind — schema-defined inductive type; params are Σ-pairs ⟨ℓ', CType ℓ'⟩ // 6 interval — cubical interval `𝕀`, lives at level zero // 7 lift — cumulativity constructor (NEW in v4): `lift A` bumps level. +// 8 El — universe-code decoder (ABI v5): `El P`. +// 9 modal — unified cohesive-modality former (ABI v7): `modal k A`. pub const TY_UNIV: u32 = 0; pub const TY_PI: u32 = 1; @@ -46,9 +71,15 @@ pub const TY_IND: u32 = 5; // REL1: schema-based inductive type pub const TY_INTERVAL: u32 = 6; // REL2: cubical interval primitive pub const TY_LIFT: u32 = 7; // ABI v4: cumulativity constructor pub const TY_EL: u32 = 8; // ABI v5: universe-code decoder `El P` -pub const TY_FLAT: u32 = 9; // ABI v6: cohesive modality `♭ A` (flat) -pub const TY_SHARP: u32 = 10; // ABI v6: cohesive modality `♯ A` (sharp) -pub const TY_SHAPE: u32 = 11; // ABI v6: cohesive modality `ʃ A` (shape) +// ABI v7: unified cohesive-modality former, `modal k A` where +// `k : ModalityKind`. Reuses tag id 9 (formerly `TY_FLAT` in v6). +// +// Reserved (gap from v6→v7 collapse, intentionally unassigned for +// future ABI v8+ extensions; do NOT reuse without bumping the version +// number again): +// 10 — was `TY_SHARP` (v6) +// 11 — was `TY_SHAPE` (v6) +pub const TY_MODAL: u32 = 9; // ── CTerm (Cubical/Syntax.lean) ──────────────────────────────────────────── @@ -69,12 +100,21 @@ 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 pub const TERM_CODE: u32 = 16; // ABI v5: universe-code encoder `code A` -pub const TERM_FLAT_INTRO: u32 = 17; // ABI v6: η_♭ — flatIntro a -pub const TERM_SHARP_INTRO: u32 = 18; // ABI v6: η_♯ — sharpIntro a -pub const TERM_SHAPE_INTRO: u32 = 19; // ABI v6: η_ʃ — shapeIntro a -pub const TERM_FLAT_ELIM: u32 = 20; // ABI v6: ♭.rec — flatElim f m -pub const TERM_SHARP_ELIM: u32 = 21; // ABI v6: ♯.rec — sharpElim f m -pub const TERM_SHAPE_ELIM: u32 = 22; // ABI v6: ʃ.rec — shapeElim f m +// ABI v7: unified modal introduction, `modalIntro k a`. Reuses tag id +// 17 (formerly `TERM_FLAT_INTRO` in v6). +pub const TERM_MODAL_INTRO: u32 = 17; +// ABI v7: unified modal elimination, `modalElim k f m`. Reuses tag id +// 18 (formerly `TERM_SHARP_INTRO` in v6, but now hosting the unified +// modal-elim arm because Lean's declaration order in `Syntax.lean` +// places `modalElim` immediately after `modalIntro`). +// +// Reserved (gaps from v6→v7 collapse, intentionally unassigned for +// future ABI v8+ extensions): +// 19 — was `TERM_SHAPE_INTRO` (v6) +// 20 — was `TERM_FLAT_ELIM` (v6) +// 21 — was `TERM_SHARP_ELIM` (v6) +// 22 — was `TERM_SHAPE_ELIM` (v6) +pub const TERM_MODAL_ELIM: u32 = 18; // ── CEnv (Cubical/Value.lean) ────────────────────────────────────────────── @@ -95,9 +135,13 @@ 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 pub const VAL_VCODE: u32 = 11; // ABI v5: universe-code value `vcode A` -pub const VAL_VFLAT_INTRO: u32 = 12; // ABI v6: vFlatIntro v — η_♭ value -pub const VAL_VSHARP_INTRO: u32 = 13; // ABI v6: vSharpIntro v — η_♯ value -pub const VAL_VSHAPE_INTRO: u32 = 14; // ABI v6: vShapeIntro v — η_ʃ value +// ABI v7: unified modal introduction value, `vModalIntro k v`. Reuses +// tag id 12 (formerly `VAL_VFLAT_INTRO` in v6). +// +// Reserved (gaps from v6→v7 collapse): +// 13 — was `VAL_VSHARP_INTRO` (v6) +// 14 — was `VAL_VSHAPE_INTRO` (v6) +pub const VAL_VMODAL_INTRO: u32 = 12; // ── CNeu (Cubical/Value.lean) ────────────────────────────────────────────── @@ -113,6 +157,10 @@ 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 -pub const NEU_NFLAT_ELIM: u32 = 12; // ABI v6: stuck nflatElim f n -pub const NEU_NSHARP_ELIM: u32 = 13; // ABI v6: stuck nsharpElim f n -pub const NEU_NSHAPE_ELIM: u32 = 14; // ABI v6: stuck nshapeElim f n +// ABI v7: unified stuck modal-eliminator neutral, `nModalElim k f n`. +// Reuses tag id 12 (formerly `NEU_NFLAT_ELIM` in v6). +// +// Reserved (gaps from v6→v7 collapse): +// 13 — was `NEU_NSHARP_ELIM` (v6) +// 14 — was `NEU_NSHAPE_ELIM` (v6) +pub const NEU_NMODAL_ELIM: u32 = 12; diff --git a/native/cubical/src/value.rs b/native/cubical/src/value.rs index 9831a3b..9ce3aee 100644 --- a/native/cubical/src/value.rs +++ b/native/cubical/src/value.rs @@ -322,65 +322,45 @@ pub(crate) fn mk_term_code(l: LeanObj, a: LeanObj) -> LeanObjMut { ctor } -// ── ABI v6: cohesive modality value/neutral builders ─────────────────────── +// ── ABI v7: unified cohesive-modality value/neutral builders ────────────── // -// Three intro values (vFlatIntro / vSharpIntro / vShapeIntro) carry one -// CVal payload. Three stuck-elim neutrals (nflatElim / nsharpElim / -// nshapeElim) carry the evaluated eliminator function (CVal) and the -// stuck scrutinee (CNeu). No implicit ULevel — modal intros and -// elims are CTerm/CVal-typed, not CType-typed (the modal's ULevel -// lives on the surrounding CType.flat/.sharp/.shape, not here). +// One intro value (`vModalIntro k v`) carrying a `ModalityKind` tag and +// the wrapped CVal payload; one stuck-elim neutral (`nModalElim k f n`) +// carrying the kind, the evaluated eliminator function (CVal) and the +// stuck scrutinee (CNeu). Replaces the v6 trio of per-modality +// builders (mk_vflat_intro / mk_vsharp_intro / mk_vshape_intro and +// mk_nflat_elim / mk_nsharp_elim / mk_nshape_elim). +// +// Lean keeps `ModalityKind` as a regular runtime object slot (it is a +// non-erased inductive); both the boxed-scalar form (`flat`/`sharp`/ +// `shape` are nullary, so they live as `lean_box(0/1/2)`) and any +// future heap-payloaded extensions are stored uniformly. Callers must +// pass an OWNED `kind` reference — the constructor field consumes it. +// +// No implicit ULevel — modal intros and elims are CTerm/CVal-typed, +// not CType-typed (the modal's ULevel lives on the surrounding +// CType.modal, not here). -/// `.vFlatIntro v` — η_♭ value (ABI v6). Layout: `[v]` (1 field). +/// `.vModalIntro k v` — η-introduction value for modality `k` (ABI v7). +/// Layout: `[k, v]` (2 fields): the `ModalityKind` discriminant and the +/// wrapped CVal payload. #[inline] -pub(crate) fn mk_vflat_intro(v: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(VAL_VFLAT_INTRO, 1); - ctor_set_field(ctor, 0, v); +pub(crate) fn mk_vmodal_intro(k: LeanObj, v: LeanObj) -> LeanObjMut { + let ctor = alloc_ctor(VAL_VMODAL_INTRO, 2); + ctor_set_field(ctor, 0, k); + ctor_set_field(ctor, 1, v); ctor } -/// `.vSharpIntro v` — η_♯ value (ABI v6). Layout: `[v]` (1 field). +/// `.nModalElim k f n` — stuck modal-eliminator neutral (ABI v7). +/// Layout: `[k, f, n]` (3 fields): the `ModalityKind` discriminant, the +/// evaluated eliminator function, and the stuck scrutinee. #[inline] -pub(crate) fn mk_vsharp_intro(v: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(VAL_VSHARP_INTRO, 1); - ctor_set_field(ctor, 0, v); - ctor -} - -/// `.vShapeIntro v` — η_ʃ value (ABI v6). Layout: `[v]` (1 field). -#[inline] -pub(crate) fn mk_vshape_intro(v: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(VAL_VSHAPE_INTRO, 1); - ctor_set_field(ctor, 0, v); - ctor -} - -/// `.nflatElim f n` — stuck flat-eliminator neutral (ABI v6). -/// Layout: `[f, n]` (2 fields): the evaluated eliminator function and -/// the stuck scrutinee. -#[inline] -pub(crate) fn mk_nflat_elim(f: LeanObj, n: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(NEU_NFLAT_ELIM, 2); - ctor_set_field(ctor, 0, f); - ctor_set_field(ctor, 1, n); - ctor -} - -/// `.nsharpElim f n` — stuck sharp-eliminator neutral (ABI v6). -#[inline] -pub(crate) fn mk_nsharp_elim(f: LeanObj, n: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(NEU_NSHARP_ELIM, 2); - ctor_set_field(ctor, 0, f); - ctor_set_field(ctor, 1, n); - ctor -} - -/// `.nshapeElim f n` — stuck shape-eliminator neutral (ABI v6). -#[inline] -pub(crate) fn mk_nshape_elim(f: LeanObj, n: LeanObj) -> LeanObjMut { - let ctor = alloc_ctor(NEU_NSHAPE_ELIM, 2); - ctor_set_field(ctor, 0, f); - ctor_set_field(ctor, 1, n); +pub(crate) fn mk_nmodal_elim(k: LeanObj, f: LeanObj, n: LeanObj) -> LeanObjMut { + let ctor = alloc_ctor(NEU_NMODAL_ELIM, 3); + ctor_set_field(ctor, 0, k); + ctor_set_field(ctor, 1, f); + ctor_set_field(ctor, 2, n); ctor }