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 declared_builtins

val declare_builtins : 
  file_name:string ->
  Elpi_runtime.Data.BuiltInPredicate.declaration list ->
  declared_builtins

Sourceval declared_builtins_of_file : file_name:string -> declared_builtins

Sourceval file_of_declared_builtins : declared_builtins -> string

Source

val document_fmt : 
  Format.formatter ->
  calc:Elpi_runtime.Data.CalcHooks.descriptor ->
  declared_builtins ->
  unit

Source

val document_file : 
  ?header:string ->
  calc:Elpi_runtime.Data.CalcHooks.descriptor ->
  file:string ->
  declared_builtins ->
  unit

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 ->
  declared_builtins list ->
  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 ->
  ?calc:Elpi_runtime.Data.CalcHooks.descriptor ->
  ?builtins:declared_builtins list ->
  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:declared_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) 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 Elpi_util.Util.StrMap.t
    Elpi_runtime.Data.State.component

Sourceval pp_uvar_body : Format.formatter -> Elpi_runtime.Data.uvar -> unit

Sourceval pp_uvar_body_raw : Format.formatter -> Elpi_runtime.Data.uvar -> 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_ : Format.formatter -> type_ -> unit

Sourcetype info = {

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

}

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

Sourceval hover : checked_compilation_unit -> info IntervalTree.t

Install

dune-project
Dependency

Authors

Maintainers

Sources

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

Module `Elpi_compiler.Compiler`Source

package elpi

Install

dune-project Dependency

Authors

Maintainers

Sources

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

Module Elpi_compiler.CompilerSource

dune-project
Dependency

Module `Elpi_compiler.Compiler`Source