stlc+reco+var.rkt (5430B)
1 #lang s-exp macrotypes/typecheck 2 (extends "stlc+tup.rkt" #:except × ×? tup proj ~×) 3 (require (only-in "stlc+tup.rkt" [~× ~stlc:×])) 4 5 ;; Simply-Typed Lambda Calculus, plus records and variants 6 ;; Types: 7 ;; - types from stlc+tup.rkt 8 ;; - redefine tuple type × to records 9 ;; - sum type constructor ∨ 10 ;; Terms: 11 ;; - terms from stlc+tup.rkt 12 ;; - redefine tup to records 13 ;; - sums (var) 14 15 (provide (type-out × ∨) tup proj var case) 16 17 ; re-define tuples as records 18 ; dont use define-type-constructor because I want the : literal syntax 19 (define-syntax × 20 (syntax-parser #:datum-literals (:) 21 [(_ [label:id : τ:type] ...) 22 #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...)) 23 #`(stlc+tup:× valid-τ ...)])) 24 (begin-for-syntax 25 (define-syntax ~× 26 (pattern-expander 27 (syntax-parser #:datum-literals (:) 28 [(_ [l : τ_l] (~and ddd (~literal ...))) 29 #'(~stlc:× ((~literal #%plain-app) (quote l) τ_l) ddd)] 30 [(_ . args) 31 #'(~and (~stlc:× ((~literal #%plain-app) (quote l) τ_l) (... ...)) 32 (~parse args #'((l τ_l) (... ...))))]))) 33 (define ×? stlc+tup:×?) 34 (define-syntax ~×* 35 (pattern-expander 36 (syntax-parser #:datum-literals (:) 37 [(_ [l : τ_l] (~and ddd (~literal ...))) 38 #'(~or (~× [l : τ_l] ddd) 39 (~and any (~do (type-error 40 #:src #'any 41 #:msg "Expected × type, got: ~a" #'any))))])))) 42 43 (begin-for-syntax 44 (define (stx-assoc-ref stx-lst lookup-k #:else [fail (λ () #f)]) 45 (define match_res (stx-assoc lookup-k stx-lst)) 46 (cond [match_res 47 (stx-cadr match_res)] 48 [else 49 (fail)])) 50 (define (×-ref ×-type l) 51 (syntax-parse ×-type 52 [(~× [l_τ : τ] ...) 53 (define res 54 (stx-assoc-ref #'([l_τ τ] ...) l #:else (λ () (error 'X-ref "bad!")))) 55 (add-orig res (get-orig res))]))) 56 57 ;; records 58 (define-typed-syntax tup #:datum-literals (=) 59 [(_ [l:id = e] ...) 60 #:with ([e- τ] ...) (infers+erase #'(e ...)) 61 (⊢ (list- (list- 'l e-) ...) : (× [l : τ] ...))]) 62 (define-typed-syntax proj #:literals (quote) 63 [(_ e_rec l:id) 64 #:with [e_rec- τ_e] (infer+erase #'e_rec) 65 #:fail-unless (×? #'τ_e) 66 (format "Expected expression ~s to have × type, got: ~a" 67 (syntax->datum #'e_rec) (type->str #'τ_e)) 68 #:with τ_l (×-ref #'τ_e #'l) 69 (⊢ (cadr- (assoc- 'l e_rec-)) : τ_l)]) 70 71 (define-type-constructor ∨/internal #:arity >= 0) 72 73 ;; variants 74 (define-syntax ∨ 75 (syntax-parser #:datum-literals (:) 76 [(_ (~and [label:id : τ:type] x) ...) 77 #:when (> (stx-length #'(x ...)) 0) 78 #:with (valid-τ ...) (stx-map mk-type #'(('label τ.norm) ...)) 79 #'(∨/internal valid-τ ...)] 80 [any 81 (type-error #:src #'any 82 #:msg (string-append 83 "Improper usage of type constructor ∨: ~a, " 84 "expected (∨ [label:id : τ:type] ...+)") 85 #'any)])) 86 (begin-for-syntax 87 (define ∨? ∨/internal?) 88 (define-syntax ~∨ 89 (pattern-expander 90 (syntax-parser #:datum-literals (:) 91 [(_ [l : τ_l] (~and ddd (~literal ...))) 92 #'(~∨/internal ((~literal #%plain-app) (quote l) τ_l) ddd)] 93 [(_ . args) 94 #'(~and (~∨/internal ((~literal #%plain-app) (quote l) τ_l) (... ...)) 95 (~parse args #'((l τ_l) (... ...))))]))) 96 (define-syntax ~∨* 97 (pattern-expander 98 (syntax-parser #:datum-literals (:) 99 [(_ [l : τ_l] (~and ddd (~literal ...))) 100 #'(~and (~or (~∨ [l : τ_l] ddd) 101 (~and any (~do (type-error 102 #:src #'any 103 #:msg "Expected ∨ type, got: ~a" #'any)))) 104 ~!)])))) ; dont backtrack here 105 106 (begin-for-syntax 107 (define (∨-ref ∨-type l #:else [fail (λ () #f)]) 108 (syntax-parse ∨-type 109 [(~∨ [l_τ : τ] ...) 110 (define res 111 (stx-assoc-ref #'([l_τ τ] ...) l #:else fail)) 112 (add-orig res (get-orig res))]))) 113 114 (define-typed-syntax var #:datum-literals (as =) 115 [(_ l:id = e as τ:type) 116 #:fail-unless (∨? #'τ.norm) 117 (format 118 "Expected the expected type to be a ∨ type, got: ~a" 119 (type->str #'τ.norm)) 120 #:with τ_match 121 (∨-ref 122 #'τ.norm #'l #:else 123 (λ () 124 (raise-syntax-error #f 125 (format "~a field does not exist" (syntax->datum #'l)) 126 stx))) 127 #:with [e- τ_e] (infer+erase #'e) 128 #:fail-unless (typecheck? #'τ_e #'τ_match) 129 (typecheck-fail-msg/1 #'τ_match #'τ_e #'e) 130 (⊢ (list- 'l e) : τ.norm)]) 131 (define-typed-syntax case 132 #:datum-literals (of =>) 133 [(_ e [l:id x:id => e_l] ...) 134 #:fail-when (null? (syntax->list #'(l ...))) "no clauses" 135 #:with [e- (~∨* [l_x : τ_x] ...)] (infer+erase #'e) 136 #:fail-unless (= (stx-length #'(l ...)) 137 (stx-length #'(l_x ...))) 138 "wrong number of case clauses" 139 #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) 140 "case clauses not exhaustive" 141 #:with (((x-) e_l- τ_el) ...) 142 (stx-map 143 (λ (bs e) (infer/ctx+erase bs e)) 144 #'(([x : τ_x]) ...) #'(e_l ...)) 145 (⊢ (let- ([l_e (car- e-)]) 146 (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...)) 147 : (⊔ τ_el ...))])