package elpi

You can search for identifiers within the package.

in-package search v0.2.0

elpi
- Elpi
  - API
    
    AlgebraicData
    
    Ast
    
    Loc
    
    BuiltIn
    
    BuiltInData
    
    BuiltInPredicate
    
    Notation
    
    Compile
    
    StrSet
    
    ContextualConversion
    
    Conversion
    
    Data
    
    StrMap
    
    Execute
    
    FlexibleData
    
    Elpi
    
    Host
    
    Map
    
    Host
    
    Show
    
    OpaqueData
    
    Parse
    
    Pp
    
    Ast
    
    Query
    
    Quotation
    
    RawData
    
    Constants
    
    RawOpaqueData
    
    RawPp
    
    Debug
    
    RawQuery
    
    Setup
    
    State
    
    Utils
    
    IntSet
    
    LocSet
    
    Map
    
    Make
    
    Ord
    
    OrderedType
    
    S
    
    Set
    
    Make
    
    Ord
    
    OrderedType
    
    S
    
    Show
    
    Show1
  - Builtin
  - Builtin_checker
elpi.lexer_config
- Elpi_lexer_config
  - Lexer_config
  - Tokens
elpi.parser
- Elpi_parser
  - Ast
    
    Chr
    
    Clause
    
    Func
    
    Map
    
    Goal
    
    Macro
    
    Mode
    
    Program
    
    Structured
    
    Term
    
    Type
    
    TypeAbbreviation
  - Error_messages
  - Grammar
    
    Make
    
    C
  - Lexer
  - Parse
    
    Config
    
    Make
    
    C
    
    Internal
    
    Parser
    
    Parser_w_Internals
    
    Internal
  - Parser_config
    
    ParseFile
elpi.trace.runtime
- Trace_ppx_runtime
  - Runtime
elpi.util
- Elpi_util
  - Util
    
    CData
    
    Digest
    
    Fork
    
    Hashtbl
    
    HashedType
    
    Make
    
    H
    
    MakeSeeded
    
    H
    
    S
    
    SeededHashedType
    
    SeededS
    
    Int
    
    IntMap
    
    IntSet
    
    Loc
    
    Map
    
    Make
    
    Ord
    
    OrderedType
    
    S
    
    Set
    
    Make
    
    Ord
    
    OrderedType
    
    S
    
    Show
    
    Show1
    
    Show2
    
    StrMap
    
    StrSet
    
    String
    
    UUID
    
    Htbl

Legend:
Library
Module
Module type
Parameter
Class
Class type

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