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 = Ast.Term.constant

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 =
  1. | Cut
  2. | And
  3. | Impl
  4. | ImplBang
  5. | RImpl
  6. | Pi
  7. | Sigma
  8. | Eq
  9. | Match
  10. | Findall
  11. | Delay
  12. | Host of constant
Sourcetype term = Data.term
Sourcetype view = private
  1. | Const of int
  2. | Lam of term
  3. | App of int * 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 is such that get_assignment uvar = None

Sourceval kool : view -> term
Sourceval mkBound : int -> 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 mkAppGlobal : constant -> term -> term list -> term
Sourceval mkAppGlobalL : constant -> term list -> term
Sourceval mkAppBound : int -> term -> term list -> term
Sourceval mkAppBoundL : int -> term list -> term
Sourceval mkBuiltin : builtin -> term list -> term
Sourceval mkConst : int -> term

no check, works for globals and bound

Sourceval mkApp : int -> term -> term list -> term
Sourceval mkAppMoreArgs : depth:int -> term -> term list -> term
Sourceval isApp : depth:int -> term -> bool
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 blockers = FlexibleData.Elpi.t list
Sourcetype suspended_goal = {
  1. context : hyps;
  2. goal : int * term;
  3. blockers : blockers;
}
Sourceval constraints : Data.constraints -> suspended_goal list
Sourceval no_constraints : Data.constraints
Sourcemodule Constants : sig ... end
Sourceval set_extra_goals_postprocessing : ?descriptor:Setup.hoas_descriptor -> (Conversion.extra_goals -> State.t -> State.t * Conversion.extra_goals) -> unit
Sourceval new_hoas_descriptor : unit -> Setup.hoas_descriptor
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