package datalog

You can search for identifiers within the package.

in-package search v0.2.0

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

type t

A database is a repository for Datalog clauses.

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

val create : ?parent:t -> unit -> t

val copy : t -> t

val clear : t -> unit

val add_fact : t -> T.t -> unit

val add_facts : t -> T.t list -> unit

val add_clause : t -> C.t -> unit

val add_clauses : t -> C.t list -> unit

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

val interpret_list : t -> (const * string * interpreter) list -> unit

Add several interpreters, with their documentation

val is_interpreted : t -> const -> bool

Is the constant interpreted by some OCaml code?

val add_builtin : t -> Const.t -> BuiltinFun.t -> unit

Add a builtin fun

val builtin_funs : t -> BuiltinFun.map

val eval : t -> T.t -> T.t

Evaluate the given term at root

val help : t -> string list

Help messages for interpreted predicates

val num_facts : t -> int

val num_clauses : t -> int

val size : t -> int

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

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

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.