package elpi
ELPI - Embeddable λProlog Interpreter
Install
dune-project
Dependency
Authors
Maintainers
Sources
elpi-3.0.1.tbz
sha256=af8074c67e94095b25556e1d1e2aaaf0d04c19f373e38919cb8f0a0d6786aae7
sha512=774612085cd3ff267bfd1aa35b7dd2629cde066f9d2393185e28f21d2c86a24c2e36ef1293dee1b2cba37636b6deb6dc6e688cebdb4e2aaff922e06de15dba0a
doc/elpi.runtime/Elpi_runtime/Data/index.html
Module Elpi_runtime.Data
Source
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 queryDiscriminationTree L
-> we use the same logic of Hash, except we use DiscriminationTree to discriminate clauses
Source
val pp_indexing :
Ppx_deriving_runtime.Format.formatter ->
indexing ->
Ppx_deriving_runtime.unit
Source
type overlap_clause = {
overlap_loc : Elpi_util.Util.Loc.t option;
has_cut : bool;
mutable timestamp : int list;
}
Source
val pp_overlap_clause :
Ppx_deriving_runtime.Format.formatter ->
overlap_clause ->
Ppx_deriving_runtime.unit
Source
val pp_overlap :
Ppx_deriving_runtime.Format.formatter ->
overlap ->
Ppx_deriving_runtime.unit
Source
type pred_info = {
indexing : indexing;
mode : Elpi_util.Util.Mode.hos;
overlap : overlap;
has_local_without_cut : Elpi_util.Util.Loc.t option;
}
Source
val pp_pred_info :
Ppx_deriving_runtime.Format.formatter ->
pred_info ->
Ppx_deriving_runtime.unit
include module type of struct include Term end
Source
type ttype = Term.ttype =
| TConst of Elpi_util.Util.constant
| TApp of Elpi_util.Util.constant * ttype * ttype list
| TPred of bool * (Elpi_util.Util.Mode.t * ttype) list
| TArr of ttype * ttype
| TCData of Elpi_util.Util.CData.t
| TLam of ttype
Source
type builtin_predicate = Term.builtin_predicate =
| Cut
| And
| Impl
| ImplBang
| RImpl
| Pi
| Sigma
| Eq
| Match
| Findall
| Delay
| Host of Elpi_util.Util.constant
Source
val compare_builtin_predicate :
builtin_predicate ->
builtin_predicate ->
Ppx_deriving_runtime.int
Source
val pp_builtin_predicate :
Ppx_deriving_runtime.Format.formatter ->
builtin_predicate ->
Ppx_deriving_runtime.unit
Source
val show_builtin_predicate :
?table:'a ->
(?table:'a -> Elpi_util.Util.constant -> string) ->
builtin_predicate ->
string
Source
val map_builtin_predicate :
(Elpi_util.Util.constant -> Elpi_util.Util.constant) ->
builtin_predicate ->
builtin_predicate
Source
type term = Term.term =
| Const of Elpi_util.Util.constant
| Lam of term
| App of Elpi_util.Util.constant * term * term list
| Cons of term * term
| Nil
| Discard
| Builtin of builtin_predicate * term list
| CData of Elpi_util.Util.CData.t
| UVar of uvar_body * int * int
| AppUVar of uvar_body * int * term list
| Arg of int * int
| AppArg of int * term list
Source
val pp_uvar_body :
Ppx_deriving_runtime.Format.formatter ->
uvar_body ->
Ppx_deriving_runtime.unit
Source
type clause = Term.clause = {
depth : int;
args : term list;
hyps : term list;
vars : int;
mode : Elpi_util.Util.Mode.hos;
loc : Elpi_util.Util.Loc.t option;
mutable timestamp : int list;
}
Source
val pp_grafting_time :
Ppx_deriving_runtime.Format.formatter ->
grafting_time ->
Ppx_deriving_runtime.unit
Source
type stuck_goal = Term.stuck_goal = {
mutable blockers : blockers;
kind : unification_def stuck_goal_kind;
}
Source
and first_lvl_idx = Term.first_lvl_idx = {
idx : second_lvl_idx Ptmap.t;
time : int;
times : times;
}
Source
and second_lvl_idx = Term.second_lvl_idx =
| TwoLevelIndex of {
mode : Elpi_util.Util.Mode.hos;
argno : int;
all_clauses : clause_list;
flex_arg_clauses : clause_list;
arg_idx : clause_list Ptmap.t;
}
| BitHash of {
mode : Elpi_util.Util.Mode.hos;
args : int list;
args_idx : clause_list Ptmap.t;
}
| IndexWithDiscriminationTree of {
mode : Elpi_util.Util.Mode.hos;
arg_depths : int list;
args_idx : clause Discrimination_tree.t;
}
Source
val pp_stuck_goal :
Ppx_deriving_runtime.Format.formatter ->
stuck_goal ->
Ppx_deriving_runtime.unit
Source
val pp_blockers :
Ppx_deriving_runtime.Format.formatter ->
blockers ->
Ppx_deriving_runtime.unit
Source
val pp_unification_def :
Ppx_deriving_runtime.Format.formatter ->
unification_def ->
Ppx_deriving_runtime.unit
Source
val pp_clause_src :
Ppx_deriving_runtime.Format.formatter ->
clause_src ->
Ppx_deriving_runtime.unit
Source
val pp_prolog_prog :
Ppx_deriving_runtime.Format.formatter ->
prolog_prog ->
Ppx_deriving_runtime.unit
Source
val pp_clause_list :
Ppx_deriving_runtime.Format.formatter ->
clause_list ->
Ppx_deriving_runtime.unit
Source
val pp_first_lvl_idx :
Ppx_deriving_runtime.Format.formatter ->
index ->
Ppx_deriving_runtime.unit
Source
val pp_second_lvl_idx :
Ppx_deriving_runtime.Format.formatter ->
second_lvl_idx ->
Ppx_deriving_runtime.unit
Source
val pp_core_symbol :
Ppx_deriving_runtime.Format.formatter ->
core_symbol ->
Ppx_deriving_runtime.unit
Source
type clause_w_info = {
clloc : Elpi_util.Util.CData.t;
clargsname : string list;
clbody : clause;
}
Source
val pp_clause_w_info :
Ppx_deriving_runtime.Format.formatter ->
clause_w_info ->
Ppx_deriving_runtime.unit
Source
type symbol_table = {
mutable c2s : Symbol.t Elpi_util.Util.Constants.Map.t;
c2t : (Elpi_util.Util.constant, term) Elpi_util.Util.Hashtbl.t;
mutable frozen_constants : int;
}
Source
val pp_symbol_table :
Ppx_deriving_runtime.Format.formatter ->
symbol_table ->
Ppx_deriving_runtime.unit
Source
type executable = {
compiled_program : prolog_prog;
chr : CHR.t;
initial_depth : int;
initial_goal : term;
initial_runtime_state : State.t;
symbol_table : symbol_table;
builtins : BuiltInPredicate.builtin_table;
assignments : term Elpi_util.Util.StrMap.t;
}
Source
type solution = {
assignments : term Elpi_util.Util.StrMap.t;
constraints : constraints;
state : State.t;
pp_ctx : pp_ctx;
state_for_relocation : int * symbol_table;
}
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>