__ocaml_lex_tables [TopDownLexer] | |
__ocaml_lex_tables [BottomUpLexer] | |
__ocaml_lex_token_rec [TopDownLexer] | |
__ocaml_lex_token_rec [BottomUpLexer] | |
A | |
add [TopDown.S.Rewriting] | Add a rule to the system |
add [TopDown.S.Index] | Add the term->data binding. |
add [TopDown.S.BuiltinFun] | Interpret the given constant by the given function. |
add_builtin [CamlInterface] | |
add_builtin [TopDown.S.DB] | Add a builtin fun |
add_clause [TopDown.S.DB] | |
add_clauses [TopDown.S.DB] | |
add_fact [TopDown.S.DB] | |
add_facts [TopDown.S.DB] | |
add_list [CamlInterface.Rel3] | |
add_list [CamlInterface.Rel2] | Add given list of axioms |
add_list [CamlInterface.Rel1] | Add given list of axioms |
add_list [TopDown.S.Rewriting] | |
add_list [TopDown.S.BuiltinFun] | |
alpha_equiv [TopDown.S] | Test for alpha equivalence. |
apply [CamlInterface.Rel3] | |
apply [CamlInterface.Rel2] | |
apply [CamlInterface.Rel1] | apply the relation symbol to some term |
are_alpha_equiv [TopDown.S] | Special version of |
arity [BottomUp.S] | Number of subliterals of the literal. |
array [CamlInterface.Univ] | |
ask [TopDown.S] | Returns the answers to a query in a given DB. |
ask [BottomUp.S.Query] | Given a list of variables, and a list of literals that contain those variables, return a set. |
ask_lits [TopDown.S] | Extension of |
B | |
bind [TopDown.S.Subst] | Bind a variable,scope to a term,scope |
bool [CamlInterface.Univ] | |
builtin [TopDown.Default] | Default builtin functions |
builtin_funs [TopDown.S.DB] | |
C | |
cardinal [BottomUp.S.Query] | Number of elements of the set |
check_safe [BottomUp.S] | A datalog clause is safe iff all variables in its head also occur in its body |
clause_are_alpha_equiv [TopDown.S] | Alpha equivalence of clauses. |
clause_of_ast [Default] | |
clause_of_ast [TopDown.PARSE] | |
clause_of_string [TopDown.PARSE] | Parse a clause from a string, or fail. |
clauses_of_ast [TopDown.PARSE] | |
clear [TopDown.S.DB] | |
clear [TopDown.S.Index] | |
compatible [CamlInterface.Univ] | |
compatible [BottomUp.Univ] | |
copy [TopDown.S.DB] | |
copy [TopDown.S.Rewriting] | Copy the rewriting system |
copy [TopDown.S.Index] | Recursive copy of the index |
create [CamlInterface.RelList] | |
create [CamlInterface.Rel3] | |
create [CamlInterface.Rel2] | |
create [CamlInterface.Rel1] | New relation, with given name and argument |
create [TopDown.S.DB] | |
create [TopDown.S.Rewriting] | New rewriting system |
create [TopDown.S.BuiltinFun] | |
create_ctx [TopDown.PARSE] | |
create_renaming [TopDown.S.Subst] | |
D | |
db_add [BottomUp.S] | Add the clause/fact to the DB as an axiom, updating fixpoint. |
db_add_fact [BottomUp.S] | Add a fact (ground unit clause) |
db_add_fun [BottomUp.S] | Add a function to be called on new literals. |
db_copy [BottomUp.S] | Deep copy of the DB |
db_create [BottomUp.S] | Create a DB |
db_explain [BottomUp.S] | Explain the given fact by returning a list of facts that imply it under the current clauses, or raise Not_found |
db_explanations [BottomUp.S] | Get all the explanations that explain why this clause is true |
db_fold [BottomUp.S] | Fold on all clauses in the current DB (including fixpoint) |
db_goal [BottomUp.S] | Add a goal to the DB. |
db_goals [BottomUp.S] | Iterate on all current goals |
db_match [BottomUp.S] | match the given literal with facts of the DB, calling the handler on each fact that match |
db_mem [BottomUp.S] | Is the clause member of the DB? |
db_premises [BottomUp.S] | Immediate premises of the fact (ie the facts that resolved with a clause to give the literal), plus the clause that has been used. |
db_query [BottomUp.S] | Like |
db_size [BottomUp.S] | Size of the DB |
db_subscribe_all_facts [BottomUp.S] | |
db_subscribe_fact [BottomUp.S] | |
db_subscribe_goal [BottomUp.S] | |
default_interpreters [TopDown.Default] | List of default interpreters for some symbols, mostly infix predicates |
deref [TopDown.S.Subst] | While the term is a variable bound in subst, follow its binding. |
E | |
embed [BottomUp.Univ] | Create a new embedding. |
empty [TopDown.S.Index] | new, empty index |
empty [TopDown.S.Subst] | Empty subst |
eq [CamlInterface.Univ] | |
eq [TopDown.S.C] | |
eq [TopDown.S.Lit] | |
eq [TopDown.S.T] | |
eq_clause [BottomUp.S] | Check whether clauses are (syntactically) equal |
eq_literal [BottomUp.S] | Are the literals equal? |
eq_term [BottomUp.S] | |
equal [TopDown.CONST] | |
error_to_string [TopDownAst] | |
eval [TopDown.S.DB] | Evaluate the given term at root |
eval [TopDown.S.BuiltinFun] | Evaluate the term at root |
eval [TopDown.S.Subst] | Apply the substitution to the term. |
eval_clause [TopDown.S.Subst] | |
eval_lit [TopDown.S.Subst] | |
eval_lits [TopDown.S.Subst] | |
F | |
fail [TopDownLexer] | |
find [CamlInterface.Rel3] | |
find [CamlInterface.Rel2] | |
find [CamlInterface.Rel1] | Iterate on all instances of the relation present in the DB |
find_clauses_head [TopDown.S.DB] | find clauses whose head unifies with the given term, and give them along with the unifier, to the callback |
find_facts [TopDown.S.DB] | find facts unifying with the given term, and give them along with the unifier, to the callback |
find_interpretation [TopDown.S.DB] | Given an interpreted goal, try all interpreters on it, and match the query against their heads. |
float [CamlInterface.Univ] | |
fmap [TopDown.S.C] | |
fmap [TopDown.S.Lit] | |
fmt [CamlInterface.Rel3] | |
fmt [CamlInterface.Rel2] | |
fmt [CamlInterface.Rel1] | |
fmt [TopDown.S.C] | |
fmt [TopDown.S.Lit] | |
fmt [TopDown.S.T] | |
from_fun [CamlInterface.Rel3] | |
from_fun [CamlInterface.Rel2] | The given function decides of the given relation (if it returns true for a couple of constants, then the relation holds for those constants) |
from_fun [CamlInterface.Rel1] | The given function decides of the given relation (if it returns true for a constant, then the relation holds for this constant) |
G | |
generalizations [TopDown.S.Index] | Retrieve data associated with terms that are a generalization of the given query term |
get [CamlInterface.RelList] | |
get [CamlInterface.Rel3] | |
get [CamlInterface.Rel2] | |
get [CamlInterface.Rel1] | Check whether this term is a "R(t)" with |
ground [TopDown.S.T] | |
H | |
hash [CamlInterface.Univ] | |
hash [TopDown.S.C] | |
hash [TopDown.S.Lit] | |
hash [TopDown.S.T] | |
hash [TopDown.CONST] | |
hash_clause [BottomUp.S] | Hash the clause |
hash_literal [BottomUp.S] | Hash the literal |
head_symbol [TopDown.S.C] | |
head_symbol [TopDown.S.T] | |
help [TopDown.S.DB] | Help messages for interpreted predicates |
I | |
int [CamlInterface.Univ] | |
interpret [TopDown.S.DB] | Add an interpreter for the given constant. |
interpret_list [TopDown.S.DB] | Add several interpreters, with their documentation |
interpreted [TopDown.S.BuiltinFun] | Is the constant interpreted by a built-in function? |
is_apply [TopDown.S.T] | |
is_const [TopDown.S.T] | |
is_fact [BottomUp.S] | A fact is a ground clause with empty body |
is_ground [BottomUp.S] | Is the literal ground (a fact)? |
is_interpreted [TopDown.S.DB] | Is the constant interpreted by some OCaml code? |
is_var [TopDown.S.T] | |
iter [TopDown.S.Index] | Iterate on bindings |
iter [BottomUp.S.Query] | Evaluate the set by iterating on it |
L | |
lexing_error [BottomUpLexer] | |
list [CamlInterface.Univ] | |
lit_of_ast [TopDown.PARSE] | |
literal_of_ast [Default] | |
load_chan [CamlInterface.Parse] | |
load_file [CamlInterface.Parse] | |
load_string [CamlInterface.Parse] | |
loc_to_str [TopDownAst] | |
M | |
make [CamlInterface.RelList] | |
make [CamlInterface.Rel3] | |
make [CamlInterface.Rel2] | |
make [CamlInterface.Rel1] | Create a term from this relation description |
make [BottomUp.Hashcons] | Hashcons the symbol |
match_ [TopDown.S] |
|
max_var [TopDown.S.C] | |
max_var [TopDown.S.T] | max var, or 0 if ground |
mk [TopDown.S.Lit] | |
mk_aggr [TopDown.S.Lit] | |
mk_apply [TopDown.S.T] | |
mk_apply_l [TopDown.S.T] | |
mk_clause [TopDown.S.C] | |
mk_clause [BottomUp.S] | Create a clause from a conclusion and a list of premises |
mk_const [TopDown.S.T] | |
mk_const [BottomUp.S] | |
mk_fact [TopDown.S.C] | |
mk_literal [BottomUp.S] | Helper to build a literal. |
mk_neg [TopDown.S.Lit] | |
mk_pos [TopDown.S.Lit] | |
mk_var [TopDown.S.T] | |
mk_var [BottomUp.S] | |
mk_vartbl [Default] | |
N | |
name [CamlInterface.RelList] | |
name [CamlInterface.Rel3] | |
name [CamlInterface.Rel2] | |
name [CamlInterface.Rel1] | Name of the relation |
new_key [CamlInterface.Univ] | Create a new key. |
num_clauses [TopDown.S.DB] | |
num_facts [TopDown.S.DB] | |
O | |
of_int [CamlInterface] | |
of_int [TopDown.PARSABLE_CONST] | |
of_soft_clause [BottomUp.S] | |
of_soft_lit [BottomUp.S] | |
of_string [CamlInterface] | |
of_string [TopDown.PARSABLE_CONST] | |
of_string [TopDown.CONST] | |
open_clause [BottomUp.S] | Deconstruct a clause |
open_literal [BottomUp.S] | Deconstruct a literal |
P | |
pack [CamlInterface.Univ] | |
pack [BottomUp.Univ] | |
pair [CamlInterface.Univ] | |
parse_chan [TopDown.PARSE] | |
parse_clause [TopDownParser] | |
parse_clause [BottomUpParser] | |
parse_file [TopDownParser] | |
parse_file [BottomUpParser] | |
parse_file [TopDown.PARSE] | |
parse_literal [TopDownParser] | |
parse_literal [BottomUpParser] | |
parse_literals [TopDownParser] | |
parse_literals [BottomUpParser] | |
parse_query [TopDownParser] | |
parse_query [BottomUpParser] | |
parse_string [TopDown.PARSE] | |
parse_term [TopDownParser] | |
pp [TopDown.S.C] | |
pp [TopDown.S.Lit] | |
pp [TopDown.S.T] | |
pp_clause [BottomUp.S] | Pretty print the clause |
pp_literal [BottomUp.S] | Pretty print the literal |
pp_plan [BottomUp.S.Query] | Print query plan |
pp_term [BottomUp.S] | |
pp_tuple [TopDown.S.T] | |
print [CamlInterface.Univ] | |
print_error [TopDownAst] | |
print_location [TopDownLexer] | |
print_location [BottomUpLexer] | |
Q | |
quantify1 [BottomUp.S] | |
quantify2 [BottomUp.S] | |
quantify3 [BottomUp.S] | |
quantify4 [BottomUp.S] | |
quantifyn [BottomUp.S] | |
query [TopDown.CONST] | Special symbol, that will never occur in any user-defined clause or term. |
query_of_ast [Default] | |
R | |
reflexive [CamlInterface.Rel2] |
|
remove [TopDown.S.Index] | Remove the term->data binding. |
rename [TopDown.S.Subst] | Rename the given variable into a variable that is unique
within variables known to the given |
reset_renaming [TopDown.S.Subst] | |
rewrite [TopDown.S.Rewriting] | Normalize the term recursively. |
rewrite_root [TopDown.S.Rewriting] | rewrite the term, but only its root. |
S | |
set_debug [TopDown.S] | |
setup_default [TopDown.Default] | Load the default interpreters and builtin functions into the DB |
setup_handlers [TopDownUnix.S] | |
size [TopDown.S.DB] | |
size [TopDown.S.Index] | Number of bindings |
string [CamlInterface.Univ] | |
subset [CamlInterface.Rel3] | |
subset [CamlInterface.Rel2] |
|
subset [CamlInterface.Rel1] |
|
symmetry [CamlInterface.Rel2] | Axiom for symmetry (ie "r(X,Y) <=> r(Y,X)") added to the DB |
T | |
tc_of [CamlInterface.Rel2] |
|
term_of_ast [TopDown.PARSE] | |
term_of_string [TopDown.PARSE] | |
to_list [TopDown.S.Rewriting] | List of rules |
to_list [BottomUp.S.Query] | Convert to a list |
to_string [CamlInterface.Rel3] | |
to_string [CamlInterface.Rel2] | |
to_string [CamlInterface.Rel1] | |
to_string [TopDown.S.C] | |
to_string [TopDown.S.Lit] | |
to_string [TopDown.S.T] | |
to_string [TopDown.CONST] | |
to_string [BottomUp.SymbolType] | |
to_term [TopDown.S.Lit] | |
token [TopDownLexer] | |
token [BottomUpLexer] | |
transitive [CamlInterface.Rel2] | Axioms for transitivity are added to the DB |
U | |
unify [TopDown.S.Index] | Retrieve data associated with terms that unify with the given query term |
unify [TopDown.S] | Unify the two terms. |
unit [CamlInterface.Univ] | |
unpack [CamlInterface.Univ] | |
unpack [BottomUp.Univ] | |
V | |
vars [TopDown.S.T] | |
version [Version] |