package elpi

  1. Overview
  2. Docs
package elpi
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module API.RawDataSource

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.

Sourcetype 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.

Sourcetype 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.

Sourcetype term = Data.term
Sourcetype 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. | Builtin of builtin * term list
  7. | CData of RawOpaqueData.t
  8. | UnifVar of FlexibleData.Elpi.t * term list
Sourceval 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

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

Smart constructors

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

Lower level smart constructors

Sourceval mkApp : constant -> term -> term list -> term
Sourceval mkAppL : constant -> term list -> term
Sourceval mkBuiltin : builtin -> term list -> term
Sourceval mkConst : constant -> term
Sourceval cmp_builtin : builtin -> builtin -> int
Sourcetype hyp = {
  1. hdepth : int;
  2. hsrc : term;
}
Sourcetype hyps = hyp list
Sourceval of_hyp : Data.hyp -> hyp
Sourceval of_hyps : Data.hyp list -> hyps
Sourcetype suspended_goal = {
  1. context : hyps;
  2. goal : int * term;
}
Sourceval constraints : Data.constraints -> suspended_goal list
Sourceval no_constraints : Data.constraints
Sourcemodule Constants : sig ... end
Sourceval set_extra_goals_postprocessing : (Conversion.extra_goals -> State.t -> State.t * Conversion.extra_goals) -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct