From 0a82e9298c7a46ee866fdb8ea6800eafcbe770c8 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 15 Aug 2014 15:33:07 -0400
Subject: [PATCH] sysf: basic forall type working

---
 sysf.rkt | 443 ++++++++++++++++---------------------------------------
 1 file changed, 129 insertions(+), 314 deletions(-)

diff --git a/sysf.rkt b/sysf.rkt
index 00116cd..8d79edb 100644
--- a/sysf.rkt
+++ b/sysf.rkt
@@ -1,272 +1,114 @@
 #lang racket/base
 (require 
-  racket/match
-  (for-syntax racket/base syntax/parse syntax/parse/experimental/template 
-              racket/set syntax/id-table syntax/stx racket/list racket/syntax
-              "stx-utils.rkt")
-  (for-meta 2 racket/base syntax/parse))
+  (for-syntax 
+   racket/base syntax/parse syntax/parse/experimental/template
+   syntax/stx racket/syntax racket/set
+   "stx-utils.rkt")
+  (for-meta 2 racket/base syntax/parse)
+  "typecheck.rkt")
+(require 
+  (except-in 
+   "stlc.rkt" 
+   define-type begin letrec #%module-begin #%app λ
+   check-type-error check-type check-type-and-result check-not-type check-equal?))
+(require (prefix-in stlc: (only-in "stlc.rkt" #%app define-type λ begin)))
+(provide (all-from-out "stlc.rkt"))
 (provide 
- (except-out
-  (all-from-out racket/base) 
-  λ #%app + #%datum let letrec cons null null? begin void
-  #%module-begin if
-  ))
-
-(provide
- define-type cases
- (rename-out
-  [λ/tc λ] [app/tc #%app] [let/tc let] [letrec/tc letrec]
-  [begin/tc begin] [void/tc void]
-  [if/tc if] [+/tc +] 
-  [datum/tc #%datum] [module-begin/tc #%module-begin]
-  [cons/tc cons] [null/tc null] [null?/tc null?] [first/tc first] [rest/tc rest]))
-
-;; System F (copied from stlc.rkt 2014-08-13)
-;; 
-;; Features:
-;; - letrec
-;; - lists
-;; - user (recursive) function definitions
-;; - user (recursive) (variant) type-definitions
-
-;; for types, just need the identifier bound
-(define-syntax-rule (define-builtin-type τ) (begin (define τ #f)  (provide τ)))
-(define-syntax-rule (define-builtin-types τ ...) (begin (define-builtin-type τ) ...))
-(define-builtin-types Int String Bool → Listof Unit)
-
-;; type environment
-(begin-for-syntax
-  (define base-type-env (hash))
-  ;; Γ : [Hashof var-symbol => type-stx]
-  ;; - can't use free-identifier=? for the hash table (or free-id-table)
-  ;;   because env must be set before expanding λ body (ie before going under λ)
-  ;;   so x's in the body won't be free-id=? to the one in the table
-  ;; use symbols instead of identifiers for now --- should be fine because
-  ;; I'm manually managing the environment
-  (define Γ (make-parameter base-type-env))
-  
-  ;; generated type vars
-  (define fvs (make-parameter (set)))
-  (define fvs-subst (make-parameter (hash)))
-  (define (fvs-subst-set x τ)
-    (hash-set (fvs-subst) (syntax->datum x) τ))
-  (define (do-subst/τ τ)
-    (syntax-parse τ
-      [x:id
-       #:when (set-member? (fvs) (syntax->datum #'x))
-       (hash-ref (fvs-subst) (syntax->datum #'x) #'???)]
-      [τ:id #'τ]
-      [(tycon τ ...)
-       #:with (τ-subst ...) (stx-map do-subst/τ #'(τ ...))
-       #'(tycon τ-subst ...)]))
-  (define (do-subst h)
-    (for/hash ([(x τ) (in-hash h)])
-      (values x (do-subst/τ τ)))))
-
-;; testing fns ----------------------------------------------------------------
-(require (for-syntax rackunit))
-(provide check-type-error check-type check-type-and-result check-not-type)
-(define-syntax (check-type-error stx)
-  (syntax-parse stx
-    [(_ e)
-     #:when (check-exn exn:fail? (λ () (expand/df #'e)))
-     #'(void)]))
-(define-syntax (check-type stx)
-  (syntax-parse stx #:datum-literals (:)
-    [(_ e : τ)
-     #:with e+ (expand/df #'e)
-     #:when (check-true (assert-type #'e+ #'τ) 
-                        (format "Expected type ~a but got type ~a" #'τ (typeof #'e)))
-     #'(void)]))
-(define-syntax (check-not-type stx)
-  (syntax-parse stx #:datum-literals (:)
-    [(_ e : τ)
-     #:with e+ (expand/df #'e)
-     #:when (check-false (type=? (typeof #'e+) #'τ) 
-                         (format "Expected type to not be ~a but got type ~a" #'τ (typeof #'e)))
-     #'(void)]))
-
-(define-syntax (check-type-and-result stx)
-  (syntax-parse stx #:datum-literals (: =>)
-    [(_ e : τ => v)
-     #'(begin (check-type e : τ)
-              (check-equal? e v))]))
-(require rackunit)
-(provide (rename-out [my-check-equal? check-equal?]))
-(define-syntax-rule (my-check-equal? x y) (check-equal? x y))
-
-(define-for-syntax (type=? τ1 τ2)
-;  (printf "type= ~a ~a\n" (syntax->datum τ1) (syntax->datum τ2))
-  (syntax-parse #`(#,τ1 #,τ2) #:literals (→)
-    [(x:id τ)
-     #:when (and (set-member? (fvs) (syntax->datum #'x))
-                 (hash-has-key? (fvs-subst) (syntax->datum #'x)))
-     (type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
-    [(x:id τ)
-     #:when (set-member? (fvs) (syntax->datum #'x))
-     #:when (fvs-subst (fvs-subst-set #'x #'τ))
-     #t]
-    [(τ x:id)
-     #:when (and (set-member? (fvs) (syntax->datum #'x))
-                 (hash-has-key? (fvs-subst) (syntax->datum #'x)))
-     (type=? (hash-ref (fvs-subst) (syntax->datum #'x)) #'τ)]
-    [(τ x:id)
-     #:when (set-member? (fvs) (syntax->datum #'x))
-     #:when (fvs-subst (fvs-subst-set #'x #'τ))
-     #t]
-    [(x:id y:id) (free-identifier=? τ1 τ2)]
-    [((tycon1 τ1 ...) (tycon2 τ2 ...)) 
-     (and (free-identifier=? #'tycon1 #'tycon2)
-          (stx-andmap type=? #'(τ1 ...) #'(τ2 ...)))]
-    [_ #f]))
-
-;; return #t if (typeof e)=τ, else type error
-(begin-for-syntax
-  (define (assert-type e τ)
-    (or (type=? (typeof e) τ)
-         (error 'TYPE-ERROR "~a (~a:~a) has type ~a, but should have type ~a"
-               (syntax->datum e)
-               (syntax-line e) (syntax-column e)
-               (syntax->datum (typeof e))
-               (syntax->datum τ))))
-  (define (assert-Unit-type e) (assert-type e #'Unit))
-  (define (assert-Int-type e) (assert-type e #'Int)))
-
-;; type env and other helper fns ----------------------------------------------
-;; attaches type τ to e (as syntax property)
-(define-for-syntax (⊢ e τ) (syntax-property e 'type τ))
-
-;; retrieves type of τ (from syntax property)
-(define-for-syntax (typeof stx) (syntax-property stx 'type))
-
-(define-for-syntax (type-env-lookup x) (hash-ref (Γ) (syntax->datum x)))
-;; returns a new hash table extended with type associations x:τs
-(define-for-syntax (type-env-extend x:τs)
-  (define xs (stx-map stx-car x:τs))
-  (define τs (stx-map stx-cadr x:τs))
-  (apply hash-set* (Γ) (append-map (λ (x τ) (list (syntax->datum x) τ)) xs τs)))
-;; must be macro because type env must be extended first, before expandinb body
-(begin-for-syntax
-  (define-syntax (with-extended-type-env stx)
-    (syntax-parse stx
-      [(_ x-τs e)
-       #'(parameterize ([Γ (type-env-extend x-τs)]) e)])))
-
-;; expand/df ------------------------------------------------------------------
-;; depth-first expand
-(define-for-syntax (expand/df e [ctx #f])
-;  (printf "expanding: ~a\n" e)
-;  (printf "typeenv: ~a\n" (Γ))
-  (cond
-    ;; 1st case handles struct constructors that are not the same name as struct
-    ;; (should always be an identifier)
-    [(syntax-property e 'constructor-for) => (λ (Cons) 
-     (⊢ e (type-env-lookup Cons)))]
-    ;; 2nd case handles identifiers that are not struct constructors
-    [(identifier? e) (⊢ e (type-env-lookup e))] ; handle this here bc there's no #%var form
-    ;; local-expand must expand all the way down, ie have no stop-list, ie stop list can't be #f
-    ;; ow forms like lambda and app won't get properly assigned types
-    [else (local-expand e 'expression null ctx)]))
-(define-for-syntax (expand/df/module-ctx def)
-  (local-expand def 'module #f))
-(define-for-syntax (expand/df/mb-ctx def)
-  (local-expand def 'module-begin #f))
-
-
+ define-type
+ (rename-out 
+  [stlc:begin begin]
+  [letrec/tc letrec]
+  [module-begin/tc #%module-begin]
+  [app/tc #%app]
+  [λ/tc λ]))
 
 ;; define-type ----------------------------------------------------------------
 (define-syntax (define-type stx)
   (syntax-parse stx #:datum-literals (variant)
-    #;[(_ (Tycon:id X ...) (variant (Cons:id τ_fld ...) ...))
+    [(_ (Tycon:id X ...) (variant (Cons:id τ_fld ...) ...))
      #:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
-     #:when (Γ (type-env-extend #'([Cons (∀ (X ...) (→ τ_fld ... Tycon))] ...)))
+     ;; weird, generate-temporaries doesnt automatically produces ids with the right scope
+;     #:with (Cons-tmp ...) (stx-map (λ (x) (format-id #'Tycon "~a" x)) (generate-temporaries #'(Cons ...)))
+;     #:when (expand/df/module-ctx
+;             #'(begin
+;                 (define-syntax (Cons-tmp stx)
+;                   (syntax-parse stx
+;                     [(_ τ (... ...))
+;                      #:with (X ...) #'(τ (... ...))
+;                      #'(→ τ_fld ... (Tycon X ...))])) ...))
+     #:when (Γ (type-env-extend #'([Cons (∀ (X ...) (→ τ_fld ... (Tycon X ...)))] ...)))
+;     #:when (Γ (type-env-extend #'([Cons (Cons-tmp (∀ (X ...) (→ τ_fld ... (Tycon X ...))))] ...)))
+;     #:when (Γ (type-env-extend #'([Cons (→ τ_fld ... Tycon)] ...)))
      #'(begin
-         (define-syntax (Tycon stx)
+;         (define-syntax (Cons-tmp stx)
+;           (syntax-parse stx
+;             [(_ τ (... ...))
+;              #:with (X ...) #'(τ (... ...))
+;              #'(→ τ_fld ... (Tycon X ...))])) ...
+         #;(define-syntax (Tycon stx)
            (syntax-parse stx
              [(_ τ (... ...))
-              #:with (X ...) (τ (... ...))
+              #:with (X ...) #'(τ (... ...))
               #'(variant (Cons τ_fld ...) ...)]))
          (struct Cons (x ...) #:transparent) ...)]
-    [(_ τ:id (variant (Cons:id τ_fld ...) ...))
-     #:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
-     #:when (Γ (type-env-extend #'([Cons (→ τ_fld ... τ)] ...)))
-     #'(begin
-         (struct Cons (x ...) #:transparent) ...)]))
-(define-syntax (cases stx)
-  (syntax-parse stx
-    [(_ e [Cons (x ...) body ... body_result] ...)
-     #:with e+ (expand/df #'e)
-     #:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
-     #:with ((→ τ ... τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
-     #:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_Cons ...))
-     #:with ((lam (x+ ...) body+ ... body_result+) ...) 
-            (stx-map (λ (bods xs τs) 
-                       (with-extended-type-env 
-                        (stx-map list xs τs)
-                        (expand/df #`(λ #,xs #,@bods))))
-                     #'((body ... body_result) ...)
-                     #'((x ...) ...)
-                     #'((τ ...) ...))
-     #:when (stx-andmap (λ (bods) (stx-andmap assert-Unit-type bods)) #'((body+ ...) ...))
-     #:with (τ_result ...) (stx-map typeof #'(body_result+ ...))
-     #:when (or (null? (syntax->list #'(τ_result ...))) ; shouldnt happen
-                (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
-                        (cdr (syntax->list #'(τ_result ...)))))
-     (⊢ (syntax/loc stx (match e+ [(Cons+ x+ ...) body+ ... body_result+] ...))
-        (car (syntax->list #'(τ_result ...))))]))
-
-;; typed forms ----------------------------------------------------------------
-(define-syntax (datum/tc stx)
-  (syntax-parse stx
-    [(_ . n:integer) (⊢ (syntax/loc stx (#%datum . n)) #'Int)]
-    [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
-    [(_ . b:boolean) (⊢ (syntax/loc stx (#%datum . b)) #'Bool)]
-    [(_ . x) 
-     #:when (error 'TYPE-ERROR "~a (~a:~a) has unknown type" 
-                   #'x (syntax-line #'x) (syntax-column #'x))
-     (syntax/loc stx (#%datum . x))]))
-
-(define-syntax (begin/tc stx)
-  (syntax-parse stx
-    [(_ e ... e_result)
-     #:with (e+ ... e_result+) (stx-map expand/df #'(e ... e_result))
-     #:when (stx-andmap assert-Unit-type #'(e+ ...))
-     (⊢ (syntax/loc stx (begin e+ ... e_result+)) (typeof #'e_result+))]))
-
-(define-syntax (void/tc stx)
-  (syntax-parse stx
-    [(_) (⊢ (syntax/loc stx (void)) #'Unit)]))
-
-(define-syntax (+/tc stx)
-  (syntax-parse stx
-    [(_ e ...)
-     #:with (e+ ...) (stx-map expand/df #'(e ...))
-     #:when (stx-andmap assert-Int-type #'(e+ ...))
-     (⊢ (syntax/loc stx (+ e+ ...)) #'Int)]))
+    [(_ any ...) #'(stlc:define-type any ...)]))
 
+;; lambda ---------------------------------------------------------------------
 (define-syntax (λ/tc stx)
   (syntax-parse stx #:datum-literals (:)
-    [(_ ([x:id : τ] ...) e ... e_result)
+    [(_ τs ([x:id : τ] ...) e ... e_result)
+     #:when (curly-parens? #'τs)
      ;; the with-extended-type-env must be outside the expand/df (instead of
      ;; around just the body) bc ow the parameter will get restored to the old
      ;; value before the local-expand happens
      #:with (lam xs e+ ... e_result+) (with-extended-type-env #'([x τ] ...)
                                         (expand/df #'(λ (x ...) e ... e_result)))
+     ;; manually handle identifiers here
+     ;; - since Racket has no #%var hook, ids didn't get "expanded" in the previous line
+     ;;   and thus didn't get a type
+     ;; TODO: can I put this somewhere else where it's more elegant?
+     #:with (e++ ... e_result++) (with-extended-type-env #'([x τ] ...)
+                                   (stx-map 
+                                    (λ (e) (if (identifier? e) (expand/df e) e))
+                                    #'(e+ ... e_result+)))
      ;; manually handle the implicit begin
-     #:when (stx-map assert-Unit-type #'(e+ ...))
-     #:with τ_body (typeof #'e_result+)
-     (⊢ (syntax/loc stx (lam xs e+ ... e_result+)) #'(→ τ ... τ_body))]))
+     #:when (stx-map assert-Unit-type #'(e++ ...))
+     #:with τ_body (typeof #'e_result++)
+     (⊢ (syntax/loc stx (lam xs e++ ... e_result++)) 
+        #'(∀ τs (→ τ ... τ_body)))]
+    [(_ any ...) #'(stlc:λ any ...)]))
 
-(define-syntax (let/tc stx)
-  (syntax-parse stx #:datum-literals (:)
-    [(_ ([x:id e_x] ...) e ... e_result)
-     #:with (e_x+ ...) (stx-map expand/df #'(e_x ...))
-     #:with (τ ...) (stx-map typeof #'(e_x+ ...))
-     #:with (lam (x+ ...) e+ ... e_result+) 
-            (with-extended-type-env #'([x τ] ...)
-              (expand/df #'(λ (x ...) e ... e_result)))
-     #:when (stx-andmap assert-Unit-type #'(e+ ...))
-     (⊢ (syntax/loc stx (let ([x+ e_x+] ...) e+ ... e_result+)) (typeof #'e_result+))]))
+(define-for-syntax (apply-forall ∀τ τs)
+  (define ctx (syntax-local-make-definition-context))
+  (define id (generate-temporary))
+  (syntax-local-bind-syntaxes
+   (list id)
+   (syntax-parse ∀τ #:datum-literals (∀)
+     [(∀ (X ...) τbody)
+      #'(λ (stx)
+          (syntax-parse stx
+            [(_ (τ (... ...)))
+             #:with (X ...) #'(τ (... ...))
+             #'τbody]))])
+   ctx)
+  (local-expand #`(#,id #,τs) 'expression (list #'#%app) ctx))
+; #%app -----------------------------------------------------------------------
+(define-syntax (app/tc stx)
+  (syntax-parse stx #:literals (→ void) 
+ ;                   #:datum-literals (:t)
+;    [(_ :t x) #'(printf "~a : ~a\n" 'x (hash-ref runtime-env 'x))]
+    [(_ e_fn τs e_arg ...)
+     #:when (curly-parens? #'τs)
+;     #:with (τ ...) #'τs
+     #:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
+;     #:when (printf "e_fn: ~a\n" (typeof #'e_fn+))
+;     #:when (printf "τs: ~a\n" #'τs)
+     #:with (∀ (X ...) (→ τX ...)) (typeof #'e_fn+)
+;     #:when (printf "applied: ~a\n" (apply-forall (typeof #'e_fn+) #'τs))
+     #:with (→ τ_arg ... τ_res) (apply-forall (typeof #'e_fn+) #'τs)
+     #:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ_arg ...))
+     (⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]
+    [(_ any ...) #:when (printf "shouldnt get here\n") #'(stlc:#%app any ...)]))
 
 (define-syntax (letrec/tc stx)
   (syntax-parse stx #:datum-literals (:)
@@ -275,73 +117,8 @@
             (expand/df #'(letrec ([f e_f] ...) body ... body_result))
     (syntax/loc stx (letrec ([f+ e_f+] ...) body+ ... body_result+))]))
 
-; #%app
-(define-syntax (app/tc stx)
-  (syntax-parse stx #:literals (→ void) 
-                    #:datum-literals (:t)
-    [(_ :t x) #'(printf "~a : ~a\n" 'x (hash-ref runtime-env 'x))]
-    [(_ e_fn e_arg ...)
-     #:with (e_fn+ e_arg+ ...) (stx-map expand/df #'(e_fn e_arg ...))
-     #:with (→ τ ... τ_res) (typeof #'e_fn+)
-     #:when (stx-andmap assert-type #'(e_arg+ ...) #'(τ ...))
-     (⊢ (syntax/loc stx (#%app e_fn+ e_arg+ ...)) #'τ_res)]))
-
-(define-syntax (if/tc stx)
-  (syntax-parse stx
-    [(_ e_test e1 e2)
-     #:with e_test+ (expand/df #'e_test)
-     #:when (assert-type #'e_test+ #'Bool)
-     #:with e1+ (expand/df #'e1)
-     #:with e2+ (expand/df #'e2)
-     #:when (type=? (typeof #'e1+) (typeof #'e2+))
-     (⊢ (syntax/loc stx (if e_test+ e1+ e2+)) (typeof #'e1+))]))
-
-;; lists ----------------------------------------------------------------------
-(define-syntax (cons/tc stx)
-  (syntax-parse stx
-    [(_ {T} e1 e2)
-     #:with e1+ (expand/df #'e1)
-     #:with e2+ (expand/df #'e2)
-     #:when (assert-type #'e1+ #'T)
-     #:when (assert-type #'e2+ #'(Listof T))
-     (⊢ (syntax/loc stx (cons e1+ e2+)) #'(Listof T))]))
-(define-syntax (null/tc stx)
-  (syntax-parse stx
-    [(_ {T}) (⊢ (syntax/loc stx null) #'(Listof T))]))
-(define-syntax (null?/tc stx)
-  (syntax-parse stx
-    [(_ {T} e)
-     #:with e+ (expand/df #'e)
-     #:when (assert-type #'e+ #'(Listof T))
-     (⊢ (syntax/loc stx (null? e+)) #'Bool)]))
-(define-syntax (first/tc stx)
-  (syntax-parse stx
-    [(_ {T} e)
-     #:with e+ (expand/df #'e)
-     #:when (assert-type #'e+ #'(Listof T))
-     (⊢ (syntax/loc stx (car e+)) #'T)]))
-(define-syntax (rest/tc stx)
-  (syntax-parse stx
-    [(_ {T} e)
-     #:with e+ (expand/df #'e)
-     #:when (assert-type #'e+ #'(Listof T))
-     (⊢ (syntax/loc stx (cdr e+)) #'(Listof T))]))
-
-;; define, module-begin -------------------------------------------------------
-#;(define-syntax (define/tc stx)
-  (syntax-parse stx #:datum-literals (:)
-    [(_ (f:id [x:id : τ] ...) e ... e_result)
-     #:with (g ...) (map (λ (fn) (datum->syntax (car (syntax->list #'(x ...))) fn)) (hash-keys (Γ)))
-     #:with (lam1 (g+ ...) (#%exp (lam2 (x+ ...) e+ ... e_result+)))
-            (with-extended-type-env #'([x τ] ...)
-              (expand/df #'(λ (g ...) (λ (x ...) e ... e_result))))
-     #:when (stx-andmap assert-Unit-type #'(e+ ...))
-     #:with τ_result (typeof #'e_result+)
-     #:when (Γ (type-env-extend #'([f (→ τ ... τ_result)])))
-     (⊢ (syntax/loc stx (define (f x+ ...) e+ ... e_result+)) #'Unit)]
-    ))
-
-
+;; module-begin and associated stx-classes
+;; - copied from stlc.rkt: 2014-08-14
 (begin-for-syntax
   (define-syntax-class maybe-def #:datum-literals (: define variant) #:literals (define-type)
     (pattern (define (f:id [x:id : τx] ...) body ...)
@@ -384,6 +161,8 @@
      #:with ((begin deftype+ ...) ...) (stx-map expand/df/module-ctx #'(deftype ...))
      #:with (structdef ...) (stx-flatten #'((deftype+ ...) ...))
      #:with (structdef+:strct ...) (stx-map expand/df/module-ctx #'(structdef ...))
+     ;; <----- everything before here gets called twice (eg try inserting printf)
+     ;; (the expand on the previous line must be calling module begin?)
      #:with (def-val:def-val ...) #'(structdef+.def-val ...)
      #:with (def-val-lhs ...) #'(def-val.lhs ...)
      #:with (def-val-rhs ...) #'(def-val.rhs ...)
@@ -403,8 +182,44 @@
         #,(expand/df #'(let-values ([def-val-lhs def-val-rhs] ...)
                          (let-syntax ([def-syn-lhs def-syn-rhs] ...)
                            (letrec/tc ([f : τ v] ...) e ... (void)))))
-        (define #,(datum->syntax stx 'runtime-env)
+        #;(define #,(datum->syntax stx 'runtime-env)
           (for/hash ([x:τ '#,(map (λ (xτ) (cons (car xτ) (syntax->datum (cdr xτ))))
                                   (hash->list (do-subst (Γ))))])
             (values (car x:τ) (cdr x:τ))))
         ))]))
+
+;; testing fns ----------------------------------------------------------------
+;; for now, these are duplicated from stlc.rkt: 2014-08-14
+;; type checking testing: -----------------------------------------------------
+(require rackunit)
+(require (for-syntax rackunit "typecheck.rkt"))
+(provide check-equal?)
+(provide check-type-error check-type check-type-and-result check-not-type)
+
+(define-syntax (check-type-error stx)
+  (syntax-parse stx
+    [(_ e)
+     #:when (check-exn exn:fail? (λ () (expand/df #'e)))
+     #'(void)]))
+
+(define-syntax (check-type stx)
+  (syntax-parse stx #:datum-literals (:)
+    [(_ e : τ)
+     #:with e+ (expand/df #'e)
+     #:when (check-true (assert-type #'e+ #'τ) 
+                        (format "Expected type ~a but got type ~a" #'τ (typeof #'e)))
+     #'(void)]))
+
+(define-syntax (check-not-type stx)
+  (syntax-parse stx #:datum-literals (:)
+    [(_ e : τ)
+     #:with e+ (expand/df #'e)
+     #:when (check-false (type=? (typeof #'e+) #'τ) 
+                         (format "Expected type to not be ~a but got type ~a" #'τ (typeof #'e)))
+     #'(void)]))
+
+(define-syntax (check-type-and-result stx)
+  (syntax-parse stx #:datum-literals (: =>)
+    [(_ e : τ => v)
+     #'(begin (check-type e : τ)
+              (check-equal? e v))]))