max/cubical-transport-hott-lean4
1
0
Fork 0
Code Issues 1 Pull requests Projects Releases Packages Wiki Activity Actions

Refactor Phase 4: Rust ABI v6 → v7 (modal tag unification)
Some checks are pending
Lean Action CI / build (push) Waiting to run
Details

Browse source 
Mirrors the Lean-side modal unification (commits 6e4936d / cfabca3 /
2b7564e) at the native level.  ABI version constant
CUBICAL_TRANSPORT_ABI_VERSION = 7.

Tag unification (15 v6 modal tags → 5 v7 unified tags):
  · TY_MODAL = 9                          (was: TY_FLAT/SHARP/SHAPE = 9-11)
  · TERM_MODAL_INTRO = 17, TERM_MODAL_ELIM = 18
                                          (was: TERM_*_INTRO/ELIM = 17-22)
  · VAL_VMODAL_INTRO = 12                 (was: VAL_V*_INTRO = 12-14)
  · NEU_NMODAL_ELIM = 12                  (was: NEU_N*_ELIM = 12-14)
  · MODKIND_FLAT/SHARP/SHAPE = 0/1/2 (u32 — matches existing tag-
                                          namespace convention)

Tag-id design choice (TERM_MODAL_ELIM = 18, not 20):
  Lean compiler assigns constructor indices in declaration order;
  Syntax.lean declares modalIntro then modalElim consecutively, so
  the runtime tag is 18, not 20.  Using 20 would break FFI
  marshalling.  Same precedent as v4's sigma/path tag ordering.

Reserved freed slots (no v7 reassignment per directive — gaps
documented in tags.rs for future v8+ extensions):
  · CType: 10, 11
  · TERM:  19, 20, 21, 22
  · VAL:   13, 14
  · NEU:   13, 14

Layout tables in cubical_transport.h v7 entry:
  · TY_MODAL          [ℓ, k, A]
  · TERM_MODAL_INTRO  [k, a]
  · TERM_MODAL_ELIM   [k, f, m]
  · VAL_VMODAL_INTRO  [k, inner_value]
  · NEU_NMODAL_ELIM   [k, eliminator_value, stuck_scrutinee]

Cascade across:
  · tags.rs — 15 deletions + 5 unified consts + 3 ModalityKind +
    reservation block
  · value.rs — CVal::VModalIntro(ModalityKind, _) and
    CNeu::NModalElim(ModalityKind, _, _) variants
  · eval.rs — 9-arm modal dispatch → 3-arm; β-rule fires only on
    matching kinds (k == k') with marker neutral on mismatch
  · subst.rs — 9 modal substDim arms → 3 unified
  · readback.rs — 6 modal readback arms → 2
  · dim_absent.rs — 9 dim-absent modal arms → 3

Files NOT touched (verified): transport.rs, composition.rs,
glue.rs, beta.rs, ffi.rs.  Wildcard catchalls handle modal types as
stuck neutrals (same as v6).

Refcount discipline for the new k field documented at every
mk_vmodal_intro / mk_nmodal_elim / mk_ty_modal call site.

Verification:
  · cargo build --release: clean
  · cargo test --release: 0 passed, 0 failed (no in-crate tests)
  · lake build: 48 jobs PASS
  · lake build CubicalTransport: 43 jobs PASS
  · lake exe cubical-test: 49/49 + 46/46 = 95/95 PASS
  · 0 new unsafe / unimplemented! / todo! / panic! catchalls

Net: -58 lines across 7 files (-397 deletions, +339 insertions).
Source-code reduction concentrated in cascade modules; tags.rs and
header grew due to reservation documentation and v7 layout tables.

Honest gap: existing test suite doesn't exercise modal terms via
FFI (modal Lean-side use sits behind sorry'd Phase 3 axioms).  The
95/95 confirms no regression of existing paths but doesn't directly
validate v7 modal marshalling.  An FFI smoke test exercising modal
terms is queued for when modal cohesion sorries discharge.

Layer 0 + elegance refactor pass COMPLETE.  All four phases landed:
Phase 1 (derive_reflect_reify macro), Phase 2 (Lean modal
unification), Phase 3 (Modal.lean rewrite + topolei consumer
cascade), Phase 4 (Rust ABI v7).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Maximus Gorog 2026-05-06 02:25:10 -06:00
parent cfabca3404
commit 567d8722d5
7 changed files with 337 additions and 395 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

142
native/cubical/include/cubical_transport.h
View file

@ -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 "<modalElim: kind mismatch>"
// | .vneu n → .vneu (.nModalElim k (eval env f) n)
// | _ → marker "<modalElim: scrutinee is not modal-canonical>"
//
// 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 `<modalElim: kind mismatch>`
// 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 <lean/lean.h>
#define CUBICAL_TRANSPORT_ABI_VERSION 6
#define CUBICAL_TRANSPORT_ABI_VERSION 7
#ifdef __cplusplus
extern "C" {

34
native/cubical/src/dim_absent.rs
View file

@ -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,

155
native/cubical/src/eval.rs
View file

@ -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 "<modalElim: kind mismatch>"
// | .vneu n → .vneu (.nModalElim k (eval env f) n)
// | _ → marker "<modalElim: scrutinee is not modal-canonical>"
// 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 `<modalElim: kind mismatch>`.
// A well-typed source cannot produce this shape;
// a bypassed typechecker conceivably could.
release(vm_ro);
stuck_marker(b"<modalElim: kind mismatch>\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"<flatElim: scrutinee is not flat-canonical>\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"<sharpElim: scrutinee is not sharp-canonical>\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"<shapeElim: scrutinee is not shape-canonical>\0")
stuck_marker(b"<modalElim: scrutinee is not modal-canonical>\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 `<vApp: vModalIntro applied
// as function>` 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"<vApp: non-function value applied>\0")

77
native/cubical/src/readback.rs
View file

@ -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
}
_ => {

162
native/cubical/src/subst.rs
View file

@ -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)

78
native/cubical/src/tags.rs
View file

@ -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(<idx>)`):
//
// 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;

84
native/cubical/src/value.rs
View file

@ -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
}