diff --git a/collects/datalog/ast.rkt b/collects/datalog/ast.rkt
new file mode 100644
index 0000000..4105270
--- /dev/null
+++ b/collects/datalog/ast.rkt
@@ -0,0 +1,110 @@
+#lang racket
+
+(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 value) #:prefab)
+(define (constant-equal? v1 v2)
+  (equal? (constant-value v1) (constant-value 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 (terms-equal? t1 t2)
+  (and (= (length t1)
+          (length t2))
+       (andmap term-equal? t1 t2)))
+
+(define-struct literal (srcloc predicate terms) #:prefab)
+(define (literal-equal? l1 l2)
+  (and (datum-equal? (literal-predicate l1)
+                     (literal-predicate l2))
+       (terms-equal? (literal-terms l1) (literal-terms l2))))
+
+(define-struct external (srcloc predicate-sym predicate arg-terms ans-terms) #:prefab)
+(define (external-equal? e1 e2)
+  (match-define (external _1 _s1 p1 ar1 an1) e1)
+  (match-define (external _2 _s2 p2 ar2 an2) e2)
+  (and (equal? p1 p2)
+       (terms-equal? ar1 ar2)
+       (terms-equal? an1 an2)))
+
+(define question/c (or/c literal? external?))
+(define (question-equal? q1 q2)
+  (or (and (literal? q1) (literal? q2)
+           (literal-equal? q1 q2))
+      (and (external? q1) (external? q2)
+           (external-equal? q1 q2))))
+
+(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 question-equal?
+               (clause-body c1)
+               (clause-body c2))))
+
+(define-struct assertion (srcloc clause) #:prefab)
+(define-struct retraction (srcloc clause) #:prefab)
+(define-struct query (srcloc question) #: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]
+                   [value any/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 external ([srcloc srcloc/c]
+                   [predicate-sym symbol?]
+                   [predicate procedure?]
+                   [arg-terms (listof term/c)]
+                   [ans-terms (listof term/c)])]
+ [external-equal? (external? external? . -> . boolean?)]
+ [question/c contract?]
+ [question-equal? (question/c question/c . -> . boolean?)]
+ [struct clause ([srcloc srcloc/c]
+                 [head literal?]
+                 [body (listof question/c)])]
+ [clause-equal? (clause? clause? . -> . boolean?)]
+ [struct assertion ([srcloc srcloc/c]
+                    [clause clause?])]
+ [struct retraction ([srcloc srcloc/c]
+                     [clause clause?])]
+ [struct query ([srcloc srcloc/c]
+                [question question/c])]
+ [statement/c contract?]
+ [program/c contract?])
diff --git a/collects/datalog/eval.rkt b/collects/datalog/eval.rkt
new file mode 100644
index 0000000..2bea9d0
--- /dev/null
+++ b/collects/datalog/eval.rkt
@@ -0,0 +1,43 @@
+#lang racket
+(require racket/list
+         "ast.rkt"
+         "pretty.rkt"
+         "runtime.rkt")
+
+(define current-theory (make-parameter (make-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 (format-statement s) (assertion-srcloc s))))))
+
+(define (print-questions ls)
+  (displayln 
+   (format-questions ls)))
+
+(define (eval-program p)
+  (for-each eval-top-level-statement p))
+
+(define (eval-top-level-statement s)
+  (define v (eval-statement s))
+  (unless (void? v)
+    (print-questions v)))
+
+(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-question s))]))
+
+(provide/contract
+ [current-theory (parameter/c theory/c)]
+ [print-questions ((listof question/c) . -> . void)]
+ [eval-program (program/c . -> . void)]
+ [eval-top-level-statement (statement/c . -> . void)]
+ [eval-statement (statement/c . -> . (or/c void (listof question/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..aed5db6
--- /dev/null
+++ b/collects/datalog/info.rkt
@@ -0,0 +1,3 @@
+#lang setup/infotab
+(define scribblings '(["scribblings/datalog.scrbl" (multi-page) (language)]))
+(define compile-omit-paths '("tests"))
\ No newline at end of file
diff --git a/collects/datalog/lang/reader.rkt b/collects/datalog/lang/reader.rkt
new file mode 100644
index 0000000..43f2068
--- /dev/null
+++ b/collects/datalog/lang/reader.rkt
@@ -0,0 +1,33 @@
+(module reader syntax/module-reader
+  #:language 'datalog/sexp/lang
+  #:read (lambda ([in (current-input-port)]) (this-read-syntax #f in))
+  #:read-syntax this-read-syntax
+  #:whole-body-readers? #t  
+  #:info (lambda (key defval default)
+           ; XXX Should have different comment character key
+           (case key
+             [(drracket:submit-predicate)
+              (dynamic-require 'datalog/tool/submit 'repl-submit?)]
+             [(color-lexer)
+              (dynamic-require 'datalog/tool/syntax-color 'get-syntax-token)]
+             [(configure-runtime)
+              (λ () (current-read-interaction even-read))]
+             [else (default key defval)]))
+  (require datalog/parse
+           datalog/private/compiler)
+  
+  (define (this-read-syntax [src #f] [in (current-input-port)])
+    (compile-program
+     (parameterize ([current-source-name src])
+       (parse-program in))))
+  
+  ; XXX This is almost certainly wrong.
+  (define (even-read src ip)
+    (begin0
+      (compile-statement
+       (parameterize ([current-source-name src])
+         (parse-statement ip)))
+      (current-read-interaction odd-read)))
+  (define (odd-read src ip)
+    (current-read-interaction even-read)
+    eof))
\ No newline at end of file
diff --git a/collects/datalog/main.rkt b/collects/datalog/main.rkt
new file mode 100644
index 0000000..4aad39a
--- /dev/null
+++ b/collects/datalog/main.rkt
@@ -0,0 +1,6 @@
+#lang racket
+(require "runtime.rkt"
+         "stx.rkt")
+(provide make-theory
+         theory/c
+         (all-from-out "stx.rkt"))
\ No newline at end of file
diff --git a/collects/datalog/parse.rkt b/collects/datalog/parse.rkt
new file mode 100644
index 0000000..83e5249
--- /dev/null
+++ b/collects/datalog/parse.rkt
@@ -0,0 +1,81 @@
+#lang racket
+(require parser-tools/lex
+         parser-tools/yacc
+         "private/lex.rkt"
+         "ast.rkt")
+
+(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
+ [current-source-name (parameter/c any/c)]
+ [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..39f92f6
--- /dev/null
+++ b/collects/datalog/pretty.rkt
@@ -0,0 +1,92 @@
+#lang racket
+(require "private/pprint.rkt"
+         "ast.rkt")
+
+(define (format-datum s)
+  (cond
+    [(symbol? s)
+     (text (symbol->string s))]
+    [else
+     (text (format "~S" s))]))
+(define (format-variable v)
+  (format-datum (variable-sym v)))
+(define (format-constant c)
+  (format-datum (constant-value c)))
+(define format-term 
+  (match-lambda
+    [(? 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 ", " (map format-term terms)))
+               rparen)]))
+(define format-external
+  (match-lambda
+    [(external _ pred-sym pred args anss)
+     (h-append (format-datum pred-sym)
+               lparen
+               (v-concat/s (apply-infix ", " (map format-term args)))
+               rparen
+               (text " = ")
+               lparen
+               (v-concat/s (apply-infix ", " (map format-term anss)))
+               rparen)]))
+(define format-question
+  (match-lambda
+    [(? literal? l)
+     (format-literal l)]
+    [(? external? e)
+     (format-external e)]))
+(define (format-questions ls)
+  (v-concat
+   (append (map (lambda (l)
+                  (h-append (format-question l) dot))
+                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 ":-") space)
+                    (apply-infix ", " (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-question (query-question 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-questions ((listof question/c) . -> . 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..2b96bc1
--- /dev/null
+++ b/collects/datalog/private/compiler.rkt
@@ -0,0 +1,56 @@
+#lang racket/base
+(require racket/contract
+         racket/match
+         datalog/ast
+         datalog/stx)
+(require (for-template datalog/stx))
+
+(provide/contract
+ [compile-program (program/c . -> . (listof syntax?))]
+ [compile-statement (statement/c . -> . syntax?)])
+
+(define (compile-program p)
+  (map compile-statement p))
+
+(define compile-statement
+  (match-lambda
+    [(assertion srcloc c)
+     (define srcstx (datum->syntax #f 'x srcloc))
+     (quasisyntax/loc srcstx
+       (! #,(compile-clause c)))]
+    [(retraction srcloc c)
+     (define srcstx (datum->syntax #f 'x srcloc))
+     (quasisyntax/loc srcstx
+       (~ #,(compile-clause c)))]
+    [(query srcloc l)
+     (define srcstx (datum->syntax #f 'x srcloc))
+     (quasisyntax/loc srcstx
+       (? #,(compile-literal l)))]))
+
+(define compile-clause
+  (match-lambda
+    [(clause srcloc head (list))
+     (define srcstx (datum->syntax #f 'x srcloc))
+     (compile-literal head)]
+    [(clause srcloc head body)
+     (define srcstx (datum->syntax #f 'x srcloc))
+     (quasisyntax/loc srcstx
+       (:- #,@(map compile-literal (list* head body))))]))
+
+(define compile-literal
+  (match-lambda
+    [(literal srcloc '= (and ts (app length 2)))
+     (define srcstx (datum->syntax #f 'x srcloc))
+     (quasisyntax/loc srcstx
+       (= #,@(map compile-term ts)))]
+    [(literal srcloc pred ts)
+     (define srcstx (datum->syntax #f 'x srcloc))
+     (quasisyntax/loc srcstx
+       (#,pred #,@(map compile-term ts)))]))
+
+(define compile-term
+  (match-lambda
+    [(variable srcloc sym)
+     (datum->syntax #f sym srcloc)]
+    [(constant srcloc sym)
+     (datum->syntax #f sym srcloc)]))
diff --git a/collects/datalog/private/env.rkt b/collects/datalog/private/env.rkt
new file mode 100644
index 0000000..8e12bed
--- /dev/null
+++ b/collects/datalog/private/env.rkt
@@ -0,0 +1,17 @@
+#lang racket
+(require "../ast.rkt")
+
+(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..58b9f49
--- /dev/null
+++ b/collects/datalog/private/lex.rkt
@@ -0,0 +1,45 @@
+#lang racket
+(require parser-tools/lex
+         (prefix-in : parser-tools/lex-sre))
+
+(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/pprint.rkt b/collects/datalog/private/pprint.rkt
new file mode 100644
index 0000000..faf3476
--- /dev/null
+++ b/collects/datalog/private/pprint.rkt
@@ -0,0 +1,20 @@
+#lang racket
+(provide (all-defined-out))
+
+(define (text s) s)
+(define (h-append . ss) (apply string-append ss))
+(define (v-concat/s ss)
+  (apply string-append ss))
+(define (v-concat ss)
+  (apply string-append (add-between ss "\n")))
+(define (apply-infix d ds)
+  (add-between ds d))
+(define line "\n")
+(define comma ",")
+(define space " ")
+(define lparen "(")
+(define rparen ")")
+(define dot ".")
+(define (nest n d) d)
+(define char string)
+(define doc? string?)
\ 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..646e66d
--- /dev/null
+++ b/collects/datalog/private/subst.rkt
@@ -0,0 +1,75 @@
+#lang racket
+(require "../ast.rkt"
+         "env.rkt")
+
+(define (subst-term env t)
+  (match t
+    [(struct variable (_ var))
+     (lookup env var t)]
+    [_
+     t]))
+
+(define (subst-terms env ts)
+  (map (curry subst-term env) ts))
+
+(define (subst-literal env lit)
+  (struct-copy 
+   literal lit
+   [terms 
+    (subst-terms env (literal-terms lit))]))
+
+(define (subst-external env ext)
+  (struct-copy 
+   external ext
+   [arg-terms 
+    (subst-terms env (external-arg-terms ext))]
+   [ans-terms 
+    (subst-terms env (external-ans-terms ext))]))
+
+(define (subst-question env q)
+  (match q
+    [(? literal?) (subst-literal env q)]
+    [(? external?) (subst-external env q)]))
+
+(define (subst-clause env c)
+  (clause (clause-srcloc c)
+          (subst-literal env (clause-head c))
+          (map (curry subst-question env)
+               (clause-body c))))
+
+(define (shuffle-terms env terms)
+  (match terms
+    [(list) 
+     env]
+    [(list-rest (constant _ value) terms)
+     (shuffle-terms env terms)]
+    [(list-rest (variable srcloc var) terms)
+     (if (lookup env var)
+         (shuffle-terms env terms)
+         (shuffle-terms (extend env var (make-variable srcloc (gensym var)))
+                        terms))]))
+
+(define (shuffle env q)
+  (match q
+    [(external _ _ pred arg-terms ans-terms)
+     (shuffle-terms env (append arg-terms ans-terms))]
+    [(literal _ pred terms)
+     (shuffle-terms env 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-question q)
+  (subst-question (shuffle (empty-env) q) q))
+
+(provide/contract
+ [subst-terms (env/c (listof term/c) . -> . (listof term/c))]
+ [subst-term (env/c term/c . -> . term/c)]
+ [subst-clause (env/c clause? . -> . clause?)]
+ [rename-clause (clause? . -> . clause?)]
+ [rename-question (question/c . -> . question/c)])
\ 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..fabbdf2
--- /dev/null
+++ b/collects/datalog/private/unify.rkt
@@ -0,0 +1,59 @@
+#lang racket
+(require "../ast.rkt"
+         "env.rkt")
+
+(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)
+  (or (and (literal? l1) (literal? l2)
+           (datum-equal? (literal-predicate l1)
+                         (literal-predicate l2))
+           (unify-terms (empty-env)
+                        (literal-terms l1)
+                        (literal-terms l2)))
+      (and (external? l1) (external? l2)
+           (equal? (external-predicate l1)
+                   (external-predicate l2))
+           (unify-terms (empty-env)
+                        (append (external-arg-terms l1)
+                                (external-ans-terms l1))
+                        (append (external-arg-terms l2)
+                                (external-ans-terms l2))))))
+
+(provide/contract
+ [unify (question/c question/c . -> . (or/c false/c env/c))]
+ [unify-terms (env/c (listof term/c) (listof term/c) . -> . (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..76b77e4
--- /dev/null
+++ b/collects/datalog/private/variant.rkt
@@ -0,0 +1,105 @@
+#lang racket
+(require "../ast.rkt"
+         "env.rkt")
+
+; 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)
+  (or 
+   (and (literal? l1) (literal? l2)
+        (datum-equal? (literal-predicate l1)
+                      (literal-predicate l2))
+        (variant-terms 
+         (empty-env) (empty-env)
+         (literal-terms l1)
+         (literal-terms l2)))
+   (and (external? l1) (external? l2)
+        (equal? (external-predicate l1)
+                (external-predicate l2))
+        (variant-terms 
+         (empty-env) (empty-env)
+         (external-arg-terms l1)
+         (external-arg-terms l2))
+        (variant-terms 
+         (empty-env) (empty-env)
+         (external-ans-terms l1)
+         (external-ans-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-value t))]))
+(define ((mk-literal-hash recur-hash) q)
+  (define-values
+    (code terms)
+    (match q
+      [(? literal? l)
+       (values (recur-hash (literal-predicate l))
+               (literal-terms l))]
+      [(? external? e)
+       (values (recur-hash (external-predicate e))
+               (append (external-arg-terms e)
+                       (external-ans-terms e)))]))
+  (let loop ([code code]
+             [i 0]
+             [terms terms])
+    (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 question/c . -> . (or/c false/c any/c))]
+ [literal-tbl-replace! (literal-tbl/c question/c any/c . -> . void)]
+ [mem-literal (question/c (listof question/c) . -> . 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..481d1c8
--- /dev/null
+++ b/collects/datalog/runtime.rkt
@@ -0,0 +1,144 @@
+#lang racket
+(require "ast.rkt"
+         "private/env.rkt"
+         "private/subst.rkt"
+         "private/unify.rkt"
+         "private/variant.rkt")
+
+; 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))
+                            (cond
+                              [(literal? l)
+                               (literal-terms l)]
+                              [(external? l)
+                               (append (external-arg-terms l)
+                                       (external-ans-terms l))])))
+                   (clause-body c)))
+          head-vars))
+
+(define 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-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 
+  (question 
+   [facts #:mutable]
+   [waiters #:mutable]))
+
+(define (resolve c q)
+  (define body (clause-body c))
+  (and (not (empty? body))
+       (cond
+         [(unify (first body) (rename-question q))
+          => (lambda (env)
+               (subst-clause env (make-clause (clause-srcloc c) (clause-head c) (rest body))))]
+         [else #f])))
+
+(define (prove thy q)
+  (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-question sg) selected)
+          => (lambda (env)
+               (add-clause! sg (subst-clause env renamed)))]))
+     (get thy (subgoal-question sg))))
+  (define (search! sg)
+    (match (subgoal-question sg)
+      [(external srcloc pred-sym pred args anss)
+       (and (andmap constant? args)
+            (call-with-values 
+             (λ ()
+               (apply pred (map constant-value args)))
+             (λ resolved-vals
+               (define resolved-anss
+                 (map (curry constant #f)
+                      resolved-vals))
+               (cond
+                 [(unify-terms (empty-env) anss resolved-anss)
+                  => (λ (env)
+                       (fact! sg (external srcloc pred-sym pred args (subst-terms env anss))))]))))]
+      [(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 q empty empty))
+  (literal-tbl-replace! subgoals q sg)
+  (search! sg)
+  (subgoal-facts sg))
+
+(provide/contract
+ [safe-clause? (clause? . -> . boolean?)]
+ [theory/c contract?]
+ [make-theory (-> theory/c)]
+ [assume! (theory/c safe-clause? . -> . void)]
+ [retract! (theory/c clause? . -> . void)]
+ [prove (theory/c question/c . -> . (listof question/c))])
\ 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..6942712
--- /dev/null
+++ b/collects/datalog/scribblings/datalog.scrbl
@@ -0,0 +1,178 @@
+#lang scribble/doc
+@(require scribble/manual
+          scribble/eval
+          scribble/basic
+          scribble/bnf
+          "utils.rkt")
+
+@title[#:tag "top"]{@bold{Datalog}: Deductive database programming}
+@author[(author+email "Jay McCarthy" "jay@racket-lang.org")]
+
+@link["http://en.wikipedia.org/wiki/Datalog"]{Datalog} is 
+@itemize[
+ @item{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.}
+ @item{a lightweight deductive database system where queries and database updates are expressed
+       in the logic language.}
+]
+
+The use of Datalog syntax and an implementation based
+on tabling intermediate results ensures that all queries terminate.
+
+@table-of-contents[]
+
+@section[#:tag "datalog"]{Datalog Module Language}
+
+@defmodulelang[@racketmodname[datalog] #:module-paths (datalog/lang/reader)]
+
+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 Unicode "Uppercase" and "Lowercase" letters, digits, and the underscore character. A variable must begin with a Unicode "Uppercase" 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 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"))                
+]
+
+The effect of running a Datalog program is to modify the database as directed
+by its statements, and then to return the literals designated by the query.
+The modified database is provided as @racket[theory].
+
+The following is a program:
+
+@verbatim[#:indent 4 #<<END
+     #lang datalog
+     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 Datalog REPL accepts new statements that are executed as if they were in the original program text.
+
+@include-section["tutorial.scrbl"]
+
+@section{Parenthetical Datalog Module Language}
+@(require (for-label datalog
+                     racket))
+
+@defmodulelang[datalog/sexp]
+
+The semantics of this language is the same as the normal Datalog language, except it uses the parenthetical syntax described in @secref{interop}.
+
+All identifiers in @racketmodname[racket/base] are available for use as predicate symbols or constant values. Top-level identifiers and datums are not otherwise allowed in the program. The program may contain @racket[require] expressions.
+
+The following is a program:
+@racketmod[datalog/sexp
+           
+(! (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))]
+
+This is also a program:
+@racketmod[datalog/sexp
+(require racket/math)
+
+(? (sqr 4 :- X))]
+
+The Parenthetical Datalog REPL accepts new statements that are executed as if they were in the original program text, except @racket[require] is not allowed.
+
+@include-section["racket.scrbl"]
+
+@section{Acknowledgments}
+
+This package was once structurally based on Dave Herman's @racketmodname[(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/racket.scrbl b/collects/datalog/scribblings/racket.scrbl
new file mode 100644
index 0000000..b0d2677
--- /dev/null
+++ b/collects/datalog/scribblings/racket.scrbl
@@ -0,0 +1,86 @@
+#lang scribble/doc
+@(require scribble/manual
+          scribble/eval
+          scribble/basic
+          scribble/bnf
+          (for-label racket/base
+                     racket/contract
+                     "../main.rkt")
+          "utils.rkt")
+
+@title[#:tag "interop"]{Racket Interoperability}
+
+@defmodule[datalog]
+
+The Datalog database can be directly used by Racket programs through this API.
+
+@examples[#:eval the-eval
+          (define family (make-theory))
+          
+          (datalog family
+                   (! (parent joseph2 joseph1))
+                   (! (parent joseph2 lucy))
+                   (! (parent joseph3 joseph2)))
+          
+          (datalog family
+                   (? (parent X joseph2)))
+ 
+          (datalog family
+                   (? (parent joseph2 X)))
+ 
+          (datalog family
+                   (? (parent joseph2 X))
+                   (? (parent X joseph2)))
+ 
+          (datalog family
+                   (! (:- (ancestor A B)
+                          (parent A B)))
+                   (! (:- (ancestor A B)
+                          (parent A C)
+                          (= D C) 
+                          (ancestor D B))))
+ 
+          (datalog family
+                   (? (ancestor A B)))
+ 
+          (let ([x 'joseph2])
+            (datalog family
+                     (? (parent x X))))
+                                       
+          (datalog family
+                   (? (add1 1 :- X)))]
+
+@defthing[theory/c contract?]{ A contract for Datalog theories. }
+
+@defproc[(make-theory) theory/c]{ Creates a theory for use with @racket[datalog]. }
+
+@defform[(datalog thy-expr
+                  stmt ...)
+         #:contracts ([thy-expr theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Returns the answers to the final query as a list of substitution dictionaries or returns @racket[empty]. }
+                                                   
+@defform[(datalog! thy-expr
+                  stmt ...)
+         #:contracts ([thy-expr theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Prints the answers to every query in the list of statements. Returns @racket[(void)]. }     
+              
+Statements are either assertions, retractions, or queries.
+
+@defform[(! clause)]{ Asserts the clause. }
+@defform[(~ clause)]{ Retracts the literal. }
+
+@defform[(:- literal question ...)]{ A conditional clause. }
+
+@defform[(? question)]{ Queries the literal and prints the result literals. }
+                                                   
+Questions are either literals or external queries.
+Literals are represented as @racket[identifier] or @racket[(identifier term ...)].
+External queries are represented as @racket[(identifier term ... :- term ...)], where @racket[identifier] is bound to a procedure that when given the first set of terms as arguments returns the second set of terms as values.
+A term is either a non-capitalized identifiers for a constant symbol, a Racket datum for a constant datum, or a capitalized identifier for a variable symbol. Bound identifiers in terms are treated as datums. 
+
+External queries invalidate Datalog's guaranteed termination. For example, this program does not terminate:
+@racketblock[
+ (datalog (make-theory)
+          (! (:- (loop X)
+                 (add1 X :- Z)
+                 (loop Z)))
+          (? (loop 1)))
+ ]
\ No newline at end of file
diff --git a/collects/datalog/scribblings/tutorial.scrbl b/collects/datalog/scribblings/tutorial.scrbl
new file mode 100644
index 0000000..d49973e
--- /dev/null
+++ b/collects/datalog/scribblings/tutorial.scrbl
@@ -0,0 +1,108 @@
+#lang scribble/doc
+@(require scribble/manual
+          scribble/eval
+          scribble/basic
+          scribble/bnf
+          (for-label racket/base
+                     racket/contract
+                     "../main.rkt")
+          "utils.rkt")
+
+@title{Tutorial}
+
+Start DrRacket and type
+
+@racketmod[datalog]
+
+in the Definitions window. Click @onscreen{Run}, then click in the REPL.
+
+@racketinput[]
+
+@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:
+
+@racketinput[#,(tt "parent(john, douglas).")]
+
+Each item in the parenthesized list following the name of the table is called a @deftech{term}.
+A term can be either a logical @racket[variable] or a @racket[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"]:
+
+@racketinput[#,(tt "parent(john, douglas)?")]
+@racketblock[#,(racketresultfont (tt "parent(john, douglas)."))]
+
+Type this to see if @litchar["john"] is the parent of @litchar["ebbon"]:
+
+@racketinput[#,(tt "parent(john, ebbon)?")]
+
+The query produced no results because @litchar["john"] is not the parent of @litchar["ebbon"]. Let's add more rows.
+
+@racketinput[#,(tt "parent(bob, john).")]
+@racketinput[#,(tt "parent(ebbon, bob).")]
+
+Type the following to list all rows in the @litchar["parent"] table:
+
+@racketinput[#,(tt "parent(A, B)?")]
+@racketblock[#,(racketresultfont (tt "parent(john, douglas)."))]
+@racketblock[#,(racketresultfont (tt "parent(bob, john)."))]
+@racketblock[#,(racketresultfont (tt "parent(ebbon, bob)."))]
+
+Type the following to list all the children of @litchar["john"]:
+
+@racketinput[#,(tt "parent(john, B)?")]
+@racketblock[#,(racketresultfont (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.
+
+@racketinput[#,(tt "parent(A, A)?")]
+
+A deductive database can use rules of inference to derive new facts. Consider the following rule:
+
+@racketinput[#,(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.
+
+@racketinput[#,(tt "ancestor(A, B) :-")
+             #,(tt "  parent(A, C),")
+             #,(tt "  ancestor(C, B).")]
+
+In the interpreter, DrRacket 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.
+
+@racketinput[#,(tt "ancestor(A, B)?")]
+@racketblock[#,(racketresultfont (tt "ancestor(ebbon, bob)."))]
+@racketblock[#,(racketresultfont (tt "ancestor(bob, john)."))]
+@racketblock[#,(racketresultfont (tt "ancestor(john, douglas)."))]
+@racketblock[#,(racketresultfont (tt "ancestor(bob, douglas)."))]
+@racketblock[#,(racketresultfont (tt "ancestor(ebbon, john)."))]
+@racketblock[#,(racketresultfont (tt "ancestor(ebbon, douglas)."))]
+@racketinput[#,(tt "ancestor(X,john)?")]
+@racketblock[#,(racketresultfont (tt "ancestor(bob, john)."))]
+@racketblock[#,(racketresultfont (tt "ancestor(ebbon, john)."))]
+
+A fact or a rule can be retracted from the database using tilde syntax:
+
+@racketinput[#,(tt "parent(bob, john)~")]
+@racketinput[#,(tt "parent(A, B)?")]
+@racketblock[#,(racketresultfont (tt "parent(john, douglas)."))]
+@racketblock[#,(racketresultfont (tt "parent(ebbon, bob)."))]
+@racketinput[#,(tt "ancestor(A, B)?")]
+@racketblock[#,(racketresultfont (tt "ancestor(ebbon, bob)."))]
+@racketblock[#,(racketresultfont (tt "ancestor(john, douglas)."))]
+
+Unlike Prolog, the order in which clauses are asserted is irrelevant. All queries terminate, and every possible answer is derived.
+
+@racketinput[#,(tt "q(X) :- p(X).")]
+@racketinput[#,(tt "q(a).")]
+@racketinput[#,(tt "p(X) :- q(X).")]
+@racketinput[#,(tt "q(X)?")]
+@racketblock[#,(racketresultfont (tt "q(a)."))]
diff --git a/collects/datalog/scribblings/utils.rkt b/collects/datalog/scribblings/utils.rkt
new file mode 100644
index 0000000..36503e1
--- /dev/null
+++ b/collects/datalog/scribblings/utils.rkt
@@ -0,0 +1,10 @@
+#lang racket/base
+
+(require scribble/eval)
+
+(provide the-eval)
+
+(define the-eval
+  (let ([the-eval (make-base-eval)])
+    (the-eval `(require datalog))
+    the-eval))
diff --git a/collects/datalog/sexp/lang.rkt b/collects/datalog/sexp/lang.rkt
new file mode 100644
index 0000000..c62dc79
--- /dev/null
+++ b/collects/datalog/sexp/lang.rkt
@@ -0,0 +1,50 @@
+#lang racket/base
+(require (for-syntax syntax/parse
+                     racket/list
+                     racket/base)
+         racket/contract
+         datalog/stx
+         datalog/runtime)
+
+(define-for-syntax (partition-requires es)
+  (define-values (rs stmts)
+    (partition 
+     (λ (e-stx)
+       (syntax-parse
+        e-stx
+        #:literals (require)
+        [(require . r)
+         #t]
+        [_
+         #f]))
+     (syntax->list es)))
+  (list rs stmts))
+
+(define-syntax (module-begin stx)
+  (syntax-case stx ()
+    [(_ . es)
+     (with-syntax ([theory (datum->syntax #'es 'theory)]
+                   [((requires ...)
+                     (stmt ...))
+                    (partition-requires #'es)])
+       (syntax/loc stx
+         (#%module-begin 
+          requires ...
+          (define theory (make-theory))
+          (datalog! theory stmt ...)
+          (provide/contract
+           [theory theory/c]))))]))
+
+(define-syntax (top-interaction stx)
+  (syntax-case stx ()
+    [(_ . stmt)
+     (with-syntax ([theory (datum->syntax #'stmt 'theory)])
+       (syntax/loc stx
+         (datalog! theory stmt)))]))
+
+(provide (rename-out [top-interaction #%top-interaction]
+                     [module-begin #%module-begin])
+         (except-out (all-from-out racket/base)
+                     #%top-interaction
+                     #%module-begin)
+         ! ~ ? :-)
\ No newline at end of file
diff --git a/collects/datalog/sexp/lang/reader.rkt b/collects/datalog/sexp/lang/reader.rkt
new file mode 100644
index 0000000..546cb06
--- /dev/null
+++ b/collects/datalog/sexp/lang/reader.rkt
@@ -0,0 +1,2 @@
+(module reader syntax/module-reader
+  #:language 'datalog/sexp/lang)
\ No newline at end of file
diff --git a/collects/datalog/stx.rkt b/collects/datalog/stx.rkt
new file mode 100644
index 0000000..8885a67
--- /dev/null
+++ b/collects/datalog/stx.rkt
@@ -0,0 +1,190 @@
+#lang racket
+(require (for-syntax syntax/parse
+                     racket/local
+                     racket/function
+                     racket/list)
+         datalog/ast
+         datalog/eval)
+
+(define-syntax (:- stx)
+  (raise-syntax-error ':- "only allowed inside ! and ~" stx))
+(define-syntax (! stx)
+  (raise-syntax-error '! "only allowed inside datalog" stx))
+(define-syntax (~ stx)
+  (raise-syntax-error '~ "only allowed inside datalog" stx))
+(define-syntax (? stx)
+  (raise-syntax-error '? "only allowed inside datalog" stx))
+
+(define (->substitutions sel ls)
+  (if (void? ls) empty
+      (map sel ls)))
+
+(define literal->sexp
+  (match-lambda
+    [(external _ pred-sym _ args anss)
+     `(,pred-sym ,@(map term->datum args)
+                 :-
+                 ,@(map term->datum anss))]
+    [(literal _ pred ts)
+     (list* pred (map term->datum ts))]))
+
+(define term->datum
+  (match-lambda
+    [(constant _ v)
+     v]))
+
+(define-syntax (datalog stx)
+  (syntax-case stx ()
+    [(_ thy-expr stmt ...)
+     (syntax/loc stx
+       (parameterize ([current-theory thy-expr])
+         (->substitutions
+          (datalog-stmt-var-selector stmt)
+          (eval-statement (datalog-stmt stmt)))
+         ...))]))
+
+(define-syntax (datalog! stx)
+  (syntax-case stx ()
+    [(_ thy-expr stmt ...)
+     (syntax/loc stx
+       (parameterize ([current-theory thy-expr])
+         (eval-top-level-statement (datalog-stmt stmt))
+         ...))]))
+
+(define-syntax (datalog-stmt stx)
+  (syntax-parse 
+   stx
+   #:literals (! ~ ?)
+   [(_ (~and tstx (! c)))
+    (quasisyntax/loc #'tstx
+      (assertion #'#,#'tstx (datalog-clause c)))]
+   [(_ (~and tstx (~ c)))
+    (quasisyntax/loc #'tstx
+      (retraction #'#,#'tstx (datalog-clause c)))]
+   [(_ (~and tstx (? l)))
+    (quasisyntax/loc #'tstx
+      (query #'#,#'tstx (datalog-literal l)))]))
+
+(define-syntax (datalog-stmt-var-selector stx)
+  (syntax-parse 
+   stx
+   #:literals (! ~ ?)
+   [(_ (~and tstx (! c)))
+    (quasisyntax/loc #'tstx (λ (l) (hasheq)))]
+   [(_ (~and tstx (~ c)))
+    (quasisyntax/loc #'tstx (λ (l) (hasheq)))]
+   [(_ (~and tstx (? l)))
+    (quasisyntax/loc #'tstx (datalog-literal-var-selector l))]))
+
+(define-syntax (datalog-clause stx)
+  (syntax-parse 
+   stx
+   #:literals (:-)
+   [(_ (~and tstx (:- head body ...)))
+    (local [(define (datalog-literal-variables stx)
+              (syntax-parse 
+               stx
+               #:literals (:-)
+               [sym:id
+                empty]
+               [(~and tstx (sym:id arg ... :- ans ...))
+                (append-map datalog-term-variables
+                            (syntax->list #'(arg ... ans ...)))]
+               [(~and tstx (sym:id e ...))
+                (append-map datalog-term-variables
+                            (syntax->list #'(e ...)))]))
+            (define (datalog-term-variables stx)
+              (syntax-parse 
+               stx
+               [sym:id
+                (list #'sym)]
+               [sym:expr
+                empty]))
+            (define head-vars (datalog-literal-variables #'head))
+            (define body-vars 
+              (append-map datalog-literal-variables (syntax->list #'(body ...))))
+            (define body-vars-in-head
+              (filter
+               (λ (bv)
+                 (findf (curry bound-identifier=? bv)
+                        head-vars))
+               body-vars))
+            (define fake-lam
+              (quasisyntax/loc #'tstx
+                (lambda #,head-vars
+                  (void #,@body-vars-in-head))))]
+      (syntax-local-lift-expression
+       fake-lam))
+    (quasisyntax/loc #'tstx
+      (clause #'#,#'tstx (datalog-literal head) 
+              (list (datalog-literal body) ...)))]
+   [(_ e)
+    (quasisyntax/loc #'e
+      (clause #'#,#'e (datalog-literal e) empty))]))
+
+(define-syntax (datalog-literal stx)
+  (syntax-parse 
+   stx
+   #:literals (:-)
+   [(_ sym:id)
+    (quasisyntax/loc #'sym
+      (literal #'#,#'sym 'sym empty))]
+   [(_ (~and tstx (sym:id arg ... :- ans ...)))
+    (quasisyntax/loc #'tstx
+      (external #'#,#'tstx 'sym sym
+                (list (datalog-term arg) ...)
+                (list (datalog-term ans) ...)))]
+   [(_ (~and tstx (sym:id e ...)))
+    (quasisyntax/loc #'tstx
+      (literal #'#,#'tstx 'sym 
+               (list (datalog-term e)
+                     ...)))]))
+
+(define-syntax (datalog-literal-var-selector stx)
+  (syntax-parse 
+   stx
+   #:literals (:-)
+   [(_ sym:id)
+    (quasisyntax/loc #'sym (λ (l) (hasheq)))]
+   [(_ (~and tstx (sym:id arg ... :- ans ...)))
+    (quasisyntax/loc #'tstx 
+      (match-lambda
+        [(external _srcloc _predsym _pred args anss)
+         (terms->hasheq (list (datalog-term arg) ...
+                              (datalog-term ans) ...)
+                        (append args anss))]))]
+   [(_ (~and tstx (sym:id e ...)))
+    (quasisyntax/loc #'tstx
+      (match-lambda
+        [(literal _srcloc _predsym ts)
+         (terms->hasheq (list (datalog-term e) ...)
+                        ts)]))]))
+
+(define (terms->hasheq src-ts res-ts)
+  (for/fold ([h (hasheq)])
+    ([src (in-list src-ts)]
+     [res (in-list res-ts)])
+    (if (variable? src)
+        (hash-set h (variable-sym src) (constant-value res))
+        h)))
+
+(define-syntax (datalog-term stx)
+  (syntax-parse 
+   stx
+   [(_ sym:id)
+    (cond
+      [(identifier-binding #'sym 0)
+       (quasisyntax/loc #'sym
+         (constant #'#,#'sym sym))]
+      [(char-upper-case? (string-ref (symbol->string (syntax->datum #'sym)) 0))
+       (quasisyntax/loc #'sym
+         (variable #'#,#'sym 'sym))]
+      [else
+       (quasisyntax/loc #'sym
+         (constant #'#,#'sym 'sym))])]
+   [(_ sym:expr)
+    (quasisyntax/loc #'sym
+      (constant #'#,#'sym sym))]))
+
+(provide datalog datalog!
+         :- ! ~ ?)
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/submit.rkt b/collects/datalog/tool/submit.rkt
new file mode 100644
index 0000000..f16281a
--- /dev/null
+++ b/collects/datalog/tool/submit.rkt
@@ -0,0 +1,54 @@
+#lang racket/base
+
+(define (delimiter-pair? x y)
+  (and (char=? x #\() (char=? y #\))))
+
+(define (repl-submit? ip has-white-space?)
+  (let loop ([blank? #t]
+             [string-char #f]
+             [delimiter-stack null]
+             [closed? #f])
+    (let ([c (read-char ip)])
+      (if (eof-object? c)
+          (and closed?
+               (not blank?)
+               (not string-char)
+               (null? delimiter-stack))
+          (case c
+            [(#\. #\? #\~)
+             (if string-char
+                 (loop #f string-char delimiter-stack #f)
+                 (loop #f #f delimiter-stack #t))]
+            [(#\()
+             (if string-char
+                 (loop #f string-char delimiter-stack #f)
+                 (loop #f #f (cons c delimiter-stack) #f))]
+            [(#\))
+             (cond
+               [string-char
+                (loop #f string-char delimiter-stack #f)]
+               [(and (pair? delimiter-stack)
+                     (delimiter-pair? (car delimiter-stack) c))
+                (loop #f #f (cdr delimiter-stack) #f)]
+               [else
+                (loop #f #f delimiter-stack #f)])]
+            [(#\")
+             (cond
+               [(and string-char (char=? c string-char))
+                (loop #f #f delimiter-stack #f)]
+               [string-char
+                (loop #f string-char delimiter-stack #f)]
+               [else
+                (loop #f c delimiter-stack #f)])]
+            [(#\\)
+             (if string-char
+                 (begin (read-char ip)
+                        (loop #f string-char delimiter-stack #f))
+                 (loop #f string-char delimiter-stack #f))]
+            [else
+             (loop (and blank? (char-whitespace? c))
+                   string-char
+                   delimiter-stack
+                   closed?)])))))
+
+(provide repl-submit?)
\ No newline at end of file
diff --git a/collects/datalog/tool/syntax-color.rkt b/collects/datalog/tool/syntax-color.rkt
new file mode 100644
index 0000000..5966b2e
--- /dev/null
+++ b/collects/datalog/tool/syntax-color.rkt
@@ -0,0 +1,36 @@
+#lang racket/base
+(require parser-tools/lex
+         (prefix-in : parser-tools/lex-sre)
+         "../private/lex.rkt")
+
+(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 'symbol #f start-pos end-pos)]
+   [identifier-re
+    (syn-val lexeme 'identifier #f start-pos end-pos)]
+   [(:or #\) #\() (syn-val lexeme 'parenthesis #f start-pos end-pos)]
+   [(:or #\= #\? #\~ #\. #\, ":-") (syn-val lexeme 'parenthesis #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
diff --git a/collects/tests/datalog/ast.rkt b/collects/tests/datalog/ast.rkt
new file mode 100644
index 0000000..ec6e6ee
--- /dev/null
+++ b/collects/tests/datalog/ast.rkt
@@ -0,0 +1,80 @@
+#lang racket
+(require rackunit
+         datalog/ast)
+
+(provide ast-tests)
+
+(define ast-tests
+  (test-suite
+   "ast"
+   
+   (test-suite
+    "datum-equal?"
+    (test-not-false "str/str" (datum-equal? "str" "str"))
+    (test-false "str/str" (datum-equal? "str1" "str2"))
+    (test-not-false "sym/sym" (datum-equal? 'sym1 'sym1))
+    (test-false "sym/sym" (datum-equal? 'sym1 'sym2))
+    (test-false "str/sym" (datum-equal? "str" 'sym))
+    (test-false "sym/str" (datum-equal? 'sym "str")))
+   
+   (test-suite
+    "variable-equal?"
+    (test-not-false "var/var" (variable-equal? (make-variable #f 'sym1) (make-variable #f 'sym1)))
+    (test-not-false "var/var" (variable-equal? (make-variable #f 'sym1) (make-variable #'sym1 'sym1)))
+    (test-false "var/var" (variable-equal? (make-variable #f 'sym1) (make-variable #f 'sym2)))
+    (test-false "var/var" (variable-equal? (make-variable #f 'sym1) (make-variable #'sym2 'sym2))))
+   
+   (test-suite
+    "constant-equal?"
+    (test-not-false "sym/sym" (constant-equal? (make-constant #f 'sym1) (make-constant #f 'sym1)))
+    (test-not-false "sym/sym" (constant-equal? (make-constant #f 'sym1) (make-constant #'sym1 'sym1)))
+    (test-false "sym/sym" (constant-equal? (make-constant #f 'sym1) (make-constant #'sym1 'sym2)))
+    (test-not-false "str/str" (constant-equal? (make-constant #f "sym1") (make-constant #f "sym1")))
+    (test-not-false "str/str" (constant-equal? (make-constant #f "sym1") (make-constant #'sym1 "sym1")))
+    (test-false "str/str" (constant-equal? (make-constant #f "sym1") (make-constant #'sym1 "sym2")))
+    (test-false "sym/str" (constant-equal? (make-constant #f 'sym1) (make-constant #'sym1 "sym2")))
+    (test-false "str/sym" (constant-equal? (make-constant #'sym1 "sym2") (make-constant #f 'sym1))))
+   
+   (test-suite
+    "term-equal?"
+    (test-not-false "var/var" (term-equal? (make-variable #f 'sym1) (make-variable #f 'sym1)))
+    (test-not-false "var/var" (term-equal? (make-variable #f 'sym1) (make-variable #'sym1 'sym1)))
+    (test-false "var/var" (term-equal? (make-variable #f 'sym1) (make-variable #f 'sym2)))
+    (test-false "var/var" (term-equal? (make-variable #f 'sym1) (make-variable #'sym2 'sym2)))
+    (test-not-false "sym/sym" (term-equal? (make-constant #f 'sym1) (make-constant #f 'sym1)))
+    (test-not-false "sym/sym" (term-equal? (make-constant #f 'sym1) (make-constant #'sym1 'sym1)))
+    (test-false "sym/sym" (term-equal? (make-constant #f 'sym1) (make-constant #'sym1 'sym2)))
+    (test-not-false "str/str" (term-equal? (make-constant #f "sym1") (make-constant #f "sym1")))
+    (test-not-false "str/str" (term-equal? (make-constant #f "sym1") (make-constant #'sym1 "sym1")))
+    (test-false "str/str" (term-equal? (make-constant #f "sym1") (make-constant #'sym1 "sym2")))
+    (test-false "sym/str" (term-equal? (make-constant #f 'sym1) (make-constant #'sym1 "sym2")))
+    (test-false "str/sym" (term-equal? (make-constant #'sym1 "sym2") (make-constant #f 'sym1)))    
+    (test-false "con/var" (term-equal? (make-constant #'sym1 "sym2") (make-variable #f 'sym1)))
+    (test-false "var/con" (term-equal? (make-variable #f 'sym1) (make-constant #'sym1 "sym2"))))
+   
+   (test-suite
+    "literal-equal?"
+    (test-not-false "lit" (literal-equal? (make-literal #f 'lit1 empty) (make-literal #'lit1 'lit1 empty)))
+    (test-not-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1)))
+                                          (make-literal #'lit1 'lit1 (list (make-variable #f 'sym1)))))
+    (test-not-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1)))
+                                          (make-literal #'lit1 'lit1 (list (make-variable #'sym1 'sym1)))))
+    (test-false "lit" (literal-equal? (make-literal #f 'lit1 empty) (make-literal #'lit1 'lit2 empty)))
+    (test-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1))) (make-literal #'lit1 'lit2 empty)))
+    (test-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1)))
+                                      (make-literal #'lit1 'lit2 (list (make-variable #'sym1 'sym2))))))
+   
+   (test-suite
+    "clause-equal?"
+    (test-not-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) empty)
+                                         (make-clause #f (make-literal #f 'lit1 empty) empty)))
+    (test-not-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))
+                                         (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))))
+    (test-not-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) empty)
+                                         (make-clause #'cl1 (make-literal #f 'lit1 empty) empty)))
+    (test-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) empty)
+                                     (make-clause #f (make-literal #f 'lit2 empty) empty)))
+    (test-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))
+                                     (make-clause #f (make-literal #f 'lit1 empty) empty)))
+    (test-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))
+                                     (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit2 empty))))))))
\ No newline at end of file
diff --git a/collects/tests/datalog/eval.rkt b/collects/tests/datalog/eval.rkt
new file mode 100644
index 0000000..3611fd5
--- /dev/null
+++ b/collects/tests/datalog/eval.rkt
@@ -0,0 +1,42 @@
+#lang racket
+(require rackunit
+         racket/runtime-path
+         datalog/parse
+         datalog/eval)
+
+(provide eval-tests)
+
+(define-runtime-path here ".")
+
+(define (test-examples examples-dir)
+  
+  (define (test-example t)
+    (define test-rkt (build-path examples-dir (format "~a.rkt" t)))
+    (define test-txt (build-path examples-dir (format "~a.txt" t)))
+    (test-equal? t
+                 (filter (lambda (l)
+                           (not (string=? l "")))
+                         (with-input-from-string
+                             (with-output-to-string
+                                 (lambda () (dynamic-require test-rkt #f)))
+                           port->lines))
+                 (filter (lambda (l)
+                           (not (string=? l "")))
+                         (file->lines test-txt))))
+  
+  (define (test-files d)
+    (for ([f (in-list (directory-list d))]
+          #:when (regexp-match #rx"rkt$" (path->bytes f)))
+      (test-example (path->string (path-replace-suffix f #"")))))
+  
+  (test-suite
+   (path->string examples-dir)
+   
+   (test-files examples-dir)))
+
+(define eval-tests
+  (test-suite
+   "eval"
+   
+   (test-examples (build-path here "examples"))
+   (test-examples (build-path here "paren-examples"))))
\ No newline at end of file
diff --git a/collects/tests/datalog/examples/ancestor.rkt b/collects/tests/datalog/examples/ancestor.rkt
new file mode 100644
index 0000000..f448960
--- /dev/null
+++ b/collects/tests/datalog/examples/ancestor.rkt
@@ -0,0 +1,12 @@
+#lang datalog
+% Equality test
+ancestor(A, B) :-
+    parent(A, B).
+ancestor(A, B) :-
+    parent(A, C),
+    D = C,      % Unification required
+    ancestor(D, B).
+parent(john, douglas).
+parent(bob, john).
+parent(ebbon, bob).
+ancestor(A, B)?
\ No newline at end of file
diff --git a/collects/tests/datalog/examples/bidipath.rkt b/collects/tests/datalog/examples/bidipath.rkt
new file mode 100644
index 0000000..cb1393b
--- /dev/null
+++ b/collects/tests/datalog/examples/bidipath.rkt
@@ -0,0 +1,7 @@
+#lang datalog
+% path test from Chen & Warren
+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) :- path(X, Z), edge(Z, Y).
+path(X, Y)?
diff --git a/collects/tests/datalog/examples/laps.rkt b/collects/tests/datalog/examples/laps.rkt
new file mode 100644
index 0000000..56bac66
--- /dev/null
+++ b/collects/tests/datalog/examples/laps.rkt
@@ -0,0 +1,12 @@
+#lang datalog
+% Laps Test
+contains(ca, store, rams_couch, rams).
+contains(rams, fetch, rams_couch, will).
+contains(ca, fetch, Name, Watcher) :-
+    contains(ca, store, Name, Owner),
+    contains(Owner, fetch, Name, Watcher).
+trusted(ca).
+permit(User, Priv, Name) :-
+    contains(Auth, Priv, Name, User),
+    trusted(Auth).
+permit(User, Priv, Name)?
diff --git a/collects/tests/datalog/examples/long.rkt b/collects/tests/datalog/examples/long.rkt
new file mode 100644
index 0000000..a8b9912
--- /dev/null
+++ b/collects/tests/datalog/examples/long.rkt
@@ -0,0 +1,8 @@
+#lang datalog
+abcdefghi(z123456789,
+z1234567890123456789,
+z123456789012345678901234567890123456789,
+z1234567890123456789012345678901234567890123456789012345678901234567890123456789).
+
+this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer.
+this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer?
diff --git a/collects/tests/datalog/examples/path.rkt b/collects/tests/datalog/examples/path.rkt
new file mode 100644
index 0000000..694aaab
--- /dev/null
+++ b/collects/tests/datalog/examples/path.rkt
@@ -0,0 +1,6 @@
+#lang datalog
+% path test from Chen & Warren
+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)?
diff --git a/collects/tests/datalog/examples/pq.rkt b/collects/tests/datalog/examples/pq.rkt
new file mode 100644
index 0000000..c5efcec
--- /dev/null
+++ b/collects/tests/datalog/examples/pq.rkt
@@ -0,0 +1,6 @@
+#lang datalog
+% p q test from Chen & Warren
+q(X) :- p(X).
+q(a).
+p(X) :- q(X).
+q(X)?
diff --git a/collects/tests/datalog/examples/revpath.rkt b/collects/tests/datalog/examples/revpath.rkt
new file mode 100644
index 0000000..15d8fe9
--- /dev/null
+++ b/collects/tests/datalog/examples/revpath.rkt
@@ -0,0 +1,6 @@
+#lang datalog
+% path test from Chen & Warren
+edge(a, b). edge(b, c). edge(c, d). edge(d, a).
+path(X, Y) :- edge(X, Y).
+path(X, Y) :- path(X, Z), edge(Z, Y).
+path(X, Y)?
diff --git a/collects/tests/datalog/examples/says.rkt b/collects/tests/datalog/examples/says.rkt
new file mode 100644
index 0000000..5ee12bb
--- /dev/null
+++ b/collects/tests/datalog/examples/says.rkt
@@ -0,0 +1,5 @@
+#lang datalog
+tpme(tpme1).
+ms(m1,'TPME',tpme1,ek,tp).
+says(TPME,M) :- tpme(TPME),ms(M,'TPME',TPME,A,B).
+says(A,B)?
diff --git a/collects/tests/datalog/examples/true.rkt b/collects/tests/datalog/examples/true.rkt
new file mode 100644
index 0000000..eed11d3
--- /dev/null
+++ b/collects/tests/datalog/examples/true.rkt
@@ -0,0 +1,3 @@
+#lang datalog
+true.
+true?
diff --git a/collects/tests/datalog/examples/tutorial.rkt b/collects/tests/datalog/examples/tutorial.rkt
new file mode 100644
index 0000000..5981f22
--- /dev/null
+++ b/collects/tests/datalog/examples/tutorial.rkt
@@ -0,0 +1,42 @@
+#lang datalog
+
+parent(john,douglas).
+parent(john,douglas)?
+% parent(john, douglas).
+
+parent(john,ebbon)?
+
+parent(bob,john).
+parent(ebbon,bob).
+parent(A,B)?
+% parent(john, douglas).
+% parent(bob, john).
+% parent(ebbon, bob).
+
+parent(john,B)?
+% parent(john, douglas).
+
+parent(A,A)?
+
+ancestor(A,B) :- parent(A,B).
+ancestor(A,B) :- parent(A,C), ancestor(C, B).
+ancestor(A, B)?
+% ancestor(ebbon, bob).
+% ancestor(bob, john).
+% ancestor(john, douglas).
+% ancestor(bob, douglas).
+% ancestor(ebbon, john).
+% ancestor(ebbon, douglas).
+
+ancestor(X,john)?
+% ancestor(bob, john).
+% ancestor(ebbon, john).
+
+parent(bob, john)~
+parent(A,B)?
+% parent(john, douglas).
+% parent(ebbon, bob).
+
+ancestor(A,B)?
+% ancestor(john, douglas).
+% ancestor(ebbon, bob).
diff --git a/collects/tests/datalog/main.rkt b/collects/tests/datalog/main.rkt
new file mode 100644
index 0000000..b73ad06
--- /dev/null
+++ b/collects/tests/datalog/main.rkt
@@ -0,0 +1,45 @@
+#lang racket
+(require racket/runtime-path
+         rackunit
+         rackunit/text-ui
+         "ast.rkt"
+         
+         "private/lex.rkt"
+         "tool/syntax-color.rkt"
+         "parse.rkt"         
+         
+         "pretty.rkt"
+         
+         "private/env.rkt"
+         "private/subst.rkt"
+         "private/unify.rkt"
+         "private/variant.rkt"
+         
+         "runtime.rkt"
+         "eval.rkt")
+
+(define-runtime-path racket-mod "racket.rkt")
+(define stdout (current-output-port))
+
+(run-tests
+ (test-suite
+  "Datalog"
+  ast-tests
+  
+  lex-tests
+  syntax-color-tests
+  parse-tests  
+  
+  pretty-tests
+  
+  env-tests
+  subst-tests
+  unify-tests
+  variant-tests
+  
+  runtime-tests
+  eval-tests
+  
+  (test-case "Racket Interop"
+             (parameterize ([current-output-port stdout])
+               (dynamic-require racket-mod #f)))))
\ No newline at end of file
diff --git a/collects/tests/datalog/paren-examples/add1.rkt b/collects/tests/datalog/paren-examples/add1.rkt
new file mode 100644
index 0000000..f89b1b0
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/add1.rkt
@@ -0,0 +1,10 @@
+#lang datalog/sexp
+(? (add1 2 :- X))
+
+(! (:- (add2 X Y)
+       (add1 X :- Z)
+       (add1 Z :- Y)))
+
+(? (add2 1 3))
+
+(? (add1 X :- 1))
\ No newline at end of file
diff --git a/collects/tests/datalog/paren-examples/add1.txt b/collects/tests/datalog/paren-examples/add1.txt
new file mode 100644
index 0000000..dc6a141
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/add1.txt
@@ -0,0 +1,3 @@
+add1(2) = (3).
+
+add2(1, 3).
diff --git a/collects/tests/datalog/paren-examples/ancestor.rkt b/collects/tests/datalog/paren-examples/ancestor.rkt
new file mode 100644
index 0000000..290994b
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/ancestor.rkt
@@ -0,0 +1,12 @@
+#lang datalog/sexp
+; Equality test
+(! (:- (ancestor A B)
+       (parent A B)))
+(! (:- (ancestor A B)
+       (parent A C)
+       (= D C) ; Unification required
+       (ancestor D B)))
+(! (parent john douglas))
+(! (parent bob john))
+(! (parent ebbon bob))
+(? (ancestor A B))
diff --git a/collects/tests/datalog/paren-examples/ancestor.txt b/collects/tests/datalog/paren-examples/ancestor.txt
new file mode 100644
index 0000000..bed107f
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/ancestor.txt
@@ -0,0 +1,6 @@
+ancestor(ebbon, bob).
+ancestor(bob, john).
+ancestor(john, douglas).
+ancestor(bob, douglas).
+ancestor(ebbon, john).
+ancestor(ebbon, douglas).
diff --git a/collects/tests/datalog/paren-examples/bidipath.rkt b/collects/tests/datalog/paren-examples/bidipath.rkt
new file mode 100644
index 0000000..5c32fbb
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/bidipath.rkt
@@ -0,0 +1,15 @@
+#lang datalog/sexp
+; path test from Chen & Warren
+(! (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)
+       (path X Z)
+       (edge Z Y)))
+(? (path X Y))
\ No newline at end of file
diff --git a/collects/tests/datalog/paren-examples/bidipath.txt b/collects/tests/datalog/paren-examples/bidipath.txt
new file mode 100644
index 0000000..6c197dd
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/bidipath.txt
@@ -0,0 +1,17 @@
+path(a, a).
+path(a, d).
+path(a, c).
+path(a, b).
+path(b, b).
+path(b, a).
+path(b, d).
+path(b, c).
+path(c, c).
+path(c, b).
+path(c, a).
+path(c, d).
+path(d, d).
+path(d, c).
+path(d, b).
+path(d, a).
+
diff --git a/collects/tests/datalog/paren-examples/laps.rkt b/collects/tests/datalog/paren-examples/laps.rkt
new file mode 100644
index 0000000..66b38a9
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/laps.rkt
@@ -0,0 +1,13 @@
+#lang datalog/sexp
+; Laps Test
+(! (contains ca store rams_couch rams))
+(! (contains rams fetch rams_couch will))
+(! (:- (contains ca fetch Name Watcher)
+       (contains ca store Name Owner)
+       (contains Owner fetch Name Watcher)))
+(! (trusted ca))
+(! (:- (permit User Priv Name)
+       (contains Auth Priv Name User)
+       (trusted Auth)))
+(? (permit User Priv Name))
+
diff --git a/collects/tests/datalog/paren-examples/laps.txt b/collects/tests/datalog/paren-examples/laps.txt
new file mode 100644
index 0000000..d87ea5f
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/laps.txt
@@ -0,0 +1,2 @@
+permit(rams, store, rams_couch).
+permit(will, fetch, rams_couch).
diff --git a/collects/tests/datalog/paren-examples/long.rkt b/collects/tests/datalog/paren-examples/long.rkt
new file mode 100644
index 0000000..ad6ef3d
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/long.rkt
@@ -0,0 +1,8 @@
+#lang datalog/sexp
+(! (abcdefghi z123456789
+              z1234567890123456789
+              z123456789012345678901234567890123456789
+              z1234567890123456789012345678901234567890123456789012345678901234567890123456789))
+(! this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer)
+(? this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer)
+
diff --git a/collects/tests/datalog/paren-examples/long.txt b/collects/tests/datalog/paren-examples/long.txt
new file mode 100644
index 0000000..ebf5669
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/long.txt
@@ -0,0 +1 @@
+this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer.
diff --git a/collects/tests/datalog/paren-examples/path.rkt b/collects/tests/datalog/paren-examples/path.rkt
new file mode 100644
index 0000000..ba2768e
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/path.rkt
@@ -0,0 +1,12 @@
+#lang datalog/sexp
+; path test from Chen & Warren
+(! (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))
diff --git a/collects/tests/datalog/paren-examples/path.txt b/collects/tests/datalog/paren-examples/path.txt
new file mode 100644
index 0000000..9319f8c
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/path.txt
@@ -0,0 +1,17 @@
+path(a, a).
+path(a, d).
+path(a, c).
+path(a, b).
+path(b, a).
+path(b, d).
+path(b, c).
+path(b, b).
+path(c, a).
+path(c, d).
+path(c, c).
+path(c, b).
+path(d, b).
+path(d, c).
+path(d, d).
+path(d, a).
+
diff --git a/collects/tests/datalog/paren-examples/pq.rkt b/collects/tests/datalog/paren-examples/pq.rkt
new file mode 100644
index 0000000..fb0a3ec
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/pq.rkt
@@ -0,0 +1,8 @@
+#lang datalog/sexp
+; p q test from Chen & Warren
+(! (:- (q X)
+       (p X)))
+(! (q a))
+(! (:- (p X)
+       (q X)))
+(? (q X))
diff --git a/collects/tests/datalog/paren-examples/pq.txt b/collects/tests/datalog/paren-examples/pq.txt
new file mode 100644
index 0000000..7526e51
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/pq.txt
@@ -0,0 +1 @@
+q(a).
diff --git a/collects/tests/datalog/paren-examples/req.rkt b/collects/tests/datalog/paren-examples/req.rkt
new file mode 100644
index 0000000..c7cfb8d
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/req.rkt
@@ -0,0 +1,4 @@
+#lang datalog/sexp
+(require racket/math)
+
+(? (sqr 4 :- X))
\ No newline at end of file
diff --git a/collects/tests/datalog/paren-examples/req.txt b/collects/tests/datalog/paren-examples/req.txt
new file mode 100644
index 0000000..8cc5574
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/req.txt
@@ -0,0 +1 @@
+sqr(4) = (16).
diff --git a/collects/tests/datalog/paren-examples/revpath.rkt b/collects/tests/datalog/paren-examples/revpath.rkt
new file mode 100644
index 0000000..5899cdf
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/revpath.rkt
@@ -0,0 +1,12 @@
+#lang datalog/sexp
+; path test from Chen & Warren
+(! (edge a b))
+(! (edge b c))
+(! (edge c d))
+(! (edge d a))
+(! (:- (path X Y)
+       (edge X Y)))
+(! (:- (path X Y)
+       (path X Z)
+       (edge Z Y)))
+(? (path X Y))
\ No newline at end of file
diff --git a/collects/tests/datalog/paren-examples/revpath.txt b/collects/tests/datalog/paren-examples/revpath.txt
new file mode 100644
index 0000000..6c197dd
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/revpath.txt
@@ -0,0 +1,17 @@
+path(a, a).
+path(a, d).
+path(a, c).
+path(a, b).
+path(b, b).
+path(b, a).
+path(b, d).
+path(b, c).
+path(c, c).
+path(c, b).
+path(c, a).
+path(c, d).
+path(d, d).
+path(d, c).
+path(d, b).
+path(d, a).
+
diff --git a/collects/tests/datalog/paren-examples/says.rkt b/collects/tests/datalog/paren-examples/says.rkt
new file mode 100644
index 0000000..90c7f71
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/says.rkt
@@ -0,0 +1,7 @@
+#lang datalog/sexp
+(! (tpme tpme1))
+(! (ms m1 "TPME" tpme1 ek tp))
+(! (:- (says TPME M)
+       (tpme TPME)
+       (ms M "TPME" TPME A B)))
+(? (says A B))
diff --git a/collects/tests/datalog/paren-examples/says.txt b/collects/tests/datalog/paren-examples/says.txt
new file mode 100644
index 0000000..473484a
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/says.txt
@@ -0,0 +1 @@
+says(tpme1, m1).
diff --git a/collects/tests/datalog/paren-examples/true.rkt b/collects/tests/datalog/paren-examples/true.rkt
new file mode 100644
index 0000000..18ccecb
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/true.rkt
@@ -0,0 +1,3 @@
+#lang datalog/sexp
+(! true)
+(? true)
\ No newline at end of file
diff --git a/collects/tests/datalog/paren-examples/true.txt b/collects/tests/datalog/paren-examples/true.txt
new file mode 100644
index 0000000..48eb7ed
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/true.txt
@@ -0,0 +1 @@
+true.
diff --git a/collects/tests/datalog/paren-examples/tutorial.rkt b/collects/tests/datalog/paren-examples/tutorial.rkt
new file mode 100644
index 0000000..6d51ed6
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/tutorial.rkt
@@ -0,0 +1,28 @@
+#lang datalog/sexp
+(! (parent john douglas))
+(? (parent john douglas))
+
+(? (parent john ebbon))
+
+(! (parent bob john))
+(! (parent ebbon bob))
+(? (parent A B))
+
+(? (parent john B))
+
+(? (parent A A))
+
+(! (:- (ancestor A B)
+       (parent A B)))
+(! (:- (ancestor A B)
+       (parent A C)
+       (ancestor C B)))
+(? (ancestor A B))
+
+(? (ancestor X john))
+
+(~ (parent bob john))
+
+(? (parent A B))
+
+(? (ancestor A B))
diff --git a/collects/tests/datalog/paren-examples/tutorial.txt b/collects/tests/datalog/paren-examples/tutorial.txt
new file mode 100644
index 0000000..629d2dc
--- /dev/null
+++ b/collects/tests/datalog/paren-examples/tutorial.txt
@@ -0,0 +1,26 @@
+parent(john, douglas).
+
+
+parent(john, douglas).
+parent(bob, john).
+parent(ebbon, bob).
+
+parent(john, douglas).
+
+
+ancestor(ebbon, bob).
+ancestor(bob, john).
+ancestor(john, douglas).
+ancestor(bob, douglas).
+ancestor(ebbon, john).
+ancestor(ebbon, douglas).
+
+ancestor(bob, john).
+ancestor(ebbon, john).
+
+parent(john, douglas).
+parent(ebbon, bob).
+
+ancestor(ebbon, bob).
+ancestor(john, douglas).
+
diff --git a/collects/tests/datalog/parse.rkt b/collects/tests/datalog/parse.rkt
new file mode 100644
index 0000000..db86b57
--- /dev/null
+++ b/collects/tests/datalog/parse.rkt
@@ -0,0 +1,52 @@
+#lang racket
+(require rackunit
+         datalog/ast
+         datalog/parse
+         "util.rkt")
+
+(provide parse-tests)
+
+(define (test-literal-parse str res)
+  (test-literal str (parse-literal (open-input-string str)) res))
+(define (test-clause-parse str res)
+  (test-clause str (parse-clause (open-input-string str)) res))
+
+(define parse-tests
+  (test-suite
+   "parse"
+   
+   (test-suite
+    "literal"
+    (test-literal-parse "parent(john, douglas)"
+                        (make-literal #f 'parent (list (make-constant #f 'john) (make-constant #f 'douglas))))
+    (test-literal-parse "1 = 2"
+                        (make-literal #f '= (list (make-constant #f '|1|) (make-constant #f '|2|))))
+    (test-literal-parse "zero-arity-literal"
+                        (make-literal #f 'zero-arity-literal empty))
+    (test-literal-parse "zero-arity-literal()"
+                        (make-literal #f 'zero-arity-literal empty))
+    (test-literal-parse "\"=\"(3,3)"
+                        (make-literal #f "=" (list (make-constant #f '|3|) (make-constant #f '|3|))))
+    (test-literal-parse "\"\"(-0-0-0,&&&,***,\"\00\")"
+                        (make-literal #f "" (list (make-constant #f '-0-0-0)
+                                                  (make-constant #f '&&&)
+                                                  (make-constant #f '***)
+                                                  (make-constant #f "\00")))))
+   
+   (test-suite
+    "clause"
+    (test-clause-parse "parent(john, douglas)"
+                       (make-clause #f (make-literal #f 'parent (list (make-constant #f 'john) (make-constant #f 'douglas))) empty))
+    (test-clause-parse "ancestor(A, B) :- parent(A, B)"
+                       (make-clause #f (make-literal #f 'ancestor (list (make-variable #f 'A) (make-variable #f 'B)))
+                                    (list (make-literal #f 'parent (list (make-variable #f 'A) (make-variable #f 'B))))))
+    (test-clause-parse "ancestor(A, B) :- parent(A, C), ancestor(C, B)"
+                       (make-clause #f (make-literal #f 'ancestor (list (make-variable #f 'A) (make-variable #f 'B)))
+                                    (list (make-literal #f 'parent (list (make-variable #f 'A) (make-variable #f 'C)))
+                                          (make-literal #f 'ancestor (list (make-variable #f 'C) (make-variable #f 'B)))))))
+   
+   (test-suite
+    "statement"
+    (test-not-false "assertion" (assertion? (parse-statement (open-input-string "parent(john, douglas)."))))
+    (test-not-false "retraction" (retraction? (parse-statement (open-input-string "parent(john, douglas)~"))))
+    (test-not-false "query" (query? (parse-statement (open-input-string "parent(john, douglas)?")))))))
\ No newline at end of file
diff --git a/collects/tests/datalog/pretty.rkt b/collects/tests/datalog/pretty.rkt
new file mode 100644
index 0000000..a0fe339
--- /dev/null
+++ b/collects/tests/datalog/pretty.rkt
@@ -0,0 +1,49 @@
+#lang racket
+(require rackunit
+         datalog/parse
+         datalog/pretty)
+(provide pretty-tests)
+
+(define pretty-tests
+  (test-suite
+   "Pretty"
+   
+   (test-equal? "program"
+ (format-program
+  (parse-program
+   (open-input-string #<<END
+parent(john, douglas).
+parent(john, douglas)?
+parent(john, ebbon)?
+parent(bob, john).
+parent(ebbon, bob).
+parent(A, B)?
+parent(john, B)?
+parent(A, A)?
+ancestor(A, B) :- parent(A, B).
+ancestor(A, B) :- 
+ parent(A, C),
+ ancestor(C, B).
+ancestor(A, B)?
+parent(bob, john)~
+parent(A,B)?
+ancestor(A,B)?
+END
+                      )))
+                #<<END
+parent(john, douglas).
+parent(john, douglas)?
+parent(john, ebbon)?
+parent(bob, john).
+parent(ebbon, bob).
+parent(A, B)?
+parent(john, B)?
+parent(A, A)?
+ancestor(A, B) :- parent(A, B).
+ancestor(A, B) :- parent(A, C), ancestor(C, B).
+ancestor(A, B)?
+parent(bob, john)~
+parent(A, B)?
+ancestor(A, B)?
+END
+                )))
\ No newline at end of file
diff --git a/collects/tests/datalog/private/env.rkt b/collects/tests/datalog/private/env.rkt
new file mode 100644
index 0000000..c9f5ad2
--- /dev/null
+++ b/collects/tests/datalog/private/env.rkt
@@ -0,0 +1,22 @@
+#lang racket
+(require rackunit
+         datalog/ast
+         datalog/private/env)
+
+(provide env-tests)
+
+(define t1 (make-constant #f 't1))
+(define t2 (make-constant #f 't2))
+
+(define env-tests
+  (test-suite
+   "env"
+   
+   (test-equal? "default" (lookup (empty-env) 'v) #f)
+   (test-equal? "default" (lookup (empty-env) 'v t1) t1)
+   (test-equal? "extend" (lookup (extend (empty-env) 'v1 t1) 'v1) t1)
+   (test-equal? "extend"
+                (lookup (extend (extend (empty-env) 'v1 t1)
+                                'v1 t1)
+                        'v1)
+                t1)))
\ No newline at end of file
diff --git a/collects/tests/datalog/private/lex.rkt b/collects/tests/datalog/private/lex.rkt
new file mode 100644
index 0000000..6648cfd
--- /dev/null
+++ b/collects/tests/datalog/private/lex.rkt
@@ -0,0 +1,37 @@
+#lang racket
+(require rackunit
+         parser-tools/lex
+         datalog/private/lex)
+
+(provide lex-tests)
+
+(define (test-lexer str tok-name [tok-value str])
+  (define pv (dlexer (open-input-string str)))
+  (define v (position-token-token pv))
+  (test-equal? (format "lexer: ~a: <~a,~a>" str tok-name tok-value)
+               (cons tok-name tok-value)
+               (cons (token-name v) (token-value v))))
+
+(define lex-tests
+  (test-suite
+   "lex"
+   
+   (test-lexer "=" 'EQUAL #f)
+   (test-lexer "?" 'QMARK #f)
+   (test-lexer "~" 'TILDE #f)
+   (test-lexer "." 'DOT #f)
+   (test-lexer ")" 'RPAREN #f)
+   (test-lexer "," 'COMMA #f)
+   (test-lexer "(" 'LPAREN #f)
+   (test-lexer "\"\"" 'STRING "")
+   (test-lexer "\"foo\"" 'STRING "foo")
+   (test-lexer "\"\\\"\"" 'STRING "\"")
+   (test-lexer ":-" 'TSTILE #f)
+   (test-lexer "" 'EOF #f)
+   (test-lexer "Va1_" 'VARIABLE)
+   (test-lexer "val_" 'IDENTIFIER)
+   (test-lexer "912Kadf" 'IDENTIFIER)
+   (test-lexer "    =" 'EQUAL #f)
+   (test-lexer "% 12453\n=" 'EQUAL #f)
+   
+   ))
\ No newline at end of file
diff --git a/collects/tests/datalog/private/subst.rkt b/collects/tests/datalog/private/subst.rkt
new file mode 100644
index 0000000..2dc0a48
--- /dev/null
+++ b/collects/tests/datalog/private/subst.rkt
@@ -0,0 +1,114 @@
+#lang racket
+(require rackunit
+         datalog/private/subst
+         datalog/ast
+         datalog/private/env)
+(require/expose datalog/private/subst (subst-literal shuffle))
+
+(provide subst-tests)
+
+(define (gensym-var? v)
+  (define s (variable-sym v))
+  (not (eq? s (string->symbol (symbol->string s)))))
+
+(define subst-tests
+  (test-suite
+   "subst"
+   
+   (test-suite
+    "subst-term"
+    (test-equal? "con" 
+                 (subst-term (empty-env) (make-constant #f 'v1))
+                 (make-constant #f 'v1))
+    (test-equal? "var def" 
+                 (subst-term (empty-env) (make-variable #f 'v1))
+                 (make-variable #f 'v1))
+    (test-equal? "var" 
+                 (subst-term (extend (empty-env) 'v1 (make-constant #f 'v1)) (make-variable #f 'v1))
+                 (make-constant #f 'v1)))
+   
+   (test-suite
+    "subst-literal"
+    (test-equal? "con"
+                 (subst-literal (empty-env) (make-literal #f 'lit (list (make-constant #f 'v1))))
+                 (make-literal #f 'lit (list (make-constant #f 'v1))))
+    (test-equal? "var def"
+                 (subst-literal (extend (empty-env) 'v1 (make-constant #f 'v1)) (make-literal #f 'lit (list (make-variable #f 'v1))))
+                 (make-literal #f 'lit (list (make-constant #f 'v1))))
+    (test-equal? "var def"
+                 (subst-literal (extend (empty-env) 'v1 (make-constant #f 'v1)) (make-literal #f 'lit (list (make-variable #f 'v1))))
+                 (make-literal #f 'lit (list (make-constant #f 'v1)))))
+   
+   (test-suite
+    "subst-clause"
+    (test-equal? "con"
+                 (subst-clause (empty-env) (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
+                 (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
+    (test-equal? "var def"
+                 (subst-clause (extend (empty-env) 'v1 (make-constant #f 'v1)) 
+                               (make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1))) empty))
+                 (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
+    (test-equal? "var def"
+                 (subst-clause (extend (empty-env) 'v1 (make-constant #f 'v1)) 
+                               (make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1))) empty))
+                 (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
+    
+    (test-equal? "con"
+                 (subst-clause (empty-env) (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) 
+                                                        (list (make-literal #f 'lit (list (make-constant #f 'v1))))))
+                 (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
+                              (list (make-literal #f 'lit (list (make-constant #f 'v1))))))
+    (test-equal? "var def"
+                 (subst-clause (extend (empty-env) 'v1 (make-constant #f 'v1)) 
+                               (make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1))) 
+                                            (list (make-literal #f 'lit (list (make-variable #f 'v1))))))
+                 (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
+                              (list (make-literal #f 'lit (list (make-constant #f 'v1))))))
+    (test-equal? "var def"
+                 (subst-clause (extend (empty-env) 'v1 (make-constant #f 'v1)) 
+                               (make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1)))
+                                            (list (make-literal #f 'lit (list (make-variable #f 'v1))))))
+                 (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
+                              (list (make-literal #f 'lit (list (make-constant #f 'v1)))))))
+   
+   (test-suite
+    "shuffle"
+    (test-equal? "con" 
+                 (shuffle (empty-env) (make-literal #f 'lit (list (make-constant #f 'v1))))
+                 (empty-env))
+    (test-equal? "var" 
+                 (shuffle (extend (empty-env) 'v1 (make-constant #f 'k1)) (make-literal #f 'lit (list (make-variable #f 'v1))))
+                 (extend (empty-env) 'v1 (make-constant #f 'k1)))
+    (test-not-false "var"
+                    (gensym-var? (lookup (shuffle (empty-env)
+                                                  (make-literal #f 'lit (list (make-variable #f 'v1))))
+                                         'v1))))
+   
+   (test-suite
+    "rename-question"
+    (test-equal? "l" (rename-question (make-literal #f 'lit (list (make-constant #f 'v1))))
+                 (make-literal #f 'lit (list (make-constant #f 'v1))))
+    (test-not-false "l"
+                    (gensym-var?
+                     (first
+                      (literal-terms
+                       (rename-question (make-literal #f 'lit (list (make-variable #f 'v1)))))))))
+   
+   (test-suite
+    "rename-clause"
+    (test-equal? "c" (rename-clause (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
+                 (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
+    (test-not-false "c"
+                    (gensym-var? 
+                     (first
+                      (literal-terms
+                       (clause-head 
+                        (rename-clause (make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1))) empty)))))))
+    (test-not-false "c"
+                    (gensym-var? 
+                     (first
+                      (literal-terms
+                       (first
+                        (clause-body
+                         (rename-clause (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
+                                                     (list (make-literal #f 'lit (list (make-variable #f 'v1)))))))))))))))
\ No newline at end of file
diff --git a/collects/tests/datalog/private/unify.rkt b/collects/tests/datalog/private/unify.rkt
new file mode 100644
index 0000000..688c381
--- /dev/null
+++ b/collects/tests/datalog/private/unify.rkt
@@ -0,0 +1,54 @@
+#lang racket
+(require rackunit
+         datalog/ast
+         datalog/private/env
+         datalog/private/unify)
+(require/expose datalog/private/unify (chase))
+
+(provide unify-tests)
+
+(define unify-tests
+  (test-suite
+   "unify"
+   
+   (test-suite
+    "chase"
+    (test-equal? "con" (chase (empty-env) (make-constant #f 'k1))
+                 (make-constant #f 'k1))
+    (test-equal? "var" (chase (empty-env) (make-variable #f 'v1))
+                 (make-variable #f 'v1))
+    (test-equal? "var->con"
+                 (chase (extend (empty-env) 'v1 (make-constant #f 'k1)) (make-variable #f 'v1))
+                 (make-constant #f 'k1))
+    (test-equal? "var->var->con"
+                 (chase (extend (extend (empty-env) 'v2 (make-constant #f 'k1))
+                                'v1 (make-variable #f 'v2))
+                        (make-variable #f 'v1))
+                 (make-constant #f 'k1)))
+   
+   (test-suite
+    "unify-term"
+    (test-equal? "con/con" (unify-term (empty-env) (make-constant #f 'k1) (make-constant #f 'k1))
+                 (empty-env))
+    (test-false "con/con" (unify-term (empty-env) (make-constant #f 'k1) (make-constant #f 'k2)))
+    (test-equal? "var/con" (unify-term (empty-env) (make-variable #f 'v1) (make-constant #f 'k2))
+                 (extend (empty-env) 'v1 (make-constant #f 'k2)))
+    (test-equal? "con/var" (unify-term (empty-env) (make-constant #f 'k2) (make-variable #f 'v1))
+                 (extend (empty-env) 'v1 (make-constant #f 'k2)))
+    (test-equal? "var/var" (unify-term (empty-env) (make-variable #f 'v1) (make-variable #f 'v2))
+                 (extend (empty-env) 'v1 (make-variable #f 'v2))))
+   
+   (test-suite
+    "unify-terms"
+    (test-equal? "con/con" (unify-terms (empty-env) (list (make-constant #f 'k1)) (list (make-constant #f 'k1)))
+                 (empty-env))
+    (test-false "con/con" (unify-terms (empty-env) (list (make-constant #f 'k1)) (list (make-constant #f 'k2))))
+    (test-false "/con" (unify-terms (empty-env) (list) (list (make-constant #f 'k2))))
+    (test-false "con/" (unify-terms (empty-env) (list (make-constant #f 'k2)) (list))))
+   
+   (test-suite
+    "unify"
+    (test-false "lit/lit" (unify (make-literal #f 'lit1 empty) (make-literal #f 'lit2 empty)))
+    (test-equal? "con/con" (unify (make-literal #f 'lit1 (list (make-constant #f 'k1)))
+                                  (make-literal #f 'lit1 (list (make-constant #f 'k1))))
+                 (empty-env)))))
\ No newline at end of file
diff --git a/collects/tests/datalog/private/variant.rkt b/collects/tests/datalog/private/variant.rkt
new file mode 100644
index 0000000..cd1299b
--- /dev/null
+++ b/collects/tests/datalog/private/variant.rkt
@@ -0,0 +1,59 @@
+#lang racket
+(require rackunit
+         datalog/ast
+         datalog/private/variant)
+(require/expose datalog/private/variant
+                (variant-terms variant-term variant-var variant? term-hash mk-literal-hash))
+
+(provide variant-tests)
+
+(define (test-not-equal? n v1 v2)
+  (test-case n (check-not-equal? v1 v2)))
+
+(define variant-tests
+  (test-suite
+   "variant"
+   
+   (test-suite 
+    "variant?"
+    (test-not-false "same" (variant? (make-literal #f 'lit1 empty) (make-literal #f 'lit1 empty)))
+    (test-false "dif lit" (variant? (make-literal #f 'lit1 empty) (make-literal #f 'lit2 empty)))
+    (test-not-false "same" (variant? (make-literal #f 'lit1 (list (make-constant #f 'k1))) 
+                                     (make-literal #f 'lit1 (list (make-constant #f 'k1)))))
+    (test-false "dif con" (variant? (make-literal #f 'lit1 (list (make-constant #f 'k1))) 
+                                    (make-literal #f 'lit1 (list (make-constant #f 'k2)))))
+    (test-false "dif var/con" (variant? (make-literal #f 'lit1 (list (make-variable #f 'v1))) 
+                                        (make-literal #f 'lit1 (list (make-constant #f 'k1)))))
+    (test-false "dif con/var" (variant? (make-literal #f 'lit1 (list (make-constant #f 'k1))) 
+                                        (make-literal #f 'lit1 (list (make-variable #f 'v1)))))
+    (test-not-false "same" (variant? (make-literal #f 'lit1 (list (make-variable #f 'v1))) 
+                                     (make-literal #f 'lit1 (list (make-variable #f 'v1)))))
+    
+    (test-not-false "var (dif name)" (variant? (make-literal #f 'lit1 (list (make-variable #f 'v2))) 
+                                               (make-literal #f 'lit1 (list (make-variable #f 'v1))))))
+   
+   (test-suite
+    "mem-literal"
+    (test-false "mt" (mem-literal (make-literal #f 'lit1 empty) empty))
+    (test-not-false "in" (mem-literal (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty))))
+    (test-not-false "var" (mem-literal (make-literal #f 'lit1 (list (make-variable #f 'v2))) 
+                                       (list (make-literal #f 'lit1 (list (make-variable #f 'v1)))))))
+   
+   (test-suite
+    "term-hash"
+    (test-equal? "var" (term-hash (make-variable #f (gensym)) equal-hash-code) 101)
+    (test-equal? "con" (term-hash (make-constant #f 'v2) equal-hash-code) (equal-hash-code 'v2)))
+   
+   (local [(define literal-hash (mk-literal-hash equal-hash-code))
+           (define (literal-hash-equal? l1 l2)
+             (equal? (literal-hash l1) (literal-hash l2)))]
+     (test-suite
+      "mk-literal-hash"
+      (test-not-false "same" (literal-hash-equal? (make-literal #f 'lit1 empty) (make-literal #f 'lit1 empty)))
+      (test-not-false "same" (literal-hash-equal? (make-literal #f 'lit1 (list (make-constant #f 'k1))) 
+                                                  (make-literal #f 'lit1 (list (make-constant #f 'k1)))))
+      (test-not-false "same" (literal-hash-equal? (make-literal #f 'lit1 (list (make-variable #f 'v1))) 
+                                                  (make-literal #f 'lit1 (list (make-variable #f 'v1)))))
+      
+      (test-not-false "var (dif name)" (literal-hash-equal? (make-literal #f 'lit1 (list (make-variable #f 'v2))) 
+                                                            (make-literal #f 'lit1 (list (make-variable #f 'v1)))))))))
\ No newline at end of file
diff --git a/collects/tests/datalog/racket.rkt b/collects/tests/datalog/racket.rkt
new file mode 100644
index 0000000..f0b78e5
--- /dev/null
+++ b/collects/tests/datalog/racket.rkt
@@ -0,0 +1,84 @@
+#lang racket
+(require datalog tests/eli-tester)
+
+(define parent (make-theory))
+
+(test
+ (datalog parent
+          (! (parent joseph2 joseph1))
+          (! (parent joseph2 lucy))
+          (! (parent joseph3 joseph2)))
+ =>
+ empty
+ 
+ (datalog parent
+          (? (parent X joseph2)))
+ =>
+ (list (hasheq 'X 'joseph3))
+ 
+ (datalog parent
+          (? (parent joseph2 X)))
+ =>
+ (list (hasheq 'X 'joseph1)
+       (hasheq 'X 'lucy))
+ 
+ (datalog parent
+          (? (parent joseph2 X))
+          (? (parent X joseph2)))
+ =>
+ (list (hasheq 'X 'joseph3))
+ 
+ (datalog parent
+          (! (:- (ancestor A B)
+                 (parent A B)))
+          (! (:- (ancestor A B)
+                 (parent A C)
+                 (= D C) ; Unification required
+                 (ancestor D B))))
+ =>
+ empty
+ 
+ (datalog parent
+          (? (ancestor A B)))
+ =>
+ (list (hasheq 'A 'joseph3 'B 'joseph2)
+       (hasheq 'A 'joseph2 'B 'lucy)
+       (hasheq 'A 'joseph2 'B 'joseph1)
+       (hasheq 'A 'joseph3 'B 'lucy)
+       (hasheq 'A 'joseph3 'B 'joseph1))
+ 
+ (let ([x 'joseph2])
+   (datalog parent
+            (? (parent x X))))
+ =>
+ (list (hasheq 'X 'joseph1)
+       (hasheq 'X 'lucy))
+ 
+ (datalog parent
+          (? (add1 1 :- X)))
+ =>
+ (list (hasheq 'X 2))
+ 
+ (local [(local-require tests/datalog/examples/ancestor)]
+   (datalog theory
+            (? (ancestor A B))))
+ =>
+ (list (hasheq 'A 'ebbon 'B 'bob)
+       (hasheq 'A 'bob 'B 'john)
+       (hasheq 'A 'john 'B 'douglas)
+       (hasheq 'A 'bob 'B 'douglas)
+       (hasheq 'A 'ebbon 'B 'john)
+       (hasheq 'A 'ebbon 'B 'douglas))
+ 
+  (local [(local-require tests/datalog/paren-examples/ancestor)]
+   (datalog theory
+            (? (ancestor A B))))
+ =>
+ (list (hasheq 'A 'ebbon 'B 'bob)
+       (hasheq 'A 'bob 'B 'john)
+       (hasheq 'A 'john 'B 'douglas)
+       (hasheq 'A 'bob 'B 'douglas)
+       (hasheq 'A 'ebbon 'B 'john)
+       (hasheq 'A 'ebbon 'B 'douglas))
+ 
+ )
\ No newline at end of file
diff --git a/collects/tests/datalog/runtime.rkt b/collects/tests/datalog/runtime.rkt
new file mode 100644
index 0000000..d68fcdc
--- /dev/null
+++ b/collects/tests/datalog/runtime.rkt
@@ -0,0 +1,44 @@
+#lang racket
+(require rackunit
+         datalog/parse
+         datalog/runtime
+         "util.rkt")
+
+(provide runtime-tests)
+
+(define pc (parse-clause (open-input-string "parent(john, douglas)")))
+(define pl (parse-literal (open-input-string "parent(john, douglas)")))
+
+(define runtime-tests
+  (test-suite
+   "runtime"
+   
+   (test-suite
+    "safe-clause?"
+    (test-not-false "safe" (safe-clause? pc))
+    (test-not-false "safe" (safe-clause? (parse-clause (open-input-string "ancestor(A, B) :- parent(A, B)"))))
+    (test-false "not safe" (safe-clause? (parse-clause (open-input-string "ancestor(A, B) :- parent(jay, B)"))))
+    (test-not-false "safe" (safe-clause? (parse-clause (open-input-string "ancestor(A, B) :- parent(A, C), ancestor(C, B)")))))
+   
+   (test-suite
+    "mut simple"
+    (test-equal? "empty" (prove (make-theory) pl) empty)
+    (test-literal "ass->prov" 
+                  (let ([thy (make-theory)])
+                    (assume! thy pc)
+                    (first (prove thy pl)))
+                  pl)
+    (test-equal? "ass->ret->prov" 
+                 (let ([thy (make-theory)])
+                   (assume! thy pc)
+                   (retract! thy pc)
+                   (prove thy pl))
+                 empty)
+    (test-equal? "ret->prov" 
+                 (let ([thy (make-theory)])
+                   (retract! thy pc)
+                   (prove thy pl))
+                 empty))
+   
+   ))
+
diff --git a/collects/tests/datalog/tool/syntax-color.rkt b/collects/tests/datalog/tool/syntax-color.rkt
new file mode 100644
index 0000000..6b48bb8
--- /dev/null
+++ b/collects/tests/datalog/tool/syntax-color.rkt
@@ -0,0 +1,37 @@
+#lang racket
+(require rackunit
+         datalog/tool/syntax-color)
+
+(provide syntax-color-tests)
+
+(define (test-color str key)
+  (define-values (lex color b start end) (get-syntax-token (open-input-string str)))
+  (test-equal? (format "Syntax Color: ~a: ~a" key str) color key))
+
+(define syntax-color-tests
+  (test-suite
+   "syntax-color"
+   
+   (test-color " " 'whitespace)
+   (test-color "   " 'whitespace)
+   (test-color "\t" 'whitespace)
+   (test-color "\n" 'whitespace)
+   (test-color "% \n" 'comment)
+   (test-color "% 12 31 2 6\n" 'comment)
+   (test-color "Var" 'symbol)
+   (test-color "V124_3" 'symbol)
+   (test-color "var" 'identifier)
+   (test-color "123var" 'identifier)
+   (test-color "(" 'parenthesis)
+   (test-color ")" 'parenthesis)
+   (test-color "=" 'parenthesis)
+   (test-color "?" 'parenthesis)
+   (test-color "~" 'parenthesis)
+   (test-color "." 'parenthesis)
+   (test-color "," 'parenthesis)
+   (test-color ":-" 'parenthesis)
+   (test-color "\"foo\"" 'string)
+   (test-color "\"fo\\\"o\"" 'string)
+   (test-color "\"fo\no\"" 'string)
+   (test-color "\"foo" 'error)
+   (test-color ":" 'error)))
\ No newline at end of file
diff --git a/collects/tests/datalog/util.rkt b/collects/tests/datalog/util.rkt
new file mode 100644
index 0000000..581c80c
--- /dev/null
+++ b/collects/tests/datalog/util.rkt
@@ -0,0 +1,12 @@
+#lang racket
+(require rackunit
+         datalog/ast)
+
+(provide test-literal test-clause)
+
+(define (test-literal str l1 l2)
+  (test-case 
+   str (check literal-equal? l1 l2)))
+(define (test-clause str c1 c2)
+  (test-case 
+   str (check clause-equal? c1 c2)))
diff --git a/collects/tests/racklog/lang/laps.txt b/collects/tests/racklog/lang/laps.txt
new file mode 100644
index 0000000..d87ea5f
--- /dev/null
+++ b/collects/tests/racklog/lang/laps.txt
@@ -0,0 +1,2 @@
+permit(rams, store, rams_couch).
+permit(will, fetch, rams_couch).
diff --git a/collects/tests/racklog/lang/long.txt b/collects/tests/racklog/lang/long.txt
new file mode 100644
index 0000000..ebf5669
--- /dev/null
+++ b/collects/tests/racklog/lang/long.txt
@@ -0,0 +1 @@
+this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer.
diff --git a/collects/tests/racklog/lang/says.txt b/collects/tests/racklog/lang/says.txt
new file mode 100644
index 0000000..473484a
--- /dev/null
+++ b/collects/tests/racklog/lang/says.txt
@@ -0,0 +1 @@
+says(tpme1, m1).
diff --git a/collects/tests/racklog/lang/true.txt b/collects/tests/racklog/lang/true.txt
new file mode 100644
index 0000000..48eb7ed
--- /dev/null
+++ b/collects/tests/racklog/lang/true.txt
@@ -0,0 +1 @@
+true.