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 ... end
module Setup : sig ... end
module Parse : sig ... end
module Data : sig ... end
module Compile : sig ... end
module Execute : sig ... end
module Pp : sig ... end
This 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 ... end
This module defines what embedding and readback functions are
module ContextualConversion : sig ... end
This module defines what embedding and readback functions are for datatypes that need the context of the program (hypothetical clauses and constraints)
module BuiltInData : sig ... end
Conversion for Elpi's built-in data types
module OpaqueData : sig ... end
Declare data from the host application that is opaque (no syntax), like int but not like list or pair
module AlgebraicData : sig ... end
Declare 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 ... end
module BuiltIn : sig ... end
Setup.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
module Query : sig ... end
Commodity module to build a simple query and extract the output from the solution found by Elpi.
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 ... end
State 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 ... end
Flexible 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 ... end
Low level module for OpaqueData
module RawData : sig ... end
This 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
look view automatically * substitutes assigned unification variables by their value.
module RawQuery : sig ... end
This module lets one generate a query by providing a RawData.term directly
module Quotation : sig ... end
module Utils : sig ... end
module RawPp : sig ... end