package datalog

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Default literal base, where symbols are just strings
1. Default symbols: hashconsed strings
2. Default implementation

package datalog

datalog
- CHANGES
- README
- Library datalog
  - Datalog
    
    AST
    
    BottomUp
    
    Univ
    
    S
    
    Query
    
    SymbolType
    
    Hashcons
    
    Make
    
    Query
    
    Default
    
    StringSymbol
    
    Query
    
    Lexer
    
    Parser
    
    Version
- Library datalog.caml_interface
  - Datalog_caml_interface
    
    TopDown
    
    Univ
    
    Logic
    
    Const
    
    T
    
    Tbl
    
    Lit
    
    C
    
    Tbl
    
    Subst
    
    BuiltinFun
    
    TVariantTbl
    
    CVariantTbl
    
    Index
    
    Rewriting
    
    DB
    
    Rel1
    
    Rel2
    
    Rel3
    
    RelList
    
    Parse
- Library datalog.top_down
  - Datalog_top_down
    
    AST
    
    Lexer
    
    Parser
    
    CONST
    
    S
    
    Const
    
    T
    
    Tbl
    
    Lit
    
    C
    
    Tbl
    
    Subst
    
    BuiltinFun
    
    TVariantTbl
    
    CVariantTbl
    
    Index
    
    Rewriting
    
    DB
    
    Make
    
    Const
    
    T
    
    Tbl
    
    Lit
    
    C
    
    Tbl
    
    Subst
    
    BuiltinFun
    
    TVariantTbl
    
    CVariantTbl
    
    Index
    
    Rewriting
    
    DB
    
    PARSABLE_CONST
    
    PARSE
    
    MakeParse
    
    Default
    
    Const
    
    T
    
    Tbl
    
    Lit
    
    C
    
    Tbl
    
    Subst
    
    BuiltinFun
    
    TVariantTbl
    
    CVariantTbl
    
    Index
    
    Rewriting
    
    DB
- Library datalog.unix
  - Datalog_unix
    
    TopDown
    
    S
    
    TD
    
    Const
    
    T
    
    Tbl
    
    Lit
    
    C
    
    Tbl
    
    Subst
    
    BuiltinFun
    
    TVariantTbl
    
    CVariantTbl
    
    Index
    
    Rewriting
    
    DB
    
    Make
    
    TD
    
    Default
    
    TD
    
    Const
    
    T
    
    Tbl
    
    Lit
    
    C
    
    Tbl
    
    Subst
    
    BuiltinFun
    
    TVariantTbl
    
    CVariantTbl
    
    Index
    
    Rewriting
    
    DB
- Sources
  - datalog
    
    AST.ml
    
    Lexer.ml
    
    Parser.ml
    
    bottomUp.ml
    
    datalog.ml
    
    default.ml
    
    version.ml
  - datalog.caml_interface
    
    Datalog_caml_interface.ml
  - datalog.top_down
    
    AST.ml
    
    Datalog_top_down.ml
    
    Lexer.ml
    
    Parser.ml
    
    datalog_top_down__.ml
  - datalog.unix
    
    Datalog_unix.ml

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Datalog.Default`Source

Default literal base, where symbols are just strings

Default symbols: hashconsed strings

Sourcetype symbol = private string

Sourcemodule StringSymbol : sig ... end

Default implementation

This is a ready-to-use instance of BottomUp.Make, with hashconsed strings as symbols. It also features some handy conversion functions from BottomUpAST.

include BottomUp.S with type symbol := symbol

Literals and clauses

Sourcetype term = private

| Var of int
| Const of symbol
(*
Individual object
*)

Sourceval mk_var : int -> term

Sourceval mk_const : symbol -> term

Sourcetype literal

A datalog atom, i.e. pred(arg_1, ..., arg_n). The first element of the array is the predicate, then arguments follow

Sourcetype clause

A datalog clause, i.e. head :- body_1, ..., body_n

Sourcetype soft_lit = symbol * term list

Sourcetype soft_clause = soft_lit * soft_lit list

Constructors and destructors

Sourceval mk_literal : symbol -> term list -> literal

Helper to build a literal. Arguments are either variables or constants

Sourceval of_soft_lit : soft_lit -> literal

Sourceval open_literal : literal -> soft_lit

Deconstruct a literal

Sourceval mk_clause : literal -> literal list -> clause

Create a clause from a conclusion and a list of premises

Sourceval of_soft_clause : soft_clause -> clause

Sourceval open_clause : clause -> soft_clause

Deconstruct a clause

Sourceval is_ground : literal -> bool

Is the literal ground (a fact)?

Sourceval arity : literal -> int

Number of subliterals of the literal. Ex for p(a,b,c) it returns 3

Comparisons

Sourceval eq_term : term -> term -> bool

Sourceval eq_literal : literal -> literal -> bool

Are the literals equal?

Sourceval hash_literal : literal -> int

Hash the literal

Sourceval check_safe : clause -> bool

A datalog clause is safe iff all variables in its head also occur in its body

Sourceval is_fact : clause -> bool

A fact is a ground clause with empty body

Sourceval eq_clause : clause -> clause -> bool

Check whether clauses are (syntactically) equal

Sourceval hash_clause : clause -> int

Hash the clause

Pretty-printing

Sourceval pp_term : Format.formatter -> term -> unit

Sourceval pp_literal : Format.formatter -> literal -> unit

Pretty print the literal

Sourceval pp_clause : 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

Sourceval quantify1 : (term -> 'a) -> 'a

Sourceval quantify2 : (term -> term -> 'a) -> 'a

Sourceval quantify3 : (term -> term -> term -> 'a) -> 'a

Sourceval quantify4 : (term -> term -> term -> term -> 'a) -> 'a

Sourceval quantifyn : int -> (term list -> 'a) -> 'a

The Datalog unit resolution algorithm

Sourceexception UnsafeClause

Sourcetype db

A database of facts and clauses, with incremental fixpoint computation

Sourcetype explanation =

| Axiom
| Resolution of clause * literal
| ExtExplanation of string * BottomUp.Univ.t
(*
Explanation for a clause or fact. It is extensible through universal types.
*)

Sourceval db_create : unit -> db

Create a DB

Sourceval db_copy : db -> db

Deep copy of the DB

Sourceval db_mem : db -> clause -> bool

Is the clause member of the DB?

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

Sourceval db_add_fact : ?expl:explanation -> db -> literal -> unit

Add a fact (ground unit clause)

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

Sourceval db_match : db -> literal -> (literal -> unit) -> unit

match the given literal with facts of the DB, calling the handler on each fact that match

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

Sourceval db_size : db -> int

Size of the DB

Sourceval db_fold : ('a -> clause -> 'a) -> 'a -> db -> 'a

Fold on all clauses in the current DB (including fixpoint)

Sourcetype fact_handler = literal -> unit

Sourcetype goal_handler = literal -> unit

Sourceval db_subscribe_fact : db -> symbol -> fact_handler -> unit

Sourceval db_subscribe_all_facts : db -> fact_handler -> unit

Sourceval db_subscribe_goal : db -> goal_handler -> unit

Sourcetype user_fun = soft_lit -> soft_lit

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

Sourceval db_goals : db -> (literal -> unit) -> unit

Iterate on all current goals

Sourceval 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

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

Sourceval db_explanations : db -> clause -> explanation list

Get all the explanations that explain why this clause is true

Querying

Sourcemodule Query : sig ... end

Sourcetype vartbl = {

mutable vartbl_count : int;
vartbl_tbl : (string, int) Hashtbl.t;

}

Sourceval mk_vartbl : unit -> vartbl

Sourceval literal_of_ast : ?tbl:vartbl -> AST.literal -> literal

Sourceval clause_of_ast : AST.clause -> clause

Sourceval query_of_ast : AST.query -> int array * literal list * literal list

package datalog

Module Datalog.DefaultSource

Default literal base, where symbols are just strings

Default symbols: hashconsed strings

Default implementation

Literals and clauses

Constructors and destructors

Comparisons

Pretty-printing

Higher level API

The Datalog unit resolution algorithm

Querying

Module `Datalog.Default`Source