package elpi

You can search for identifiers within the package.

in-package search v0.2.0

ELPI - Embeddable λProlog Interpreter

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (7)

Authors

Maintainers

E

Enrico Tassi <enrico.tassi@inria.fr>

Sources

elpi-3.0.0.tbz

sha256=424e5a4631f5935a1436093b614917210b00259d16700912488ba4cd148115d1

sha512=fa54ce05101fafe905c6db2e5fa7ad79d714ec3b580add4ff711bad37fc9545a58795f69056d62f6c18d8c87d424acc1992ab7fb667652e980d182d4ed80ba16

doc/elpi.compiler/Elpi_compiler/Compiler/index.html

Module `Elpi_compiler.Compiler`Source

Sourcetype flags = {

defined_variables : Elpi_util.Util.StrSet.t;
print_units : bool;
time_typechecking : bool;
skip_det_checking : 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 total_det_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) Stdlib.Result.t

Source

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

Source

val pp_goal : 
  (pp_ctx:Elpi_runtime.Data.pp_ctx ->
    depth:int ->
    Stdlib.Format.formatter ->
    Elpi_runtime.Data.term ->
    unit) ->
  Stdlib.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

Source

val pp_uvar_body : 
  Stdlib.Format.formatter ->
  Elpi_runtime.Data.uvar_body ->
  unit

Source

val pp_uvar_body_raw : 
  Stdlib.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

Sourcemodule IntervalTree : sig ... end

Sourcetype type_

Sourceval pp_type_ : Stdlib.Format.formatter -> type_ -> unit

Sourcetype info = {

defined : Elpi_parser.Ast.Loc.t option;
type_ : type_ option;

}

Sourceval pp_info : Stdlib.Format.formatter -> info -> unit

Sourceval hover : checked_compilation_unit -> info IntervalTree.t

package elpi

Install

Dune Dependency

Authors

Maintainers

Sources

doc/elpi.compiler/Elpi_compiler/Compiler/index.html

Module Elpi_compiler.CompilerSource

Module `Elpi_compiler.Compiler`Source