commit dff0f2b79f06e097e767c67834c1c0ecf78aba96
parent e490825797c957d3a324c4dfda9300c6026a1961
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 13 Aug 2014 14:28:45 -0400
add stlc tests for recursive define-types (ie intlist)
Diffstat:
2 files changed, 37 insertions(+), 8 deletions(-)
diff --git 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
@@ -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
