Skip to content

Commit fd3c6d9

Browse files
fix(abi-emit-manifest): skip GADT-style data … where declarations (#34)
`iseriser abi-emit-manifest` bombed with "data declaration has no `=`" on any Idris2 module that declared a GADT — e.g. boj-server's vordr-mcp `MonotonicDegradation` proof relation: data MonotonicDegradation : IntegrityState -> IntegrityState -> Type where StayHealthy : MonotonicDegradation Healthy Healthy ... These are proof / relation types, not exported enums, and have no place in the ABI manifest. The emitter must walk past them without choking the way it must already walk past records, interfaces, and function definitions. `collect_data_body` now detects GADT form (body starts with `:`, not `=`) and delegates to a new `skip_gadt_block` helper that consumes the type signature + indented constructor block. Empty variant lists were already silently dropped by `parse_enum_declarations` so no further plumbing is needed. Two unit tests added: a vordr-mcp shape (real ADT + sibling GADT + to-int mapping) and a degenerate signature-only GADT (`data Phantom : Type` with no `where`). Both pass; all 8 emitter tests + 9 integration tests stay green. Verified end-to-end against the real cartridge: $ iseriser abi-emit-manifest \ --idris …/vordr-mcp/abi/VordrMcp/SafeVordr.idr \ --cartridge vordr-mcp --out /tmp/v.json abi-emit-manifest: wrote /tmp/v.json (0 enums, 0 transitions) $ iseriser abi-verify --manifest /tmp/v.json --zig-ffi …/vordr_ffi.zig abi-verify: OK exit: 0 Refs hyperpolymath/standards#92 (Phase 2 allowlist expansion). Refs hyperpolymath/boj-server#111 (the cartridge that motivated the fix). Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent a4a7312 commit fd3c6d9

0 file changed

File tree

    0 commit comments

    Comments
     (0)