suzanne.soy/datalog
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Initial add of Datalog

Browse Source 
original commit: 940db1ab6c81cc04a9a856021eb4ccc0d88fac07
This commit is contained in:
Jay McCarthy 2010-06-24 13:44:07 -06:00
commit c26d108e75
19 changed files with 1767 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

86
collects/datalog/ast.rkt Normal file
View File

@ -0,0 +1,86 @@
#lang scheme
(define srcloc/c
(or/c syntax?
false/c
(list/c any/c
(or/c exact-positive-integer? #f)
(or/c exact-nonnegative-integer? #f)
(or/c exact-nonnegative-integer? #f)
(or/c exact-positive-integer? #f))))
(define datum/c (or/c string? symbol?))
(define datum-equal? equal?)
(define-struct variable (srcloc sym) #:prefab)
(define (variable-equal? v1 v2)
(eq? (variable-sym v1) (variable-sym v2)))
(define-struct constant (srcloc datum) #:prefab)
(define (constant-equal? v1 v2)
(datum-equal? (constant-datum v1) (constant-datum v2)))
(define term/c (or/c variable? constant?))
(define (term-equal? t1 t2)
(cond
[(and (variable? t1) (variable? t2))
(variable-equal? t1 t2)]
[(and (constant? t1) (constant? t2))
(constant-equal? t1 t2)]
[else
#f]))
(define-struct literal (srcloc predicate terms) #:prefab)
(define (literal-equal? l1 l2)
(and (datum-equal? (literal-predicate l1)
(literal-predicate l2))
(= (length (literal-terms l1))
(length (literal-terms l2)))
(andmap term-equal?
(literal-terms l1)
(literal-terms l2))))
(define-struct clause (srcloc head body) #:prefab)
(define (clause-equal? c1 c2)
(and (literal-equal? (clause-head c1)
(clause-head c2))
(= (length (clause-body c1))
(length (clause-body c2)))
(andmap literal-equal?
(clause-body c1)
(clause-body c2))))
(define-struct assertion (srcloc clause) #:prefab)
(define-struct retraction (srcloc clause) #:prefab)
(define-struct query (srcloc literal) #:prefab)
(define statement/c (or/c assertion? retraction? query?))
(define program/c (listof statement/c))
(provide/contract
[srcloc/c contract?]
[datum/c contract?]
[datum-equal? (datum/c datum/c . -> . boolean?)]
[struct variable ([srcloc srcloc/c]
[sym symbol?])]
[variable-equal? (variable? variable? . -> . boolean?)]
[struct constant ([srcloc srcloc/c]
[datum datum/c])]
[constant-equal? (constant? constant? . -> . boolean?)]
[term/c contract?]
[term-equal? (term/c term/c . -> . boolean?)]
[struct literal ([srcloc srcloc/c]
[predicate datum/c]
[terms (listof term/c)])]
[literal-equal? (literal? literal? . -> . boolean?)]
[struct clause ([srcloc srcloc/c]
[head literal?]
[body (listof literal?)])]
[clause-equal? (clause? clause? . -> . boolean?)]
[struct assertion ([srcloc srcloc/c]
[clause clause?])]
[struct retraction ([srcloc srcloc/c]
[clause clause?])]
[struct query ([srcloc srcloc/c]
[literal literal?])]
[statement/c contract?]
[program/c contract?])

58
collects/datalog/eval.rkt Normal file
View File

@ -0,0 +1,58 @@
#lang scheme
(require scheme/list
(except-in (planet dherman/pprint:4) empty)
"ast.ss"
"pretty.ss"
"runtime.ss")
(define current-theory (make-parameter (make-mutable-theory)))
(define (assume-if-safe assume thy s)
(let ([c (assertion-clause s)])
(if (safe-clause? c)
(assume thy c)
(raise-syntax-error 'datalog
"Unsafe clause in assertion"
(datum->syntax #f (pretty-format (format-statement s)) (assertion-srcloc s))))))
(define (print-literals ls)
(pretty-print
(format-literals ls)))
(define (eval-program p)
(for-each (lambda (s)
(define v (eval-statement s))
(unless (void? v)
(print-literals v)))
p))
(define (eval-statement s)
(cond
[(assertion? s)
(assume-if-safe assume! (current-theory) s)]
[(retraction? s)
(retract! (current-theory) (retraction-clause s))]
[(query? s)
(prove (current-theory) (query-literal s))]))
(define (eval-program/fresh p)
(let loop ([thy (make-immutable-theory)]
[p p])
(if (empty? p)
thy
(let ([s (first p)])
(loop
(cond
[(assertion? s)
(assume-if-safe assume thy s)]
[(retraction? s)
(retract thy (retraction-clause s))]
[(query? s)
(print-literals (prove thy (query-literal s)))
thy])
(rest p))))))
(provide/contract
[current-theory (parameter/c mutable-theory/c)]
[eval-program (program/c . -> . void)]
[eval-statement (statement/c . -> . (or/c void (listof literal?)))]
[eval-program/fresh (program/c . -> . immutable-theory/c)])

10
collects/datalog/info.rkt Normal file
View File

@ -0,0 +1,10 @@
#lang setup/infotab
(define name "Datalog")
(define blurb
(list "An implementation of Datalog as a Racket language."))
(define scribblings '(["scribblings/datalog.scrbl" (multi-page)]))
(define categories '(devtools))
(define primary-file "main.ss")
(define compile-omit-paths '("tests"))
(define release-notes (list))
(define repositories '("4.x"))

18
collects/datalog/lang/reader.rkt Normal file
View File

@ -0,0 +1,18 @@
(module reader syntax/module-reader
#:language `(planet ,(this-package-version-symbol lang/module))
#:read (lambda ([in (current-input-port)])
(let ([ast (parse-program in)])
(list `(#%module-begin ,@ast))))
#:read-syntax (lambda ([source-name #f] [in (current-input-port)])
(let ([ast (parse-program in)])
(list `(#%module-begin ,@ast))))
#:whole-body-readers? #t
#:info (lambda (key defval default)
; XXX Should have comment character key
; XXX repl submit
(case key
[(color-lexer)
(dynamic-require `(planet ,(this-package-version-symbol drscheme/syntax-color)) 'get-syntax-token)]
[else (default key defval)]))
(require (planet cce/scheme:6/planet)
"../parse.ss"))

13
collects/datalog/main.rkt Normal file
View File

@ -0,0 +1,13 @@
#lang scheme
(require "ast.ss"
"parse.ss"
"sexp.ss"
"pretty.ss"
"runtime.ss"
"eval.ss")
(provide (all-from-out "ast.ss"
"parse.ss"
"sexp.ss"
"pretty.ss"
"runtime.ss"
"eval.ss"))

110
collects/datalog/parse.rkt Normal file
View File

@ -0,0 +1,110 @@
#lang scheme
(require parser-tools/lex
parser-tools/yacc
"private/lex.ss"
"ast.ss")
#|
5.1 Literals
A literal, is a predicate symbol followed by an optional parenthesized list of comma separated terms. A predicate symbol is either an identifier or a string. A term is either a variable or a constant. As with predicate symbols, a constant is either an identifier or a string. The following are literals:
parent(john, douglas)
zero-arity-literal
aBcD(-0, "\n\FF")
"="(3,3)
""(-0-0-0,&&&,***,"\00")
5.2 Clauses
A clause is a head literal followed by an optional body. A body is a comma separated list of literals. A clause without a body is called a fact, and a rule when it has one. The punctuation `:-' separates the head of a rule from its body. A clause is safe if every variable in its head occurs in some literal in its body. The following are safe clauses:
parent(john, douglas)
ancestor(A, B) :-
parent(A, B)
ancestor(A, B) :-
parent(A, C),
ancestor(C, B)
5.3 Programs
A Datalog reader consumes a Datalog program. A program is a sequence of zero or more statements, followed by an optional query. A statement is an assertion or a retraction. An assertion is a clause followed by a period, and it adds the clause to the database if it is safe. A retraction is a clause followed by a tilde, and it removes the clause from the database. A query is a literal followed by a question mark. The effect of reading a Datalog program is to modify the database as directed by its statements, and then to return the literal designated as the query. If no query is specified, a reader returns a literal know to have no answers. The following is a program:
edge(a, b). edge(b, c). edge(c, d). edge(d, a).
path(X, Y) :- edge(X, Y).
path(X, Y) :- edge(X, Z), path(Z, Y).
path(X, Y)?
|#
(define current-source-name (make-parameter #f))
(define (make-srcloc start-pos end-pos)
(list (current-source-name)
(position-line start-pos)
(position-col start-pos)
(position-offset start-pos)
(- (position-offset end-pos) (position-offset start-pos))))
(define-values
(program-parser statement-parser clause-parser literal-parser)
(apply
values
(parser
(start program statement clause literal)
(end EOF)
(tokens dtokens dpunct)
(src-pos)
(error
(lambda (tok-ok? tok-name tok-value start-pos end-pos)
(raise-syntax-error 'datalog
(if tok-ok?
(format "Unexpected token ~S" tok-name)
(format "Invalid token ~S" tok-name))
(datum->syntax #f tok-value (make-srcloc start-pos end-pos)))))
(grammar
(program [(statements) $1])
(statements [(statement) (list $1)]
[(statement statements) (list* $1 $2)])
(statement [(assertion) $1]
[(query) $1]
[(retraction) $1])
(assertion [(clause DOT) (make-assertion (make-srcloc $1-start-pos $2-end-pos) $1)])
(retraction [(clause TILDE) (make-retraction (make-srcloc $1-start-pos $2-end-pos) $1)])
(query [(literal QMARK) (make-query (make-srcloc $1-start-pos $2-end-pos) $1)])
(clause [(literal TSTILE body) (make-clause (make-srcloc $1-start-pos $3-end-pos) $1 $3)]
[(literal) (make-clause (make-srcloc $1-start-pos $1-end-pos) $1 empty)])
(body [(literal COMMA body) (list* $1 $3)]
[(literal) (list $1)])
(literal [(predicate-sym LPAREN RPAREN) (make-literal (make-srcloc $1-start-pos $3-end-pos) $1 empty)]
[(predicate-sym LPAREN terms RPAREN) (make-literal (make-srcloc $1-start-pos $4-end-pos) $1 $3)]
[(predicate-sym) (make-literal (make-srcloc $1-start-pos $1-end-pos) $1 empty)]
[(term EQUAL term) (make-literal (make-srcloc $1-start-pos $3-end-pos) '= (list $1 $3))])
(predicate-sym [(IDENTIFIER) (string->symbol $1)]
[(STRING) $1])
(terms [(term) (list $1)]
[(term COMMA terms) (list* $1 $3)])
(term [(VARIABLE) (make-variable (make-srcloc $1-start-pos $1-end-pos) (string->symbol $1))]
[(constant) (make-constant (make-srcloc $1-start-pos $1-end-pos) $1)])
(constant [(IDENTIFIER) (string->symbol $1)]
[(STRING) $1]))
(suppress))))
(define ((mk-parser which) ip)
(define (go)
(port-count-lines! ip)
(which (lambda () (dlexer ip))))
(if (current-source-name)
(go)
(parameterize ([current-source-name (object-name ip)]
[file-path (object-name ip)])
(go))))
(define parse-literal (mk-parser literal-parser))
(define parse-clause (mk-parser clause-parser))
(define parse-statement (mk-parser statement-parser))
(define parse-program (mk-parser program-parser))
(provide/contract
[parse-literal (input-port? . -> . literal?)]
[parse-clause (input-port? . -> . clause?)]
[parse-statement (input-port? . -> . statement/c)]
[parse-program (input-port? . -> . program/c)])

75
collects/datalog/pretty.rkt Normal file
View File

@ -0,0 +1,75 @@
#lang scheme
(require (planet dherman/pprint:4)
"ast.ss")
(define (format-datum s)
(cond
[(string? s)
(text (format "~S" s))]
[(symbol? s)
(text (symbol->string s))]))
(define (format-variable v)
(format-datum (variable-sym v)))
(define (format-constant c)
(format-datum (constant-datum c)))
(define (format-term t)
(cond
[(variable? t)
(format-variable t)]
[(constant? t)
(format-constant t)]))
(define (format-literal l)
(match l
[(struct literal (_ pred (list)))
(format-datum pred)]
[(struct literal (_ '= (list a b)))
(h-append (format-term a) space (text "=") space (format-term b))]
[(struct literal (_ pred terms))
(h-append (format-datum pred)
lparen
(v-concat/s (apply-infix comma (map format-term terms)))
rparen)]))
(define (format-literals ls)
(v-concat
(append (map (lambda (l)
(format-assertion (make-assertion #f (make-clause #f l (list)))))
ls)
(list line))))
(define (format-clause c)
(if (empty? (clause-body c))
(format-literal (clause-head c))
(nest 4
(v-concat/s
(list* (h-append (format-literal (clause-head c)) space (text ":-"))
(apply-infix comma (map format-literal (clause-body c))))))))
(define (format-assertion a)
(h-append (format-clause (assertion-clause a))
dot))
(define (format-retraction r)
(h-append (format-clause (retraction-clause r))
(char #\~)))
(define (format-query q)
(h-append (format-literal (query-literal q))
(char #\?)))
(define (format-statement s)
(cond
[(assertion? s) (format-assertion s)]
[(retraction? s) (format-retraction s)]
[(query? s) (format-query s)]))
(define (format-program p)
(v-concat (map format-statement p)))
(provide/contract
[format-datum (datum/c . -> . doc?)]
[format-variable (variable? . -> . doc?)]
[format-constant (constant? . -> . doc?)]
[format-term (term/c . -> . doc?)]
[format-literal (literal? . -> . doc?)]
[format-literals ((listof literal?) . -> . doc?)]
[format-clause (clause? . -> . doc?)]
[format-assertion (assertion? . -> . doc?)]
[format-retraction (retraction? . -> . doc?)]
[format-query (query? . -> . doc?)]
[format-statement (statement/c . -> . doc?)]
[format-program (program/c . -> . doc?)])

20
collects/datalog/private/compiler.rkt Normal file
View File

@ -0,0 +1,20 @@
#lang scheme/base
(require scheme/contract
"../ast.ss"
(for-syntax scheme/base))
(require (for-template scheme/base
"../eval.ss"))
(define (compile-module asts)
(with-syntax ([(s ...) asts])
(syntax
(begin (eval-statement s) ...))))
(define (compile-stmt ast)
(with-syntax ([s ast])
(syntax
(eval-statement s))))
(provide/contract
[compile-module (list? . -> . syntax?)]
[compile-stmt (statement/c . -> . syntax?)])

17
collects/datalog/private/env.rkt Normal file
View File

@ -0,0 +1,17 @@
#lang scheme
(require "../ast.ss")
(define env/c
(and/c hash? immutable?))
(define (empty-env)
(make-immutable-hash empty))
(define (lookup env var [def #f])
(hash-ref env var def))
(define (extend env var val)
(hash-set env var val))
(provide/contract
[env/c contract?]
[empty-env (-> env/c)]
[lookup ((env/c symbol?) (term/c) . ->* . (or/c false/c term/c))]
[extend (env/c symbol? term/c . -> . void)])

61
collects/datalog/private/lex.rkt Normal file
View File

@ -0,0 +1,61 @@
#lang scheme
(require parser-tools/lex
(prefix-in : parser-tools/lex-sre))
#|
5 Syntax
In Datalog input, whitespace characters are ignored except when they separate adjacent tokens or when they occur in strings. Comments are also considered to be whitespace. The character `%' introduces a comment, which extends to the next line break. Comments do not occur inside strings.
The characters in Datalog input are collected into tokens according to the rules that follow. There are four classes of tokens: punctuations, variables, identifiers, and strings. The punctuation tokens are: `(', `,', `)', `=', `:-', `.', `~', `?', and `"'.
A variable is a sequence of Latin capital and small letters, digits, and the underscore character. A variable must begin with a Latin capital letter.
An identifier is a sequence of printing characters that does not contain any of the following characters: `(', `,', `)', `=', `:', `.', `~', `?', `"', `%', and space. An identifier must not begin with a Latin capital letter. Note that the characters that start punctuation are forbidden in identifiers, but the hyphen character is allowed.
A string is a sequence of characters enclosed in double quotes. Characters other than double quote, newline, and backslash may be directly included in a string. The remaining characters may be specified using escape characters, `\"', `\n', and `\\' respectively.
Other escape characters can be used to improve the readability of the input. If a string is too long to fit conveniently on one line, all but the final line containing the string can be ended with a backslash character, and each backslash newline pair is ignored. The character escape codes from the C programming language are allowed—`\a', `\b', `\f', `\n', `\r', `\t', `\v', `\'', and `\?'. The numeric escape codes consist of exactly two uppercase hex digits. Thus the ASCII character newline is `\0A', and zero is `\00'.
|#
(define-tokens dtokens (VARIABLE IDENTIFIER STRING))
(define-empty-tokens dpunct (LPAREN COMMA RPAREN TSTILE DOT EQUAL TILDE QMARK EOF))
(define-lex-abbrev line-break #\newline)
(define-lex-abbrev id-chars (char-complement (char-set "(,)=:.~?\"% \n")))
(define-lex-abbrev variable-re (:: upper-case (:* (:or upper-case lower-case (char-set "0123456789_")))))
(define-lex-abbrev identifier-re (:: id-chars (:* (:or upper-case id-chars))))
(define-lex-abbrev comment-re (:: "%" (complement (:: any-string line-break any-string)) line-break))
(define get-string-token
(lexer
[(:~ #\" #\\) (cons (car (string->list lexeme))
(get-string-token input-port))]
[(:: #\\ #\\) (cons #\\ (get-string-token input-port))]
[(:: #\\ #\newline) (cons #\newline (get-string-token input-port))]
[(:: #\\ #\") (cons #\" (get-string-token input-port))]
[#\" null]))
(define dlexer
(lexer-src-pos
[whitespace
(return-without-pos (dlexer input-port))]
[comment-re
(return-without-pos (dlexer input-port))]
[variable-re
(token-VARIABLE lexeme)]
[identifier-re
(token-IDENTIFIER lexeme)]
[":-" (token-TSTILE)]
[#\" (token-STRING (list->string (get-string-token input-port)))]
[#\( (token-LPAREN)]
[#\, (token-COMMA)]
[#\) (token-RPAREN)]
[#\. (token-DOT)]
[#\~ (token-TILDE)]
[#\? (token-QMARK)]
[#\= (token-EQUAL)]
[(eof) (token-EOF)]))
(provide dtokens dpunct
line-break id-chars variable-re identifier-re comment-re
dlexer)

54
collects/datalog/private/subst.rkt Normal file
View File

@ -0,0 +1,54 @@
#lang scheme
(require "../ast.ss"
"env.ss")
(define (subst-term env t)
(match t
[(struct variable (_ var))
(lookup env var t)]
[_
t]))
(define (subst-literal env lit)
(make-literal (literal-srcloc lit)
(literal-predicate lit)
(map (lambda (t) (subst-term env t))
(literal-terms lit))))
(define (subst-clause env c)
(make-clause (clause-srcloc c)
(subst-literal env (clause-head c))
(map (lambda (l) (subst-literal env l))
(clause-body c))))
(define (shuffle env lit)
(match lit
[(struct literal (_ pred terms))
(let loop ([env env]
[terms terms])
(match terms
[(list)
env]
[(list-rest (struct constant (_ value)) terms)
(loop env terms)]
[(list-rest (struct variable (srcloc var)) terms)
(if (lookup env var)
(loop env terms)
(loop (extend env var (make-variable srcloc (gensym var))) terms))]))]))
(define (rename-clause c)
(define env
(foldl (lambda (e a)
(shuffle a e))
(shuffle (empty-env) (clause-head c))
(clause-body c)))
(subst-clause env c))
(define (rename-literal lit)
(subst-literal (shuffle (empty-env) lit) lit))
(provide/contract
[subst-term (env/c term/c . -> . term/c)]
[subst-clause (env/c clause? . -> . clause?)]
[rename-clause (clause? . -> . clause?)]
[rename-literal (literal? . -> . literal?)])

49
collects/datalog/private/unify.rkt Normal file
View File

@ -0,0 +1,49 @@
#lang scheme
(require "../ast.ss"
"env.ss")
(define (chase env t)
(match t
[(struct variable (_ var))
(cond
[(lookup env var)
=> (lambda (term) (chase env term))]
[else t])]
[_ t]))
(define (unify-term env t1 t2)
(define t1-p (chase env t1))
(define t2-p (chase env t2))
(if (term-equal? t1-p t2-p)
env
(match t1-p
[(struct variable (_ var))
(extend env var t2-p)]
[_
(match t2-p
[(struct variable (_ var))
(extend env var t1-p)]
[_
#f])])))
(define (unify-terms env ts1 ts2)
(if (empty? ts1)
(if (empty? ts2)
env
#f)
(if (empty? ts2)
#f
(match (unify-term env (first ts1) (first ts2))
[#f #f]
[env (unify-terms env (rest ts1) (rest ts2))]))))
(define (unify l1 l2)
(and (datum-equal? (literal-predicate l1)
(literal-predicate l2))
(unify-terms (empty-env)
(literal-terms l1)
(literal-terms l2))))
(provide/contract
[unify (literal? literal? . -> . (or/c false/c env/c))]
[unify-term (env/c term/c term/c . -> . (or/c false/c env/c))])

83
collects/datalog/private/variant.rkt Normal file
View File

@ -0,0 +1,83 @@
#lang scheme
(require "../ast.ss"
"env.ss")
; Variants
(define (variant-terms env1 env2 ts1 ts2)
(if (empty? ts1)
(empty? ts2)
(and (not (empty? ts2))
(variant-term
env1 env2
(first ts1) (first ts2)
(rest ts1) (rest ts2)))))
(define (variant-term env1 env2 t1 t2 ts1 ts2)
(or (and (variable? t1) (variable? t2)
(variant-var
env1 env2
(variable-sym t1) (variable-sym t2)
ts1 ts2))
(and (term-equal? t1 t2)
(variant-terms env1 env2 ts1 ts2))))
(define (variant-var env1 env2 v1 v2 ts1 ts2)
(match (cons (lookup env1 v1) (lookup env2 v2))
[(list-rest #f #f)
(variant-terms
(extend env1 v1 (make-variable #f v2))
(extend env2 v2 (make-variable #f v1))
ts1 ts2)]
[(list (struct variable (_ v1-p)) (struct variable (_ v2-p)))
(and (datum-equal? v1-p v2)
(datum-equal? v2-p v1)
(variant-terms env1 env2 ts1 ts2))]
[_ #f]))
(define (variant? l1 l2)
(and
(datum-equal? (literal-predicate l1)
(literal-predicate l2))
(variant-terms
(empty-env) (empty-env)
(literal-terms l1)
(literal-terms l2))))
(define (mem-literal lit ls)
(ormap (lambda (l) (variant? lit l)) ls))
; Literal Tables modulo variant?
(define (term-hash t recur-hash)
(cond
[(variable? t)
101]
[(constant? t)
(recur-hash (constant-datum t))]))
(define ((mk-literal-hash recur-hash) l)
(let loop ([code (recur-hash (literal-predicate l))]
[i 0]
[terms (literal-terms l)])
(if (empty? terms)
code
(loop (+ code (term-hash (first terms) recur-hash) (* i -7))
(add1 i)
(rest terms)))))
(define literal-tbl/c
(coerce-contract 'variant dict?))
(define (make-literal-tbl)
(make-custom-hash
variant?
(mk-literal-hash equal-hash-code)
(mk-literal-hash equal-secondary-hash-code)))
(define (literal-tbl-find ltbl s)
(dict-ref ltbl s #f))
(define (literal-tbl-replace! ltbl s x)
(dict-set! ltbl s x))
(provide/contract
[literal-tbl/c contract?]
[make-literal-tbl (-> literal-tbl/c)]
[literal-tbl-find (literal-tbl/c literal? . -> . (or/c false/c any/c))]
[literal-tbl-replace! (literal-tbl/c literal? any/c . -> . void)]
[mem-literal (literal? (listof literal?) . -> . boolean?)])

135
collects/datalog/runtime.rkt Normal file
View File

@ -0,0 +1,135 @@
#lang scheme
(require "ast.ss"
"private/env.ss"
"private/subst.ss"
"private/unify.ss"
"private/variant.ss")
; A clause is safe if every variable in its head occurs in some literal in its body.
(define (safe-clause? c)
(define head-vars (filter variable? (literal-terms (clause-head c))))
(andmap (lambda (v)
(ormap (lambda (l)
(ormap (lambda (t) (term-equal? t v))
(literal-terms l)))
(clause-body c)))
head-vars))
(define theory/c (coerce-contract 'exec hash?))
(define immutable-theory/c (and/c hash? immutable?))
(define mutable-theory/c (and/c hash? (not/c immutable?)))
(define (literal-key l)
(format "~a/~a" (literal-predicate l) (length (literal-terms l))))
(define (clause-key c)
(literal-key (clause-head c)))
(define (make-immutable-theory)
(make-immutable-hash empty))
(define (make-mutable-theory)
(make-hash))
(define ((mk-assume hash-update) thy c)
(hash-update
thy (clause-key c)
(lambda (clauses)
(list* c clauses))
empty))
(define ((mk-retract hash-update) thy rc)
(hash-update
thy (clause-key rc)
(lambda (clauses)
(filter (lambda (c)
(not (clause-equal? c rc)))
clauses))
empty))
(define assume (mk-assume hash-update))
(define retract (mk-retract hash-update))
(define assume! (mk-assume hash-update!))
(define retract! (mk-retract hash-update!))
(define (get thy lit)
(hash-ref thy (literal-key lit) empty))
(define-struct subgoal
(literal
[facts #:mutable]
[waiters #:mutable]))
(define (resolve c lit)
(define body (clause-body c))
(and (not (empty? body))
(cond
[(unify (first body) (rename-literal lit))
=> (lambda (env)
(subst-clause env (make-clause (clause-srcloc c) (clause-head c) (rest body))))]
[else #f])))
(define (prove thy lit)
(define subgoals (make-literal-tbl))
(define (fact! sg lit)
(unless (mem-literal lit (subgoal-facts sg))
(set-subgoal-facts! sg (list* lit (subgoal-facts sg)))
(for-each (lambda (w)
(cond
[(resolve (cdr w) lit)
=> (lambda (cs-p) (add-clause! (car w) cs-p))]))
(subgoal-waiters sg))))
(define (rule! sg1 c s)
(define sg2 (literal-tbl-find subgoals s))
(if sg2
(begin
(set-subgoal-waiters! sg2 (list* (cons sg1 c) (subgoal-waiters sg2)))
(for-each (lambda (fact)
(cond
[(resolve c fact)
=> (lambda (cs) (add-clause! sg1 cs))]))
(subgoal-facts sg2)))
(let ([sg2 (make-subgoal s empty (list (cons sg1 c)))])
(literal-tbl-replace! subgoals s sg2)
(search! sg2))))
(define (add-clause! sg c)
(match c
[(struct clause (_ lit (list)))
(fact! sg lit)]
[(struct clause (_ _ (list-rest selected _)))
(rule! sg c selected)]))
(define (search-theory! sg)
(for-each
(lambda (clause)
(define renamed (rename-clause clause))
(define selected (clause-head renamed))
(cond
[(unify (subgoal-literal sg) selected)
=> (lambda (env)
(add-clause! sg (subst-clause env renamed)))]))
(get thy (subgoal-literal sg))))
(define (search! sg)
(match (subgoal-literal sg)
[(struct literal (srcloc '= (list a b)))
(define (equal-test a b)
(when (term-equal? a b)
(fact! sg (make-literal srcloc '= (list a b)))))
(cond
[(unify-term (empty-env) a b)
=> (lambda (env) (equal-test (subst-term env a) (subst-term env b)))]
[else (equal-test a b)])]
[_
(search-theory! sg)]))
(define sg (make-subgoal lit empty empty))
(literal-tbl-replace! subgoals lit sg)
(search! sg)
(subgoal-facts sg))
(provide/contract
[safe-clause? (clause? . -> . boolean?)]
[theory/c contract?]
[immutable-theory/c contract?]
[mutable-theory/c contract?]
[make-mutable-theory (-> mutable-theory/c)]
[make-immutable-theory (-> immutable-theory/c)]
[assume (immutable-theory/c safe-clause? . -> . immutable-theory/c)]
[retract (immutable-theory/c clause? . -> . immutable-theory/c)]
[assume! (mutable-theory/c safe-clause? . -> . void)]
[retract! (mutable-theory/c clause? . -> . void)]
[prove (theory/c literal? . -> . (listof literal?))])

931
collects/datalog/scribblings/datalog.scrbl Normal file
View File

@ -0,0 +1,931 @@
#lang scribble/doc
@(require scribble/manual
scribble/eval
scribble/basic
scribble/bnf
(planet cce/scheme:6/planet)
(planet cce/scheme:6/scribble)
(for-label (planet dherman/pprint:4)
scheme/base
scheme/contract
"../main.ss")
"utils.ss")
@title[#:tag "top"]{@bold{Datalog} for PLT Scheme}
@author[(author+email "Jay McCarthy" "jay@plt-scheme.org")]
This package contains a lightweight deductive database system. Queries and database updates are expressed
using @link["http://en.wikipedia.org/wiki/Datalog"]{Datalog}---a declarative logic language in which each
formula is a function-free Horn clause, and every variable
in the head of a clause must appear in the body of the clause. The use of Datalog syntax and an implementation based
on tabling intermediate results ensures that all queries terminate.
@table-of-contents[]
@section{Datalog for PLT Scheme}
@subsection{Getting Started}
The easiest way to get started using Datalog for PLT Scheme is with the main module:
@defmodule/this-package[]
This module provides everything in the entire package. Subsequent sections of this
manual describe the functionality of the individual libraries included, which can also be
required individually.
@examples[#:eval the-eval
(define example-program
#<<END
ancestor(A, B) :-
parent(A, B).
ancestor(A, B) :-
parent(A, C),
D = C,
ancestor(D, B).
parent(john, douglas).
parent(bob, john).
parent(ebbon, bob).
ancestor(A, B)?
END
)
(require (planet dherman/pprint))
(pretty-print
(format-program
(parse-program
(open-input-string
example-program))))
(void
(eval-program/fresh
(parse-program
(open-input-string
example-program))))]
@subsection{Datalog Language for DrScheme}
Installing this PLaneT package also automatically registers a DrScheme language called @tt{Datalog},
filed under @tt{Experimental Languages}. Selecting the @tt{Datalog} language from DrScheme's
@tt{Language} menu allows you to create and load Datalog programs and interact with Datalog at
the REPL.
Datalog is also available as a module language. This can be used by beginning a Datalog source file with the line:
@(scheme #,(hash-lang) planet #,(this-package-version-symbol))
You can omit the PLaneT version numbers if you prefer. Programs without the version number
do not need to be updated when this PLaneT package is upgraded. However, it is then the
responsibility of the programmer to address any backwards-incompatible changes to the
Datalog semantics.
@section{Tutorial}
Start DrScheme and choose the @tt{Datalog} language from DrScheme's
@tt{Language} menu under @tt{Experimental Languages}. Click @onscreen{Run}, then
click in the REPL.
@schemeinput[]
@tech{Facts} are stored in tables. If the name of the table is @litchar["parent"], and
@litchar["john"] is the parent of @litchar["douglas"], store the fact in the database with
this:
@schemeinput[#,(tt "parent(john, douglas).")]
Each item in the parenthesized list following the name of the table is called a @tech{term}.
A term can be either a logical @scheme[variable] or a @scheme[constant].
Thus far, all the terms shown have been constant terms.
A query can be used to see if a particular row is in a table. Type this to see if @litchar["john"]
is the parent of @litchar["douglas"]:
@schemeinput[#,(tt "parent(john, douglas)?")]
@schemeblock[#,(schemeresultfont (tt "parent(john, douglas)."))]
Type this to see if @litchar["john"] is the parent of @litchar["ebbon"]:
@schemeinput[#,(tt "parent(john, ebbon)?")]
The query produced no results because @litchar["john"] is not the parent of @litchar["ebbon"]. Let's add more rows.
@schemeinput[#,(tt "parent(bob, john).")]
@schemeinput[#,(tt "parent(ebbon, bob).")]
Type the following to list all rows in the @litchar["parent"] table:
@schemeinput[#,(tt "parent(A, B)?")]
@schemeblock[#,(schemeresultfont (tt "parent(john, douglas)."))]
@schemeblock[#,(schemeresultfont (tt "parent(bob, john)."))]
@schemeblock[#,(schemeresultfont (tt "parent(ebbon, bob)."))]
Type the following to list all the children of @litchar["john"]:
@schemeinput[#,(tt "parent(john, B)?")]
@schemeblock[#,(schemeresultfont (tt "parent(john, douglas)."))]
A term that begins with a capital letter is a logical variable.When producing a set of answers, the
Datalog interpreter lists all rows that match the query when each variable in the query is substituted
for a constant. The following example produces no answers, as there are no substitutions for the variable
@litchar["A"] that produce a fact in the database. This is because no one is the parent of oneself.
@schemeinput[#,(tt "parent(A, A)?")]
A deductive database can use rules of inference to derive new facts. Consider the following rule:
@schemeinput[#,(tt "ancestor(A, B) :- parent(A, B).")]
The rule says that if A is the parent of B, then A is an ancestor of B.
The other rule defining an ancestor says that if A is the parent of C,
C is an ancestor of B, then A is an ancestor of B.
@schemeinput[#,(tt "ancestor(A, B) :-")
#,(tt " parent(A, C),")
#,(tt " ancestor(C, B).")]
In the interpreter, DrScheme knows that the clause is not complete, so by pressing Return, it doesn't interpret the line.
Rules are used to answer queries just as is done for facts.
@schemeinput[#,(tt "ancestor(A, B)?")]
@schemeblock[#,(schemeresultfont (tt "ancestor(ebbon, bob)."))]
@schemeblock[#,(schemeresultfont (tt "ancestor(bob, john)."))]
@schemeblock[#,(schemeresultfont (tt "ancestor(john, douglas)."))]
@schemeblock[#,(schemeresultfont (tt "ancestor(bob, douglas)."))]
@schemeblock[#,(schemeresultfont (tt "ancestor(ebbon, john)."))]
@schemeblock[#,(schemeresultfont (tt "ancestor(ebbon, douglas)."))]
@schemeinput[#,(tt "ancestor(X,john)?")]
@schemeblock[#,(schemeresultfont (tt "ancestor(bob, john)."))]
@schemeblock[#,(schemeresultfont (tt "ancestor(ebbon, john)."))]
A fact or a rule can be retracted from the database using tilde syntax:
@schemeinput[#,(tt "parent(bob, john)~")]
@schemeinput[#,(tt "parent(A, B)?")]
@schemeblock[#,(schemeresultfont (tt "parent(john, douglas)."))]
@schemeblock[#,(schemeresultfont (tt "parent(ebbon, bob)."))]
@schemeinput[#,(tt "ancestor(A, B)?")]
@schemeblock[#,(schemeresultfont (tt "ancestor(ebbon, bob)."))]
@schemeblock[#,(schemeresultfont (tt "ancestor(john, douglas)."))]
Unlike Prolog, the order in which clauses are asserted is irrelevant. All queries terminate, and every possible answer is derived.
@schemeinput[#,(tt "q(X) :- p(X).")]
@schemeinput[#,(tt "q(a).")]
@schemeinput[#,(tt "p(X) :- q(X).")]
@schemeinput[#,(tt "q(X)?")]
@schemeblock[#,(schemeresultfont (tt "q(a)."))]
@section{Abstract Syntax}
This library provides the structures that represent Datalog syntax. It can be required via:
@defmodule/this-package[ast]
@defthing[srcloc/c contract?]{
Contract for the third argument to @scheme[datum->syntax].
Equivalent to
@schemeblock[
(or/c syntax?
false/c
(list/c any/c
(or/c exact-positive-integer? #f)
(or/c exact-nonnegative-integer? #f)
(or/c exact-nonnegative-integer? #f)
(or/c exact-positive-integer? #f)))
]
}
@defthing[datum/c contract?]{
Contract for @deftech{datum}s.
Equivalent to @scheme[(or/c string? symbol?)].
}
@defproc[(datum-equal? [d1 datum/c] [d2 datum/c])
boolean?]{
Equivalent to @scheme[(equal? d1 d2)].
@examples[#:eval the-eval
(datum-equal? 'sym1 'sym2)
(datum-equal? 'sym1 'sym1)
(datum-equal? "str1" "str2")
(datum-equal? "str1" "str1")]
}
@defstruct[variable ([srcloc srcloc/c]
[sym symbol?])]{
A logic variable in Datalog.
(This structure does not enforce the requirements for what characters variables can contain, so if you print one out,
it might not be parseable, but it will be executeable.)
}
@defproc[(variable-equal? [v1 variable?] [v2 variable?])
boolean?]{
Equivalent to @scheme[(equal? v1 v2)] modulo source location.
@examples[#:eval the-eval
(variable-equal? (make-variable #f 'sym)
(make-variable #'sym 'sym))
(variable-equal? (make-variable #f 'sym1)
(make-variable #f 'sym2))]
}
@defstruct[constant ([srcloc srcloc/c]
[datum datum/c])]{
A constant in Datalog.
(This structure does not enforce the requirements for what characters constants can contain, so if you print one out,
it might not be parseable, but it will be executeable.)
}
@defproc[(constant-equal? [c1 constant?] [c2 constant?])
boolean?]{
Equivalent to @scheme[(equal? c1 c2)] modulo source location.
@examples[#:eval the-eval
(constant-equal? (make-constant #f 'sym)
(make-constant #'sym 'sym))
(constant-equal? (make-constant #f 'sym)
(make-constant #f "str"))]
}
@defthing[term/c contract?]{
Contract for @deftech{term}s. Equivalent to @scheme[(or/c variable? constant?)].
}
@defproc[(term-equal? [t1 term/c] [t2 term/c])
boolean?]{
Equivalent to @scheme[(equal? t1 t2)] modulo source location.
@examples[#:eval the-eval
(term-equal? (make-constant #f 'sym) (make-constant #'sym 'sym))
(term-equal? (make-constant #f 'sym) (make-constant #f "str"))]
}
@defstruct[literal ([srcloc srcloc/c]
[predicate datum/c]
[terms (listof term/c)])]{
A literal in Datalog.
}
@defproc[(literal-equal? [l1 literal?] [l2 literal?])
boolean?]{
Equivalent to @scheme[(equal? l1 l2)] modulo source location.
@examples[#:eval the-eval
(literal-equal? (make-literal #f 'ancestor (list))
(make-literal #'ancestor 'ancestor (list)))
(literal-equal? (make-literal #f 'ancestor (list))
(make-literal #f 'parent (list)))
(literal-equal? (make-literal #f 'ancestor (list))
(make-literal #f 'ancestor
(list (make-constant #f 'jack))))]
}
@defstruct[clause ([srcloc srcloc/c]
[head literal?]
[body (listof literal?)])]{
A Datalog clause.
}
@defproc[(clause-equal? [c1 clause?] [c2 clause?])
boolean?]{
Equivalent to @scheme[(equal? c1 c2)] modulo source location.
@examples[#:eval the-eval
(clause-equal?
(make-clause #f (make-literal #f 'ancestor (list)) (list))
(make-clause #'clause
(make-literal #f 'ancestor (list)) (list)))
(clause-equal?
(make-clause #f (make-literal #f 'ancestor (list)) (list))
(make-clause #f (make-literal #f 'parent (list)) (list)))]
}
@defstruct[assertion ([srcloc srcloc/c]
[clause clause?])]{
A Datalog assertion.
}
@defstruct[retraction ([srcloc srcloc/c]
[clause clause?])]{
A Datalog retraction.
}
@defstruct[query ([srcloc srcloc/c]
[clause clause?])]{
A Datalog query.
}
@defthing[statement/c contract?]{
Contract for @deftech{statement}s.
Equivalent to @scheme[(or/c assertion? retraction? query?)].
}
@defthing[program/c contract?]{
Contract for @deftech{program}s.
Equivalent to @scheme[(listof statement/c)].
}
@section{Lexing and Parsing}
This library provides facilities for parsing Datalog source. It can be required via:
@defmodule/this-package[parse]
@subsection{Datalog Syntax}
In Datalog input, whitespace characters are ignored except when they separate adjacent tokens or when they occur in strings.
Comments are also considered to be whitespace. The character @litchar["%"] introduces a comment, which extends to the next line break.
Comments do not occur inside strings.
A variable is a sequence of Latin capital and small letters, digits, and the underscore character. A variable must begin with a Latin capital letter.
An identifier is a sequence of printing characters that does not contain any of the following characters: @litchar["("], @litchar["`"],
@litchar["'"], @litchar[")"], @litchar["="], @litchar[":"], @litchar["."], @litchar["~"], @litchar["?"], @litchar["\""], @litchar["%"], and space.
An identifier must not begin with a Latin capital letter. Note that the characters that start punctuation are forbidden in identifiers,
but the hyphen character is allowed.
A string is a sequence of characters enclosed in double quotes. Characters other than double quote, newline, and backslash may be directly
included in a string. The remaining characters may be specified using escape characters, @litchar["\\\""], @litchar["\\\n"], and
@litchar["\\\\"] respectively.
A literal, is a predicate symbol followed by an optional parenthesized list of comma separated terms. A predicate symbol is either an identifier
or a string. A term is either a variable or a constant. As with predicate symbols, a constant is either an identifier or a string. As a special case,
two terms separated by @litchar["="] is a literal for the equality predicate.
The following are literals:
@verbatim[#:indent 4 #<<END
parent(john, douglas)
zero-arity-literal
"="(3,3)
""(-0-0-0,&&&,***,"\00")
END
]
A clause is a head literal followed by an optional body. A body is a comma separated list of literals. A clause without a body is called a @deftech{fact},
and a rule when it has one. The punctuation @litchar[":-"] separates the head of a rule from its body. A clause is safe if every variable in its head
occurs in some literal in its body. The following are safe clauses:
@verbatim[#:indent 4 #<<END
parent(john, douglas)
ancestor(A, B) :-
parent(A, B)
ancestor(A, B) :-
parent(A, C),
ancestor(C, B)
END
]
A program is a sequence of zero or more statements. A statement is an assertion, a retraction, or a query. An assertion is a clause followed by
a period, and it adds the clause to the database if it is safe. A retraction is a clause followed by a tilde, and it removes the clause from
the database. A query is a literal followed by a question mark. The effect of reading a Datalog program is to modify the database as directed
by its statements, and then to return the literal designated as the query. If no query is specified, a reader returns a literal know to have no
answers. The following is a program:
@verbatim[#:indent 4 #<<END
edge(a, b). edge(b, c). edge(c, d). edge(d, a).
path(X, Y) :- edge(X, Y).
path(X, Y) :- edge(X, Z), path(Z, Y).
path(X, Y)?
END
]
The following BNF describes the syntax of Datalog.
@BNF[
(list (nonterm "program")
(kleenestar (nonterm "statement")))
(list (nonterm "statement")
(nonterm "assertion")
(nonterm "retraction")
(nonterm "query"))
(list (nonterm "assertion")
(BNF-seq (nonterm "clause") (litchar ".")))
(list (nonterm "retraction")
(BNF-seq (nonterm "clause") (litchar "~")))
(list (nonterm "query")
(BNF-seq (nonterm "literal") (litchar "?")))
(list (nonterm "clause")
(BNF-seq (nonterm "literal") (litchar ":-") (nonterm "body"))
(nonterm "literal"))
(list (nonterm "body")
(BNF-seq (nonterm "literal") (litchar ",") (nonterm "body"))
(nonterm "literal"))
(list (nonterm "literal")
(BNF-seq (nonterm "predicate-sym") (litchar "(") (litchar ")"))
(BNF-seq (nonterm "predicate-sym") (litchar "(") (nonterm "terms") (litchar ")"))
(nonterm "predicate-sym")
(BNF-seq (nonterm "term") (litchar "=") (nonterm "term")))
(list (nonterm "predicate-sym")
(nonterm "IDENTIFIER")
(nonterm "STRING"))
(list (nonterm "terms")
(nonterm "term")
(BNF-seq (nonterm "term") (litchar ",") (nonterm "terms")))
(list (nonterm "term")
(nonterm "VARIABLE")
(nonterm "constant"))
(list (nonterm "constant")
(nonterm "IDENTIFIER")
(nonterm "STRING"))
]
@subsection{Parser API}
@defproc[(parse-literal [ip input-port?])
literal?]{
Parses a @scheme[literal] from @scheme[ip].
@examples[#:eval the-eval
(parse-literal (open-input-string "parent(john,douglas)"))
(parse-literal (open-input-string "zero-arity-literal"))
(parse-literal (open-input-string "\"=\"(3,3)"))
(parse-literal
(open-input-string "\"\"(-0-0-0,&&&,***,\"\00\")"))
(parse-literal (open-input-string "3 = 3"))]
}
@defproc[(parse-clause [ip input-port?])
clause?]{
Parses a @scheme[clause] from @scheme[ip].
@examples[#:eval the-eval
(parse-clause
(open-input-string "parent(john, douglas)"))
(parse-clause
(open-input-string "ancestor(A, B) :- parent(A, B)"))
(parse-clause
(open-input-string
(string-append "ancestor(A, B) :- parent(A, C),"
"ancestor(C, B)")))]
}
@defproc[(parse-statement [ip input-port?])
statement/c]{
Parses a @tech{statement} from @scheme[ip].
@examples[#:eval the-eval
(parse-statement
(open-input-string "parent(john, douglas)."))
(parse-statement
(open-input-string "parent(john, douglas)~"))
(parse-statement
(open-input-string "parent(john, douglas)?"))]
}
@defproc[(parse-program [ip input-port?])
program/c]{
Parses a @tech{program} from @scheme[ip].
@examples[#:eval the-eval
(parse-program
(open-input-string
(string-append
"edge(a, b). edge(b, c)."
"edge(c, d). edge(d, a)."
"path(X, Y) :- edge(X, Y)."
"path(X, Y) :- edge(X, Z), path(Z, Y)."
"path(X, Y)?")))]
}
@section{Parenthetical Datalog}
This package recognizes an alternative, Scheme-like front-end syntax for Datalog. It can be required via:
@defmodule/this-package[sexp]
@subsection{Parenthetical Datalog Syntax}
@schemegrammar*[
#:literals (:- ! ~ ?)
[program (begin statement ...)]
[statement assertion
retraction
query]
[assertion (! clause)]
[retraction (~ clause)]
[query (? literal)]
[clause (:- literal literal ...)
literal]
[literal (datum term ...)]
[term variable
constant]
[variable ,symbol]
[constant datum]
[datum symbol
string]]
@subsection{Parethetical Parser API}
@defproc[(stx->term [stx syntax?])
term/c]{
Parses @scheme[stx] as a @tech{term}.
}
@defproc[(stx->literal [stx syntax?])
literal?]{
Parses @scheme[stx] as a @scheme[literal].
}
@defproc[(stx->clause [stx syntax?])
clause?]{
Parses @scheme[stx] as a @scheme[clause].
}
@defproc[(stx->statement [stx syntax?])
statement/c]{
Parses @scheme[stx] as a @tech{statement}.
}
@defproc[(stx->program [stx syntax?])
program/c]{
Parses @scheme[stx] as a @tech{program}.
}
@defproc[(sexp->term [sexp sexpr?]) term/c]{@scheme[stx->term] composed with @scheme[datum->syntax].}
@defproc[(sexp->literal [sexp sexpr?]) literal?]{@scheme[stx->literal] composed with @scheme[datum->syntax].}
@defproc[(sexp->clause [sexp sexpr?]) clause?]{@scheme[stx->clause] composed with @scheme[datum->syntax].}
@defproc[(sexp->statement [sexp sexpr?]) statement/c]{@scheme[stx->statement] composed with @scheme[datum->syntax].}
@defproc[(sexp->program [sexp sexpr?]) program/c]{@scheme[stx->program] composed with @scheme[datum->syntax].}
@section{Pretty-Printing}
This library provides facilities for pretty-printing Datalog source. It can be required via:
@defmodule/this-package[pretty]
This library depends on the @tt{pprint} PLaneT package, which can be required via:
@schemeblock[(require (planet dherman/pprint:4))]
See the documentation for @tt{pprint} for information on how to use it.
@defproc[(format-datum [d datum/c])
doc?]{
Formats a @tech{datum}.
@examples[#:eval the-eval
(pretty-print (format-datum 'sym))
(pretty-print (format-datum "str"))]
}
@defproc[(format-variable [v variable?])
doc?]{
Formats a @scheme[variable].
@examples[#:eval the-eval
(pretty-print (format-variable (make-variable #f 'Ancestor)))]
}
@defproc[(format-constant [c constant?])
doc?]{
Formats a @scheme[constant].
@examples[#:eval the-eval
(pretty-print (format-constant (make-constant #f 'joseph)))
(pretty-print (format-constant (make-constant #f "whom")))]
}
@defproc[(format-term [t term/c])
doc?]{
Formats a @tech{term}.
@examples[#:eval the-eval
(pretty-print (format-term (make-variable #f 'Ancestor)))
(pretty-print (format-term (make-constant #f 'joseph)))
(pretty-print (format-term (make-constant #f "whom")))]
}
@defproc[(format-literal [l literal?])
doc?]{
Formats a @scheme[literal].
@examples[#:eval the-eval
(pretty-print (format-literal (make-literal #f 'true (list))))
(pretty-print
(format-literal
(make-literal #f 'ancestor
(list (make-variable #f 'A) (make-constant #f 'jay)))))
(pretty-print
(format-literal
(make-literal #f '=
(list (make-constant #f 'joseph) (make-constant #f 'jay)))))]
}
@defproc[(format-literals [ls (listof literal?)])
doc?]{
Formats a list of @scheme[literal]s as @scheme[assertion]s for formatting @scheme[prove] results.
@examples[#:eval the-eval
(pretty-print
(format-literals
(list
(make-literal #f 'true (list))
(make-literal #f 'ancestor
(list (make-constant #f 'joseph) (make-constant #f 'jay)))
(make-literal #f '=
(list (make-constant #f 'joseph) (make-constant #f 'jay))))))]
}
@defproc[(format-clause [c clause?])
doc?]{
Formats a @scheme[clause].
@examples[#:eval the-eval
(pretty-print
(format-clause
(make-clause
#f (make-literal #f 'ancestor
(list (make-constant #f 'joseph)
(make-constant #f 'jay)))
(list))))
(pretty-print
(format-clause
(make-clause
#f (make-literal
#f 'ancestor
(list (make-constant #f 'A) (make-constant #f 'B)))
(list (make-literal
#f 'parent
(list (make-constant #f 'A) (make-constant #f 'B)))))))
(pretty-print
(format-clause
(make-clause
#f (make-literal
#f 'ancestor
(list (make-constant #f 'A) (make-constant #f 'B)))
(list (make-literal
#f 'parent
(list (make-constant #f 'A) (make-constant #f 'C)))
(make-literal
#f 'ancestor
(list (make-constant #f 'C) (make-constant #f 'B)))))))]
}
@defproc[(format-assertion [a assertion?])
doc?]{
Formats a @scheme[assertion].
@examples[#:eval the-eval
(pretty-print
(format-assertion
(make-assertion
#f (make-clause
#f (make-literal #f 'ancestor
(list (make-constant #f 'joseph)
(make-constant #f 'jay)))
(list)))))]
}
@defproc[(format-retraction [r retraction?])
doc?]{
Formats a @scheme[retraction].
@examples[#:eval the-eval
(pretty-print
(format-retraction
(make-retraction
#f (make-clause
#f (make-literal #f 'ancestor
(list (make-constant #f 'joseph)
(make-constant #f 'jay)))
(list)))))]
}
@defproc[(format-query [q query?])
doc?]{
Formats a @scheme[query].
@examples[#:eval the-eval
(pretty-print
(format-query
(make-query
#f (make-literal #f 'ancestor
(list (make-constant #f 'joseph)
(make-constant #f 'jay))))))]
}
@defproc[(format-statement [s statement/c])
doc?]{
Formats a @tech{statement}.
@examples[#:eval the-eval
(pretty-print
(format-statement
(make-query
#f (make-literal #f 'ancestor
(list (make-constant #f 'joseph)
(make-constant #f 'jay))))))]
}
@defproc[(format-program [p program/c])
doc?]{
Formats a @tech{program}.
@examples[#:eval the-eval
(pretty-print
(format-program
(list
(make-assertion
#f (make-clause
#f (make-literal #f 'ancestor
(list (make-constant #f 'joseph)
(make-constant #f 'jay)))
(list)))
(make-query
#f (make-literal #f 'ancestor
(list (make-constant #f 'joseph)
(make-constant #f 'jay)))))))]
}
@section{Runtime System}
This library implements the Datalog runtime system. It can be required via:
@defmodule/this-package[runtime]
@defthing[theory/c contract?]{
A contract for @deftech{theories}.
}
@defthing[immutable-theory/c contract?]{
A contract for immutable @tech{theories}.
}
@defthing[mutable-theory/c contract?]{
A contract for mutable @tech{theories}.
}
@defproc[(make-mutable-theory)
mutable-theory/c]{
Constructs a mutable @tech{theory}.
}
@defproc[(make-immutable-theory)
immutable-theory/c]{
Constructs a immutable @tech{theory}.
}
@defproc[(safe-clause? [c clause?])
boolean?]{
Determines if a @scheme[clause] is safe.
A @scheme[clause] is safe if every @scheme[variable] in its head occurs in some @scheme[literal] in its body.
@examples[#:eval the-eval
(safe-clause?
(parse-clause (open-input-string "ancestor(joseph,jay)")))
(safe-clause?
(parse-clause
(open-input-string "ancestor(A,B) :- parent(A,B)")))
(safe-clause?
(parse-clause
(open-input-string "ancestor(A,B) :- parent(A,jay)")))]
}
@defproc[(assume [thy immutable-theory/c]
[c safe-clause?])
immutable-theory/c]{
Adds @scheme[c] to @scheme[thy] in a persistent way.
}
@defproc[(retract [thy immutable-theory/c]
[c clause?])
immutable-theory/c]{
Removes @scheme[c] from @scheme[thy] in a persistent way.
}
@defproc[(assume! [thy mutable-theory/c]
[c safe-clause?])
mutable-theory/c]{
Adds @scheme[c] to @scheme[thy].
}
@defproc[(retract! [thy mutable-theory/c]
[c clause?])
mutable-theory/c]{
Removes @scheme[c] from @scheme[thy].
}
@defproc[(prove [thy theory/c]
[l literal?])
(listof literal?)]{
Attempts to prove @scheme[l] using the @tech{theory} @scheme[thy], returning all
the results of the query.
@examples[#:eval the-eval
(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)")))))
(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)")))))]
}
@section{Evaluation}
This library provides facilities for evaluating Datalog. It can be required via:
@defmodule/this-package[eval]
@defthing[current-theory (parameter/c mutable-theory/c)]{
The @tech{theory} used by @scheme[eval-program] and @scheme[eval-stmt].
}
@defproc[(eval-program [p program/c])
void]{
Evaluates @scheme[p] using @scheme[(current-theory)] as the @tech{theory}, printing query answers as it goes.
This will raise a syntax error if given an @scheme[assertion] of a @scheme[clause] that is not a @scheme[safe-clause?].
@examples[#:eval the-eval
(parameterize ([current-theory (make-mutable-theory)])
(eval-program
(parse-program
(open-input-string
(string-append
"edge(a, b). edge(b, c). edge(c, d). edge(d, a)."
"path(X, Y) :- edge(X, Y)."
"path(X, Y) :- edge(X, Z), path(Z, Y)."
"path(X, Y)?")))))
(eval-program
(parse-program
(open-input-string
"path(X, Y) :- edge(X, a).")))]
}
@defproc[(eval-statement [s statement/c])
(or/c void (listof literal?))]{
Evaluates @scheme[s] using @scheme[(current-theory)] as the @tech{theory}.
This will raise a syntax error if given an @scheme[assertion] of a @scheme[clause] that is not a @scheme[safe-clause?].
@examples[#:eval the-eval
(parameterize ([current-theory (make-mutable-theory)])
(eval-statement
(parse-statement
(open-input-string
"edge(a, b).")))
(eval-statement
(parse-statement
(open-input-string
"path(X, Y) :- edge(X, Y).")))
(eval-statement
(parse-statement
(open-input-string
"path(X, Y)?"))))
(eval-statement
(parse-statement
(open-input-string
"path(X, Y) :- edge(X, a).")))]
}
@defproc[(eval-program/fresh [p program/c])
immutable-theory/c]{
Evaluates @scheme[p] in a fresh @tech{theory} and returns the final @tech{theory}, printing query answers as it goes.
This will raise a syntax error if given an @scheme[assertion] of a @scheme[clause] that is not a @scheme[safe-clause?].
@examples[#:eval the-eval
(void
(eval-program/fresh
(parse-program
(open-input-string
(string-append
"edge(a, b). edge(b, c). edge(c, d). edge(d, a)."
"path(X, Y) :- edge(X, Y)."
"path(X, Y) :- edge(X, Z), path(Z, Y)."
"path(X, Y)?")))))
(eval-program/fresh
(parse-program
(open-input-string
"path(X, Y) :- edge(X, a).")))]
}
@index-section[]
@section{Acknowledgments}
This package is based on Dave Herman's @schememodname[(planet dherman/javascript)] library and
John Ramsdell's @link["http://www.ccs.neu.edu/home/ramsdell/tools/datalog/datalog.html"]{Datalog library}.
The package uses the tabled logic programming algorithm described in
@link["http://scholar.google.com/scholar?q=author:%22Chen%22+intitle:%22Efficient+top-down+computation+of+queries+under+the+...%22+&oi=scholarr"]{Efficient Top-Down Computation of Queries under the Well-Founded Semantics} by W. Chen, T. Swift, and D. S. Warren.
Another important reference is
@link["http://portal.acm.org/citation.cfm?id=227597"]{Tabled Evaluation with Delaying for General Logic Programs} by W. Chen and D. S. Warren.
Datalog is described in
@link["http://doi.ieeecomputersociety.org/10.1109/69.43410"]{What You Always Wanted to Know About Datalog (And Never Dared to Ask)}
by Stefano Ceri, Georg Gottlob, and Letizia Tanca.

11
collects/datalog/scribblings/utils.rkt Normal file
View File

@ -0,0 +1,11 @@
#lang scheme/base
(require scribble/eval
(planet cce/scheme:6/planet))
(provide the-eval)
(define the-eval
(let ([the-eval (make-base-eval)])
(the-eval `(require (planet ,(this-package-version-symbol))))
the-eval))

BIN
collects/datalog/tool/datalog.png Normal file
View File

Binary file not shown.
Side by Side

After

Width:  |  Height:  |  Size: 2.1 KiB

36
collects/datalog/tool/syntax-color.rkt Normal file
View File

@ -0,0 +1,36 @@
#lang scheme
(require parser-tools/lex
(prefix-in : parser-tools/lex-sre)
"../private/lex.ss")
(provide get-syntax-token)
(define (syn-val lex a b c d)
(values lex a b (position-offset c) (position-offset d)))
(define (colorize-string my-start-pos)
(define lxr
(lexer
[(:~ #\" #\\) (lxr input-port)]
[(:: #\\ #\\) (lxr input-port)]
[(:: #\\ #\newline) (lxr input-port)]
[(:: #\\ #\") (lxr input-port)]
[(eof) (syn-val "" 'error #f my-start-pos end-pos)]
[#\" (syn-val "" 'string #f my-start-pos end-pos)]))
lxr)
(define get-syntax-token
(lexer
[(:+ whitespace)
(syn-val lexeme 'whitespace #f start-pos end-pos)]
[comment-re
(syn-val lexeme 'comment #f start-pos end-pos)]
[variable-re
(syn-val lexeme 'identifier #f start-pos end-pos)]
[identifier-re
(syn-val lexeme 'keyword #f start-pos end-pos)]
[(:or #\) #\() (syn-val lexeme 'parenthesis #f start-pos end-pos)]
[(:or #\= #\? #\~ #\. #\, ":-") (syn-val lexeme 'default #f start-pos end-pos)]
[(eof) (syn-val lexeme 'eof #f start-pos end-pos)]
[#\" ((colorize-string start-pos) input-port)]
[any-char (syn-val lexeme 'error #f start-pos end-pos)]))

0
collects/plai/collector/lang/reader.ss → collects/plai/collector/lang/reader.rkt
View File