On this page:
theory/ c
immutable-theory/ c
mutable-theory/ c
make-mutable-theory
make-immutable-theory
safe-clause?
assume
retract
assume!
retract!
prove
Version: 4.1.5.1

7 Runtime System

This library implements the Datalog runtime system. It can be required via:

 (require (planet jaymccarthy/datalog:1:1/runtime))

theory/c : contract?

A contract for theories.

immutable-theory/c : contract?

A contract for immutable theories.

mutable-theory/c : contract?

A contract for mutable theories.

(make-mutable-theory)  mutable-theory/c

Constructs a mutable theory.

(make-immutable-theory)  immutable-theory/c

Constructs a immutable theory.

(safe-clause? c)  boolean?
  c : clause?

Determines if a clause is safe. A clause is safe if every variable in its head occurs in some literal in its body.

Examples:

  > (safe-clause?
     (parse-clause (open-input-string "ancestor(joseph,jay)")))

  #t

  > (safe-clause?
     (parse-clause
      (open-input-string "ancestor(A,B) :- parent(A,B)")))

  #t

  > (safe-clause?
     (parse-clause
      (open-input-string "ancestor(A,B) :- parent(A,jay)")))

  #f

(assume thy c)  immutable-theory/c
  thy : immutable-theory/c
  c : safe-clause?

Adds c to thy in a persistent way.

(retract thy c)  immutable-theory/c
  thy : immutable-theory/c
  c : clause?

Removes c from thy in a persistent way.

(assume! thy c)  mutable-theory/c
  thy : mutable-theory/c
  c : safe-clause?

Adds c to thy.

(retract! thy c)  mutable-theory/c
  thy : mutable-theory/c
  c : clause?

Removes c from thy.

(prove thy l)  (listof literal?)
  thy : theory/c
  l : literal?

Attempts to prove l using the theory thy, returning all the results of the query.

Examples:

  > (pretty-print
     (format-literals
      (prove
       (assume
        (make-immutable-theory)
        (parse-clause (open-input-string "parent(joseph1,joseph2)")))
       (parse-literal
        (open-input-string "parent(joseph1,joseph2)")))))

  parent(joseph1, joseph2).

  

  > (pretty-print
     (format-literals
      (prove
       (retract
        (assume
         (make-immutable-theory)
         (parse-clause
          (open-input-string "parent(joseph1,joseph2)")))
        (parse-clause (open-input-string "parent(joseph1,joseph2)")))
       (parse-literal
        (open-input-string "parent(joseph1,joseph2)")))))

  

  > (pretty-print
     (format-literals
      (prove
       (assume
        (make-immutable-theory)
        (parse-clause (open-input-string "parent(joseph1,joseph2)")))
       (parse-literal (open-input-string "parent(A,B)")))))

  parent(joseph1, joseph2).