package elpi

  1. Overview
  2. Docs
exception No_clause
type name = string
type doc = string
type 'a arg =
  1. | Data of 'a
  2. | Flex of Data.term
  3. | Discard
exception TypeErr of Data.term
type 'a data = {
  1. to_term : 'a -> Data.term;
  2. of_term : depth:int -> Data.term -> 'a arg;
  3. ty : string;
}
type ('function_type, 'inernal_outtype_in) ffi =
  1. | In : 't data * doc * ('i, 'o) ffi -> ('t -> 'i, 'o) ffi
  2. | Out : 't data * doc * ('i, 'o * 't option) ffi -> ('t arg -> 'i, 'o) ffi
  3. | Easy : doc -> (depth:int -> 'o, 'o) ffi
  4. | Read : doc -> (depth:int -> Data.hyps -> Data.solution -> 'o, 'o) ffi
  5. | Full : doc -> (depth:int -> Data.hyps -> Data.solution -> Data.custom_constraints * 'o, 'o) ffi
  6. | VariadicIn : 't data * doc -> ('t list -> depth:int -> Data.hyps -> Data.solution -> Data.custom_constraints * 'o, 'o) ffi
  7. | VariadicOut : 't data * doc -> ('t arg list -> depth:int -> Data.hyps -> Data.solution -> Data.custom_constraints * ('o * 't option list option), 'o) ffi
type t =
  1. | Pred : name * ('a, unit) ffi * 'a -> t
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 t * doc_spec
  2. | LPDoc of string
  3. | LPCode of string
val int : int data

Type descriptors

val float : float data
val string : string data
val list : 'a data -> 'a list data
val poly : string -> Data.term data
val any : Data.term data
val data_of_cdata : name:string -> ?constants:'a Data.Constants.Map.t -> 'a CData.cdata -> 'a data
val document : Format.formatter -> declaration list -> unit

Prints in LP syntax the "external" declarations

val builtin_of_declaration : declaration list -> Setup.builtins

What is passed to Setup.init

module Notation : sig ... end