Index of values

__ocaml_lex_tables [TopDownLexer]
__ocaml_lex_tables [BottomUpLexer]
__ocaml_lex_token_rec [TopDownLexer]
__ocaml_lex_token_rec [BottomUpLexer]

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 [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 alpha_equiv, using distinct scopes for the two terms to test, and discarding the result
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 TopDown.S.ask, where the query ranges over the list of variables (the term list), all of which must be bound in the list of literals that form a constraint.

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]

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]
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]

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 BottomUp.S.db_match, but the additional int list is used to select bindings of variables in the literal.
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.

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]

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)

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 t an object packed with the appropriate key, and "R" the name of the given relation
ground [TopDown.S.T]

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

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

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]

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]
match_ a sa b sb matches the pattern a in scope sa with term b in scope sb.
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]

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]

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

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 [BottomUpLexer]

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]

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 renaming
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.

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 db r1 r2 adds to db the axiom that r2(X,Y) :- r1(X,Y); in other words, r1 is a subset of r2 as a relation
subset [CamlInterface.Rel1]
subset db r1 r2 adds to db the axiom that r2(X) :- r1(X); in other words, r1 is a subset of r2 as a relation
symmetry [CamlInterface.Rel2]
Axiom for symmetry (ie "r(X,Y) <=> r(Y,X)") added to the DB

term_of_ast [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

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]

vars [TopDown.S.T]
version [Version]