Compiler (u.c73734534e52e3c7e3a6ab4ddda12c49.elpi.3.4.5.doc.elpi.compiler.Elpi

type flags = {

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

}

val default_flags : flags

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

type 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

type program

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

type scoped_program

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

type checked_compilation_unit

type unchecked_compilation_unit

val empty_base : header:header -> program

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

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

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

type checked_compilation_unit_signature

val signature_of_checked_compilation_unit : 
  checked_compilation_unit ->
  checked_compilation_unit_signature

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

type query

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

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

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

val total_type_checking_time : query -> float

val total_det_checking_time : query -> float

val optimize_query : query -> Elpi_runtime.Data.executable

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

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

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

val elpi_language : Compiler_data.Scope.language

val elpi : Compiler_data.QuotationHooks.quotation

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

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

val pp_uvar_body_raw : Format.formatter -> Elpi_runtime.Data.uvar -> unit

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

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

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

module IntervalTree : sig ... end

type type_

val pp_type_ : Format.formatter -> type_ -> unit

type info = {

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

}

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

val hover : checked_compilation_unit -> info IntervalTree.t