▼Datalog for PLT Scheme
On this page:
theory/ c
immutable-theory/ c
mutable-theory/ c
make-mutable-theory
make-immutable-theory
safe-clause?
assume
retract
assume!
retract!
prove
  ← prev  up  next → 

7 Runtime System

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

 (require (planet jaymccarthy/datalog:1:3/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).

  

  ← prev  up  next →