elpi 1.19.2 · OCaml Package

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.

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_hyp : Data.hyp -> hyp

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 : 
  ?descriptor:Setup.hoas_descriptor ->
  (Conversion.extra_goals -> State.t -> State.t * Conversion.extra_goals) ->
  unit

val new_hoas_descriptor : unit -> Setup.hoas_descriptor

package elpi