ext-stlc.rkt (5604B)
1 #lang s-exp macrotypes/typecheck 2 (extends "stlc+lit.rkt" #:except #%datum) 3 4 ;; Simply-Typed Lambda Calculus, plus extensions (TAPL ch11) 5 ;; Types: 6 ;; - types from stlc+lit.rkt 7 ;; - Bool, String 8 ;; - Unit 9 ;; Terms: 10 ;; - terms from stlc+lit.rkt 11 ;; - literals: bool, string 12 ;; - boolean prims, numeric prims 13 ;; - if 14 ;; - prim void : (→ Unit) 15 ;; - begin 16 ;; - ascription (ann) 17 ;; - let, let*, letrec 18 ;; Top-level: 19 ;; - define (values only) 20 ;; - define-type-alias 21 22 (provide define-type-alias 23 (for-syntax current-join) ⊔ 24 (type-out Bool String Float Char Unit) 25 zero? = 26 (rename-out [typed- -] [typed* *]) 27 ;; test all variations of typed-out 28 (typed-out [add1 (→ Int Int)] 29 [sub1 : (→ Int Int)] 30 [[not- (→ Bool Bool)] not] 31 [[void- : (→ Unit)] void]) 32 define #%datum and or if begin ann let let* letrec) 33 34 (define-base-types Bool String Float Char Unit) 35 36 ;; test all variations of define-primop-out 37 (define-primop zero? (→ Int Bool)) 38 (define-primop = : (→ Int Int Bool)) 39 (define-primop typed- - (→ Int Int Int)) 40 (define-primop typed* * : (→ Int Int Int)) 41 42 ;; τ.norm in 1st case causes "not valid type" error when file is compiled 43 (define-syntax define-type-alias 44 (syntax-parser 45 [(_ alias:id τ:any-type) 46 #'(define-syntax- alias 47 (make-variable-like-transformer #'τ))] 48 [(_ (f:id x:id ...) ty) 49 #'(define-syntax- (f stx) 50 (syntax-parse stx 51 [(_ x ...) 52 #:with τ:any-type #'ty 53 #'τ.norm]))])) 54 55 (define-typed-syntax define 56 [(_ x:id e) 57 #:with (e- τ) (infer+erase #'e) 58 #:with y (generate-temporary) 59 #'(begin- 60 (define-syntax x (make-rename-transformer (⊢ y : τ))) 61 (define- y e-))]) 62 63 (define-typed-syntax #%datum 64 [(_ . b:boolean) (⊢ #,(syntax/loc stx (#%datum- . b)) : Bool)] 65 [(_ . s:str) (⊢ #,(syntax/loc stx (#%datum- . s)) : String)] 66 [(_ . f) #:when (flonum? (syntax-e #'f)) 67 (⊢ #,(syntax/loc stx (#%datum- . f)) : Float)] 68 [(_ . c:char) (⊢ #,(syntax/loc stx (#%datum- . c)) : Char)] 69 [(_ . x) (syntax/loc stx (stlc+lit:#%datum . x))]) 70 71 (define-typed-syntax and 72 [(_ e1 e2) 73 #:with Bool* ((current-type-eval) #'Bool) 74 #:with [e1- τ_e1] (infer+erase #'e1) 75 #:with [e2- τ_e2] (infer+erase #'e2) 76 #:fail-unless (typecheck? #'τ_e1 #'Bool*) 77 (typecheck-fail-msg/1 #'Bool* #'τ_e1 #'e1) 78 #:fail-unless (typecheck? #'τ_e2 #'Bool*) 79 (typecheck-fail-msg/1 #'Bool* #'τ_e2 #'e2) 80 (⊢ (and- e1- e2-) : Bool)]) 81 82 (define-typed-syntax or 83 [(_ e ...) 84 #:with ([_ Bool*] ...) #`([e #,((current-type-eval) #'Bool)] ...) 85 #:with ([e- τ_e] ...) (infers+erase #'(e ...)) 86 #:fail-unless (typechecks? #'(τ_e ...) #'(Bool* ...)) 87 (typecheck-fail-msg/multi 88 #'(Bool* ...) #'(τ_e ...) #'(e ...)) 89 (⊢ (or- e- ...) : Bool)]) 90 91 (begin-for-syntax 92 (define current-join 93 (make-parameter 94 (λ (x y) 95 (unless (typecheck? x y) 96 (type-error 97 #:src x 98 #:msg "branches have incompatible types: ~a and ~a" x y)) 99 x)))) 100 101 (define-syntax ⊔ 102 (syntax-parser 103 [(⊔ τ1 τ2 ...) 104 (for/fold ([τ ((current-type-eval) #'τ1)]) 105 ([τ2 (in-list (stx-map (current-type-eval) #'[τ2 ...]))]) 106 ((current-join) τ τ2))])) 107 108 (define-typed-syntax if 109 [(_ e_tst e1 e2) 110 #:with τ-expected (get-expected-type stx) 111 #:with [e_tst- _] (infer+erase #'e_tst) 112 #:with e1_ann #'(add-expected e1 τ-expected) 113 #:with e2_ann #'(add-expected e2 τ-expected) 114 #:with (e1- τ1) (infer+erase #'e1_ann) 115 #:with (e2- τ2) (infer+erase #'e2_ann) 116 (⊢ (if- e_tst- e1- e2-) : (⊔ τ1 τ2))]) 117 118 (define-typed-syntax begin 119 [(_ e_unit ... e) 120 #:with ([e_unit- _] ...) (infers+erase #'(e_unit ...)) 121 #:with (e- τ) (infer+erase #'e) 122 (⊢/no-teval (begin- e_unit- ... e-) : τ)]) 123 124 (define-typed-syntax ann #:datum-literals (:) 125 [(_ e : ascribed-τ:type) 126 #:with (e- τ) (infer+erase #'(add-expected e ascribed-τ.norm)) 127 #:fail-unless (typecheck? #'τ #'ascribed-τ.norm) 128 (typecheck-fail-msg/1 #'ascribed-τ.norm #'τ #'e) 129 (⊢/no-teval e- : ascribed-τ.norm)]) 130 131 (define-typed-syntax let 132 [(_ ([x e] ...) e_body) 133 #:with τ-expected (get-expected-type stx) 134 #:with ((e- τ) ...) (infers+erase #'(e ...)) 135 #:with ((x- ...) e_body- τ_body) 136 (infer/ctx+erase #'([x τ] ...) #'(add-expected e_body τ-expected)) 137 #:fail-unless (or (not (syntax-e #'τ-expected)) ; no expected type 138 (typecheck? #'τ_body ((current-type-eval) #'τ-expected))) 139 (typecheck-fail-msg/1 #'τ-expected #'τ_body #'e_body) 140 (⊢/no-teval (let- ([x- e-] ...) e_body-) : τ_body)]) 141 142 ; dont need to manually transfer expected type 143 ; result template automatically propagates properties 144 ; - only need to transfer expected type when local expanding an expression 145 ; - see let/tc 146 (define-typed-syntax let* 147 [(_ () e_body) 148 #:with τ-expected (get-expected-type stx) 149 #'e_body] 150 [(_ ([x e] [x_rst e_rst] ...) e_body) 151 #:with τ-expected (get-expected-type stx) 152 #'(let ([x e]) (let* ([x_rst e_rst] ...) e_body))]) 153 154 (define-typed-syntax letrec 155 [(_ ([b:type-bind e] ...) e_body) 156 #:with ((x- ...) (e- ... e_body-) (τ ... τ_body)) 157 (infers/ctx+erase #'(b ...) #'((add-expected e b.type) ... e_body)) 158 #:fail-unless (typechecks? #'(b.type ...) #'(τ ...)) 159 (typecheck-fail-msg/multi #'(b.type ...) #'(τ ...) #'(e ...)) 160 (⊢/no-teval (letrec- ([x- e-] ...) e_body-) : τ_body)])