Scope

ff-owl-unsafe is a compact integration layer for bringing external OBOGraph JSON into Agda while a module is being typechecked. Its macro machinery combines Agda reflection with an executable bridge that derives checked terms from file paths. Imported data can remain a native JSON value or be decoded as an OBOGraph document and translated into the library’s portable OWL 2 representation. The example module exercises both the staged decoding path and a convenience import path using a logical-definition document. This deliberately unsafe boundary is isolated in a companion library whose flags explicitly permit external execution.

Most important results

The library provides a macro that imports an OBOGraph file directly as a native JSON value. A second macro performs decoding and conversion so that the generated term has the portable OWL 2 ontology-document type. Failed external commands are converted into typechecking errors that preserve the source path together with captured standard output and standard error. The checked example establishes successful decoding and constructs ontology-document values through both explicit and convenience workflows.