commit 857fee962f9176a0fd19cb021d17d81a3c740631
parent 4783c7f93e512193bf0691902c3120c2a6b66e67
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 14 Aug 2014 14:28:18 -0400
fix some stlc bugs
- need to manually check for lone identifiers in lambda body
- ow they wont get expanded and wont get a type
- in type=?, make sure tycons have same number of args
Diffstat:
| M | stlc-tests.rkt | | | 140 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ |
| M | stlc.rkt | | | 15 | ++++++++++++--- |
2 files changed, 152 insertions(+), 3 deletions(-)
diff --git a/stlc-tests.rkt b/stlc-tests.rkt
@@ -5,6 +5,15 @@
(check-equal? ((λ ([x : Int]) (+ x 1)) 10) 11) ; identifier used out of context
(check-type-and-result ((λ ([x : Int]) (+ x 1)) 10) : Int => 11)
+; check fns with literal or id bodies
+(check-type (λ ([x : Int]) x) : (→ Int Int))
+(check-type (λ ([x : Unit] [y : Int]) x y) : (→ Unit Int Int))
+
+;; check fns with multi-expr body
+(check-type (λ ([x : Int]) (void) x) : (→ Int Int))
+(check-type-error (λ ([x : Int]) 1 x))
+(check-type (λ ([x : Int]) (void) (void) x) : (→ Int Int))
+
; HO fn
(check-type-and-result ((λ ([f : (→ Int Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
(check-type (λ ([f : (→ Int Int)]) (f 10)) : (→ (→ Int Int) Int))
@@ -97,6 +106,98 @@
(check-type-and-result (maybeint->bool (None)) : Bool => #f)
(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
(check-type-error (maybeint->bool 25))
+(check-type-error (define (maybeint->wrong [maybint : MaybeIn; HO fn
+(check-type-and-result ((λ ([f : (→ Int Int)]) (f 10)) (λ ([x : Int]) (+ x 1))) : Int => 11)
+(check-type (λ ([f : (→ Int Int)]) (f 10)) : (→ (→ Int Int) Int))
+(check-type (λ ([f : (→ Int Int)]) (λ ([x : Int]) (f (f x)))) : (→ (→ Int Int) (→ Int Int)))
+(check-type-error (λ (f : (→ Int Int)) (λ (x : String) (f (f x)))))
+
+;; shadowed var
+(check-type-error ((λ ([x : Int]) ((λ ([x : String]) x) x)) 10))
+(check-type-and-result ((λ ([x : String]) ((λ ([x : Int]) (+ x 1)) 10)) "ten") : Int => 11)
+
+;; let
+(check-type-and-result (let ([x 1] [y 2]) (+ x y)) : Int => 3)
+(check-type-error (let ([x 1] [y "two"]) (+ x y)))
+(check-type-and-result (let ([x "one"]) (let ([x 2]) (+ x x))) : Int => 4)
+
+;; lists
+(check-type-and-result (first {Int} (cons {Int} 1 (null {Int}))) : Int => 1)
+(check-type-and-result (rest {Int} (cons {Int} 1 (null {Int}))) : (Listof Int) => (null {Int}))
+(check-type-error (cons {Int} 1 (null {String})))
+(check-type-error (cons {Int} "one" (null {Int})))
+(check-type-error (cons {String} 1 (null {Int})))
+(check-type-error (cons {String} 1 (null {Int})))
+(check-type-error (cons {String} "one" (cons {Int} "two" (null {String}))))
+(check-type-and-result (first {String} (cons {String} "one" (cons {String} "two" (null {String}))))
+ : String => "one")
+(check-type-and-result (null? {String} (null {String})) : Bool => #t)
+(check-type-and-result (null? {String} (cons {String} "one" (null {String}))) : Bool => #f)
+(check-type-error (null? {String} (null {Int})))
+(check-type-error (null? {Int} (null {String})))
+(check-type-error (null? {Int} 1))
+(check-type-error (null? {Int} "one"))
+(check-type-error (null? {Int} (cons {String} "one" (null {String}))))
+
+; begin and void
+(check-type (void) : Unit)
+(check-type-and-result (begin (void) 1) : Int => 1)
+(check-type-and-result (begin (void) (void) 1) : Int => 1)
+(check-type-and-result (begin (void) (void) (void)) : Unit => (void))
+(check-type-and-result (begin (+ 1 2)) : Int => 3)
+(check-type-error (begin 1 2))
+
+(check-type (λ ([x : Int]) (void) (+ x 1)) : (→ Int Int))
+(check-type-error (λ ([x : Int]) 1 1))
+(check-type (λ ([x : Int] [y : Int]) (+ x y)) : (→ Int Int Int))
+(check-type-and-result ((λ ([a : Int] [b : Int] [c : Int]) (void) (void) (+ a b c)) 1 2 3)
+ : Int => 6)
+
+; define
+(define (g [y : Int]) (+ (f y) 1))
+(define (f [x : Int]) (+ x 1))
+(check-type-and-result (f 10) : Int => 11)
+(check-type-and-result (g 100) : Int => 102)
+(check-not-type (f 10) : String)
+(check-not-type (g 100) : String)
+
+;; if
+(check-type-and-result (if (null? {Int} (null {Int})) 1 2) : Int => 1)
+(check-type-and-result (if (null? {Int} (cons {Int} 1 (null {Int}))) 1 2) : Int => 2)
+(check-type-error (if (null? {Int} (null {Int})) 1 "one"))
+(check-type-error (if (null? {Int} (null {Int})) "one" 1))
+(check-type-error (if 1 2 3))
+
+;;; recursive fn
+(define (add1 [x : Int]) (+ x 1))
+(define (map [f : (→ Int Int)] [lst : (Listof Int)])
+ (if (null? {Int} lst)
+ (null {Int})
+ (cons {Int} (f (first {Int} lst)) (map f (rest {Int} lst)))))
+(check-type-and-result (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
+ : (Listof Int)
+ => (cons {Int} 2 (cons {Int} 3 (null {Int}))))
+(check-not-type (map add1 (cons {Int} 1 (cons {Int} 2 (null {Int}))))
+ : (Listof String))
+
+;; recursive types
+(define (a [x : Int]) (b x))
+(define (b [x : Int]) (a x))
+(define (ff [x : Int]) (ff x))
+
+;; define-type (non parametric)
+(define-type MaybeInt (variant (None) (Just Int)))
+(check-type (None) : MaybeInt)
+(check-type (Just 10) : MaybeInt)
+(check-type-error (Just "ten"))
+(check-type-error (Just (None)))
+(define (maybeint->bool [maybint : MaybeInt])
+ (cases maybint
+ [None () #f]
+ [Just (x) #t]))
+(check-type-and-result (maybeint->bool (None)) : Bool => #f)
+(check-type-and-result (maybeint->bool (Just 25)) : Bool => #t)
+(check-type-error (maybeint->bool 25))
(check-type-error (define (maybeint->wrong [maybint : MaybeInt])
(cases maybint
[None () #f]
@@ -136,4 +237,43 @@
(cases lst
[Null () (None)]
[Cons (x xs) (Just x)]))
+ (Null)) : MaybeInt)t])
+ (cases maybint
+ [None () #f]
+ [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)
+;; check typename is available
+(check-type (λ ([lst : IntList])
+ (cases lst
+ [Null () (None)]
+ [Cons (x xs) (Just x)]))
+ : (→ IntList MaybeInt))
+(check-type ((λ ([lst : IntList])
+ (cases lst
+ [Null () (None)]
+ [Cons (x xs) (Just x)]))
(Null)) : MaybeInt)
\ No newline at end of file
diff --git a/stlc.rkt b/stlc.rkt
@@ -116,6 +116,7 @@
[(x:id y:id) (free-identifier=? τ1 τ2)]
[((tycon1 τ1 ...) (tycon2 τ2 ...))
(and (free-identifier=? #'tycon1 #'tycon2)
+ (= (length (syntax->list #'(τ1 ...))) (length (syntax->list #'(τ2 ...))))
(stx-andmap type=? #'(τ1 ...) #'(τ2 ...)))]
[_ #f]))
@@ -241,10 +242,18 @@
;; 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++)) #'(→ τ ... τ_body))]))
(define-syntax (let/tc stx)
(syntax-parse stx #:datum-literals (:)
