elpi 2.0.4 · OCaml Package

type flags = {

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

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

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

val elpi_language : Compiler_data.Scope.language

val elpi : Compiler_data.QuotationHooks.quotation

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

val pp : Stdlib.Format.formatter -> Elpi_runtime.Data.uvar_body -> 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

package elpi