From 1985a987c9fbbc573749750dc97a035180337499 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 3 Sep 2014 18:50:38 -0400 Subject: [PATCH] stlc+define+cons/racket-ext: check unit type in cases clauses --- 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 index 59331d3..ffc3968 100644 --- 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 ...)))))