module DB:sig
..end
type
t
A database is a repository for Datalog clauses.
typeinterpreter =
TopDown.S.T.t -> TopDown.S.C.t list
Interpreted predicate. It takes terms which have a given symbol as head, and return a list of (safe) clauses that have the same symbol as head, and should unify with the query term.
val create : ?parent:t -> unit -> t
val copy : t -> t
val clear : t -> unit
val add_fact : t -> TopDown.S.T.t -> unit
val add_facts : t -> TopDown.S.T.t list -> unit
val add_clause : t -> TopDown.S.C.t -> unit
val add_clauses : t -> TopDown.S.C.t list -> unit
val interpret : ?help:string ->
t -> TopDown.S.const -> interpreter -> unit
Add an interpreter for the given constant. Goals that start with this constant will be given to all registered interpreters, all of which can add new clauses. The returned clauses must have the constant as head symbol.
val interpret_list : t ->
(TopDown.S.const * string * interpreter) list -> unit
Add several interpreters, with their documentation
val is_interpreted : t -> TopDown.S.const -> bool
Is the constant interpreted by some OCaml code?
val add_builtin : t -> Const.t -> TopDown.S.BuiltinFun.t -> unit
Add a builtin fun
val builtin_funs : t -> TopDown.S.BuiltinFun.map
val eval : t -> TopDown.S.T.t -> TopDown.S.T.t
Evaluate the given term at root
val help : t -> string list
Help messages for interpreted predicates
val num_facts : t -> int
val num_clauses : t -> int
val size : t -> int
val find_facts : ?oc:bool ->
t ->
TopDown.S.scope ->
TopDown.S.T.t ->
TopDown.S.scope -> (TopDown.S.T.t -> TopDown.S.Subst.t -> unit) -> unit
find facts unifying with the given term, and give them along with the unifier, to the callback
val find_clauses_head : ?oc:bool ->
t ->
TopDown.S.scope ->
TopDown.S.T.t ->
TopDown.S.scope -> (TopDown.S.C.t -> TopDown.S.Subst.t -> unit) -> unit
find clauses whose head unifies with the given term, and give them along with the unifier, to the callback
val find_interpretation : ?oc:bool ->
t ->
TopDown.S.scope ->
TopDown.S.T.t ->
TopDown.S.scope -> (TopDown.S.C.t -> TopDown.S.Subst.t -> unit) -> unit
Given an interpreted goal, try all interpreters on it, and match the query against their heads. Returns clauses whose head unifies with the goal, along with the substitution.