package elpi

  1. Overview
  2. Docs
exception No_clause
type name = string
type doc = string
type ty_ast =
  1. | TyName of string
  2. | TyApp of string * ty_ast * ty_ast list
type 'a oarg =
  1. | Keep
  2. | Discard
type 'a ioarg =
  1. | Data of 'a
  2. | NoData
type extra_goals = Data.term list
type 'a embedding = depth:int -> Data.hyps -> Data.solution -> 'a -> Data.custom_state * Data.term * extra_goals
type 'a readback = depth:int -> Data.hyps -> Data.solution -> Data.term -> Data.custom_state * 'a
type 'a data = {
  1. ty : ty_ast;
  2. doc : doc;
  3. embed : 'a embedding;
  4. readback : 'a readback;
}
exception TypeErr of ty_ast * Data.term
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 oarg -> 'i, 'o) ffi
  3. | InOut : 't data * doc * ('i, 'o * 't option) ffi -> ('t ioarg -> 'i, 'o) ffi
  4. | Easy : doc -> (depth:int -> 'o, 'o) ffi
  5. | Read : doc -> (depth:int -> Data.hyps -> Data.solution -> 'o, 'o) ffi
  6. | Full : doc -> (depth:int -> Data.hyps -> Data.solution -> Data.custom_state * 'o, 'o) ffi
  7. | VariadicIn : 't data * doc -> ('t list -> depth:int -> Data.hyps -> Data.solution -> Data.custom_state * 'o, 'o) ffi
  8. | VariadicOut : 't data * doc -> ('t oarg list -> depth:int -> Data.hyps -> Data.solution -> Data.custom_state * ('o * 't option list option), 'o) ffi
  9. | VariadicInOut : 't data * doc -> ('t ioarg list -> depth:int -> Data.hyps -> Data.solution -> Data.custom_state * ('o * 't option list option), 'o) ffi
type t =
  1. | Pred : name * ('a, unit) ffi * 'a -> t
module ADT : sig ... end

Commodity API for representing simple ADT: no binders! * * Example of: pred getenv i:string, o:option string. * * (* define the ADT for "option a" *) * let option_adt a = * ty = TyApp("option",a.ty,[]); * doc = "The option type (aka Maybe)"; * constructors = [ * * K("none","nothing in this case", * N, (* no arguments *) * None, (* builder *) * (fun ~ok ~ko -> function None -> ok | _ -> ko)); (* matcher *) * K("some","something in this case", * A(a,N), (* one argument of type a *) * (fun x -> Some x), (* builder *) * (fun ~ok ~ko -> function Some x -> ok x | _ -> ko)); (* matcher *) * ] * * (* compile the ADT to data types to be used in predicate signatures *) * let option a : a data = adt (option_adt a) * * (* define a predicate using "option" *) * let getenv : t = * Pred("getenv", * In(string, "VarName", * Out(option string, "Value", * Easy "Like Sys.getenv")), * (fun name _ ~depth -> * try !: (Some (Sys.getenv name)) * with Not_found -> !: None)) *

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. | MLADT : 'a ADT.adt -> declaration
  3. | MLCData : 'a data * 'a CData.cdata -> declaration
  4. | LPDoc of string
  5. | LPCode of string
val int : int data

Type descriptors (see also Elpi_builtin)

val float : float data
val string : string data
val list : 'a data -> 'a list data
val loc : Ast.Loc.t data
val poly : string -> Data.term data
val any : Data.term data
val cdata : name:string -> ?doc:doc -> ?constants:'a Data.Constants.Map.t -> 'a CData.cdata -> 'a data
val adt : 'a ADT.adt -> 'a data
val map_acc_embed : (Data.solution -> 'a -> Data.custom_state * 'b * extra_goals) -> Data.solution -> 'a list -> Data.custom_state * 'b list * extra_goals
val map_acc_readback : (Data.solution -> 'a -> Data.custom_state * 'b) -> Data.solution -> 'a list -> Data.custom_state * 'b list
val document : Format.formatter -> declaration list -> 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 builtin_of_declaration : file_name:string -> declaration list -> Setup.builtins

What is passed to Setup.init

module Notation : sig ... end