elpi

ELPI - Embeddable λProlog Interpreter
package elpi
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library elpi
Module Elpi . API . RawData
type constant = int

De Bruijn levels (not indexes): the distance of the binder from the root. Starts at 0 and grows for bound variables; global constants have negative values.

type builtin

De Bruijn levels (not indexes): the distance of the binder from the root. Starts at 0 and grows for bound variables; global constants have negative values.

type term = Data.term
type view = private
| Const of constant
| Lam of term
| App of constant * term * term list
| Cons of term * term
| Nil
| Builtin of builtin * term list
| CData of RawOpaqueData.t
| UnifVar of FlexibleData.Elpi.t * term list
val look : depth:int -> term -> view

Terms must be inspected after dereferencing their head. If the resulting term is UVar then its uvar_body is such that get_assignment uvar_body = None

val kool : view -> term
val mkBound : constant -> term

Smart constructors

val mkLam : term -> term
val mkCons : term -> term -> term
val mkNil : term
val mkDiscard : term
val mkCData : RawOpaqueData.t -> term
val mkUnifVar : FlexibleData.Elpi.t -> args:term list -> State.t -> term
val mkGlobal : constant -> term

Lower level smart constructors

val mkApp : constant -> term -> term list -> term
val mkAppL : constant -> term list -> term
val mkBuiltin : builtin -> term list -> term
val mkConst : constant -> term
val cmp_builtin : builtin -> builtin -> int
type hyp = {
hdepth : int;
hsrc : term;
}
type hyps = hyp list
val of_hyps : Data.hyp list -> hyps
type suspended_goal = {
context : hyps;
goal : int * term;
}
val constraints : Data.constraints -> suspended_goal list
val no_constraints : Data.constraints
module Constants : sig ... end
type Conversion.extra_goal +=
| RawGoal of Data.term
val set_extra_goals_postprocessing : ( Conversion.extra_goals -> State.t -> State.t * Conversion.extra_goals ) -> unit