commit bb7ed03f3c9241a22b8020c7d6d9dbf28b4d2eea
parent c4813ebd95508c59278e468d45560d72067e9263
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 20 May 2015 19:27:19 -0400
add stlc+tup
Diffstat:
8 files changed, 270 insertions(+), 7 deletions(-)
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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.")]))
