Setup.init takes a list of declarations of data types and predicates, plus some doc and eventually some Elpi code. All this constitutes the "prelude", that is what is avaiable to an Elpi program
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 stringval declare : file_name:string -> declaration list -> Setup.builtinsWhat is passed to Setup.init
val document_fmt :
Format.formatter ->
?calc:Setup.calc_descriptor ->
Setup.builtins ->
unitPrints 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 ->
?calc:Setup.calc_descriptor ->
Setup.builtins ->
unit