From bb7ed03f3c9241a22b8020c7d6d9dbf28b4d2eea Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 20 May 2015 19:27:19 -0400
Subject: [PATCH] add stlc+tup

---
 tapl/ext-stlc.rkt             |   5 +-
 tapl/stlc+tup.rkt             |  29 ++++++++++
 tapl/stlc+var.rkt             |  19 ++++++
 tapl/stx-utils.rkt            |   5 +-
 tapl/tests/ext-stlc-tests.rkt |   3 +-
 tapl/tests/stlc+tup-tests.rkt | 103 +++++++++++++++++++++++++++++++++
 tapl/tests/stlc+var-tests.rkt | 105 ++++++++++++++++++++++++++++++++++
 tapl/typecheck.rkt            |   4 +-
 8 files changed, 267 insertions(+), 6 deletions(-)
 create mode 100644 tapl/stlc+tup.rkt
 create mode 100644 tapl/stlc+var.rkt
 create mode 100644 tapl/tests/stlc+tup-tests.rkt
 create mode 100644 tapl/tests/stlc+var-tests.rkt

diff --git a/tapl/ext-stlc.rkt b/tapl/ext-stlc.rkt
index 31b63aa..d1090ee 100644
--- a/tapl/ext-stlc.rkt
+++ b/tapl/ext-stlc.rkt
@@ -21,11 +21,12 @@
 ;; Terms:
 ;; - terms from stlc+lit.rkt
 ;; - literals: bool, string
-;; - prims: and, or, not, zero?
+;; - boolean prims, numeric prims
+;; - if
 ;; - prim void : (→ Unit)
 ;; - begin
 ;; - ascription (ann)
-;; - let
+;; - let, let*, letrec
 
 (define-base-type Bool)
 (define-base-type String)
diff --git a/tapl/stlc+tup.rkt b/tapl/stlc+tup.rkt
new file mode 100644
index 0000000..78a303f
--- /dev/null
+++ b/tapl/stlc+tup.rkt
@@ -0,0 +1,29 @@
+#lang racket/base
+(require
+  (for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
+  "typecheck.rkt")
+(require (prefix-in stlc: (only-in "ext-stlc.rkt" #%app λ))
+         (except-in "ext-stlc.rkt" #%app λ))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])
+         tup proj)
+(provide (all-from-out "ext-stlc.rkt"))
+ 
+;; Simply-Typed Lambda Calculus, plus tuples
+;; Types:
+;; - types from ext-stlc.rkt
+;; Terms:
+;; - terms from ext-stlc.rkt
+
+(define-syntax (tup stx)
+  (syntax-parse stx
+    [(_ e ...)
+     #:with ((e- τ) ...) (infers+erase #'(e ...))
+     (⊢ #'(list e- ...) #'(τ ...))]))
+(define-syntax (proj stx)
+  (syntax-parse stx
+    [(_ tup n:integer)
+     #:with (tup- τ_tup) (infer+erase #'tup)
+     #:fail-unless (not (identifier? #'τ_tup)) "not tuple type"
+     #:fail-unless (< (syntax->datum #'n) (stx-length #'τ_tup)) "proj index too large"
+     (⊢ #'(list-ref tup n) (stx-list-ref #'τ_tup (syntax->datum #'n)))]))
+   
\ No newline at end of file
diff --git a/tapl/stlc+var.rkt b/tapl/stlc+var.rkt
new file mode 100644
index 0000000..84953a2
--- /dev/null
+++ b/tapl/stlc+var.rkt
@@ -0,0 +1,19 @@
+#lang racket/base
+(require
+  (for-syntax racket/base syntax/parse syntax/stx racket/string "stx-utils.rkt")
+  "typecheck.rkt")
+(require (prefix-in stlc: (only-in "stlc+tup.rkt" #%app λ))
+         (except-in "stlc+tup.rkt" #%app λ))
+(provide (rename-out [stlc:#%app #%app] [stlc:λ λ])
+         tup proj)
+(provide (all-from-out "stlc+tup.rkt"))
+ 
+;; Simply-Typed Lambda Calculus, plus variants
+;; Types:
+;; - types from stlc+tup.rkt
+;; Terms:
+;; - terms from stlc+tup.rkt
+
+(provide Tmp Tmp2)
+(define-syntax Tmp (make-rename-transformer #'Int))
+(define-syntax Tmp2 (λ (stx) (syntax-parse stx [x:id #'(Int Int → Int)])))
\ No newline at end of file
diff --git a/tapl/stx-utils.rkt b/tapl/stx-utils.rkt
index ccb46d4..43cec5c 100644
--- a/tapl/stx-utils.rkt
+++ b/tapl/stx-utils.rkt
@@ -19,4 +19,7 @@
 
 (define (stx-length stx) (length (syntax->list stx)))
 
-(define (stx-last stx) (last (syntax->list stx)))
\ No newline at end of file
+(define (stx-last stx) (last (syntax->list stx)))
+
+(define (stx-list-ref stx i)
+  (list-ref (syntax->list stx) i))
\ No newline at end of file
diff --git a/tapl/tests/ext-stlc-tests.rkt b/tapl/tests/ext-stlc-tests.rkt
index dad46df..d59372c 100644
--- a/tapl/tests/ext-stlc-tests.rkt
+++ b/tapl/tests/ext-stlc-tests.rkt
@@ -64,7 +64,8 @@
                   (is-even? (sub1 n))))])
    (is-odd? 11)) : Bool ⇒ #t)
 
-;; tests from stlc+lit-tests.rkt - most should still pass --------------------------
+;; tests from stlc+lit-tests.rkt --------------------------
+; most should pass, some failing may now pass due to added types/forms
 (check-type 1 : Int)
 ;(check-not-type 1 : (Int → Int))
 ;(typecheck-fail "one") ; literal now supported
diff --git a/tapl/tests/stlc+tup-tests.rkt b/tapl/tests/stlc+tup-tests.rkt
new file mode 100644
index 0000000..845faa9
--- /dev/null
+++ b/tapl/tests/stlc+tup-tests.rkt
@@ -0,0 +1,103 @@
+#lang s-exp "../stlc+tup.rkt"
+(require "rackunit-typechecking.rkt")
+
+;; tests for tuples
+(check-type (tup 1 2 3) : (Int Int Int))
+(check-type (tup 1 "1" #f +) : (Int String Bool (Int Int → Int)))
+(check-not-type (tup 1 "1" #f +) : (Unit String Bool (Int Int → Int)))
+(check-not-type (tup 1 "1" #f +) : (Int Unit Bool (Int Int → Int)))
+(check-not-type (tup 1 "1" #f +) : (Int String Unit (Int Int → Int)))
+(check-not-type (tup 1 "1" #f +) : (Int String Bool (Int Int → Unit)))
+
+(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
+(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
+(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
+(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
+(typecheck-fail (proj 1 2)) ; not tuple
+
+;; ext-stlc.rkt tests ---------------------------------------------------------
+;; should still pass
+
+;; new literals and base types
+(check-type "one" : String) ; literal now supported
+(check-type #f : Bool) ; literal now supported
+
+(check-type (λ ([x : Bool]) x) : (Bool → Bool)) ; Bool is now valid type
+
+;; Unit
+(check-type (void) : Unit)
+(check-type void : (→ Unit))
+(typecheck-fail ((λ ([x : Unit]) x) 2))
+(typecheck-fail ((λ ([x : Unit])) void))
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(typecheck-fail (begin))
+(check-type (begin 1) : Int)
+(typecheck-fail (begin 1 2 3))
+(check-type (begin (void) 1) : Int ⇒ 1)
+
+;;ascription
+(typecheck-fail (ann 1 : Bool))
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(typecheck-fail (let ([x #f]) (+ x 1)))
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
+
+; letrec
+(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
+(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (Int → String))
+           (λ ([i : Int])
+             (if (= i 0)
+                 "liftoff"
+                 (countdown (- i 1))))])
+   (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (Int → Bool))
+           (λ ([n : Int])
+             (or (zero? n)
+                 (is-odd? (sub1 n))))]
+          [(is-odd? : (Int → Bool))
+           (λ ([n : Int])
+             (and (not (zero? n))
+                  (is-even? (sub1 n))))])
+   (is-odd? 11)) : Bool ⇒ #t)
+
+;; tests from stlc+lit-tests.rkt --------------------------
+; most should pass, some failing may now pass due to added types/forms
+(check-type 1 : Int)
+;(check-not-type 1 : (Int → Int))
+;(typecheck-fail "one") ; literal now supported
+;(typecheck-fail #f) ; literal now supported
+(check-type (λ ([x : Int] [y : Int]) x) : (Int Int → Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (Int → Int))
+(check-type (λ ([f : (Int → Int)]) 1) : ((Int → Int) → Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y))
+            : ((Int Int → Int) Int Int → Int))
+(check-type ((λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (Int → Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
diff --git a/tapl/tests/stlc+var-tests.rkt b/tapl/tests/stlc+var-tests.rkt
new file mode 100644
index 0000000..92cddba
--- /dev/null
+++ b/tapl/tests/stlc+var-tests.rkt
@@ -0,0 +1,105 @@
+#lang s-exp "../stlc+var.rkt"
+(require "rackunit-typechecking.rkt")
+
+(check-type ((λ ([x : Tmp]) (+ x 2)) 3) : Tmp)
+
+;; tests for tuples -----------------------------------------------------------
+(check-type (tup 1 2 3) : (Int Int Int))
+(check-type (tup 1 "1" #f +) : (Int String Bool (Int Int → Int)))
+(check-not-type (tup 1 "1" #f +) : (Unit String Bool (Int Int → Int)))
+(check-not-type (tup 1 "1" #f +) : (Int Unit Bool (Int Int → Int)))
+(check-not-type (tup 1 "1" #f +) : (Int String Unit (Int Int → Int)))
+(check-not-type (tup 1 "1" #f +) : (Int String Bool (Int Int → Unit)))
+
+(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
+(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
+(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f)
+(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large
+(typecheck-fail (proj 1 2)) ; not tuple
+
+;; ext-stlc.rkt tests ---------------------------------------------------------
+;; should still pass
+
+;; new literals and base types
+(check-type "one" : String) ; literal now supported
+(check-type #f : Bool) ; literal now supported
+
+(check-type (λ ([x : Bool]) x) : (Bool → Bool)) ; Bool is now valid type
+
+;; Unit
+(check-type (void) : Unit)
+(check-type void : (→ Unit))
+(typecheck-fail ((λ ([x : Unit]) x) 2))
+(typecheck-fail ((λ ([x : Unit])) void))
+(check-type ((λ ([x : Unit]) x) (void)) : Unit)
+
+;; begin
+(typecheck-fail (begin))
+(check-type (begin 1) : Int)
+(typecheck-fail (begin 1 2 3))
+(check-type (begin (void) 1) : Int ⇒ 1)
+
+;;ascription
+(typecheck-fail (ann 1 : Bool))
+(check-type (ann 1 : Int) : Int ⇒ 1)
+(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
+
+; let
+(check-type (let () (+ 1 1)) : Int ⇒ 2)
+(check-type (let ([x 10]) (+ 1 2)) : Int)
+(typecheck-fail (let ([x #f]) (+ x 1)))
+(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
+(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier
+
+(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
+(typecheck-fail (let* ([x #t] [y (+ x 1)]) 1))
+
+; letrec
+(typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y))
+(typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x))
+
+(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
+
+;; recursive
+(check-type
+ (letrec ([(countdown : (Int → String))
+           (λ ([i : Int])
+             (if (= i 0)
+                 "liftoff"
+                 (countdown (- i 1))))])
+   (countdown 10)) : String ⇒ "liftoff")
+
+;; mutually recursive
+(check-type
+ (letrec ([(is-even? : (Int → Bool))
+           (λ ([n : Int])
+             (or (zero? n)
+                 (is-odd? (sub1 n))))]
+          [(is-odd? : (Int → Bool))
+           (λ ([n : Int])
+             (and (not (zero? n))
+                  (is-even? (sub1 n))))])
+   (is-odd? 11)) : Bool ⇒ #t)
+
+;; tests from stlc+lit-tests.rkt --------------------------
+; most should pass, some failing may now pass due to added types/forms
+(check-type 1 : Int)
+;(check-not-type 1 : (Int → Int))
+;(typecheck-fail "one") ; literal now supported
+;(typecheck-fail #f) ; literal now supported
+(check-type (λ ([x : Int] [y : Int]) x) : (Int Int → Int))
+(check-not-type (λ ([x : Int]) x) : Int)
+(check-type (λ ([x : Int]) x) : (Int → Int))
+(check-type (λ ([f : (Int → Int)]) 1) : ((Int → Int) → Int))
+(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
+;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
+(check-type (λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y))
+            : ((Int Int → Int) Int Int → Int))
+(check-type ((λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (Int → Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
+(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
+
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 11d45fc..7457d25 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -25,7 +25,7 @@
     [(_ τ:id)
      #:with τ? (format-id #'τ "~a?" #'τ)
      #'(begin
-         (provide τ)
+         (provide τ (for-syntax τ?))
          (define-syntax (τ stx)
            (syntax-parse stx
              [_ (error 'Int "Cannot use type at run time.")]))
@@ -37,7 +37,7 @@
     [(_ τ:id)
      #:with τ? (format-id #'τ "~a?" #'τ)
      #'(begin
-         (provide τ)
+         (provide τ (for-syntax τ?))
          (define-syntax (τ stx)
            (syntax-parse stx
              [_ (error 'Int "Cannot use type at run time.")]))