package elpi

  1. Overview
  2. Docs
package elpi
Legend:
Library
Module
Module type
Parameter
Class
Class type
val id_term : Elpi_util.Util.UUID.t
type 'unification_def 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 arg_mode = Elpi_util.Util.arg_mode =
  1. | Input
  2. | Output
val pp_arg_mode : Ppx_deriving_runtime.Format.formatter -> arg_mode -> Ppx_deriving_runtime.unit
val show_arg_mode : arg_mode -> Ppx_deriving_runtime.string
val compare_arg_mode : arg_mode -> arg_mode -> Ppx_deriving_runtime.int
type mode_aux = Elpi_util.Util.mode_aux =
  1. | Fo of arg_mode
  2. | Ho of arg_mode * mode
and mode = mode_aux list
val pp_mode_aux : Ppx_deriving_runtime.Format.formatter -> mode_aux -> Ppx_deriving_runtime.unit
val show_mode_aux : mode_aux -> Ppx_deriving_runtime.string
val pp_mode : Ppx_deriving_runtime.Format.formatter -> mode -> Ppx_deriving_runtime.unit
val compare_mode_aux : mode_aux -> mode_aux -> Ppx_deriving_runtime.int
val compare_mode : mode -> mode -> Ppx_deriving_runtime.int
type ttype =
  1. | TConst of Elpi_util.Util.constant
  2. | TApp of Elpi_util.Util.constant * ttype * ttype list
  3. | TPred of bool * (arg_mode * ttype) list
  4. | TArr of ttype * ttype
  5. | TCData of Elpi_util.Util.CData.t
  6. | TLam of ttype
val pp_ttype : Ppx_deriving_runtime.Format.formatter -> ttype -> Ppx_deriving_runtime.unit
val compare_ttype : ttype -> ttype -> Ppx_deriving_runtime.int
type 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 Elpi_util.Util.constant * term list
  8. | CData of Elpi_util.Util.CData.t
  9. | UVar of uvar_body * int * int
  10. | AppUVar of uvar_body * int * term list
  11. | Arg of int * int
  12. | AppArg of int * term list
and uvar_body = {
  1. mutable contents : term;
  2. mutable uid_private : int;
}
val pp_term : Ppx_deriving_runtime.Format.formatter -> term -> Ppx_deriving_runtime.unit
val pp_uvar_body : Ppx_deriving_runtime.Format.formatter -> uvar_body -> Ppx_deriving_runtime.unit
val show_uvar_body : uvar_body -> Ppx_deriving_runtime.string
val compare_term : term -> term -> Ppx_deriving_runtime.int
val compare_uvar_body : uvar_body -> uvar_body -> Ppx_deriving_runtime.int
val cons2tcons : ?loc:Elpi_util.Util.Loc.t -> term -> ttype
val uvar_id : uvar_body -> int
val uvar_is_a_blocker : uvar_body -> bool
val uvar_isnt_a_blocker : uvar_body -> bool
val uvar_set_blocker : uvar_body -> unit
val uvar_unset_blocker : uvar_body -> unit
type clause = {
  1. depth : int;
  2. args : term list;
  3. hyps : term list;
  4. vars : int;
  5. mode : mode;
  6. loc : Elpi_util.Util.Loc.t option;
  7. mutable timestamp : int list;
}
val pp_clause : Ppx_deriving_runtime.Format.formatter -> clause -> Ppx_deriving_runtime.unit
val show_clause : clause -> Ppx_deriving_runtime.string
val compare_clause : clause -> clause -> Ppx_deriving_runtime.int
val get_arg_mode : mode_aux -> arg_mode
val to_mode : bool -> mode_aux
type grafting_time = int list
val pp_grafting_time : Ppx_deriving_runtime.Format.formatter -> grafting_time -> Ppx_deriving_runtime.unit
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 pp_times : Ppx_deriving_runtime.Format.formatter -> times -> Ppx_deriving_runtime.unit
val compare_times : times -> times -> Ppx_deriving_runtime.int
type stuck_goal = {
  1. mutable blockers : blockers;
  2. kind : unification_def stuck_goal_kind;
}
and blockers = uvar_body list
and unification_def = {
  1. adepth : int;
  2. env : term array;
  3. bdepth : int;
  4. a : term;
  5. b : term;
  6. matching : bool;
}
and clause_src = {
  1. hdepth : int;
  2. hsrc : term;
}
and 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 = {
  1. idx : second_lvl_idx Ptmap.t;
  2. time : int;
  3. times : times;
}
and second_lvl_idx =
  1. | TwoLevelIndex of {
    1. mode : mode;
    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 : mode;
    2. args : int list;
    3. args_idx : clause_list Ptmap.t;
    }
  3. | IndexWithDiscriminationTree of {
    1. mode : mode;
    2. arg_depths : int list;
    3. args_idx : clause Discrimination_tree.t;
    }
val pp_stuck_goal : Ppx_deriving_runtime.Format.formatter -> stuck_goal -> Ppx_deriving_runtime.unit
val show_stuck_goal : stuck_goal -> Ppx_deriving_runtime.string
val pp_blockers : Ppx_deriving_runtime.Format.formatter -> blockers -> Ppx_deriving_runtime.unit
val show_blockers : blockers -> Ppx_deriving_runtime.string
val pp_unification_def : Ppx_deriving_runtime.Format.formatter -> unification_def -> Ppx_deriving_runtime.unit
val show_unification_def : unification_def -> Ppx_deriving_runtime.string
val pp_clause_src : Ppx_deriving_runtime.Format.formatter -> clause_src -> Ppx_deriving_runtime.unit
val show_clause_src : clause_src -> Ppx_deriving_runtime.string
val pp_prolog_prog : Ppx_deriving_runtime.Format.formatter -> prolog_prog -> Ppx_deriving_runtime.unit
val show_prolog_prog : prolog_prog -> Ppx_deriving_runtime.string
val pp_clause_list : Ppx_deriving_runtime.Format.formatter -> clause_list -> Ppx_deriving_runtime.unit
val show_clause_list : clause_list -> Ppx_deriving_runtime.string
val pp_index : Ppx_deriving_runtime.Format.formatter -> index -> Ppx_deriving_runtime.unit
val pp_first_lvl_idx : Ppx_deriving_runtime.Format.formatter -> index -> Ppx_deriving_runtime.unit
val show_first_lvl_idx : first_lvl_idx -> Ppx_deriving_runtime.string
val pp_second_lvl_idx : Ppx_deriving_runtime.Format.formatter -> second_lvl_idx -> Ppx_deriving_runtime.unit
val show_second_lvl_idx : second_lvl_idx -> Ppx_deriving_runtime.string
val stop : bool Stdlib.ref
val close_index : index -> index
type constraints = stuck_goal list
type hyps = clause_src list
type suspended_goal = {
  1. context : hyps;
  2. goal : int * term;
}
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 pp_indexing : Ppx_deriving_runtime.Format.formatter -> indexing -> Ppx_deriving_runtime.unit
val show_indexing : indexing -> Ppx_deriving_runtime.string
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 : Elpi_util.Util.constant -> term list -> term
val mkCData : Elpi_util.Util.CData.t -> term
val mkUVar : uvar_body -> int -> int -> term
val mkAppUVar : uvar_body -> int -> term list -> term
val mkArg : int -> int -> term
val mkAppArg : int -> term list -> term
module C : sig ... end
val destConst : term -> Elpi_util.Util.constant
val oref : term -> uvar_body
val (!!) : uvar_body -> term
type env = term array
val empty_env : 'a array
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct