Module `Logic.DB`Source

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

Source

val 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

Source

val 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

Source

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/datalog.caml_interface/Datalog_caml_interface/Logic/DB/index.html

Module `Logic.DB`Source

package datalog

Install

Dune Dependency

Authors

Maintainers

Sources

doc/datalog.caml_interface/Datalog_caml_interface/Logic/DB/index.html

Module Logic.DBSource

Module `Logic.DB`Source