Module Elpi_runtime.Data

module Fmt = Format
type indexing =
  1. | MapOn of int
  2. | Hash of int list
  3. | DiscriminationTree of int list

Used to index the parameters of a predicate P

  • MapOn N -> N-th argument at depth 1 (head symbol only)
  • Hash L -> L is the list of depths given by the urer for the parameters of P. Indexing is done by hashing all the parameters with a non zero depth and comparing it with the hashing of the parameters of the query
  • DiscriminationTree L -> we use the same logic of Hash, except we use DiscriminationTree to discriminate clauses
val show_indexing : indexing -> Ppx_deriving_runtime.string
val compare_indexing : indexing -> indexing -> Ppx_deriving_runtime.int
type overlap_clause = {
  1. overlap_loc : Elpi_util.Util.Loc.t option;
  2. has_cut : bool;
  3. mutable timestamp : int list;
  4. arg_nb : int;
}
val show_overlap_clause : overlap_clause -> Ppx_deriving_runtime.string
type overlap =
  1. | Allowed
  2. | Forbidden of overlap_clause Discrimination_tree.t
val show_overlap : overlap -> Ppx_deriving_runtime.string
val mk_Forbidden : indexing -> overlap
type pred_info = {
  1. indexing : indexing;
  2. mode : Elpi_util.Util.Mode.hos;
  3. overlap : overlap;
  4. has_local_without_cut : Elpi_util.Util.Loc.t option;
  5. occur_check : bool;
}
val show_pred_info : pred_info -> Ppx_deriving_runtime.string
val same_indexing : pred_info -> pred_info -> bool
module Term : sig ... end
include module type of struct include Term end
val id_term : Elpi_util.Util.UUID.t
type 'unification_def stuck_goal_kind = 'unification_def Term.stuck_goal_kind = ..
val pp_stuck_goal_kind : 'a -> 'b -> 'c -> unit
val show_stuck_goal_kind : 'a -> 'b -> string
val equal_stuck_goal_kind : 'a -> 'b -> 'b -> bool
type stuck_goal_kind +=
  1. | Unification of 'unification_def
type ttype = Term.ttype =
  1. | TConst of Elpi_util.Util.constant
  2. | TApp of Elpi_util.Util.constant * ttype * ttype list
  3. | TPred of bool * (Elpi_util.Util.Mode.t * ttype) list
  4. | TArr of ttype * ttype
  5. | TCData of Elpi_util.Util.CData.t
  6. | TLam of ttype
val compare_ttype : ttype -> ttype -> Ppx_deriving_runtime.int
type builtin_predicate = Term.builtin_predicate =
  1. | Cut
  2. | And
  3. | Impl
  4. | ImplBang
  5. | RImpl
  6. | Pi
  7. | Sigma
  8. | Eq
  9. | Match
  10. | Findall
  11. | Delay
  12. | Host of Elpi_util.Util.constant
val compare_builtin_predicate : builtin_predicate -> builtin_predicate -> Ppx_deriving_runtime.int
val builtin_predicates : builtin_predicate list
val builtin_predicate_max : int
val func_of_builtin_predicate : (Elpi_util.Util.constant -> F.t) -> builtin_predicate -> F.t
val show_builtin_predicate : ?table:'a -> (?table:'a -> Elpi_util.Util.constant -> string) -> builtin_predicate -> string
val const_of_builtin_predicate : builtin_predicate -> Elpi_util.Util.constant
val is_builtin_predicate : int -> bool
val builtin_predicate_of_const : int -> builtin_predicate
type term = Term.term =
  1. | Const of Elpi_util.Util.constant
  2. | Lam of term
  3. | App of Elpi_util.Util.constant * term * term list
  4. | Cons of term * term
  5. | Nil
  6. | Discard
  7. | Builtin of builtin_predicate * term list
  8. | CData of Elpi_util.Util.CData.t
  9. | UVar of uvar * int
  10. | AppUVar of uvar * term list
  11. | Arg of int * int
  12. | AppArg of int * term list
and uvar = Term.uvar = {
  1. vardepth : int;
  2. mutable contents : term;
  3. mutable uid_private : int;
}
val compare_term : term -> term -> Ppx_deriving_runtime.int
val compare_uvar : uvar -> uvar -> Ppx_deriving_runtime.int
val cons2tcons : ?loc:Elpi_util.Util.Loc.t -> term -> ttype
val uvar_id : uvar -> int
val uvar_is_a_blocker : uvar -> bool
val uvar_isnt_a_blocker : uvar -> bool
val uvar_set_blocker : uvar -> unit
val uvar_unset_blocker : uvar -> unit
type clause = Term.clause = {
  1. depth : int;
  2. args : term list;
  3. hyps : term list;
  4. vars : int;
  5. oc : bool;
  6. mode : Elpi_util.Util.Mode.hos;
  7. loc : Elpi_util.Util.Loc.t option;
  8. mutable timestamp : int list;
}
val show_clause : clause -> Ppx_deriving_runtime.string
val compare_clause : clause -> clause -> Ppx_deriving_runtime.int
type grafting_time = int list
val show_grafting_time : grafting_time -> Ppx_deriving_runtime.string
val compare_grafting_time : grafting_time -> grafting_time -> Ppx_deriving_runtime.int
val compare_constant : Elpi_util.Util.constant -> Elpi_util.Util.constant -> int
val compare_times : times -> times -> Ppx_deriving_runtime.int
type stuck_goal = Term.stuck_goal = {
  1. mutable blockers : blockers;
  2. kind : unification_def stuck_goal_kind;
}
and blockers = uvar list
and unification_def = Term.unification_def = {
  1. adepth : int;
  2. env : term array;
  3. bdepth : int;
  4. a : term;
  5. b : term;
  6. matching : bool;
  7. oc : bool;
}
and clause_src = Term.clause_src = {
  1. hdepth : int;
  2. hsrc : term;
}
and prolog_prog = Term.prolog_prog = {
  1. src : clause_src list;
  2. index : index;
}
and clause_list = clause Bl.t
and index = first_lvl_idx
and first_lvl_idx = Term.first_lvl_idx = {
  1. idx : second_lvl_idx Ptmap.t;
  2. time : int;
  3. times : times;
}
and second_lvl_idx = Term.second_lvl_idx =
  1. | TwoLevelIndex of {
    1. mode : Elpi_util.Util.Mode.hos;
    2. argno : int;
    3. all_clauses : clause_list;
    4. flex_arg_clauses : clause_list;
    5. arg_idx : clause_list Ptmap.t;
    }
  2. | BitHash of {
    1. mode : Elpi_util.Util.Mode.hos;
    2. args : int list;
    3. args_idx : clause_list Ptmap.t;
    }
  3. | IndexWithDiscriminationTree of {
    1. mode : Elpi_util.Util.Mode.hos;
    2. arg_depths : int list;
    3. args_idx : clause Discrimination_tree.t;
    }
val show_stuck_goal : stuck_goal -> Ppx_deriving_runtime.string
val show_blockers : blockers -> Ppx_deriving_runtime.string
val show_unification_def : unification_def -> Ppx_deriving_runtime.string
val show_clause_src : clause_src -> Ppx_deriving_runtime.string
val show_prolog_prog : prolog_prog -> Ppx_deriving_runtime.string
val show_clause_list : clause_list -> Ppx_deriving_runtime.string
val show_first_lvl_idx : index -> Ppx_deriving_runtime.string
val show_second_lvl_idx : second_lvl_idx -> Ppx_deriving_runtime.string
type occur_check = Term.occur_check =
  1. | Skip
  2. | No
  3. | Check of uvar
val stop : bool ref
val close_index : index -> index
type constraints = stuck_goal list
type hyps = clause_src list
type suspended_goal = Term.suspended_goal = {
  1. context : hyps;
  2. goal : int * term;
  3. blockers : blockers;
}
val mkLam : term -> term
val mkApp : Elpi_util.Util.constant -> term -> term list -> term
val mkCons : term -> term -> term
val mkNil : term
val mkDiscard : term
val mkBuiltin : builtin_predicate -> term list -> term
val mkCData : Elpi_util.Util.CData.t -> term
val mkUVar : uvar -> int -> term
val mkAppUVar : uvar -> term list -> term
val mkArg : int -> int -> term
val mkAppArg : int -> term list -> term
module C = Term.C
val destConst : term -> Elpi_util.Util.constant
val oref : depth:int -> term -> uvar
val (!!) : uvar -> term
type env = term array
val empty_env : 'a array
module State : sig ... end
val elpi_state_descriptor : State.descriptor
type core_symbol =
  1. | As
  2. | Uv
  3. | ECons
  4. | ENil
val min_core_symbol : int
val max_core_symbol : int
val core_symbol_to_enum : core_symbol -> int
val core_symbol_of_enum : int -> core_symbol option
val compare_core_symbol : core_symbol -> core_symbol -> Ppx_deriving_runtime.int
val show_core_symbol : core_symbol -> Ppx_deriving_runtime.string
val func_of_core_symbol : core_symbol -> F.t
val is_core_symbol : F.t -> bool
module Symbol : sig ... end
module Global_symbols : sig ... end
val dummy : term
val dummy_uvar_body : uvar
module CHR : sig ... end
type clause_w_info = {
  1. clloc : Elpi_util.Util.CData.t;
  2. clargsname : string list;
  3. clbody : clause;
}
val show_clause_w_info : clause_w_info -> Ppx_deriving_runtime.string
exception No_clause
exception No_more_steps
exception Flex_head
module Conversion : sig ... end
module ContextualConversion : sig ... end
val while_compiling : bool State.component
module HoasHooks : sig ... end
module CalcHooks : sig ... end
module BuiltInPredicate : sig ... end
type symbol_table = {
  1. mutable c2s : Symbol.t Elpi_util.Util.Constants.Map.t;
  2. c2t : (Elpi_util.Util.constant, term) Elpi_util.Util.Hashtbl.t;
  3. mutable frozen_constants : int;
}
val show_symbol_table : symbol_table -> Ppx_deriving_runtime.string
type executable = {
  1. compiled_program : prolog_prog;
  2. chr : CHR.t;
  3. initial_depth : int;
  4. initial_goal : term;
  5. initial_runtime_state : State.t;
  6. symbol_table : symbol_table;
  7. builtins : BuiltInPredicate.builtin_table;
  8. assignments : term Elpi_util.Util.StrMap.t;
}
type pp_ctx = {
  1. uv_names : (string Elpi_util.Util.IntMap.t * int) ref;
  2. table : symbol_table;
}
type solution = {
  1. assignments : term Elpi_util.Util.StrMap.t;
  2. constraints : constraints;
  3. state : State.t;
  4. pp_ctx : pp_ctx;
  5. state_for_relocation : int * symbol_table;
}
type 'a outcome =
  1. | Success of solution
  2. | Failure
  3. | NoMoreSteps
exception CannotDeclareClauseForBuiltin of Elpi_util.Util.Loc.t option * builtin_predicate