Scope

ff-generics-unsafe provides an execution-enabled extension to generic programming over primitive atoms in Agda. It builds on ff-generics and ff-json to turn generic descriptions into JSON-mediated values during typechecking. The Macro module covers interactive and source-oriented value choice, including certified paths and mocked invocation modes. FamilyMacro uses reflection to inspect constructors and fields and to synthesize machinery for related datatype families. The examples and mock tests exercise sums, records, recursive families, and combinations of string, natural-number, integer, and Boolean fields.

Most important results

Runtime-backed macros can invoke a Node.js chooser during elaboration and decode its JSON response into a value described by Generic PrimAtoms. Parallel source modes ask Agda to typecheck generated source before accepting it, while mock modes make the same boundary reproducible without launching the interface. Family reflection derives datatype descriptions, constructor names, encoders, decoders, and both directions of the round-trip property for a related set of declarations. The checked examples establish definitional equalities for decoded mocks across constructors, records, certified generics, and mixed primitive fields.