elpi 1.2.0 · 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. The UVar * and AppUVar node hence stand for unassigned unification variables.

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 uvar_body

type term

type view = private

| Const of constant
| Lam of term
| App of constant * term * term list
| Cons of term * term
| Nil
| Discard
| Builtin of builtin * term list
| CData of CData.t
| UVar of uvar_body * int * int
| AppUVar of uvar_body * int * term list
| Arg of int * int
| AppArg of int * term list

val mkGlobalS : string -> term

Smart constructors

val mkBound : constant -> term

val mkLam : term -> term

val mkAppS : string -> term -> term list -> term

val mkCons : term -> term -> term

val mkNil : term

val mkDiscard : term

val mkBuiltinS : string -> term list -> term

val mkCData : CData.t -> term

val mkGlobal : constant -> term

Lower level smart constructors

val mkApp : constant -> term -> term list -> term

val mkBuiltin : builtin -> term list -> term

val mkUVar : uvar_body -> int -> int -> term

val mkAppUVar : uvar_body -> int -> term list -> term

val mkConst : constant -> term

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

type clause_src = {

hdepth : int;
hsrc : term;

}

val of_term : Data.term -> term

val fresh_uvar_body : unit -> uvar_body

type custom_state = Data.custom_state

type constraints = Data.constraints

module StrMap = Data.StrMap

type solution = {

assignments : term StrMap.t;
constraints : constraints;
state : custom_state;

}

val of_solution : Data.solution -> solution

type hyps = clause_src list

type suspended_goal = {

context : hyps;
goal : int * term;

}

val constraints : Data.constraints -> suspended_goal list

module C : sig ... end

LambdaProlog built-in data types

module Constants : sig ... end

LambdaProlog built-in global constants

package elpi