Module `Flambda2_datalog.Datalog`

Well-typed Datalog implementation.

type nil = private

| Nil

Marker type for the end of heterogenous lists.

module Column : sig ... end

Datalog tables are represented as a nesting of multiple maps; for instance, a binary relation on integers is represented as a unit Int.Map.t Int.Map.t.

type (!'t, !'k, !'v) table

val create_table : 
  ?provenance:bool ->
  name:string ->
  default_value:'v ->
  ('t, 'k, 'v) Column.hlist ->
  ('t, 'k, 'v) table

The provenance argument is true by default. If set to false, provenance tracking will be disabled for this table. This is useful for derived tables that are defined by a single rule, such as indices defined by a permutation of another table.

val columns : ('t, 'k, 'v) table -> ('t, 'k, 'v) Column.hlist

type ('t, 'k) relation = ('t, 'k, unit) table

val create_relation : 
  ?provenance:bool ->
  name:string ->
  ('t, 'k, unit) Column.hlist ->
  ('t, 'k) relation

create_relation ~name schema creates a new relation with name name and schema schema.

The schema is given as a heterogenous list of column types, and the relation is represented in memory as a series of nested maps following this list. If the schema ty1; ty2; ty3 is provided, the relation will be represented as a map from ty1 whose values are maps from ty2 to ty2. The order of arguments provided to a relation thus have profound implication for the performance of iterations on the relation, and needs to be chosen carefully.

See documentation of create_table for the provenance argument.

raises Misc.Fatal_error
if schema is empty.

Example

The following code defines a binary edge relationship between nodes, represented as a map from a node to its successors, and an unary predicate to distinguish some sort of marked nodes.

let marked_pred : node rel1 = create_relation ~name:"marked" [node]

let edge_rel : (node, node) rel2 =
  create_relation ~name:"edge" [node; node]

module Constant : sig ... end

The Constant module only provides a heterogenous list to represent lists of values.

module Term : sig ... end

type atom

type equality

type filter

type hypothesis = [

| `Atom of atom
| `Not_atom of atom
| `Distinct of equality
| `Filter of filter

]

val atom : ('t, 'k) relation -> 'k Term.hlist -> [> `Atom of atom ]

atom rel args represents the application of relation rel to the arguments args.

When writing queries or rules, it can be helpful to partially apply atom to relations in order to improve readability.

Example

let marked = atom marked_pred

let edge = atom edge_rel

val not : [< `Atom of atom ] -> [> `Not_atom of atom ]

val distinct : 
  (_, 'k, _) Column.id ->
  'k Term.t ->
  'k Term.t ->
  [> `Distinct of equality ]

val filter : 
  ('k Constant.hlist -> bool) ->
  'k Term.hlist ->
  [> `Filter of filter ]

type database

val print : Format.formatter -> database -> unit

val empty : database

val get_table : ('t, 'k, 'v) table -> database -> 't

val set_table : ('t, 'k, 'v) table -> 't -> database -> database

val add_fact : ('t, 'k) relation -> 'k Constant.hlist -> database -> database

add_fact rel args db records a fact into the database db.

Example

The following code populates a database with a small graph and a single marked node n1.

let n1 = Node.make ()

let n2 = Node.make ()

let n3 = Node.make ()

let n4 = Node.make ()

let n5 = Node.make ()

let db =
  add_fact marked_pred [n1]
  @@ add_fact edge_rel [n1; n2]
  @@ add_fact edge_rel [n3; n2]
  @@ add_fact edge_rel [n2; n5]
  @@ add_fact edge_rel [n5; n4]
  @@ add_fact edge_rel [n4; n2]
  @@ empty

module String : sig ... end

Pseudo-heterogenous lists of strings.

module Cursor : sig ... end

A cursor represents a query on the database. Cursors provide iter and fold functions to iterate over the matching facts.

type rule

The type of compiled rules.

Rule specifications must be compiled to low-level rules using compile_rule before being applied to a database using Schedule.rules.

Note: Although compiled rules are mutable data structures, this mutability is only exploited while the compiled rule is executing (e.g. during Schedule.run). It is thus safe to reuse a rule across multiple schedules or within the same schedule.

module Schedule : sig ... end

type bindings

val print_bindings : Format.formatter -> bindings -> unit

type ('p, 'a) program

The type ('p, 'v) program is the type of programs returning values of type 'v with parameters 'p.

The output of programs is either queries or rules; the use of a shared types allows writing combinators that work in both cases.

val compile : 'v String.hlist -> ('v Term.hlist -> (nil, 'a) program) -> 'a

Compile a program and returns the resulting value.

Note: As a convenience, compile takes a list of variables and binds them immediately with foreach. To compile an existing program with no free variables, use compile [] (fun [] -> program).

Repeated compilation of a program building mutable values (such as cursors) create new values each time they are compiled.

val compile_with_parameters : 
  'p String.hlist ->
  'v String.hlist ->
  ('p Term.hlist -> 'v Term.hlist -> ('p, 'a) program) ->
  'a

val foreach : 
  'a String.hlist ->
  ('a Term.hlist -> ('p, 'b) program) ->
  ('p, 'b) program

foreach vars prog binds the variables vars in prog.

The order variables are provided in vars is the iteration order during evaluation.

val where : hypothesis list -> ('p, 'a) program -> ('p, 'a) program

val yield : 'v Term.hlist -> ('p, ('p, 'v) Cursor.with_parameters) program

yield args is a query program that outputs the tuple args.

type deduction = [

| `Atom of atom
| `And of deduction list

]

val and_ : 'a list -> [> `And of 'a list ]

val deduce : deduction -> (nil, rule) program

deduce rel args adds the fact rel args to the database.

module Schema : sig ... end

Module Flambda2_datalog.Datalog

Module `Flambda2_datalog.Datalog`