ext-stlc.rkt (5673B)
1 #lang turnstile/lang 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 ;; - let, let*, letrec 17 ;; Top-level: 18 ;; - define (values and functions) 19 ;; - define-type-alias 20 21 (provide define-type-alias 22 (for-syntax current-join) ⊔ 23 (type-out Bool String Float Char Unit) 24 zero? = 25 (rename-out [typed- -] [typed* *]) 26 (typed-out [add1 (→ Int Int)] 27 [sub1 : (→ Int Int)] 28 [[not- (→ Bool Bool)] not] 29 [[void- : (→ Unit)] void]) 30 define #%datum and or if begin let let* letrec) 31 32 (define-base-types Bool String Float Char Unit) 33 34 ;; test all variations of define-primop and typed-out 35 (define-primop zero? (→ Int Bool)) 36 (define-primop = : (→ Int Int Bool)) 37 (define-primop typed- - (→ Int Int Int)) 38 (define-primop typed* * : (→ Int Int Int)) 39 40 ;; τ.norm in 1st case causes "not valid type" error when file is compiled 41 (define-syntax define-type-alias 42 (syntax-parser 43 [(_ alias:id τ:any-type) 44 #'(define-syntax- alias 45 (make-variable-like-transformer #'τ))] 46 [(_ (f:id x:id ...) ty) 47 #'(define-syntax- (f stx) 48 (syntax-parse stx 49 [(_ x ...) 50 #:with τ:any-type #'ty 51 #'τ.norm]))])) 52 53 (define-typed-syntax define 54 [(_ x:id (~datum :) τ:type e:expr) ≫ 55 ;[⊢ e ≫ e- ⇐ τ.norm] 56 #:with y (generate-temporary #'x) 57 -------- 58 [≻ (begin- 59 (define-syntax x (make-rename-transformer (⊢ y : τ.norm))) 60 (define- y (ann e : τ.norm)))]] 61 [(_ x:id e) ≫ 62 ;This won't work with mutually recursive definitions 63 [⊢ e ≫ e- ⇒ τ] 64 #:with y (generate-temporary #'x) 65 #:with y+props (transfer-props #'e- (assign-type #'y #'τ)) 66 -------- 67 [≻ (begin- 68 (define-syntax x (make-rename-transformer #'y+props)) 69 (define- y e-))]] 70 [(_ (f [x (~datum :) ty] ... (~or (~datum →) (~datum ->)) ty_out) e ...+) ≫ 71 #:with f- (add-orig (generate-temporary #'f) #'f) 72 -------- 73 [≻ (begin- 74 (define-syntax- f 75 (make-rename-transformer (⊢ f- : (→ ty ... ty_out)))) 76 (define- f- 77 (stlc+lit:λ ([x : ty] ...) 78 (stlc+lit:ann (begin e ...) : ty_out))))]]) 79 80 (define-typed-syntax #%datum 81 [(_ . b:boolean) ≫ 82 -------- 83 [⊢ (#%datum- . b) ⇒ Bool]] 84 [(_ . s:str) ≫ 85 -------- 86 [⊢ (#%datum- . s) ⇒ String]] 87 [(_ . f) ≫ 88 #:when (flonum? (syntax-e #'f)) 89 -------- 90 [⊢ (#%datum- . f) ⇒ Float]] 91 [(_ . c:char) ≫ 92 -------- 93 [⊢ (#%datum- . c) ⇒ Char]] 94 [(_ . x) ≫ 95 -------- 96 [≻ (stlc+lit:#%datum . x)]]) 97 98 (define-typed-syntax (and e ...) ≫ 99 [⊢ e ≫ e- ⇐ Bool] ... 100 -------- 101 [⊢ (and- e- ...) ⇒ Bool]) 102 103 (define-typed-syntax (or e ...) ≫ 104 [⊢ e ≫ e- ⇐ Bool] ... 105 -------- 106 [⊢ (or- e- ...) ⇒ Bool]) 107 108 (begin-for-syntax 109 (define current-join 110 (make-parameter 111 (λ (x y) 112 (unless (typecheck? x y) 113 (type-error 114 #:src x 115 #:msg "branches have incompatible types: ~a and ~a" x y)) 116 x)))) 117 118 (define-syntax ⊔ 119 (syntax-parser 120 [(⊔ τ1 τ2 ...) 121 (for/fold ([τ ((current-type-eval) #'τ1)]) 122 ([τ2 (in-list (stx-map (current-type-eval) #'[τ2 ...]))]) 123 ((current-join) τ τ2))])) 124 125 (define-typed-syntax if 126 [(_ e_tst e1 e2) ⇐ τ-expected ≫ 127 [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. 128 [⊢ e1 ≫ e1- ⇐ τ-expected] 129 [⊢ e2 ≫ e2- ⇐ τ-expected] 130 -------- 131 [⊢ (if- e_tst- e1- e2-)]] 132 [(_ e_tst e1 e2) ≫ 133 [⊢ e_tst ≫ e_tst- ⇒ _] ; Any non-false value is truthy. 134 [⊢ e1 ≫ e1- ⇒ τ1] 135 [⊢ e2 ≫ e2- ⇒ τ2] 136 -------- 137 [⊢ (if- e_tst- e1- e2-) ⇒ (⊔ τ1 τ2)]]) 138 139 (define-typed-syntax begin 140 [(_ e_unit ... e) ⇐ τ_expected ≫ 141 [⊢ e_unit ≫ e_unit- ⇒ _] ... 142 [⊢ e ≫ e- ⇐ τ_expected] 143 -------- 144 [⊢ (begin- e_unit- ... e-)]] 145 [(_ e_unit ... e) ≫ 146 [⊢ e_unit ≫ e_unit- ⇒ _] ... 147 [⊢ e ≫ e- ⇒ τ_e] 148 -------- 149 [⊢ (begin- e_unit- ... e-) ⇒ τ_e]]) 150 151 (define-typed-syntax let 152 [(_ ([x e] ...) e_body ...) ⇐ τ_expected ≫ 153 [⊢ e ≫ e- ⇒ : τ_x] ... 154 [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- ⇐ τ_expected] 155 -------- 156 [⊢ (let- ([x- e-] ...) e_body-)]] 157 [(_ ([x e] ...) e_body ...) ≫ 158 [⊢ e ≫ e- ⇒ : τ_x] ... 159 [[x ≫ x- : τ_x] ... ⊢ (begin e_body ...) ≫ e_body- ⇒ τ_body] 160 -------- 161 [⊢ (let- ([x- e-] ...) e_body-) ⇒ τ_body]]) 162 163 ; dont need to manually transfer expected type 164 ; result template automatically propagates properties 165 ; - only need to transfer expected type when local expanding an expression 166 ; - see let/tc 167 (define-typed-syntax let* 168 [(_ () e_body ...) ≫ 169 -------- 170 [≻ (begin e_body ...)]] 171 [(_ ([x e] [x_rst e_rst] ...) e_body ...) ≫ 172 -------- 173 [≻ (let ([x e]) (let* ([x_rst e_rst] ...) e_body ...))]]) 174 175 (define-typed-syntax letrec 176 [(_ ([b:type-bind e] ...) e_body ...) ⇐ τ_expected ≫ 177 [[b.x ≫ x- : b.type] ... 178 ⊢ [e ≫ e- ⇐ b.type] ... [(begin e_body ...) ≫ e_body- ⇐ τ_expected]] 179 -------- 180 [⊢ (letrec- ([x- e-] ...) e_body-)]] 181 [(_ ([b:type-bind e] ...) e_body ...) ≫ 182 [[b.x ≫ x- : b.type] ... 183 ⊢ [e ≫ e- ⇐ b.type] ... [(begin e_body ...) ≫ e_body- ⇒ τ_body]] 184 -------- 185 [⊢ (letrec- ([x- e-] ...) e_body-) ⇒ τ_body]]) 186 187