package datalog

You can search for identifiers within the package.

in-package search v0.2.0

An in-memory datalog implementation for OCaml

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (8)

Authors

S

Simon Cruanes

Maintainers

S

simon.cruanes.2007@m4x.org

Sources

datalog-0.7.tbz

sha256=13ca520bddf4f0c44d1468bc89347be72ec543be58fff29469a0da24956be541

sha512=25d6e9cb5abe8aa1110730d884abb9e51ae78bf681b3f21709efa32359b9cbdd97d9076761c91562580c090cbce12ce159c97533ae5d9d427c24cb329e950793

doc/datalog.top_down/Datalog_top_down/Default/index.html

Module `Datalog_top_down.Default`Source

include S with type Const.t = const

Sourcemodule Const : CONST with type t = const

Sourcetype const = Const.t

Sourceval set_debug : bool -> unit

Terms

Sourcemodule T : sig ... end

Literals

Sourcemodule Lit : sig ... end

Clauses

Sourcemodule C : sig ... end

Substs

This module is used for variable bindings.

Sourcemodule Subst : sig ... end

Unification, matching...

Sourcetype scope = Subst.scope

Sourceexception UnifFail

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

Source

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

Unify the two terms.

raises UnifFail
if it fails

Source

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

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

Test for alpha equivalence.

raises UnifFail
if it fails

Sourceval 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

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

Sourcemodule BuiltinFun : sig ... end

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

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

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

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

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

Sourceexception NonStratifiedProgram

Sourcemodule DB : sig ... end

Query

Source

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)

Source

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.

Sourceval default_interpreters : (const * string * DB.interpreter) list

List of default interpreters for some symbols, mostly infix predicates

Sourceval builtin : (const * BuiltinFun.t) list

Default builtin functions

Sourceval setup_default : DB.t -> unit

Load the default interpreters and builtin functions into the DB

include PARSE with type term = T.t and type lit = Lit.t and type clause = C.t

Sourcetype term = T.t

Sourcetype lit = Lit.t

Sourcetype clause = C.t

Sourcetype name_ctx = (string, term) Hashtbl.t

Sourceval create_ctx : unit -> name_ctx

Sourceval term_of_ast : ctx:name_ctx -> AST.term -> term

Sourceval lit_of_ast : ctx:name_ctx -> AST.literal -> lit

Sourceval clause_of_ast : ?ctx:name_ctx -> AST.clause -> clause

Sourceval clauses_of_ast : ?ctx:name_ctx -> AST.clause list -> clause list

Sourceval parse_chan : in_channel -> [ `Ok of clause list | `Error of string ]

Sourceval parse_file : string -> [ `Ok of clause list | `Error of string ]

Sourceval parse_string : string -> [ `Ok of clause list | `Error of string ]

Sourceval clause_of_string : string -> clause

Parse a clause from a string, or fail. Useful shortcut to define properties of relations without building terms by hand.

raises Failure
if the string is not a valid clause

Sourceval term_of_string : string -> term

raises Failure
if the string is not a valid term

package datalog

Install

Dune Dependency

Authors

Maintainers

Sources

doc/datalog.top_down/Datalog_top_down/Default/index.html

Module Datalog_top_down.DefaultSource

Terms

Literals

Clauses

Substs

Unification, matching...

Special built-in functions

Index

Rewriting

DB

Query

Module `Datalog_top_down.Default`Source