diff --git a/collects/plai/datatype.ss b/collects/plai/datatype.ss
new file mode 100644
index 0000000000..a5480e578a
--- /dev/null
+++ b/collects/plai/datatype.ss
@@ -0,0 +1,10 @@
+
+(module datatype mzscheme
+  (require "private/datatype.ss")
+
+  (define-type-case type-case else)
+  
+  (provide type-case
+	   define-type
+	   provide-type))
+
diff --git a/collects/plai/doc.txt b/collects/plai/doc.txt
new file mode 100644
index 0000000000..4c901032fb
--- /dev/null
+++ b/collects/plai/doc.txt
@@ -0,0 +1,134 @@
+
+The _Programming Languages: Application and Interpretations_ languages
+are companion to the textbook, and to the _CS173_ class at Brown university.
+
+In the language dialog box, you will find the four _PLAI_ language:
+
+      PLAI - Beginning Student
+      PLAI - Intermediate Student with lambda
+      PLAI - Advanced Student
+      PLAI - Pretty Big
+
+This language sequence follows the same progression as the book "How
+to Design Programs" (htdp). If you are learning Scheme with the book
+while taking the class, the PLAI languages will provide the same
+support as the htdp languages. Namely, at each language level the
+error messages you receive are explained in term of the constructs you
+know so far, and are tailored to address the common errors done at that
+level.
+
+The PLAI languages provide constructs that are essential to the
+coding style prescribed in the class:
+
+ - Lists are only for holding multiple elements of the same type. Use
+   DEFINE-TYPE and TYPE-CASE to group elements of different types.
+
+ - All functions must have tests that exercise non-trivial cases. Use
+   TEST, TEST/PRED and TEST/EXN (below) to create a persistent
+   collection of tests for your code.
+
+
+> (define-type id (variant-id (field-id predicate-expr) ...) ...)
+
+  Defines the datatype ID and a function ID? that returns true for
+  instances of the datatype, and false for any other value. Here, the
+  name ID? means the given name ID, with an added question mark.
+
+  For each VARIANT-ID, a constructor VARIANT-ID is defined.  The
+  constructor takes as many arguments as the variant's FIELD-ID's, and
+  returns and instance of this datatype. Each argument to the
+  constructor is checked by applying the function produced by the
+  variant's PREDICATE-EXPR. DEFINE-TYPE can also use contracts as
+  defined in (lib "contract.ss"), instead of predicates.
+
+  The instance constructed by the VARIANT-ID can be deconstructed
+  using TYPE-CASE. Also, for each VARIANT-ID, DEFINE-TYPE also provide
+  functions that accesses the individual fields, and a predicate
+  VARIANT-ID? which recognizes instances of that particular variant.
+  
+
+
+> (type-case datatype-id expr (variant-id (field-id ...) result-expr ...) ...)
+> (type-case datatype-id expr (variant-id (field-id ...) result-expr ...) ... (else else-expr ...))
+
+  Branches on the datatype instance produced by EXPR, which must be
+  an instance of the specified DATATYPE-ID (previously defined with
+  DEFINE-DATATYPE). Each clause pattern automatically extract the
+  values stored in the fields of the structure. It binds the extracted
+  values them to the names FIELD-IDs in the order that the
+  fields were declared in the corresponding definition in the
+  define-datatype.
+
+  TYPE-CASE will complains if you do not handle all the variants in a
+  datatype. You can use the ELSE keyword as the last clause of a CASES
+  to create a catch-all clause. In that case, variants which are not
+  handled by the other clauses will trigger the evaluation of the
+  ELSE-EXPR.
+
+  If it should not be possible to reach the else clause according to
+  the logic of your program, your ELSE-EXPR should be a call to
+  ERROR, which will raise an exception. For example:
+
+       (cases shape a-circle
+              [circle (c r) (* pi (sqr r))]
+              [else (error "expected a circle!")])
+
+> (test result expected-value)
+
+  Compares the result of a test expression to the expected value, and
+  return a list of three elements: the first element is the symbol
+  'good (if the test passed) or 'bad (if the test failed), the second
+  element is the result, and the third element is the expected value.
+
+> (test/pred result predicate)
+
+  Applies the predicate to the result, and return a list of three
+  elements: the first element is the symbol 'good (if the predicate
+  returned true), or 'bad (if the predicate returned false), the
+  second element is the result, and the third element is the expected
+  values.
+
+> (test/exn (lambda () expression) expected-error-message)
+
+  Evaluates the expression expecting an exception. This is useful to
+  verify that your program correctly detects error conditions. If the
+  expression does not raise an exception, TEST/PRED returns the list:
+
+      (list 'bad result expected-error-message)
+ 
+  If the evaluation of the expression did throw an exception, TEST/PRED
+  will pattern match the error message against the
+  expected-error-message, and return 'bad if the error was not the
+  expected error. EXPECTED-ERROR-MESSAGE should be a few words from
+  the expected error message. For example:
+
+     (text/exn (lambda () (/ 3 0)) "by zero") 
+
+  evaluates to:
+
+     (list 'good #(struct:exn) "by zero")
+
+> (print-tests false|true|'good|'bad|'stop)
+
+  PRINT-TESTS controls printing of test by TEST, TEST/PRED and TEST/EXN.
+  You can pass one of five values to PRINT-TESTS:
+
+     false   Test result are not printed, they are simply returned.  The
+             results of tests evaluated at the top-level will be
+             printed by DrScheme in the interaction panel, as usual. 
+             (this is the default)
+      
+     true    all test results are printed
+
+     'good   only successful test results are printed
+
+     'bad    only failed test results are printed
+
+     'stop   testing will stops at the first test that fails, by throwing
+             an exn:test exception.
+
+> (test-inexact-epsilon number)
+
+  Sets the precision used by TEST to check the correctness of inexact
+  numbers. By default, floating-point results are considered correct
+  if they fall within 0.01 from their the expected value.
diff --git a/collects/plai/info.ss b/collects/plai/info.ss
new file mode 100644
index 0000000000..1e23d3cd1b
--- /dev/null
+++ b/collects/plai/info.ss
@@ -0,0 +1,6 @@
+(module info (lib "infotab.ss" "setup")
+  (define name "PLAI")
+  (define doc.txt "doc.txt")
+  (define tools (list "plai-tool.ss"))
+  (define tool-names (list "Programming Languages: Application and Interpretation"))
+  (define tool-urls (list "http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/")))
diff --git a/collects/plai/plai-advanced.ss b/collects/plai/plai-advanced.ss
new file mode 100644
index 0000000000..5257c09e08
--- /dev/null
+++ b/collects/plai/plai-advanced.ss
@@ -0,0 +1,20 @@
+(module plai-advanced mzscheme
+  (require (rename (lib "htdp-advanced.ss" "lang") plai-else else)
+	   "private/datatype.ss"
+           "test-harness.ss")
+
+  ;; This macro requires & provides bindings without
+  ;;  making them locally visible:
+  (define-syntax (provide-advanced stx)
+    #'(begin
+	(require (lib "htdp-advanced.ss" "lang"))
+	(provide (all-from-except (lib "htdp-advanced.ss" "lang")
+				  plai-else))))
+  (provide-advanced)
+		   
+  (provide (rename advanced-type-case type-case)
+	   define-type
+	   require provide provide-type
+           (all-from "test-harness.ss"))
+
+  (define-type-case advanced-type-case plai-else))
diff --git a/collects/plai/plai-beginner.ss b/collects/plai/plai-beginner.ss
new file mode 100644
index 0000000000..b95f543fe1
--- /dev/null
+++ b/collects/plai/plai-beginner.ss
@@ -0,0 +1,71 @@
+(module plai-beginner mzscheme
+  (require (rename (lib "htdp-beginner.ss" "lang") plai-else else)
+	   (lib "prim.ss" "lang")
+	   "private/datatype.ss"
+	   "private/datatype-core.ss"
+           "test-harness.ss")
+
+  ;; This macro requires & provides bindings without
+  ;;  making them locally visible:
+  (define-syntax (provide-beginner stx)
+    #'(begin
+	(require (lib "htdp-beginner.ss" "lang"))
+	(provide (all-from-except (lib "htdp-beginner.ss" "lang")
+				  plai-else))))
+  (provide-beginner)
+		   
+  (provide (rename beginner-type-case type-case)
+	   (rename beginner-define-type define-type)
+	   require provide provide-type
+           (all-from "test-harness.ss"))
+
+  (define-syntax (name-it stx)
+    (syntax-case stx ()
+      [(_ id expr)
+       (identifier? #'id)
+       #'(let ([id expr]) id)]
+      [(_ non-id expr)
+       #'expr]))
+
+  ;; For beginner, `define-type' requires predicates for
+  ;;  contracts, and it doesn't define contracts
+  (define-syntax (beginner-define-type stx)
+    (syntax-case stx (represented-as)
+      [(_ name (variant (field predicate) ...) ...)
+       (let ([name #'name])
+	 (unless (identifier? name)
+	   (raise-syntax-error
+	    #f
+	    "expected an identifier for the type name"
+	    stx
+	    name))
+	 (with-syntax ([orig-stx stx]
+		       [name name]
+		       [name? (datum->syntax-object name
+						    (string->symbol
+						     (format "~a?" (syntax-e name))))])
+	   #'(define-datatype-core orig-stx
+	       (define-selectors define-predicates (kind "type"))
+	       define-proc-values
+	       name () name?
+	       (variant (field (name-it predicate (lambda (x) (predicate x)))) ...)
+	       ...)))]
+      ;; If the above pattern doesn't match, let `define-type' handle the syntax errors:
+      [(_ name-stx . variants)
+       (identifier? #'name-stx)
+       #'(define-type name-stx . variants)]
+      [(_ . __)
+       (raise-syntax-error
+	#f
+	"expected an identifier for the type name"
+	stx)]))
+
+  (define-syntax (define-proc-values stx)
+    (syntax-case stx ()
+      [(_ (id ...) expr)
+       (with-syntax ([(alt-id ...) (generate-temporaries #'(id ...))])
+	 #'(begin
+	     (define-values (alt-id ...) expr)
+	     (define-primitive id alt-id) ...))]))
+
+  (define-type-case beginner-type-case plai-else))
diff --git a/collects/plai/plai-intermediate.ss b/collects/plai/plai-intermediate.ss
new file mode 100644
index 0000000000..b60bd764f3
--- /dev/null
+++ b/collects/plai/plai-intermediate.ss
@@ -0,0 +1,20 @@
+(module plai-intermediate mzscheme
+  (require (rename (lib "htdp-intermediate-lambda.ss" "lang") plai-else else)
+	   "private/datatype.ss"
+           "test-harness.ss")
+
+  ;; This macro requires & provides bindings without
+  ;;  making them locally visible:
+  (define-syntax (provide-intermediate stx)
+    #'(begin
+	(require (lib "htdp-intermediate-lambda.ss" "lang"))
+	(provide (all-from-except (lib "htdp-intermediate-lambda.ss" "lang")
+				  plai-else))))
+  (provide-intermediate)
+		   
+  (provide (rename intermediate-type-case type-case)
+	   define-type
+	   require provide provide-type
+           (all-from "test-harness.ss"))
+
+  (define-type-case intermediate-type-case plai-else))
diff --git a/collects/plai/plai-pretty-big.ss b/collects/plai/plai-pretty-big.ss
new file mode 100644
index 0000000000..f5dfaff786
--- /dev/null
+++ b/collects/plai/plai-pretty-big.ss
@@ -0,0 +1,18 @@
+(module plai-pretty-big mzscheme
+  (require "private/datatype.ss"
+           "test-harness.ss")
+
+  ;; This macro requires & provides bindings without
+  ;;  making them locally visible:
+  (define-syntax (provide-advanced stx)
+    #'(begin
+	(require (lib "plt-pretty-big.ss" "lang"))
+	(provide (all-from (lib "plt-pretty-big.ss" "lang")))))
+  (provide-advanced)
+		   
+  (provide (rename pretty-big-type-case type-case)
+	   define-type
+	   provide-type
+           (all-from "test-harness.ss"))
+
+  (define-type-case pretty-big-type-case else))
diff --git a/collects/plai/plai-reader.ss b/collects/plai/plai-reader.ss
new file mode 100644
index 0000000000..9f4d008b00
--- /dev/null
+++ b/collects/plai/plai-reader.ss
@@ -0,0 +1,17 @@
+(module plai-reader mzscheme
+  (require (lib "etc.ss"))
+
+  (provide (rename plai-read-syntax read-syntax))
+
+  (define (read-syntax/namespace-introduce . args)
+    (let ([v (apply read-syntax args)])
+      (if (syntax? v)
+          (namespace-syntax-introduce v)
+          v)))
+  
+  (define (plai-read-syntax . args)
+    (parameterize ([read-case-sensitive #t])
+      (apply read-syntax/namespace-introduce args)))
+
+
+  )
\ No newline at end of file
diff --git a/collects/plai/plai-tool.ss b/collects/plai/plai-tool.ss
new file mode 100644
index 0000000000..77389cf548
--- /dev/null
+++ b/collects/plai/plai-tool.ss
@@ -0,0 +1,86 @@
+
+#|
+
+The PLAI languages can almost be specified via info.ss fields, but
+the default printing style shold be 'constructor instead of 'write
+
+|#
+
+(module plai-tool mzscheme
+  (require (lib "unitsig.ss")
+	   (lib "class.ss")
+	   (lib "struct.ss")
+	   (lib "tool.ss" "drscheme")
+           (lib "string-constant.ss" "string-constants"))
+  
+  (provide tool@)
+
+  (define tool@
+    (unit/sig drscheme:tool-exports^
+      (import drscheme:tool^)
+
+      (define (add-language! modname lang langnum summary)
+	(define base%
+	  (class* object% (drscheme:language:simple-module-based-language<%>)
+	    (define/public (get-language-numbers)
+	      langnum)
+	    (define/public (get-language-position)
+	      (list (string-constant teaching-languages)
+		    "Programming Languages: Application and Interpretation"
+		    lang))
+	    (define/public (get-module)
+	      modname)
+	    (define/public (get-one-line-summary)
+	      summary)
+	    (define/public (get-language-url)
+	      "http://www.cs.brown.edu/~sk/Publications/Books/ProgLangs/")
+	    (define/public (get-reader)
+	      (lambda (src port)
+		(let ([v (read-syntax src port)])
+		  (if (eof-object? v)
+		      v
+		      (namespace-syntax-introduce v)))))
+	    (super-instantiate ())))
+	(drscheme:language-configuration:add-language 
+	 (make-object 
+	  ((drscheme:language:get-default-mixin)
+	   (class (drscheme:language:module-based-language->language-mixin
+		   (drscheme:language:simple-module-based-language->module-based-language-mixin
+		    base%))
+	     (define/override (use-namespace-require/copy?) #t)
+	     
+	     ;; Change print style in default settings from 'write to 'constructor:
+	     (define/override (default-settings)
+	       (let ([s (super default-settings)])
+		 (to-style s 'constructor)))
+	     (define/override (default-settings? s)
+	       (and (eq? (drscheme:language:simple-settings-printing-style s) 'constructor)
+		    (super default-settings? (to-style s 'write))))
+
+	     (define/private (to-style s v)
+	       (drscheme:language:make-simple-settings
+		(drscheme:language:simple-settings-case-sensitive s)
+		v
+		(drscheme:language:simple-settings-fraction-style s)
+		(drscheme:language:simple-settings-show-sharing s)
+		(drscheme:language:simple-settings-insert-newlines s)
+		(drscheme:language:simple-settings-annotations s)))
+	     
+	     (super-instantiate ()))))))
+
+      (define (phase1) (void))
+      (define (phase2)
+	(map add-language! 
+	     '((lib "plai-beginner.ss" "plai") 
+	       (lib "plai-intermediate.ss" "plai") 
+	       (lib "plai-advanced.ss" "plai")
+	       (lib "plai-pretty-big.ss" "plai"))
+	     '("PLAI - Beginning Student"
+	       "PLAI - Intermediate Student with lambda"
+	       "PLAI - Advanced Student"
+	       "PLAI - Pretty Big")
+	     '((-500 0 0) (-500 0 1) (-500 0 3) (-500 0 4))
+	     '("PLAI: beginning students"
+	       "PLAI: beginner plus lexical scope and higher-order functions" 
+	       "PLAI: intermediate plus lambda and mutation"
+	       "PLAI: professional plt plus define-datatype"))))))
diff --git a/collects/plai/private/core-utils.ss b/collects/plai/private/core-utils.ss
new file mode 100644
index 0000000000..9020c62c46
--- /dev/null
+++ b/collects/plai/private/core-utils.ss
@@ -0,0 +1,27 @@
+
+(module core-utils mzscheme
+
+  (define-values (struct:dt make-dt dt? dt-selector dt-accessor)
+    (make-struct-type 'dt #f 3 0 #f null (current-inspector)	       
+		      (lambda (dt stx)
+			(raise-syntax-error
+			 #f
+			 (format "illegal use of ~a name" (dt-kind dt))
+			 stx))))
+  (define dt-pred-stx (make-struct-field-accessor dt-selector 0 'pred-stx))
+  (define dt-variants (make-struct-field-accessor dt-selector 1 'variants))
+  (define dt-kind (make-struct-field-accessor dt-selector 2 'kind))
+		  
+  (define-struct vt (name-stx predicate-stx accessor-stx selector-stxes field-count))
+  
+  ;; Helper function:
+  (define (variant-assq name-stx variants)
+    (let loop ([l variants])
+      (if (module-identifier=? name-stx 
+			       (vt-name-stx (car l)))
+	  (car l)
+	  (loop (cdr l)))))
+  
+  (provide make-dt dt? dt-pred-stx dt-variants
+	   (struct vt (name-stx predicate-stx accessor-stx selector-stxes field-count))
+	   variant-assq))
diff --git a/collects/plai/private/datatype-core.ss b/collects/plai/private/datatype-core.ss
new file mode 100644
index 0000000000..99e5b1e68d
--- /dev/null
+++ b/collects/plai/private/datatype-core.ss
@@ -0,0 +1,529 @@
+
+;; Shared infrastructure for define-type and define-datatype (eventually)
+
+;; NOTE: datatypes are currently transparent. This works with EoPL's
+;; use of `equal?', and also makes constructor-style printing show
+;; all fields.
+
+(module datatype-core mzscheme
+  (require (lib "pconvert-prop.ss")
+	   (lib "contract.ss" "mzlib" "private"))
+  (require-for-syntax "core-utils.ss")
+
+  (provide define-datatype-core
+	   cases-core
+	   provide-datatype-core)
+
+  (define (projection-contract name proc)
+    (let ([name `(,(car name) ,@(map (lambda (c)
+				       (if (contract? c)
+					   (contract-name c)
+					   (or (object-name c)
+					       c)))
+				     (cdr name)))])
+      (make-contract name
+		     (lambda (pos neg src-info orig-str)
+		       (let ([proc (proc pos neg src-info orig-str)])
+			 (lambda (v)
+			   (let ([v2 (proc v)])
+			     (unless v2
+			       (raise-contract-error
+				src-info
+				pos
+				neg
+				orig-str
+				"expected <~a>, given: ~e"
+				name
+				v))
+			     v2)))))))
+
+  (define (dt-contract-proc c)
+    (contract-proc
+     (if (contract? c)
+	 c
+	 (flat-contract c))))
+
+  ;; Syntax:
+  ;;   (define-datatype-core orig-form d-v (option ...) name (alpha ...) pred-name variant ...)
+  ;; where the syntax is like `define-datatype' starting with `pred-name'.
+  ;; The `orig-stx' part is used for syntax-error reporting.
+  ;; The `d-v' is used in place of `define-values' to binding procedures.
+  ;; Each `alpha' is a parameter to the contract expressions of each variant field;
+  ;;   using `x-of' for variant `x' allows the parameter contracts to be supplied, 
+  ;;   while using `x' directly instantiates each parameter as `any/c'.
+  ;; The syntax for each `variant' is checked here; perform other syntax
+  ;;  checks before using `define-datatype-core'.
+  ;; The valid options are:
+  ;;   define-predicates : include `x?' for each variant `x'
+  ;;   define-selectors : include `x-f' for each field `f' of each variant `x'
+  ;;   define-polymorphic : include a definition of `x-of' for each variant `x'
+  ;;   define-contracts : include a definition of `x-of/c' for each variant `x'
+  ;;                      requires define-selectors
+  ;;   define-compatibility: include `make-x' for each variant `x'
+  ;;   (kind "str") : uses "str" to name the result, either "type" or "datatype"
+  (define-syntax define-datatype-core
+    (lambda (stx)
+      (syntax-case stx ()
+	[(_ orig-stx (option ...) define-proc-values name (alpha ...) pred-name 
+	    (variant-name (field-name field-pred) ...) 
+	    ...)
+	 (let ([stx #'orig-stx]
+	       [options (syntax-object->datum #'(option ...))]
+	       [variant-names (syntax->list (syntax (variant-name ...)))]
+	       [field-nameses (map syntax->list
+				   (syntax->list (syntax ((field-name ...) ...))))])
+	   ;; More syntax checks...
+	   (unless (identifier? (syntax name))
+	     (raise-syntax-error #f
+				 "expected an identifier for the datatype name"
+				 stx (syntax name)))
+	   (unless (identifier? (syntax pred-name))
+	     (raise-syntax-error #f
+				 "expected an identifier for the predicate name"
+				 stx (syntax pred-name)))
+	   (for-each (lambda (vt fields)
+		       (unless (identifier? vt)
+			 (raise-syntax-error 
+			  #f
+			  "expected an identifier for the variant name"
+			  stx vt))
+		       (for-each (lambda (field)
+				   (unless (identifier? field)
+				     (raise-syntax-error 
+				      #f
+				      "expected an identifier for the field name"
+				      stx field)))
+				 fields))
+		     variant-names
+		     field-nameses)
+	   ;; Count the fields for each variant:
+	   (with-syntax ([(variant-field-count ...) 
+			  (map (lambda (n) 
+				 (datum->syntax-object (quote-syntax here) n #f))
+			       (map length field-nameses))]
+			 [(variant-name/no-contract ...)
+			  (generate-temporaries variant-names)]
+                         [(variant-of ...)
+			  (map (lambda (variant-name) 
+				 (datum->syntax-object variant-name
+						       (string->symbol
+							(format "~a-of" (syntax-e variant-name)))))
+			       variant-names)]
+			 [(variant-of/c ...)
+			  (map (lambda (variant-name) 
+				 (datum->syntax-object variant-name
+						       (string->symbol
+							(format "~a-of/c" (syntax-e variant-name)))))
+			       variant-names)]
+                         [type-of/c (datum->syntax-object #'name
+							  (string->symbol
+							   (format "~a-of/c" (syntax-e #'name))))]
+                         [(variant? ...)
+                          (map (lambda (vn)
+                                 (datum->syntax-object
+                                  vn
+                                  ((if (memq 'define-predicates options) string->symbol string->uninterned-symbol)
+                                   (format "~a?" (syntax-e vn)))))
+                               variant-names)]
+                         [(variant-accessor ...)
+                          (map (lambda (vn)
+                                 (datum->syntax-object
+                                  vn
+                                  (string->uninterned-symbol
+                                   (format "~a-accessor" (syntax-e vn)))))
+                               variant-names)]
+			 [(variant-mutator ...)
+                          (generate-temporaries variant-names)]
+                         [(make-variant ...)
+                          (generate-temporaries variant-names)]
+                         [(struct:variant ...)
+                          (generate-temporaries variant-names)]
+			 [((selector-name ...) ...)
+			  (map (lambda (variant-name field-names)
+				 (if (memq 'define-selectors options)
+				     (map (lambda (field-name)
+					    (datum->syntax-object
+					     variant-name
+					     (string->symbol
+					      (format "~a-~a" 
+						      (syntax-e variant-name)
+						      (syntax-e field-name)))))
+					  field-names)
+				     null))
+			       variant-names
+			       field-nameses)]
+			 [((sub-contract-proc ...) ...)
+			  (map (lambda (field-names)
+				 (generate-temporaries field-names))
+			       field-nameses)]
+			 [((field-pos ...) ...)
+			  (map (lambda (field-names)
+				 (let loop ([l field-names][i 0])
+				   (if (null? l)
+				       null
+				       (cons i (loop (cdr l) (add1 i))))))
+			       field-nameses)]
+                         [(make-variant-name ...)
+                          (map (lambda (vn)
+                                 (datum->syntax-object
+                                  vn
+                                  (string->symbol
+                                   (format "make-~a" (syntax-e vn)))))
+                               variant-names)]
+			 [datatype-str (or (ormap (lambda (option)
+						    (and (pair? option)
+							 (eq? 'kind (car option))
+							 (cadr option)))
+						  options)
+					   "datatype")])
+	     (quasisyntax
+	      (begin
+		(define-syntax name 
+		  ;; Note: we're back to the transformer environment, here.
+		  ;; Also, this isn't a transformer function, so any direct
+		  ;;  use of the name will trigger a syntax error. The name
+		  ;;  can be found by `syntax-local-value', though.
+		  (let ([cert (syntax-local-certifier)])
+		    (make-set!-transformer
+		     (make-dt (cert (syntax pred-name))
+			      (list
+			       (make-vt (cert (quote-syntax variant-name))
+					(cert (quote-syntax variant?))
+					(cert (quote-syntax variant-accessor))
+					(list (quote-syntax selector-name) ...)
+					variant-field-count)
+			       ...)
+			      datatype-str))))
+		;; Bind the predicate and selector functions:
+		(define-proc-values (pred-name
+				     variant-name/no-contract ...
+				     variant? ...
+				     variant-accessor ...
+				     selector-name ... ...
+				     variant-name ...)
+		  ;; Create a new structure for the datatype (using the
+		  ;; datatype name in `struct', so it prints nicely).
+		  (let-values ([(struct:x make-x x? acc mut)
+				(make-struct-type 'name #f 0 0 #f null (make-inspector))])
+                    (let-values ([(struct:variant make-variant variant? 
+                                                  variant-accessor variant-mutator)
+                                  (make-struct-type 'variant-name struct:x variant-field-count 0
+                                                    #f 
+						    `((,prop:print-convert-constructor-name . variant-name))
+						    (make-inspector))]
+                                 ...)
+		      (let-values #,(if (memq 'define-selectors options)
+					#`([(selector-name ...)
+					    (let ([accessor variant-accessor])
+					      (values (make-struct-field-accessor accessor field-pos 'field-name)
+						      ...))]
+					   ...)
+					())
+			;; User-available functions:
+			(values
+			 x? ;; The datatype predicate
+			 ;; Rename the constructor:
+			 make-variant ...
+			 variant? ...
+			 variant-accessor ...
+			 selector-name ... ...
+			 ;; Constructors:
+			 (let ([f (delay (contract (let ([alpha any/c] ...) (-> field-pred ... x?))
+						   make-variant
+						   'definition 'use (quote-syntax variant-name)))])
+			   (let ([variant-name (lambda (field-name ...) ((force f) field-name ...))])
+			     variant-name))
+			 ...)))))
+		#,@(if (memq 'define-contracts options)
+		       #`((define (type-of/c alpha ...)
+			    (projection-contract
+			     `(type-of/c ,alpha ...)
+			     (lambda (pos neg src-info orig-str)
+			       (let ([sub-contract-proc (delay
+							  ((dt-contract-proc field-pred) pos neg src-info orig-str))]
+				     ... ...)
+				 (lambda (x)
+				   (and (pred-name x)
+					(or (and (variant? x)
+						 (variant-name/no-contract
+						  ((force sub-contract-proc) (selector-name x)) ...))
+					    ...)))))))
+			  (define (variant-of/c alpha ...)
+			    (projection-contract
+			     `(variant-of/c ,alpha ...)
+			     (lambda (pos neg src-info orig-str)
+			       (let ([sub-contract-proc (delay
+							  ((dt-contract-proc field-pred) pos neg src-info orig-str))]
+				     ...)
+				 (lambda (x)
+				   (and (variant? x)
+					(variant-name/no-contract
+					 ((force sub-contract-proc) (selector-name x)) ...)))))))
+			  ...)
+		       null)
+		#,@(if (memq 'define-polymorphic options)
+		       #`((define (variant-of alpha ...)
+			    (let ([f (contract (-> field-pred ... pred-name)
+					       variant-name/no-contract
+					       'definition 'use (quote-syntax variant-name))])
+			      (let ([variant-name (lambda (field-name ...)
+						    (f field-name ...))])
+				variant-name)))
+			  ...)
+		       null)
+		;; Compatibility bindings
+		#,@(if (memq 'define-compatibility options)
+		      #`((define-proc-values (make-variant-name ...) (values variant-name ...)))
+		      null)))))]
+        [(_ orig-stx (option ...) name pred-name variant ...)
+         ;; Must be a bad variant...
+         (for-each (lambda (variant)
+                     (syntax-case variant ()
+                       [(variant-name field ...)
+                        (let ([name (syntax variant-name)])
+                          (unless (identifier? name)
+                            (raise-syntax-error
+                             #f
+                             "expected an identifier for the variant name"
+                             #'orig-stx
+                             name))
+                          ;; Must be a bad field:
+                          (for-each (lambda (field)
+                                      (syntax-case field ()
+                                        [(field-name field-pred)
+                                         (let ([name (syntax field-name)])
+                                           (unless (identifier? name)
+                                             (raise-syntax-error
+                                              #f
+                                              "expected an identifier for the field name"
+                                              #'orig-stx
+                                              name)))]
+                                        [_else
+                                         (raise-syntax-error
+                                          #f
+                                          "expected a field name followed by a predicate expression, all in parentheses"
+                                          #'orig-stx
+                                          field)]))
+                                    (syntax->list (syntax (field ...)))))]
+                       [_else
+                        (raise-syntax-error
+                         #f
+                         "expected a variant name followed by a sequence of field declarations, all in parentheses"
+                         #'orig-stx
+                         variant)]))
+                   (syntax->list (syntax (variant ...))))]
+	[(_ orig_stx . __)
+	 ;; trigger "bad syntax" error:
+	 (syntax-case #'orig-stx ())])))
+
+  (define-for-syntax (lookup-datatype datatype)
+    (let ([v (and (identifier? datatype)
+		  (syntax-local-value datatype (lambda () #f)))])
+      (and v
+	   (set!-transformer? v)
+	   (set!-transformer-procedure v))))
+
+  (define-syntax cases-core
+    (lambda (stx)
+      (syntax-case stx ()
+	[(_ orig-stx datatype-str cases-else
+	    datatype expr 
+	    clause
+	    ...)
+	 ;; Get datatype information:
+	 (let ([stx #'orig-stx]
+	       [dt (lookup-datatype #'datatype)])
+	   (unless (dt? dt)
+	     (raise-syntax-error 
+	      #f
+	      (format "not a ~a name" (syntax-e #'datatype-str))
+	      stx
+	      (syntax datatype)))
+	   
+	   ;; Parse clauses:
+	   (let-values ([(vts field-idss bodys else-body)
+			 (let loop ([clauses (syntax->list (syntax (clause ...)))][saw-cases null])
+			   (cond
+			    [(null? clauses)
+			     (values null null null #f)]
+			    [else
+			     (let ([clause (car clauses)])
+			       (syntax-case* clause (else) (lambda (a b)
+							     (module-identifier=? a #'cases-else))
+				 [(variant (field-id ...) body0 body1 ...)
+				  (let* ([variant (syntax variant)]
+					 [vt
+					  (ormap (lambda (dtv) 
+						   (let ([vt-name (vt-name-stx dtv)])
+						     (and (module-identifier=? variant vt-name)
+							  dtv)))
+						 (dt-variants dt))]
+                                         [orig-variant (and vt (vt-name-stx vt))])
+				    (unless orig-variant
+				      (raise-syntax-error 
+				       #f
+				       (format "not a variant of `~a'"
+					       (syntax-object->datum (syntax datatype)))
+				       stx
+				       variant))
+
+				    (let ([field-ids (syntax->list (syntax (field-id ...)))])
+				      (for-each (lambda (fid)
+						  (unless (identifier? fid)
+						    (raise-syntax-error
+						     #f
+						     "expected an identifier for a field"
+						     stx
+						     fid)))
+						field-ids)
+				      (let ([dtv (variant-assq variant (dt-variants dt))])
+					(unless (= (length field-ids)
+						   (vt-field-count dtv))
+					  (raise-syntax-error
+					   #f
+					   (format
+					    "variant case `~a' for `~a' has wrong field count (expected ~a, found ~a)"
+					    (syntax-object->datum variant)
+					    (syntax-object->datum (syntax datatype))
+					    (vt-field-count dtv)
+					    (length field-ids))
+					   stx
+					   clause)))
+
+				      ;; Check for duplicate local field ids:
+				      (let ([dup (check-duplicate-identifier field-ids)])
+					(when dup
+					  (raise-syntax-error
+					   #f
+					   "duplicate field identifier"
+					   stx
+					   dup)))
+
+				      ;; Check for redundant case:
+				      (when (memq orig-variant saw-cases)
+					(raise-syntax-error
+					 #f
+					 "duplicate case"
+					 stx
+					 clause))
+				    
+				      ;; This clause is ok:
+				      (let-values ([(vts idss bodys else)
+						    (loop (cdr clauses) (cons orig-variant saw-cases))])
+					(values (cons vt vts)
+						(cons field-ids idss)
+						(cons (syntax (begin body0 body1 ...)) bodys)
+						else))))]
+				 [(else body0 body1 ...)
+				  (begin
+				    (unless (null? (cdr clauses))
+				      (raise-syntax-error
+				       #f
+				       "else clause must be last"
+				       stx
+				       clause))
+				    (values null null null (syntax (begin body0 body1 ...))))]
+				 [_else (raise-syntax-error
+					 #f
+					 "bad clause"
+					 stx
+					 clause)]))]))])
+             
+             ;; Missing any variants?
+             (unless (or else-body
+                         (= (length vts) (length (dt-variants dt))))
+               (let* ([here (map vt-name-stx vts)]
+                      [missing (let loop ([l (dt-variants dt)])
+                                (cond
+                                  [(null? l) ""]
+                                  [(ormap (lambda (i) (module-identifier=? (vt-name-stx (car l)) i)) here)
+                                   (loop (cdr l))]
+                                  [else
+                                   (format " ~a~a" 
+                                           (syntax-e (vt-name-stx (car l)))
+                                           (loop (cdr l)))]))])
+                 (raise-syntax-error
+                  #f
+                  (format "missing cases for the following variants:~a" missing)
+                  stx)))
+
+	     (with-syntax ([form-name (syntax-case stx () [(name . _) #'name])])
+
+	       ;; Create the result:
+	       (with-syntax ([pred (dt-pred-stx dt)]
+			     [(variant? ...) (map vt-predicate-stx vts)]
+			     [((field-extraction ...) ...) 
+			      (map (lambda (vt)
+				     (with-syntax ([accessor (vt-accessor-stx vt)])
+				       (let loop ([n 0])
+					 (if (= n (vt-field-count vt))
+					     null
+					     (cons (with-syntax ([n n])
+						     (syntax (accessor v n)))
+						   (loop (add1 n)))))))
+				   vts)]
+			     [((field-id ...) ...) field-idss]
+			     [(body ...) bodys]
+			     [else-body (or else-body
+					    (syntax 
+					     (error 'form-name "no variant case matched")))])
+		 (syntax/loc stx
+		   (let ([v expr])
+		     (if (not (pred v))
+			 (error 'form-name "not a ~a: ~e" 
+				(quote datatype) v)
+			 (cond
+			  [(variant? v)
+			   (let ([field-id field-extraction] ...)
+			     body)]
+			  ...
+			  [else else-body]))))))))]
+	[(_ orig-stx datatype-str cases-else datatype)
+	 (begin
+	   (unless (dt? (lookup-datatype #'datatype))
+	     (raise-syntax-error 
+	      #f
+	      (format "not a ~a name"  (syntax-e #'datatype-str))
+	      #'orig-stx
+	      (syntax datatype)))
+	   (raise-syntax-error
+	    #f
+	    (format "expected an expression after the ~a name" (syntax-e #'datatype-str))
+	    #'orig-stx))]
+	[(_ orig-stx datatype-str cases-else)
+	 (raise-syntax-error
+	  #f
+	  (format "expected a ~a name" (syntax-e #'datatype-str))
+	  #'orig-stx)]
+	[(_ orig_stx . __)
+	 ;; trigger "bad syntax" error:
+	 (syntax-case #'orig-stx ())])))
+  
+  (define-syntax provide-datatype-core
+    (lambda (stx)
+      (syntax-case stx ()
+	[(_ orig-stx datatype)
+	 (let ([stx #'orig-stx]
+	       [dt (syntax-local-value (syntax datatype) (lambda () #f))])
+	   (unless (dt? dt)
+	     (raise-syntax-error
+	      #f
+	      "not a datatype name" 
+	      stx
+	      (syntax datatype)))
+	   (with-syntax ([pred (dt-pred-stx dt)]
+			 [(orig-variant ...) 
+			  (map vt-name-stx (dt-variants dt))]
+			 [((selector ...) ...)
+			  (map vt-selector-stxes (dt-variants dt))]
+			 [(variant? ...)
+			  (map vt-predicate-stx (dt-variants dt))])
+	     (syntax
+	      (provide datatype
+		       pred
+		       orig-variant ...
+		       variant? ...
+		       selector ... ...))))]
+	[(_ orig_stx . __)
+	 ;; trigger "bad syntax" error:
+	 (syntax-case #'orig-stx ())]))))
diff --git a/collects/plai/private/datatype.ss b/collects/plai/private/datatype.ss
new file mode 100644
index 0000000000..191b950dd3
--- /dev/null
+++ b/collects/plai/private/datatype.ss
@@ -0,0 +1,60 @@
+
+(module datatype mzscheme
+
+  (require "datatype-core.ss")
+  
+  (define-for-syntax (do-define-type stx name type-params variants)
+    (unless (identifier? name)
+      (raise-syntax-error
+       #f
+       "expected an identifier for the type name"
+       stx
+       name))
+    (for-each (lambda (type-param)
+		(unless (identifier? type-param)
+		  (raise-syntax-error
+		   #f
+		   "expected an identifier for a type parameter"
+		   stx
+		   type-param)))
+	      type-params)
+    (with-syntax ([orig-stx stx]
+		  [name name]
+		  [name? (datum->syntax-object name
+					       (string->symbol
+						(format "~a?" (syntax-e name))))]
+		  [(type-param ...) type-params]
+		  [variants variants])
+      #'(define-datatype-core orig-stx
+	  (define-selectors define-predicates define-polymorphic define-contracts (kind "type"))
+	  define-values
+	  name (type-param ...) name?
+	  . variants)))
+
+  (define-syntax (define-type stx)
+    (syntax-case stx (represented-as)
+      [(_ (name-stx type-param-stx ...) . variants)
+       (do-define-type stx #'name-stx (syntax->list #'(type-param-stx ...)) #'variants)]
+      [(_ name-stx . variants)
+       (do-define-type stx #'name-stx null #'variants)]
+      [(_ . __)
+       (raise-syntax-error
+	#f
+	"expected an identifier for the type name"
+	stx)]))
+  
+  (define-syntax define-type-case
+    (syntax-rules ()
+      [(_ type-case else)
+       (define-syntax (type-case stx)
+	 (syntax-case stx ()
+	   [(_ . rest) #`(cases-core #,stx "type" else . rest)]))]))
+
+  (define-syntax (provide-type stx)
+    (syntax-case stx ()
+      [(provide-type . rest)
+       #`(provide-datatype-core #,stx . rest)]))
+  
+  (provide provide-type
+           define-type
+	   define-type-case))
diff --git a/collects/plai/test-harness.ss b/collects/plai/test-harness.ss
new file mode 100644
index 0000000000..7808b16e8b
--- /dev/null
+++ b/collects/plai/test-harness.ss
@@ -0,0 +1,73 @@
+(module test-harness mzscheme
+  (provide (all-defined))
+  (require (lib "list.ss")
+           (lib "pretty.ss"))
+
+  (define print-tests (make-parameter #f))
+  (define test-inspector (make-parameter (current-inspector)))
+  (define test-inexact-epsilon (make-parameter 0.01))
+
+  (define-struct (exn:test exn) ())
+
+  (define (install-test-inspector)
+    (test-inspector (current-inspector))
+    (current-inspector (make-inspector))
+    (print-struct #t))
+
+  (define (may-print-result result)
+    (parameterize ([current-inspector (test-inspector)]
+                   [print-struct #t])
+      (when (or (eq? (print-tests) (first result))
+                (eq? (print-tests) #t))
+        
+        (pretty-print result))
+      (when (and (eq? (print-tests) 'stop)
+                 (eq? (first result) 'bad))
+        (raise (make-exn:test (string->immutable-string (format "test failed: ~a" result))
+                              (current-continuation-marks))))))
+    
+  
+  (define (test result expected)
+    (let* ([test-result
+            (cond [(or (and (number? result) (not (exact? result)))
+                       (and (number? expected) (not (exact? expected))))
+                   (< (abs (- result expected)) (test-inexact-epsilon))]
+                  [else
+                   (parameterize ([current-inspector (test-inspector)])
+                     (equal? result expected))])]
+           [to-print (if test-result 
+                         (list 'good result expected)
+                         (list 'bad result expected))])
+      
+      (may-print-result to-print)
+      to-print))
+
+  (define (test/pred result pred)
+    (let* ([test-result (pred result)]
+           [to-print (if test-result
+                         (list 'good result test-result)
+                         (list 'bad result test-result))])
+      (may-print-result to-print)
+      to-print))
+
+  (define (test/exn thunk expected-exception-msg)
+    (unless (and (procedure? thunk)
+                 (procedure-arity-includes? thunk 0))
+      (error (format
+              "the first argument to test/exn should be a function of no arguments (a \"thunk\"), got ~a"
+              thunk)))
+    (let* ([result
+           (with-handlers 
+               ([exn:fail? (lambda (exn) exn)])
+             (thunk))]
+           [test-result
+            (if (and (exn? result)
+                     (regexp-match expected-exception-msg (exn-message result)))
+                (list 'good result expected-exception-msg)
+                (list 'bad result expected-exception-msg))])
+      (may-print-result test-result)
+      test-result))
+
+  (install-test-inspector))
+
+
diff --git a/collects/tests/plai/all.scm b/collects/tests/plai/all.scm
new file mode 100644
index 0000000000..dc938c200c
--- /dev/null
+++ b/collects/tests/plai/all.scm
@@ -0,0 +1,37 @@
+(define-type AE
+  [num (n number?)]
+  [add (lhs AE?)
+       (rhs AE?)]
+  [sub (lhs AE?)
+       (rhs AE?)])
+
+;; calc : AE -> number
+;; to define a calculator for AEs
+
+(define (calc an-ae)
+  (type-case AE an-ae
+             [num (n) n]
+             [add (l r) (+ (calc l) (calc r))]
+             [sub (l r) (- (calc l) (calc r))]))
+
+(test (calc (num 3)) 3)
+(test (calc (add (num 3) (num 4))) 7)
+(test (calc (add (sub (num 3) (num 4)) (num 7))) 6)
+
+;; parse : sexp -> AE
+;; to convert s-expressions into AEs
+
+(define (parse sexp)
+  (cond
+   [(number? sexp) (num sexp)]
+   [(list? sexp)
+    (case (first sexp)
+      [(+) (add (parse (second sexp))
+                     (parse (third sexp)))]
+      [(-) (sub (parse (second sexp))
+                     (parse (third sexp)))])]))
+
+(test (calc (parse 3)) 3)
+(test (calc (parse (list '+ 3 4))) 7)
+(test (calc (parse (list '+ (list '- 3 4) 7))) 6)
+
diff --git a/collects/tests/plai/arith-interp.scm b/collects/tests/plai/arith-interp.scm
new file mode 100644
index 0000000000..fc0b013890
--- /dev/null
+++ b/collects/tests/plai/arith-interp.scm
@@ -0,0 +1,17 @@
+(define-type AE
+  [num (n number?)]
+  [add (lhs AE?)
+       (rhs AE?)])
+
+;; calc : AE -> number
+;; to define a calculator for AEs
+
+(define (calc an-ae)
+  (type-case AE an-ae
+             [num (n) n]
+             [add (l r) (+ (calc l) (calc r))]))
+
+(test (calc (num 3)) 3)
+(test (calc (add (num 3) (num 4))) 7)
+(test (calc (add (add (num 3) (num 4)) (num 7))) 14)
+
diff --git a/collects/tests/plai/datatype-test.ss b/collects/tests/plai/datatype-test.ss
new file mode 100644
index 0000000000..196ff2d27f
--- /dev/null
+++ b/collects/tests/plai/datatype-test.ss
@@ -0,0 +1,111 @@
+(module datatype-test mzscheme
+  (require (lib "datatype.ss" "plai")
+           (lib "test-harness.ss" "plai")
+           (lib "contract.ss"))
+  
+  (print-tests 'stop)
+  
+  ;; TODO:
+  ;; ? Make sure the contract expressions are only evaluated once
+  ;; - Test that helpful error messages are generated
+  
+  (define-type (Option a)
+    [Some (item a)]
+    [None])
+  
+  (define-type (List a)
+      [Cons (item a) (rest (List-of/c a))]
+      [Nil])
+  
+  (define-type (TreeMap a b)
+    [RedNode (left (TreeMap-of/c a b)) (key a) (val b) (right (TreeMap-of/c a b))]
+    [BlackNode (left (TreeMap-of/c a b)) (key a) (val b) (right (TreeMap-of/c a b))]
+    [Leaf])
+  
+  (define-type (a-List a)
+    [a-Cons (item a) (rest (b-List-of/c a))]
+    [a-Nil])
+  
+  (define-type (b-List b)
+    [b-Cons (item b) (rest (a-List-of/c b))]
+    [b-Nil])
+  
+  ;; Error Messages
+  (test/exn (lambda () (expand #'(define-type (BadOption a)
+                                  [Some (item a)]
+                                  [Some (item a)])))
+            "duplicate")
+  
+  (test/exn (lambda () (expand #'(define-type (BadList 123)
+                                   [Cons (item a) (rest (BadList-of/c a))]
+                                   [Nil])))
+            "expected an identifier")
+  
+  ;; Option Test
+  (test/pred (Some 1) Option?)
+  (test/pred (Some 1) Some?)
+  (test/pred (None) Option?)
+  (test/pred (None) None?)
+  
+  (test ((Some-of integer?) 1) (Some 1))
+  (test (contract (Option-of/c integer?) (Some 1) 'p 'n) (Some 1))
+  (test (contract (Some-of/c integer?) (Some 1) 'p 'n) (Some 1))
+  
+  (test ((None-of integer?)) (None))
+  (test (contract (Option-of/c integer?) (None) 'p 'n) (None))
+  (test (contract (None-of/c symbol?) (None) 'p 'n) (None))
+  
+  (test (Some-item (Some 1)) 1) 
+  
+  (test/exn (lambda () ((Some-of integer?) 'a)) "broke the contract")
+  (test/exn (lambda () (contract (Some-of/c integer?) (Some 'symbol) 'p 'n)) "broke the contract")
+  (test/exn (lambda () (contract (Option-of/c integer?) (Some 'symbol) 'p 'n)) "broke the contract") 
+  
+  ;; List Test
+  (test/pred (Nil) List?)
+  (test/pred (Nil) Nil?)
+  (test/pred (Cons 1 (Nil)) List?)
+  (test/pred (Cons 1 (Nil)) Cons?)
+  
+  (test ((Cons-of integer?) 1 (Cons 2 (Cons 3 (Nil))))
+        (Cons 1 (Cons 2 (Cons 3 (Nil)))))
+  (test (contract (List-of/c integer?) (Cons 1 (Cons 2 (Cons 3 (Nil)))) 'p 'n)
+        (Cons 1 (Cons 2 (Cons 3 (Nil)))))
+  (test (contract (Cons-of/c integer?) (Cons 1 (Cons 2 (Cons 3 (Nil)))) 'p 'n)
+        (Cons 1 (Cons 2 (Cons 3 (Nil)))))
+
+  (test ((Nil-of integer?)) (Nil))
+  (test (contract (List-of/c integer?) (Nil) 'p 'n) (Nil))
+  (test (contract (Nil-of/c integer?) (Nil) 'p 'n) (Nil))
+  
+  (test/exn (lambda () ((Cons-of integer?) 1 2)) "broke the contract") 
+  (test/exn (lambda () (contract (Cons-of/c integer?) (Cons 1 2) 'p 'n)) "broke the contract")
+  (test/exn (lambda () ((Cons-of integer?) 1 (Cons 2 (Cons 'symbol (Nil))))) "broke the contract")
+  
+  ;; TreeMap Test
+  (test/pred (Leaf) TreeMap?)
+  (test/pred (Leaf) Leaf?)
+  (test/pred (RedNode (Leaf) 1 2 (Leaf)) TreeMap?)
+  (test/pred (RedNode (Leaf) 1 2 (Leaf)) RedNode?)
+  (test/pred (BlackNode (Leaf) 1 2 (Leaf)) TreeMap?)
+  (test/pred (BlackNode (Leaf) 1 2 (Leaf)) BlackNode?)
+  
+  ;; Alternating List Test
+  (test/pred (a-Nil) a-List?)
+  (test/pred (a-Nil) a-Nil?)
+  (test/pred (b-Nil) b-List?)
+  (test/pred (b-Nil) b-Nil?)
+  (test/pred (a-Cons 1 (b-Nil)) a-List?)
+  (test/pred (a-Cons 1 (b-Nil)) a-Cons?)
+  (test/pred (b-Cons 1 (a-Nil)) b-List?)
+  (test/pred (b-Cons 1 (a-Nil)) b-List?)
+  
+  (test ((a-Cons-of integer?) 1 (b-Nil)) (a-Cons 1 (b-Nil)))
+  (test (contract (a-List-of/c integer?) (a-Cons 1 (b-Nil)) 'p 'n) (a-Cons 1 (b-Nil)))
+  (test (contract (a-Cons-of/c integer?) (a-Cons 1 (b-Nil)) 'p 'n) (a-Cons 1 (b-Nil)))
+  (test ((b-Cons-of integer?) 1 (a-Nil)) (b-Cons 1 (a-Nil)))
+  (test (contract (b-List-of/c integer?) (b-Cons 1 (a-Nil)) 'p 'n) (b-Cons 1 (a-Nil)))
+  (test (contract (b-Cons-of/c integer?) (b-Cons 1 (a-Nil)) 'p 'n) (b-Cons 1 (a-Nil)))
+  
+  (test/exn (lambda () ((a-Cons-of integer?) 1 (a-Nil))) "broke the contract")
+  )
\ No newline at end of file
diff --git a/collects/tests/plai/hof-env-buggy.scm b/collects/tests/plai/hof-env-buggy.scm
new file mode 100644
index 0000000000..320f180c52
--- /dev/null
+++ b/collects/tests/plai/hof-env-buggy.scm
@@ -0,0 +1,107 @@
+(define-type FWAE
+  [num (n number?)]
+  [add (lhs FWAE?) (rhs FWAE?)]
+  [sub (lhs FWAE?) (rhs FWAE?)]
+  [id (name symbol?)]
+  [with (name symbol?) (named-expr FWAE?) (body FWAE?)]
+  [fun (param symbol?) (body FWAE?)]
+  [app (fun-expr FWAE?) (arg-expr FWAE?)])
+
+;; parse : sexp $\longrightarrow$ FWAE
+;; to convert s-expressions into FWAEs
+
+(define (parse sexp)
+  (cond
+   [(symbol? sexp) (id sexp)]
+   [(number? sexp) (num sexp)]
+   [(list? sexp)
+    (case (first sexp)
+      [(+) (add (parse (second sexp))
+                     (parse (third sexp)))]
+      [(-) (sub (parse (second sexp))
+                     (parse (third sexp)))]
+      [(with) (with (first (second sexp))
+                         (parse (second (second sexp)))
+                         (parse (third sexp)))]
+      [(fun) (fun (first (second sexp)) (parse (third sexp)))]
+      [else (app (parse (first sexp)) (parse (second sexp)))])]))
+
+;; num+ : \scheme|num| \scheme|num| -> \scheme|num|
+
+(define (num+ n1 n2)
+  (num (+ (num-n n1) (num-n n2))))
+
+;; num- : \scheme|num| \scheme|num| -> \scheme|num|
+
+(define (num- n1 n2)
+  (num (- (num-n n1) (num-n n2))))
+
+(define-type Subcache
+  [mtSub]
+  [aSub (name symbol?) (value FWAE?) (sc Subcache?)])
+
+;; lookup : symbol \scheme|SubCache| -> \scheme|FWAE|
+
+(define (lookup name sc)
+  (type-case Subcache sc
+             [mtSub () (error 'lookup "no binding for identifier")]
+             [aSub (bound-name bound-value rest-sc)
+                   (if (symbol=? bound-name name)
+                       bound-value
+                       (lookup name rest-sc))]))
+
+;; interp : \scheme|FWAE| \scheme|SubCache| $\rightarrow$ \scheme|FWAE|
+;; evaluates \scheme|FWAE| expressions by reducing them to their corresponding values
+;; return values are either \scheme|num| or \scheme|fun|
+
+(define (interp expr sc)
+  (type-case FWAE expr
+             [num (n) expr]
+             [add (l r) (num+ (interp l sc) (interp r sc))]
+             [sub (l r) (num- (interp l sc) (interp r sc))]
+             [with (bound-id named-expr bound-body)
+                   (interp bound-body
+                           (aSub bound-id
+                                      (interp named-expr sc)
+                                      sc))]
+             [id (v) (lookup v sc)]
+             [fun (bound-id bound-body)
+                  expr]
+             [app (fun-expr arg-expr)
+                  (local ([define fun-val (interp fun-expr sc)])
+                         (interp (fun-body fun-val)
+                                 (aSub (fun-param fun-val)
+                                            (interp arg-expr sc)
+                                            sc)))]))
+
+(define (interp-test expr ans)
+  (test (interp (parse expr) (mtSub)) (num ans)))
+
+(define (interp-test-error expr expected-exception-msg)
+  (test/exn (lambda () (interp (parse expr) (mtSub))) expected-exception-msg))
+
+
+(interp-test 5 5)
+(interp-test '{+ 5 5} 10)
+(interp-test '{with {x {+ 5 5}} {+ x x}} 20)
+(interp-test '{with {x 5} {+ x x}} 10)
+(interp-test '{with {x {+ 5 5}} {with {y {- x 3}} {+ y y}}} 14)
+(interp-test '{with {x 5} {with {y {- x 3}} {+ y y}}} 4)
+(interp-test '{with {x 5} {+ x {with {x 3} 10}}} 15)
+(interp-test '{with {x 5} {+ x {with {x 3} x}}} 8)
+(interp-test '{with {x 5} {+ x {with {y 3} x}}} 10)
+(interp-test '{with {x 5} {with {y x} y}} 5)
+(interp-test '{with {x 5} {with {x x} x}} 5)
+(interp-test '{{fun {x} {+ x 5}} 5} 10)
+(interp-test '{with {double {fun {x} {+ x x}}} {+ {double 5} {double 10}}} 30)
+(interp-test '{{{fun {x} x} {fun {x} {+ x 5}}} 3} 8)
+"expect error: should yield 7, dyn scope yields 9"
+(interp-test '{with {f {with {x 3} {fun {y} {+ x y}}}}
+                    {with {x 5} {f 4}}} 7)
+
+(test/pred (interp (parse '{fun {x} x}) (mtSub)) fun?)
+
+(test/pred (interp (parse '{with {x 3} {fun {y} {+ x y}}}) (mtSub)) fun?)
+
+(interp-test-error '{with {x x} x} "no binding")
+
diff --git a/collects/tests/plai/hof-env.scm b/collects/tests/plai/hof-env.scm
new file mode 100644
index 0000000000..c07c0421cd
--- /dev/null
+++ b/collects/tests/plai/hof-env.scm
@@ -0,0 +1 @@
+;; see ../repn-meta/env-proc-rep.scm
\ No newline at end of file
diff --git a/collects/tests/plai/hof-subst.scm b/collects/tests/plai/hof-subst.scm
new file mode 100644
index 0000000000..c5ebf0ea8d
--- /dev/null
+++ b/collects/tests/plai/hof-subst.scm
@@ -0,0 +1,140 @@
+(define-type FWAE
+  [num (n number?)]
+  [add (lhs FWAE?) (rhs FWAE?)]
+  [sub (lhs FWAE?) (rhs FWAE?)]
+  [id (name symbol?)]
+  [with (name symbol?) (named-expr FWAE?) (body FWAE?)]
+  [fun (param symbol?) (body FWAE?)]
+  [app (fun-expr FWAE?) (arg-expr FWAE?)])
+
+;; parse : sexp $\longrightarrow$ FWAE
+;; to convert s-expressions into FWAEs
+
+(define (parse sexp)
+  (cond
+   [(symbol? sexp) (id sexp)]
+   [(number? sexp) (num sexp)]
+   [(list? sexp)
+    (case (first sexp)
+      [(+) (add (parse (second sexp))
+                     (parse (third sexp)))]
+      [(-) (sub (parse (second sexp))
+                     (parse (third sexp)))]
+      [(with) (with (first (second sexp))
+                         (parse (second (second sexp)))
+                         (parse (third sexp)))]
+      [(fun) (fun (first (second sexp)) (parse (third sexp)))]
+      [else (app (parse (first sexp)) (parse (second sexp)))])]))
+
+;; subst : \scheme|FWAE| symbol \scheme|FWAE| $\rightarrow$ \scheme|FWAE|
+;; substitutes second argument with third argument in first argument,
+;; as per the rules of substitution; the resulting expression contains
+;; no free instances of the second argument
+
+(define (subst expr sub-id val)
+  (type-case FWAE expr
+             [num (n) expr]
+             [add (l r) (add (subst l sub-id val)
+                                  (subst r sub-id val))]
+             [sub (l r) (sub (subst l sub-id val)
+                                  (subst r sub-id val))]
+             [id (v) (if (symbol=? v sub-id) val expr)]
+             [with (bound-id named-expr bound-body)
+                   (if (symbol=? bound-id sub-id)
+                       (with bound-id
+                                  (subst named-expr sub-id val)
+                                  bound-body)
+                       (with bound-id
+                                  (subst named-expr sub-id val)
+                                  (subst bound-body sub-id val)))]
+             [fun (bound-id bound-body)
+                  (if (symbol=? bound-id sub-id)
+                      expr
+                      (fun bound-id
+                                (subst bound-body sub-id val)))]
+             [app (fun-expr arg-expr)
+                  (app (subst fun-expr sub-id val)
+                            (subst arg-expr sub-id val))]))
+
+
+(test (subst (add (id 'x) (id 'x)) 'x (num 5))
+      (add (num 5) (num 5)))
+
+(test (subst (with 'x (num 5) (add (id 'x) (id 'x))) 'x (num 3))
+      (with 'x (num 5) (add (id 'x) (id 'x))))
+
+(test (subst (add (id 'x) (with 'x (num 3) (num 10))) 'x (num 5))
+      (add (num 5) (with 'x (num 3) (num 10))))
+
+(test (subst (add (id 'x) (with 'x (num 3) (id 'x))) 'x (num 5))
+      (add (num 5) (with 'x (num 3) (id 'x))))
+
+(test (subst (parse '{fun {x} {+ x y}}) 'x (num 5))
+      (parse '{fun {x} {+ x y}}))
+
+(test (subst (parse '{fun {x} {+ x y}}) 'y (num 5))
+      (parse '{fun {x} {+ x 5}}))
+
+(test (subst (parse '{{fun {x} {+ x y}} {fun {y} {+ x y}}}) 'y (num 3))
+      (parse '{{fun {x} {+ x 3}} {fun {y} {+ x y}}}))
+
+
+;; num+ : \scheme|num| \scheme|num| -> \scheme|num|
+
+(define (num+ n1 n2)
+  (num (+ (num-n n1) (num-n n2))))
+
+;; num- : \scheme|num| \scheme|num| -> \scheme|num|
+
+(define (num- n1 n2)
+  (num (- (num-n n1) (num-n n2))))
+
+;; interp : \scheme|FWAE| $\rightarrow$ \scheme|FWAE|
+;; evaluates \scheme|FWAE| expressions by reducing them to their corresponding values
+;; return values are either \scheme|num| or \scheme|fun|
+
+(define (interp expr)
+  (type-case FWAE expr
+             [num (n) expr]
+             [add (l r) (num+ (interp l) (interp r))]
+             [sub (l r) (num- (interp l) (interp r))]
+             [with (bound-id named-expr bound-body)
+                   (interp (subst bound-body
+                                  bound-id
+                                  (interp named-expr)))]
+             [id (v) (error 'interp "free identifier")]
+             [fun (bound-id bound-body)
+                  expr]
+             [app (fun-expr arg-expr)
+                  (local ([define fun-val (interp fun-expr)])
+                         (interp (subst (fun-body fun-val)
+                                        (fun-param fun-val)
+                                        (interp arg-expr))))]))
+
+(define (interp-test expr ans)
+  (test (interp (parse expr)) (num ans)))
+
+(define (interp-test-error expr expected-exception-msg)
+  (test-exn (lambda () (interp (parse expr))) expected-exception-msg))
+
+(interp-test '5 5)
+(interp-test '{+ 5 5} 10)
+(interp-test '{with {x {+ 5 5}} {+ x x}} 20)
+(interp-test '{with {x 5} {+ x x}} 10)
+(interp-test '{with {x {+ 5 5}} {with {y {- x 3}} {+ y y}}} 14)
+(interp-test '{with {x 5} {with {y {- x 3}} {+ y y}}} 4)
+(interp-test '{with {x 5} {+ x {with {x 3} 10}}} 15)
+(interp-test '{with {x 5} {+ x {with {x 3} x}}} 8)
+(interp-test '{with {x 5} {+ x {with {y 3} x}}} 10)
+(interp-test '{with {x 5} {with {y x} y}} 5)
+(interp-test '{with {x 5} {with {x x} x}} 5)
+(interp-test '{{fun {x} {+ x 5}} 5} 10)
+(interp-test '{with {double {fun {x} {+ x x}}} {+ {double 5} {double 10}}} 30)
+(interp-test '{{{fun {x} x} {fun {x} {+ x 5}}} 3} 8)
+(interp-test '{with {f {with {x 3} {fun {y} {+ x y}}}}
+                    {with {x 5} {f 4}}} 7)
+
+(test/pred (interp (parse '{fun {x} x})) fun?)
+(test/pred (interp (parse '{with {x 3} {fun {y} {+ x y}}})) fun?)
+
+(test/exn (lambda () (interp (parse '{with {x x} x}))) "free identifier")
diff --git a/collects/tests/plai/subst.scm b/collects/tests/plai/subst.scm
new file mode 100644
index 0000000000..910f261054
--- /dev/null
+++ b/collects/tests/plai/subst.scm
@@ -0,0 +1,82 @@
+(define-type WAE
+  [num (n number?)]
+  [add (lhs WAE?) (rhs WAE?)]
+  [sub (lhs WAE?) (rhs WAE?)]
+  [id (name symbol?)]
+  [with (name symbol?) (named-expr WAE?) (body WAE?)])
+
+;; parse : sexp $\longrightarrow$ AE
+;; to convert s-expressions into AEs
+
+(define (parse sexp)
+  (cond
+   [(symbol? sexp) (id sexp)]
+   [(number? sexp) (num sexp)]
+   [(list? sexp)
+    (case (first sexp)
+      [(+) (add (parse (second sexp))
+                     (parse (third sexp)))]
+      [(-) (sub (parse (second sexp))
+                     (parse (third sexp)))]
+      [(with) (with (first (second sexp))
+                         (parse (second (second sexp)))
+                         (parse (third sexp)))])]))
+
+;; subst : \scheme|WAE| symbol \scheme|WAE| $\rightarrow$ \scheme|WAE|
+;; substitutes second argument with third argument in first argument,
+;; as per the rules of substitution; the resulting expression contains
+;; no free instances of the second argument
+
+(define (subst expr sub-id val)
+  (type-case WAE expr
+             [num (n) expr]
+             [add (l r) (add (subst l sub-id val)
+                                  (subst r sub-id val))]
+             [sub (l r) (sub (subst l sub-id val)
+                                  (subst r sub-id val))]
+             [id (v) (if (symbol=? v sub-id) val expr)]
+             [with (bound-id named-expr bound-body)
+                   (if (symbol=? bound-id sub-id)
+                       (with bound-id
+                                  (subst named-expr sub-id val)
+                                  bound-body)
+                       (with bound-id
+                                  (subst named-expr sub-id val)
+                                  (subst bound-body sub-id val)))]))
+
+
+(test (subst (add (id 'x) (id 'x)) 'x (num 5))
+      (add (num 5) (num 5)))
+
+(test (subst (with 'x (num 5) (add (id 'x) (id 'x))) 'x (num 3))
+      (with 'x (num 5) (add (id 'x) (id 'x))))
+
+(test (subst (add (id 'x) (with 'x (num 3) (num 10))) 'x (num 5))
+      (add (num 5) (with 'x (num 3) (num 10))))
+
+(test (subst (add (id 'x) (with 'x (num 3) (id 'x))) 'x (num 5))
+      (add (num 5) (with 'x (num 3) (id 'x))))
+
+(define (calc expr)
+  (type-case WAE expr
+             [num (n) n]
+             [add (l r) (+ (calc l) (calc r))]
+             [sub (l r) (- (calc l) (calc r))]
+             [with (bound-id named-expr bound-body)
+                   (calc (subst bound-body
+                                bound-id
+                                (num (calc named-expr))))]
+             [id (v) (error 'calc "free identifier")]))
+
+(test (calc (parse '5)) 5)
+(test (calc (parse '{+ 5 5})) 10)
+(test (calc (parse '{with {x {+ 5 5}} {+ x x}})) 20)
+(test (calc (parse '{with {x 5} {+ x x}})) 10)
+(test (calc (parse '{with {x {+ 5 5}} {with {y {- x 3}} {+ y y}}})) 14)
+(test (calc (parse '{with {x 5} {with {y {- x 3}} {+ y y}}})) 4)
+(test (calc (parse '{with {x 5} {+ x {with {x 3} 10}}})) 15)
+(test (calc (parse '{with {x 5} {+ x {with {x 3} x}}})) 8)
+(test (calc (parse '{with {x 5} {+ x {with {y 3} x}}})) 10)
+(test (calc (parse '{with {x 5} {with {y x} y}})) 5)
+(test (calc (parse '{with {x 5} {with {x x} x}})) 5)
+(test/exn (lambda () (calc (parse '{with {x x} x}))) "free identifier")
diff --git a/collects/tests/plai/test.ss b/collects/tests/plai/test.ss
new file mode 100644
index 0000000000..424b5d7f37
--- /dev/null
+++ b/collects/tests/plai/test.ss
@@ -0,0 +1,6 @@
+
+(load "all.scm")
+(load "arith-interp.scm")
+(load "hof-env-buggy.scm")
+(load "hof-subst.scm")
+(load "subst.scm")