module Make:
Build a Datalog module. This allows to specialize Datalog for a user-defined type of atoms. Strings are a good default, but more complicated types can be useful.
Parameters: |
|
type
symbol
Abstract type of symbols (individual objects)
type
term = private
| |
Var of |
|||
| |
Const of |
(* | Individual object | *) |
val mk_var : int -> term
val mk_const : symbol -> term
type
literal
A datalog atom, i.e. pred(arg_1, ..., arg_n). The first element of the array is the predicate, then arguments follow
type
clause
A datalog clause, i.e. head :- body_1, ..., body_n
typesoft_lit =
symbol * term list
typesoft_clause =
soft_lit * soft_lit list
val mk_literal : symbol -> term list -> literal
Helper to build a literal. Arguments are either variables or constants
val of_soft_lit : soft_lit -> literal
val open_literal : literal -> soft_lit
Deconstruct a literal
val mk_clause : literal -> literal list -> clause
Create a clause from a conclusion and a list of premises
val of_soft_clause : soft_clause -> clause
val open_clause : clause -> soft_clause
Deconstruct a clause
val is_ground : literal -> bool
Is the literal ground (a fact)?
val arity : literal -> int
Number of subliterals of the literal. Ex for p(a,b,c) it returns 3
val eq_term : term -> term -> bool
val eq_literal : literal -> literal -> bool
Are the literals equal?
val hash_literal : literal -> int
Hash the literal
val check_safe : clause -> bool
A datalog clause is safe iff all variables in its head also occur in its body
val is_fact : clause -> bool
A fact is a ground clause with empty body
val eq_clause : clause -> clause -> bool
Check whether clauses are (syntactically) equal
val hash_clause : clause -> int
Hash the clause
val pp_term : Format.formatter -> term -> unit
val pp_literal : Format.formatter -> literal -> unit
Pretty print the literal
val pp_clause : Format.formatter -> clause -> unit
Pretty print the clause
This part of the API can be used to avoid building variables
yourself. Calling quantify3 f
with call f
with 3 distinct
variables, and f
can use those variables to, for instance,
build a clause
val quantify1 : (term -> 'a) -> 'a
val quantify2 : (term -> term -> 'a) -> 'a
val quantify3 : (term -> term -> term -> 'a) -> 'a
val quantify4 : (term ->
term -> term -> term -> 'a) ->
'a
val quantifyn : int -> (term list -> 'a) -> 'a
exception UnsafeClause
type
db
A database of facts and clauses, with incremental fixpoint computation
type
explanation =
| |
Axiom |
|||
| |
Resolution of |
|||
| |
ExtExplanation of |
(* | Explanation for a clause or fact. It is extensible through universal types. | *) |
val db_create : unit -> db
Create a DB
val db_copy : db -> db
Deep copy of the DB
val db_mem : db -> clause -> bool
Is the clause member of the DB?
val db_add : ?expl:explanation -> db -> clause -> unit
Add the clause/fact to the DB as an axiom, updating fixpoint.
UnsafeRule will be raised if the rule is not safe (see BottomUp.S.check_safe
)
val db_add_fact : ?expl:explanation -> db -> literal -> unit
Add a fact (ground unit clause)
val db_goal : db -> literal -> unit
Add a goal to the DB. The goal is used to trigger backward chaining (calling goal handlers that could help solve the goal)
val db_match : db -> literal -> (literal -> unit) -> unit
match the given literal with facts of the DB, calling the handler on each fact that match
val db_query : db ->
literal -> int list -> (symbol list -> unit) -> unit
Like BottomUp.S.db_match
, but the additional int list is used to select
bindings of variables in the literal. Their bindings, in the same
order, are given to the callback.
val db_size : db -> int
Size of the DB
val db_fold : ('a -> clause -> 'a) -> 'a -> db -> 'a
Fold on all clauses in the current DB (including fixpoint)
typefact_handler =
literal -> unit
typegoal_handler =
literal -> unit
val db_subscribe_fact : db -> symbol -> fact_handler -> unit
val db_subscribe_all_facts : db -> fact_handler -> unit
val db_subscribe_goal : db -> goal_handler -> unit
typeuser_fun =
soft_lit -> soft_lit
val db_add_fun : db -> symbol -> user_fun -> unit
Add a function to be called on new literals. Only one function per symbol can be registered.
val db_goals : db -> (literal -> unit) -> unit
Iterate on all current goals
val db_explain : db -> literal -> literal list
Explain the given fact by returning a list of facts that imply it under the current clauses, or raise Not_found
val db_premises : db ->
literal -> clause * literal list
Immediate premises of the fact (ie the facts that resolved with a clause to give the literal), plus the clause that has been used.
val db_explanations : db -> clause -> explanation list
Get all the explanations that explain why this clause is true
module Query:sig
..end