package elpi

  1. Overview
  2. Docs

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
  1. | Const of constant
  2. | Lam of term
  3. | App of constant * term * term list
  4. | Cons of term * term
  5. | Nil
  6. | Discard
  7. | Builtin of builtin * term list
  8. | CData of CData.t
  9. | UVar of uvar_body * int * int
  10. | AppUVar of uvar_body * int * term list
  11. | Arg of int * int
  12. | AppArg of int * term list
val mkConst : constant -> term

Smart constructors

val mkLam : term -> term
val mkApp : constant -> term -> term list -> term
val mkCons : term -> term -> term
val mkNil : term
val mkDiscard : term
val mkBuiltin : builtin -> term list -> term
val mkBuiltinName : string -> term list -> term
val mkCData : CData.t -> term
val mkUVar : uvar_body -> int -> int -> term
val mkAppUVar : uvar_body -> int -> term list -> 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 = {
  1. hdepth : int;
  2. hsrc : term;
}
val of_term : Data.term -> term
val fresh_uvar_body : unit -> uvar_body
type custom_constraints = Data.custom_constraints
type solution = Data.solution
type idx
type hyps = clause_src list
type suspended_goal = {
  1. context : hyps;
  2. goal : int * term;
}
val constraints : Data.syntactic_constraints -> suspended_goal list
module C : sig ... end

LambdaProlog built-in data types

module Constants : sig ... end

LambdaProlog built-in global constants