www

commit 1985a987c9fbbc573749750dc97a035180337499
parent 35b36b37811f09fc26dee76b05c131e777e70a45
Author: Stephen Chang <stchang@ccs.neu.edu>
Date:   Wed,  3 Sep 2014 18:50:38 -0400

stlc+define+cons/racket-ext: check unit type in cases clauses

Diffstat:
M
stlc+define+cons-via-racket-extended.rkt
 | 
5
+++--

1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/stlc+define+cons-via-racket-extended.rkt b/stlc+define+cons-via-racket-extended.rkt
@@ -1,7 +1,7 @@
 #lang s-exp "racket-extended-for-implementing-typed-langs.rkt"
 (extends "stlc-via-racket-extended.rkt" λ)
 (inherit-types Int →)
-(require (for-syntax syntax/stx) "typecheck.rkt")
+(require (for-syntax syntax/stx "stx-utils.rkt") "typecheck.rkt")
 
 ;; Simply-Typed Lambda Calculus+
 ;; - stlc extended with practical language feature
@@ -18,6 +18,7 @@
 ;; - var args: TODO: primops can handle multiple args but not general application
 
 (declare-base-types String Bool Listof Unit)
+(define-for-syntax (assert-Unit-type e) (assert-type e #'Unit))
 
 (define-literal-type-rule boolean : Bool)
 (define-literal-type-rule str : String)
@@ -34,7 +35,7 @@
 (define-typed-syntax
   (cases e_test [Cons (x ...) e_body ... e_result] ...) : τ_res
   #:where
-;  (e_body : Unit) ... ...
+  (when: (stx-andmap (λ (bods) (stx-andmap assert-Unit-type bods)) #'((e_body ...) ...)))
   (let (τ ... → τ_Cons) := (typeof Cons)) ...
   (when: (or (null? (syntax->list #'(τ_Cons ...)))
              (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_Cons ...)))))