elpi 1.1.0 · OCaml Package

exception No_clause

type name = string

type doc = string

type 'a arg =

| Data of 'a
| Flex of Data.term
| Discard

exception TypeErr of Data.term

type 'a data = {

to_term : 'a -> Data.term;
of_term : depth:int -> Data.term -> 'a arg;
ty : string;

}

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 arg -> '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 arg 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

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
| LPDoc of string
| 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

package elpi