Commit c97077a
fix(abi-emit-manifest): skip GADT-style
`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>data … where declarations (#37)1 parent 6b4a2a8 commit c97077a
0 file changed
0 commit comments