Module Datalog

module Datalog: sig .. end

Main Datalog module




Datalog is a fragment of first-order logic. It can be viewed as relational algebra with deduction/recursion (through Horn clauses).

A Datalog database contains facts and clauses (or rules). A fact is simply a relational atom, like mother(mary, john). A Horn clause is a deduction rule, for instance grandmother(X,Y) :- mother(X,Z), parent(Z,Y) and parent(X,Y) :- mother(X,Y).

The Datalog_cli module provides a simple client that demonstrates most of the features of Datalog. Some basic examples can be found in the tests/ directory.



Universal type


module Univ: sig .. end
This module is present to allow the user to extend explanations with her own types.

Main module type



Main module, that exposes datatypes for logic literals and clauses, functions to manipulate them, and functions to compute the fixpoint of a set of clauses
module type S = sig .. end

Signature for a symbol type


module type SymbolType = sig .. end
A symbol must be hashable, comparable and printable.

Hashconsing of symbols


module Hashcons: 
functor (S : SymbolType) -> sig .. end

Main functor


module Make: 
functor (Symbol : SymbolType) -> S with type symbol = Symbol.t
Build a Datalog module.

AST for Datalog files


module Ast: sig .. end

Parser for Datalog files


module Parser: sig .. end
The syntax is a subset of prolog.

Lexer for parsing Datalog files


module Lexer: sig .. end

Default symbols: hashconsed strings


module StringSymbol: SymbolType  with type t = string

Default implementation


module Default: sig .. end
This is a ready-to-use instance of Datalog.Make, with hashconsed strings as symbols.
val version : string
Version of the library