package elpi

You can search for identifiers within the package.

in-package search v0.2.0

package elpi

elpi
- Library elpi
  - Elpi
    
    API
    
    Ast
    
    Loc
    
    Name
    
    Set
    
    Map
    
    Scope
    
    Map
    
    Opaque
    
    Type
    
    Term
    
    Setup
    
    StrMap
    
    Parse
    
    Compile
    
    StrSet
    
    Data
    
    StrMap
    
    Execute
    
    Pp
    
    Ast
    
    Conversion
    
    ContextualConversion
    
    BuiltInData
    
    OpaqueData
    
    AlgebraicData
    
    BuiltInPredicate
    
    Notation
    
    HOAdaptors
    
    BuiltIn
    
    State
    
    FlexibleData
    
    Elpi
    
    Host
    
    Map
    
    Show
    
    RawOpaqueData
    
    Calc
    
    RawData
    
    Constants
    
    Map
    
    Set
    
    RawQuery
    
    Quotation
    
    Utils
    
    Show
    
    Show1
    
    Map
    
    S
    
    OrderedType
    
    Make
    
    Set
    
    S
    
    OrderedType
    
    Make
    
    IntSet
    
    LocSet
    
    RawPp
    
    Debug
    
    Builtin
    
    Builtin_map
    
    Builtin_set
    
    Builtin_stdlib
- Library elpi.compiler
  - Elpi_compiler
    
    Compiler
    
    Compiler_data
    
    F
    
    Scope
    
    Map
    
    Set
    
    ScopeContext
    
    ScopedTypeExpression
    
    SimpleType
    
    MutableOnce
    
    TypeAssignment
    
    ScopedTerm
    
    SimpleTerm
    
    QTerm
    
    TypeList
    
    State
    
    QuotationHooks
    
    Arity
    
    Determinacy_checker
    
    merger
    
    Type_checker
- Library elpi.lexer_config
  - Elpi_lexer_config
    
    Lexer_config
    
    Tokens
- Library elpi.parser
  - Elpi_parser
    
    Ast
    
    Loc
    
    Func
    
    Map
    
    Set
    
    Mode
    
    TypeExpression
    
    Term
    
    Clause
    
    Chr
    
    Macro
    
    Type
    
    TypeAbbreviation
    
    Program
    
    Goal
    
    Structured
    
    Error_messages
    
    Grammar
    
    Make
    
    Lexer
    
    Parse
    
    Parser
    
    Parser_w_Internals
    
    Internal
    
    Config
    
    Make
    
    Internal
    
    Parser_config
    
    ParseFile
- Library elpi.runtime
  - Elpi_runtime
    
    Bl
    
    Data
    
    Fmt
    
    F
    
    Term
    
    C
    
    C
    
    State
    
    Global_symbols
    
    CHR
    
    Conversion
    
    ContextualConversion
    
    HoasHooks
    
    CalcHooks
    
    BuiltInPredicate
    
    ADT
    
    Discrimination_tree
    
    Path
    
    Internal
    
    Ptmap
    
    Runtime
    
    Pp
    
    CompileTime
    
    Runtime_trace_off
    
    Pp
    
    CompileTime
- Library elpi.util
  - Elpi_util
    
    Util
    
    Show
    
    Show1
    
    Show2
    
    Map
    
    S
    
    OrderedType
    
    Make
    
    Set
    
    S
    
    OrderedType
    
    Make
    
    Int
    
    Bool
    
    String
    
    StrMap
    
    IntMap
    
    StrSet
    
    IntSet
    
    Digest
    
    S
    
    BLAKE128
    
    BLAKE256
    
    BLAKE512
    
    MD5
    
    Hashtbl
    
    HashedType
    
    S
    
    Make
    
    SeededHashedType
    
    SeededS
    
    MakeSeeded
    
    Loc
    
    UUID
    
    Htbl
    
    Fork
    
    CData
    
    Constants
    
    Map
    
    Set
- Library trace_ppx
  - Trace_ppx
- Library trace_ppx_runtime
  - Trace_ppx_runtime
    
    Runtime
- Sources
  - elpi
    
    API.ml
    
    builtin.ml
    
    elpi.ml
  - elpi.compiler
    
    compiler.ml
    
    compiler_data.ml
    
    determinacy_checker.ml
    
    elpi_compiler.ml
    
    type_checker.ml
  - elpi.lexer_config
    
    elpi_lexer_config.ml
    
    lexer_config.ml
    
    tokens.ml
  - elpi.parser
    
    ast.ml
    
    elpi_parser.ml
    
    error_messages.ml
    
    grammar.ml
    
    lexer.ml
    
    parse.ml
    
    parser_config.ml
  - elpi.runtime
    
    bl.ml
    
    data.ml
    
    discrimination_tree.ml
    
    elpi_runtime.ml
    
    ptmap.ml
    
    runtime.ml
    
    runtime_trace_off.ml
  - elpi.util
    
    elpi_util.ml
    
    util.ml
  - trace_ppx
    
    trace_ppx.ml
  - trace_ppx_runtime
    
    runtime.ml
    
    trace_ppx_runtime.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Elpi_compiler.Compiler`Source

Sourcetype flags = {

defined_variables : Elpi_util.Util.StrSet.t;
print_units : bool;
time_typechecking : bool;

}

Sourceval default_flags : flags

Sourcetype builtins = string * Elpi_runtime.Data.BuiltInPredicate.declaration list

Sourcetype header

Source

val header_of_ast : 
  flags:flags ->
  parser:(module Elpi_parser.Parse.Parser) ->
  Elpi_runtime.Data.State.descriptor ->
  Compiler_data.QuotationHooks.descriptor ->
  Elpi_runtime.Data.HoasHooks.descriptor ->
  Elpi_runtime.Data.CalcHooks.descriptor ->
  builtins list ->
  Elpi_parser.Ast.Program.t ->
  header

Sourcetype program

Source

val program_of_ast : 
  flags:flags ->
  header:header ->
  Elpi_parser.Ast.Program.t ->
  program

Sourcetype scoped_program

Source

val scoped_of_ast : 
  flags:flags ->
  header:header ->
  Elpi_parser.Ast.Program.t ->
  scoped_program

Sourcetype checked_compilation_unit

Sourcetype unchecked_compilation_unit

Sourceval empty_base : header:header -> program

Source

val unit_of_scoped : 
  flags:flags ->
  header:header ->
  ?builtins:builtins list ->
  scoped_program ->
  unchecked_compilation_unit

Source

val append_unit : 
  flags:flags ->
  base:program ->
  checked_compilation_unit ->
  program

Source

val check_unit : 
  flags:flags ->
  base:program ->
  unchecked_compilation_unit ->
  checked_compilation_unit

Sourcetype checked_compilation_unit_signature

Source

val signature_of_checked_compilation_unit : 
  checked_compilation_unit ->
  checked_compilation_unit_signature

Source

val append_unit_signature : 
  flags:flags ->
  base:program ->
  checked_compilation_unit_signature ->
  program

Sourcetype query

Source

val query_of_ast : 
  program ->
  Elpi_parser.Ast.Goal.t ->
  (Elpi_runtime.Data.State.t -> Elpi_runtime.Data.State.t) ->
  query

Source

val query_of_scoped_term : 
  program ->
  (Elpi_runtime.Data.State.t ->
    Elpi_runtime.Data.State.t * Compiler_data.ScopedTerm.t) ->
  query

Source

val query_of_raw_term : 
  program ->
  (Elpi_runtime.Data.State.t ->
    Elpi_runtime.Data.State.t
    * Elpi_runtime.Data.term
    * Elpi_runtime.Data.Conversion.extra_goals) ->
  query

Sourceval total_type_checking_time : query -> float

Sourceval optimize_query : query -> Elpi_runtime.Data.executable

Source

val relocate_closed_term : 
  from:Elpi_runtime.Data.symbol_table ->
  to_:program ->
  Elpi_runtime.Data.term ->
  (Elpi_runtime.Data.term, string) Result.t

Source

val pp_program : 
  (pp_ctx:Elpi_runtime.Data.pp_ctx ->
    depth:int ->
    Format.formatter ->
    Elpi_runtime.Data.term ->
    unit) ->
  Format.formatter ->
  program ->
  unit

Source

val pp_goal : 
  (pp_ctx:Elpi_runtime.Data.pp_ctx ->
    depth:int ->
    Format.formatter ->
    Elpi_runtime.Data.term ->
    unit) ->
  Format.formatter ->
  query ->
  unit

Sourceval elpi_language : Compiler_data.Scope.language

Sourceval elpi : Compiler_data.QuotationHooks.quotation

Source

val uvk : 
  Elpi_runtime.Data.uvar_body Elpi_util.Util.StrMap.t
    Elpi_runtime.Data.State.component

Sourceval pp : Format.formatter -> Elpi_runtime.Data.uvar_body -> unit

Source

val compile_term_to_raw_term : 
  ?check:bool ->
  Elpi_runtime.Data.State.t ->
  program ->
  ?ctx:Elpi_util.Util.constant Compiler_data.Scope.Map.t ->
  depth:int ->
  Compiler_data.ScopedTerm.t ->
  Elpi_runtime.Data.State.t * Elpi_runtime.Data.term

Source

val runtime_hack_term_to_raw_term : 
  Elpi_runtime.Data.State.t ->
  program ->
  ?ctx:Elpi_util.Util.constant Compiler_data.Scope.Map.t ->
  depth:int ->
  Compiler_data.ScopedTerm.t ->
  Elpi_runtime.Data.term

Source

val global_name_to_constant : 
  Elpi_runtime.Data.State.t ->
  string ->
  Elpi_util.Util.constant

package elpi

Module Elpi_compiler.CompilerSource

Module `Elpi_compiler.Compiler`Source