package elpi

  1. Overview
  2. Docs

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

type doc_spec =
  1. | DocAbove
  2. | 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 =
  1. | MLCode of BuiltInPredicate.t * doc_spec
  2. | MLData : 'a Conversion.t -> declaration
  3. | MLDataC : ('a, 'h, 'c) ContextualConversion.t -> declaration
  4. | LPDoc of string
  5. | LPCode of string
val declare : file_name:string -> declaration list -> Setup.builtins

What is passed to Setup.init

val document_fmt : Stdlib.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