This module is the API for clients of the Elpi library.
These APIs are sufficient to parse programs and queries from text, run the interpreter and finally print the result
module Ast : sig ... endmodule Setup : sig ... endmodule Parse : sig ... endmodule Compile : sig ... endmodule Data : sig ... endmodule Execute : sig ... endmodule Pp : sig ... endThis API lets one exchange with the host application opaque (primitive) data such as integers or strings as well as algebraic data such OCaml's ADT. No support for binders or unification variables at this point, see the RawData module.
module Conversion : sig ... endThis module defines what embedding and readback functions are
module ContextualConversion : sig ... endThis module defines what embedding and readback functions are for datatypes that need the context of the program (hypothetical clauses and constraints)
module BuiltInData : sig ... endConversion for Elpi's built-in data types
module OpaqueData : sig ... endDeclare data from the host application that is opaque (no syntax), like int but not like list or pair
module AlgebraicData : sig ... endDeclare data from the host application that has syntax, like list or pair but not like int. So far there is no support for data with binder using this API. The type of each constructor is described using a GADT so that the code to build or match the data can be given the right type. Example: define the ADT for "option a"
module BuiltInPredicate : sig ... endmodule BuiltIn : sig ... endSetup.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
This API lets one access the low lever representation of terms in order to exchange data with binders and unification variables with the host application. It also lets one define quotations and extend the state theraded by Elpi with custom data.
module State : sig ... endState is a collection of purely functional piece of data carried by the interpreter. Such data is kept in sync with the backtracking, i.e. changes made in a branch are lost if that branch fails. It can be used to both store custom constraints to be manipulated by custom solvers, or any other piece of data the host application may need to use.
module FlexibleData : sig ... endFlexible data is for unification variables. One can use Elpi's unification variables to represent the host equivalent, here the API the keep a link between the two.
module RawOpaqueData : sig ... endLow level module for OpaqueData
module Calc : sig ... endmodule RawData : sig ... endThis module exposes the low level representation of terms. * * The data type term is opaque and can only be accessed by using the * look API that exposes a term view. The look view automatically * substitutes assigned unification variables by their value.
module RawQuery : sig ... endThis module lets one generate a query by providing a RawData.term directly
module Quotation : sig ... endmodule Utils : sig ... endmodule RawPp : sig ... end