package elpi

  1. Overview
  2. Docs
ELPI - Embeddable λProlog Interpreter

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (11)

Authors

  1. C
    Claudio Sacerdoti Coen
  2. E
    Enrico Tassi

Maintainers

  1. E
    Enrico Tassi <enrico.tassi@inria.fr>

Sources

elpi-3.0.1.tbz
sha256=af8074c67e94095b25556e1d1e2aaaf0d04c19f373e38919cb8f0a0d6786aae7
sha512=774612085cd3ff267bfd1aa35b7dd2629cde066f9d2393185e28f21d2c86a24c2e36ef1293dee1b2cba37636b6deb6dc6e688cebdb4e2aaff922e06de15dba0a

doc/elpi.runtime/Elpi_runtime/Data/index.html

Module Elpi_runtime.DataSource

Sourcemodule Fmt = Format
Sourcetype 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
Sourceval compare_indexing : indexing -> indexing -> Ppx_deriving_runtime.int
Sourcetype overlap_clause = {
  1. overlap_loc : Elpi_util.Util.Loc.t option;
  2. has_cut : bool;
  3. mutable timestamp : int list;
}
Sourcetype overlap =
  1. | Allowed
  2. | Forbidden of overlap_clause Discrimination_tree.t
Sourceval mk_Forbidden : indexing -> overlap
Sourcetype 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;
}
Sourceval same_indexing : pred_info -> pred_info -> bool
Sourcemodule Term : sig ... end
include module type of struct include Term end
Sourcetype 'unification_def stuck_goal_kind = 'unification_def Term.stuck_goal_kind = ..
Sourceval pp_stuck_goal_kind : 'a -> 'b -> 'c -> unit
Sourceval show_stuck_goal_kind : 'a -> 'b -> string
Sourceval equal_stuck_goal_kind : 'a -> 'b -> 'b -> bool
Sourcetype stuck_goal_kind +=
  1. | Unification of 'unification_def
Sourcetype 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
Sourceval compare_ttype : ttype -> ttype -> Ppx_deriving_runtime.int
Sourcetype 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
Sourceval builtin_predicates : builtin_predicate list
Sourceval builtin_predicate_max : int
Sourceval func_of_builtin_predicate : (Elpi_util.Util.constant -> F.t) -> builtin_predicate -> F.t
Sourceval show_builtin_predicate : ?table:'a -> (?table:'a -> Elpi_util.Util.constant -> string) -> builtin_predicate -> string
Sourceval const_of_builtin_predicate : builtin_predicate -> Elpi_util.Util.constant
Sourceval is_builtin_predicate : int -> bool
Sourceval builtin_predicate_of_const : int -> builtin_predicate
Sourcetype 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_body * int * int
  10. | AppUVar of uvar_body * int * term list
  11. | Arg of int * int
  12. | AppArg of int * term list
Sourceand uvar_body = Term.uvar_body = {
  1. mutable contents : term;
  2. mutable uid_private : int;
}
Sourceval pp_uvar_body : Ppx_deriving_runtime.Format.formatter -> uvar_body -> Ppx_deriving_runtime.unit
Sourceval show_uvar_body : uvar_body -> Ppx_deriving_runtime.string
Sourceval compare_term : term -> term -> Ppx_deriving_runtime.int
Sourceval compare_uvar_body : uvar_body -> uvar_body -> Ppx_deriving_runtime.int
Sourceval cons2tcons : ?loc:Elpi_util.Util.Loc.t -> term -> ttype
Sourceval uvar_id : uvar_body -> int
Sourceval uvar_is_a_blocker : uvar_body -> bool
Sourceval uvar_isnt_a_blocker : uvar_body -> bool
Sourceval uvar_set_blocker : uvar_body -> unit
Sourceval uvar_unset_blocker : uvar_body -> unit
Sourcetype clause = Term.clause = {
  1. depth : int;
  2. args : term list;
  3. hyps : term list;
  4. vars : int;
  5. mode : Elpi_util.Util.Mode.hos;
  6. loc : Elpi_util.Util.Loc.t option;
  7. mutable timestamp : int list;
}
Sourceval compare_clause : clause -> clause -> Ppx_deriving_runtime.int
Sourcetype grafting_time = int list
Sourceval compare_times : times -> times -> Ppx_deriving_runtime.int
Sourcetype stuck_goal = Term.stuck_goal = {
  1. mutable blockers : blockers;
  2. kind : unification_def stuck_goal_kind;
}
Sourceand blockers = uvar_body list
Sourceand unification_def = Term.unification_def = {
  1. adepth : int;
  2. env : term array;
  3. bdepth : int;
  4. a : term;
  5. b : term;
  6. matching : bool;
}
Sourceand clause_src = Term.clause_src = {
  1. hdepth : int;
  2. hsrc : term;
}
Sourceand prolog_prog = Term.prolog_prog = {
  1. src : clause_src list;
  2. index : index;
}
Sourceand clause_list = clause Bl.t
Sourceand first_lvl_idx = Term.first_lvl_idx = {
  1. idx : second_lvl_idx Ptmap.t;
  2. time : int;
  3. times : times;
}
Sourceand 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;
    }
Sourceval stop : bool ref
Sourceval close_index : index -> index
Sourcetype constraints = stuck_goal list
Sourcetype hyps = clause_src list
Sourcetype suspended_goal = Term.suspended_goal = {
  1. context : hyps;
  2. goal : int * term;
  3. blockers : blockers;
}
Sourceval mkLam : term -> term
Sourceval mkApp : Elpi_util.Util.constant -> term -> term list -> term
Sourceval mkCons : term -> term -> term
Sourceval mkNil : term
Sourceval mkDiscard : term
Sourceval mkBuiltin : builtin_predicate -> term list -> term
Sourceval mkUVar : uvar_body -> int -> int -> term
Sourceval mkAppUVar : uvar_body -> int -> term list -> term
Sourceval mkArg : int -> int -> term
Sourceval mkAppArg : int -> term list -> term
Sourcemodule C = Term.C
Sourceval oref : term -> uvar_body
Sourceval (!!) : uvar_body -> term
Sourcetype env = term array
Sourceval empty_env : 'a array
Sourcemodule State : sig ... end
Sourceval elpi_state_descriptor : State.descriptor
Sourcetype core_symbol =
  1. | As
  2. | Uv
  3. | ECons
  4. | ENil
Sourceval min_core_symbol : int
Sourceval max_core_symbol : int
Sourceval core_symbol_to_enum : core_symbol -> int
Sourceval core_symbol_of_enum : int -> core_symbol option
Sourceval func_of_core_symbol : core_symbol -> F.t
Sourceval is_core_symbol : F.t -> bool
Sourcemodule Symbol : sig ... end
Sourcemodule Global_symbols : sig ... end
Sourceval dummy : term
Sourceval dummy_uvar_body : uvar_body
Sourcemodule CHR : sig ... end
Sourcetype clause_w_info = {
  1. clloc : Elpi_util.Util.CData.t;
  2. clargsname : string list;
  3. clbody : clause;
}
Sourceexception No_clause
Sourceexception No_more_steps
Sourceexception Flex_head
Sourcemodule Conversion : sig ... end
Sourcemodule ContextualConversion : sig ... end
Sourceval while_compiling : bool State.component
Sourcemodule HoasHooks : sig ... end
Sourcemodule CalcHooks : sig ... end
Sourcemodule BuiltInPredicate : sig ... end
Sourcetype 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;
}
Sourcetype 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;
}
Sourcetype pp_ctx = {
  1. uv_names : (string Elpi_util.Util.IntMap.t * int) ref;
  2. table : symbol_table;
}
Sourcetype 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;
}
Sourcetype 'a outcome =
  1. | Success of solution
  2. | Failure
  3. | NoMoreSteps
Sourceexception CannotDeclareClauseForBuiltin of Elpi_util.Util.Loc.t option * builtin_predicate
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