package datalog

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Terms
Literals
Clauses
Substs
Unification, matching...
Special built-in functions
Index
Rewriting
DB
Query

package datalog

datalog
- Datalog
  - AST
  - BottomUp
    
    Hashcons
    
    S
    
    Make
    
    Query
    
    Symbol
    
    S
    
    Query
    
    SymbolType
    
    Univ
  - Default
    
    Query
    
    StringSymbol
  - Lexer
  - Parser
  - Version
datalog.caml_interface
- Datalog_caml_interface
  - Logic
    
    BuiltinFun
    
    C
    
    Tbl
    
    CVariantTbl
    
    Const
    
    DB
    
    Index
    
    Data
    
    Lit
    
    Rewriting
    
    Subst
    
    T
    
    Tbl
    
    TVariantTbl
  - Parse
  - Rel1
  - Rel2
  - Rel3
  - RelList
  - Univ
datalog.top_down
- Datalog_top_down
  - AST
  - CONST
  - Default
    
    BuiltinFun
    
    C
    
    Tbl
    
    CVariantTbl
    
    Const
    
    DB
    
    Index
    
    Data
    
    Lit
    
    Rewriting
    
    Subst
    
    T
    
    Tbl
    
    TVariantTbl
  - Lexer
  - Make
    
    BuiltinFun
    
    C
    
    Tbl
    
    CVariantTbl
    
    Const
    
    DB
    
    Index
    
    Data
    
    Lit
    
    Rewriting
    
    Subst
    
    T
    
    Tbl
    
    TVariantTbl
  - MakeParse
    
    C
    
    TD
    
    BuiltinFun
    
    C
    
    Tbl
    
    CVariantTbl
    
    Const
    
    DB
    
    Index
    
    Data
    
    Lit
    
    Rewriting
    
    Subst
    
    T
    
    Tbl
    
    TVariantTbl
  - PARSABLE_CONST
  - PARSE
  - Parser
  - S
    
    BuiltinFun
    
    C
    
    Tbl
    
    CVariantTbl
    
    Const
    
    DB
    
    Index
    
    Data
    
    Lit
    
    Rewriting
    
    Subst
    
    T
    
    Tbl
    
    TVariantTbl
datalog.unix
- Datalog_unix
  - Default
    
    TD
    
    BuiltinFun
    
    C
    
    Tbl
    
    CVariantTbl
    
    DB
    
    Index
    
    Data
    
    Lit
    
    Rewriting
    
    Subst
    
    T
    
    Tbl
    
    TVariantTbl
  - Make
    
    TD
    
    BuiltinFun
    
    C
    
    Tbl
    
    CVariantTbl
    
    Const
    
    DB
    
    Index
    
    Data
    
    Lit
    
    Rewriting
    
    Subst
    
    T
    
    Tbl
    
    TVariantTbl
  - S
    
    TD
    
    BuiltinFun
    
    C
    
    Tbl
    
    CVariantTbl
    
    Const
    
    DB
    
    Index
    
    Data
    
    Lit
    
    Rewriting
    
    Subst
    
    T
    
    Tbl
    
    TVariantTbl

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Const : Datalog_top_down.CONST

type const = Const.t

val set_debug : bool -> unit

Terms

module T : sig ... end

Literals

module Lit : sig ... end

Clauses

module C : sig ... end

Substs

This module is used for variable bindings.

module Subst : sig ... end

Unification, matching...

type scope = Subst.scope

exception UnifFail

For unify and match_, the optional parameter oc is used to enable or disable occur-check. It is disabled by default.

val unify : 
  ?oc:bool ->
  ?subst:Subst.t ->
  T.t ->
  scope ->
  T.t ->
  scope ->
  Subst.t

Unify the two terms.

raises UnifFail
if it fails

val match_ : 
  ?oc:bool ->
  ?subst:Subst.t ->
  T.t ->
  scope ->
  T.t ->
  scope ->
  Subst.t

match_ a sa b sb matches the pattern a in scope sa with term b in scope sb.

raises UnifFail
if it fails

val alpha_equiv : ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t

Test for alpha equivalence.

raises UnifFail
if it fails

val are_alpha_equiv : T.t -> T.t -> bool

Special version of alpha_equiv, using distinct scopes for the two terms to test, and discarding the result

val clause_are_alpha_equiv : C.t -> C.t -> bool

Alpha equivalence of clauses.

Special built-in functions

The built-in functions are symbols that have a special meaning. The meaning is given by a set of OCaml functions that can evaluate applications of the function symbol to arguments.

For instance, sum is a special built-in function that tries to add its arguments if those are constants.

Note that a constant will never be interpreted.

module BuiltinFun : sig ... end

The following hashtables use alpha-equivalence checking instead of regular, syntactic equality

module TVariantTbl : Hashtbl.S with type key = T.t

module CVariantTbl : Hashtbl.S with type key = C.t

Index

An index is a specialized data structured that is used to efficiently store and retrieve data by a key, where the key is a term. Retrieval involves finding all data associated with terms that match, or unify with, a given term.

module Index (Data : Hashtbl.HashedType) : sig ... end

Rewriting

Rewriting consists in having a set of rules, oriented from left to right, that we will write l -> r (say "l rewrites to r"). Any term t that l matches is rewritten into r by replacing it by sigma(r), where sigma(l) = t.

module Rewriting : sig ... end

DB

A DB stores facts and clauses, that constitute a logic program. Facts and clauses can only be added.

Non-stratified programs will be rejected with NonStratifiedProgram.

exception NonStratifiedProgram

module DB : sig ... end

Query

val ask : 
  ?oc:bool ->
  ?with_rules:C.t list ->
  ?with_facts:T.t list ->
  DB.t ->
  T.t ->
  T.t list

Returns the answers to a query in a given DB. Additional facts and rules can be added in a local scope.

parameter oc
enable occur-check in unification (default false)

val ask_lits : 
  ?oc:bool ->
  ?with_rules:C.t list ->
  ?with_facts:T.t list ->
  DB.t ->
  T.t list ->
  Lit.t list ->
  T.t list

Extension of ask, where the query ranges over the list of variables (the term list), all of which must be bound in the list of literals that form a constraint.

ask_lits db vars lits queries over variables vars with the constraints given by lits.

Conceptually, the query adds a clause (v1, ..., vn) :- lits, which should respect the same safety constraint as other clauses.

returns
a list of answers, each of which is a list of terms that map to the given list of variables.