elpi

ELPI - Embeddable λProlog Interpreter
package elpi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library elpi
Module Elpi . API . BuiltIn
type doc_spec =
| DocAbove
| DocNext

Where to print the documentation. For the running example DocAbove * generates * % div N M D R division of N by M gives D with reminder R * pred div i:int, i:int, o:int, o:int. * while DocNext generates * pred div % division of N by M gives D with reminder R * i:int, % N * i:int, % M * o:int, % D * o:int. % R * The latter format it is useful to give longer doc for each argument.

type declaration =
| MLCode of BuiltInPredicate.t * doc_spec
| MLData : 'a Conversion.t -> declaration
| MLDataC : ( 'a, 'h, 'c ) ContextualConversion.t -> declaration
| LPDoc of string
| LPCode of string
val declare : file_name:string -> declaration list -> Setup.builtins

What is passed to Setup.init

val document_fmt : Format.formatter -> Setup.builtins -> unit

Prints in LP syntax the "external" declarations. * The file builtin.elpi is generated by calling this API on the * declaration list from elpi_builtin.ml

val document_file : ?header:string -> Setup.builtins -> unit