From e05e60a5668d6c40dde62df5493fd8e7198c448f Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 28 Aug 2014 16:23:17 -0400 Subject: [PATCH] stlc+define-ext: add begin, void, if --- stlc+define+cons-via-racket-extended.rkt | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/stlc+define+cons-via-racket-extended.rkt b/stlc+define+cons-via-racket-extended.rkt index ee89dd5..bdaf914 100644 --- a/stlc+define+cons-via-racket-extended.rkt +++ b/stlc+define+cons-via-racket-extended.rkt @@ -1,5 +1,6 @@ #lang s-exp "racket-extended-for-implementing-typed-langs.rkt" (extends "stlc-via-racket-extended.rkt") + ;(require "stlc-via-racket-extended.rkt") ;(provide Int → + λ #%app #%top-interaction #%module-begin) ;(provide #%top-interaction) @@ -50,6 +51,7 @@ (declare-base-types String Bool Listof Unit) (define-literal-type-rule boolean : Bool) +(define-literal-type-rule str : String) ;(define-and-provide-builtin-types String Bool Listof Unit) ;(provide (for-syntax assert-Unit-type assert-String-type)) @@ -99,6 +101,12 @@ [(_ . b:boolean) (⊢ (syntax/loc stx (#%datum . b)) #'Bool)] [(_ . x) #'(stlc:#%datum . x)])) +(define-simple-syntax/type-rule + (begin e ... e_result) : τ_result + #:where + (e : Unit) ... + (let τ_result := (typeof e_result))) + #;(define-syntax (begin/tc stx) (syntax-parse stx [(_ e ... e_result) @@ -110,6 +118,9 @@ (syntax-parse stx [(_) (⊢ (syntax/loc stx (void)) #'Unit)])) +(define-simple-syntax/type-rule + (void) : Unit) + #;(define-syntax (printf/tc stx) (syntax-parse stx [(_ τs str . args) @@ -189,6 +200,13 @@ #'e1 (typeof #'e1+) #'e2 (typeof #'e2+))) (⊢ (syntax/loc stx (if e_test+ e1+ e2+)) (typeof #'e1+))])) +(define-simple-syntax/type-rule + (if e_test e1 e2) : τ2 + #:where + (e_test : Bool) + (let τ1 := (typeof e1)) + (let τ2 := (typeof e2)) + (τ1 == τ2)) ;; lists ---------------------------------------------------------------------- #;(define-syntax (cons/tc stx)