Compiler (p.elpi.2.0.6.doc.elpi.compiler.Elpi

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

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