diff --git a/collects/datalog/ast.rkt b/collects/datalog/ast.rkt
new file mode 100644
index 0000000..9e51487
--- /dev/null
+++ b/collects/datalog/ast.rkt
@@ -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?])
diff --git a/collects/datalog/eval.rkt b/collects/datalog/eval.rkt
new file mode 100644
index 0000000..2e10fdc
--- /dev/null
+++ b/collects/datalog/eval.rkt
@@ -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)])
\ No newline at end of file
diff --git a/collects/datalog/info.rkt b/collects/datalog/info.rkt
new file mode 100644
index 0000000..e9f35bd
--- /dev/null
+++ b/collects/datalog/info.rkt
@@ -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"))
diff --git a/collects/datalog/lang/reader.rkt b/collects/datalog/lang/reader.rkt
new file mode 100644
index 0000000..4155f05
--- /dev/null
+++ b/collects/datalog/lang/reader.rkt
@@ -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"))
\ No newline at end of file
diff --git a/collects/datalog/main.rkt b/collects/datalog/main.rkt
new file mode 100644
index 0000000..0bf1fc0
--- /dev/null
+++ b/collects/datalog/main.rkt
@@ -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"))
\ No newline at end of file
diff --git a/collects/datalog/parse.rkt b/collects/datalog/parse.rkt
new file mode 100644
index 0000000..caa20d0
--- /dev/null
+++ b/collects/datalog/parse.rkt
@@ -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)])
\ No newline at end of file
diff --git a/collects/datalog/pretty.rkt b/collects/datalog/pretty.rkt
new file mode 100644
index 0000000..167d972
--- /dev/null
+++ b/collects/datalog/pretty.rkt
@@ -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?)])
\ No newline at end of file
diff --git a/collects/datalog/private/compiler.rkt b/collects/datalog/private/compiler.rkt
new file mode 100644
index 0000000..79e9209
--- /dev/null
+++ b/collects/datalog/private/compiler.rkt
@@ -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?)])
\ No newline at end of file
diff --git a/collects/datalog/private/env.rkt b/collects/datalog/private/env.rkt
new file mode 100644
index 0000000..625c93d
--- /dev/null
+++ b/collects/datalog/private/env.rkt
@@ -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)])
\ No newline at end of file
diff --git a/collects/datalog/private/lex.rkt b/collects/datalog/private/lex.rkt
new file mode 100644
index 0000000..59d61fa
--- /dev/null
+++ b/collects/datalog/private/lex.rkt
@@ -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)
\ No newline at end of file
diff --git a/collects/datalog/private/subst.rkt b/collects/datalog/private/subst.rkt
new file mode 100644
index 0000000..b5fade6
--- /dev/null
+++ b/collects/datalog/private/subst.rkt
@@ -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?)])
\ No newline at end of file
diff --git a/collects/datalog/private/unify.rkt b/collects/datalog/private/unify.rkt
new file mode 100644
index 0000000..354f9be
--- /dev/null
+++ b/collects/datalog/private/unify.rkt
@@ -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))])
\ No newline at end of file
diff --git a/collects/datalog/private/variant.rkt b/collects/datalog/private/variant.rkt
new file mode 100644
index 0000000..4499654
--- /dev/null
+++ b/collects/datalog/private/variant.rkt
@@ -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?)])
\ No newline at end of file
diff --git a/collects/datalog/runtime.rkt b/collects/datalog/runtime.rkt
new file mode 100644
index 0000000..0cca202
--- /dev/null
+++ b/collects/datalog/runtime.rkt
@@ -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?))])
\ No newline at end of file
diff --git a/collects/datalog/scribblings/datalog.scrbl b/collects/datalog/scribblings/datalog.scrbl
new file mode 100644
index 0000000..0d10689
--- /dev/null
+++ b/collects/datalog/scribblings/datalog.scrbl
@@ -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.
\ No newline at end of file
diff --git a/collects/datalog/scribblings/utils.rkt b/collects/datalog/scribblings/utils.rkt
new file mode 100644
index 0000000..f4c281c
--- /dev/null
+++ b/collects/datalog/scribblings/utils.rkt
@@ -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))
diff --git a/collects/datalog/tool/datalog.png b/collects/datalog/tool/datalog.png
new file mode 100644
index 0000000..6f55fb1
Binary files /dev/null and b/collects/datalog/tool/datalog.png differ
diff --git a/collects/datalog/tool/syntax-color.rkt b/collects/datalog/tool/syntax-color.rkt
new file mode 100644
index 0000000..c81e3e4
--- /dev/null
+++ b/collects/datalog/tool/syntax-color.rkt
@@ -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)]))
\ No newline at end of file
diff --git a/collects/plai/collector/lang/reader.ss b/collects/plai/collector/lang/reader.rkt
similarity index 100%
rename from collects/plai/collector/lang/reader.ss
rename to collects/plai/collector/lang/reader.rkt