7 Runtime System
This library implements the Datalog runtime system. It can be required via:
(make-mutable-theory) → mutable-theory/c |
(make-immutable-theory) → immutable-theory/c |
Constructs a immutable
theory.
Determines if a clause is safe.
A clause is safe if every variable in its head occurs in some literal in its body.
(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). | |
|