elpi 1.3.1 · OCaml Package

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 ADS. No support for binders or unification variables at thil point.

module Conversion : sig ... end

This module defines what embedding and readback functions are

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" | let option_declaration a = { ty = TyApp("option",a.ty,[]); doc = "The option type (aka Maybe)"; pp = (fun fmt -> function | None -> Format.fprintf fmt "None" | Some x -> Format.fprintf fmt "Some %a" a.pp x); constructors = [ K("none","nothing in this case", N, (* no arguments *) B None, (* builder *) M (fun ~ok ~ko -> function None -> ok | _ -> ko ())); (* matcher *) K("some","something in this case", A (a,N), (* one argument of type a *) B (fun x -> Some x), (* builder *) M (fun ~ok ~ko -> function Some x -> ok x | _ -> ko ())); (* matcher *) ]

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 view. The 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

package elpi