From dff0f2b79f06e097e767c67834c1c0ecf78aba96 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 13 Aug 2014 14:28:45 -0400
Subject: [PATCH] add stlc tests for recursive define-types (ie intlist)

---
 stlc-tests.rkt | 27 ++++++++++++++++++++++++++-
 stlc.rkt       | 16 ++++++++++------
 2 files changed, 36 insertions(+), 7 deletions(-)

diff --git a/stlc-tests.rkt b/stlc-tests.rkt
index d6008be..5113568 100644
--- a/stlc-tests.rkt
+++ b/stlc-tests.rkt
@@ -100,4 +100,29 @@
 (check-type-error (define (maybeint->wrong [maybint : MaybeInt])
                     (cases maybint
                       [None () #f]
-                      [Just (x) x])))
\ No newline at end of file
+                      [Just (x) x])))
+
+(define-type IntList (variant (Null) (Cons Int IntList)))
+(check-type-and-result (Null) : IntList => (Null))
+(check-type-and-result (Cons 1 (Null)) : IntList => (Cons 1 (Null)))
+(check-type-error (Cons "one" (Null)))
+(check-type-error (Cons 1 2))
+(define (map/IntList [f : (→ Int Int)] [lst : IntList])
+  (cases lst
+    [Null () (Null)]
+    [Cons (x xs) (Cons (f x) (map/IntList f xs))]))
+(check-type-and-result (map/IntList add1 (Null)) : IntList => (Null))
+(check-type-and-result (map/IntList add1 (Cons 1 (Null))) : IntList => (Cons 2 (Null)))
+(check-type-and-result (map/IntList add1 (Cons 2 (Cons 1 (Null)))) 
+                       : IntList => (Cons 3 (Cons 2 (Null))))
+(check-type-error (map/IntList (λ ([n : Int]) #f) (Null)))
+(define-type BoolList (variant (BoolNull) (BoolCons Bool BoolList)))
+(define (map/BoolList [f : (→ Bool Int)] [lst : BoolList])
+  (cases lst
+    [BoolNull () (Null)]
+    [BoolCons (x xs) (Cons (f x) (map/BoolList f xs))]))
+(check-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : IntList)
+(check-type-and-result 
+ (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
+ : IntList => (Cons 1 (Null)))
+(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
\ No newline at end of file
diff --git a/stlc.rkt b/stlc.rkt
index 8dfa200..3c175bc 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -21,8 +21,12 @@
   [datum/tc #%datum] [module-begin/tc #%module-begin]
   [cons/tc cons] [null/tc null] [null?/tc null?] [first/tc first] [rest/tc rest]))
 
-;; TODO:
-;; - type of top level (or module level) vars not checked
+;; Simply-Typed Lambda Calculus+
+;; 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 τ)))
@@ -176,7 +180,7 @@
      #:with ((x ...) ...) (stx-map generate-temporaries #'((τ_fld ...) ...))
      #:when (Γ (type-env-extend #'([Cons (→ τ_fld ... τ)] ...)))
      #'(begin
-         (struct Cons (x ...)) ...)]))
+         (struct Cons (x ...) #:transparent) ...)]))
 (define-syntax (cases stx)
   (syntax-parse stx
     [(_ e [Cons (x ...) body ... body_result] ...)
@@ -184,7 +188,7 @@
      #:with (Cons+ ...) (stx-map expand/df #'(Cons ...))
      #:with ((→ τ ... τ_Cons) ...) (stx-map typeof #'(Cons+ ...))
      #:when (stx-andmap (λ (τ) (assert-type #'e+ τ)) #'(τ_Cons ...))
-     #:with ((lam xs+ body+ ... body_result+) ...) 
+     #:with ((lam (x+ ...) body+ ... body_result+) ...) 
             (stx-map (λ (bods xs τs) 
                        (with-extended-type-env 
                         (stx-map list xs τs)
@@ -197,7 +201,7 @@
      #:when (or (null? (syntax->list #'(τ_result ...)))
                 (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
                         (cdr (syntax->list #'(τ_result ...)))))
-     #'(match e+ [(Cons+ x ...) body+ ... body_result+] ...)]))
+     #`(match e+ [(Cons+ x+ ...) body+ ... body_result+] ...)]))
 
 ;; typed forms ----------------------------------------------------------------
 (define-syntax (datum/tc stx)
@@ -379,7 +383,7 @@
      #:with (τ ...) (template ((?@ . mb-form.τ) ...))
      #:with (e ...) (template ((?@ . mb-form.e) ...))
      #:when (Γ (type-env-extend #'([f τ] ...)))
-     #:when (printf "fvs :~a\n" (fvs))
+;     #:when (printf "fvs :~a\n" (fvs))
 ;; error: "Just10: unbound identifier; also, no #%top syntax transformer is bound"
 ;; cause: for struct def, define-values must come before define-syntaxes
      (quasisyntax/loc stx