Module Make.DBSource

Sourcetype t

A database is a repository for Datalog clauses.

Sourcetype interpreter = T.t -> 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.

Sourceval create : ?parent:t -> unit -> t
Sourceval copy : t -> t
Sourceval clear : t -> unit
Sourceval add_fact : t -> T.t -> unit
Sourceval add_facts : t -> T.t list -> unit
Sourceval add_clause : t -> C.t -> unit
Sourceval add_clauses : t -> C.t list -> unit
Sourceval interpret : ?help:string -> t -> 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.

Sourceval interpret_list : t -> (const * string * interpreter) list -> unit

Add several interpreters, with their documentation

Sourceval is_interpreted : t -> const -> bool

Is the constant interpreted by some OCaml code?

Sourceval add_builtin : t -> Const.t -> BuiltinFun.t -> unit

Add a builtin fun

Sourceval builtin_funs : t -> BuiltinFun.map
Sourceval eval : t -> T.t -> T.t

Evaluate the given term at root

Sourceval help : t -> string list

Help messages for interpreted predicates

Sourceval num_facts : t -> int
Sourceval num_clauses : t -> int
Sourceval size : t -> int
Sourceval find_facts : ?oc:bool -> t -> scope -> T.t -> scope -> (T.t -> Subst.t -> unit) -> unit

find facts unifying with the given term, and give them along with the unifier, to the callback

Sourceval find_clauses_head : ?oc:bool -> t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit

find clauses whose head unifies with the given term, and give them along with the unifier, to the callback

Sourceval find_interpretation : ?oc:bool -> t -> scope -> T.t -> scope -> (C.t -> 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.