elpi 1.2.0 · OCaml Package

exception No_clause

type name = string

type doc = string

type ty_ast =

| TyName of string
| TyApp of string * ty_ast * ty_ast list

type 'a oarg =

| Keep
| Discard

type 'a ioarg =

| Data of 'a
| 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 = {

ty : ty_ast;
doc : doc;
embed : 'a embedding;
readback : 'a readback;

}

exception TypeErr of ty_ast * Data.term

type ('function_type, 'inernal_outtype_in) ffi =

| In : 't data * doc * ('i, 'o) ffi -> ('t -> 'i, 'o) ffi
| Out : 't data * doc * ('i, 'o * 't option) ffi -> ('t oarg -> 'i, 'o) ffi
| InOut : 't data * doc * ('i, 'o * 't option) ffi -> ('t ioarg -> 'i, 'o) ffi
| Easy : doc -> (depth:int -> 'o, 'o) ffi
| Read : doc -> (depth:int -> Data.hyps -> Data.solution -> 'o, 'o) ffi
| Full : doc -> (depth:int -> Data.hyps -> Data.solution -> Data.custom_state * 'o, 'o) ffi
| VariadicIn : 't data * doc -> ('t list -> depth:int -> Data.hyps -> Data.solution -> Data.custom_state * 'o, 'o) ffi
| VariadicOut : 't data * doc -> ('t oarg list -> depth:int -> Data.hyps -> Data.solution -> Data.custom_state * ('o * 't option list option), 'o) ffi
| 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 =

| 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 =

| 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 t * doc_spec
| MLADT : 'a ADT.adt -> declaration
| MLCData : 'a data * 'a CData.cdata -> declaration
| LPDoc of string
| 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

package elpi