package datalog

  1. Overview
  2. Docs

Literals and clauses

type symbol

Abstract type of symbols (individual objects)

type term = private
  1. | Var of int
  2. | Const of symbol
    (*

    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

type soft_lit = symbol * term list
type soft_clause = soft_lit * soft_lit list

Constructors and destructors

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

Comparisons

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

Pretty-printing

val pp_term : Stdlib.Format.formatter -> term -> unit
val pp_literal : Stdlib.Format.formatter -> literal -> unit

Pretty print the literal

val pp_clause : Stdlib.Format.formatter -> clause -> unit

Pretty print the clause

Higher level API

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

The Datalog unit resolution algorithm

exception UnsafeClause
type db

A database of facts and clauses, with incremental fixpoint computation

type explanation =
  1. | Axiom
  2. | Resolution of clause * literal
  3. | ExtExplanation of string * Univ.t
    (*

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

type fact_handler = literal -> unit
type goal_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
type user_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

Querying

module Query : sig ... end
OCaml

Innovation. Community. Security.