Scope

ff-json-unsafe extends ff-json with compile-time integrations that execute external programs. Its module hierarchy covers generation through a Node-based script, validation through jq, validation samples, and dedicated test modules. Reflection code connects external command output back to Agda terms and the typechecker. Separate generation and validation tests exercise this boundary against the library’s native JSON representation. With --allow-exec enabled at library level, this package is intentionally the external-tool integration layer rather than the core JSON model.

Most important results

The library provides a macro that converts literal JSON input into a checked JsonValue through an external Node generator. It also provides a jq-backed macro that accepts valid rendered JSON and turns rejection into an Agda type error. Both external paths retain command input, standard output, and standard error for useful failure diagnostics. Generator tests, general JSON tests, and validation samples make these integrations part of the typechecked library surface.