stlc+reco+var.rkt (5070B)
1 #lang turnstile/lang 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 [l:id (~datum =) e] ...) ≫ 59 [⊢ e ≫ e- ⇒ τ] ... 60 -------- 61 [⊢ (list- (list- 'l e-) ...) ⇒ (× [l : τ] ...)]) 62 (define-typed-syntax (proj e_rec l:id) ≫ 63 [⊢ e_rec ≫ e_rec- ⇒ τ_e] 64 #:fail-unless (×? #'τ_e) 65 (format "Expected expression ~s to have × type, got: ~a" 66 (syntax->datum #'e_rec) (type->str #'τ_e)) 67 #:with τ_l (×-ref #'τ_e #'l) 68 -------- 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 -------- 117 [≻ (ann (var l = e) : τ.norm)]] 118 [(_ l:id = e) ⇐ τ ≫ 119 #:fail-unless (∨? #'τ) 120 (format "Expected the expected type to be a ∨ type, got: ~a" (type->str #'τ)) 121 #:with τ_e 122 (∨-ref #'τ #'l #:else 123 (λ () (raise-syntax-error #f 124 (format "~a field does not exist" (syntax->datum #'l)) 125 this-syntax))) 126 [⊢ e ≫ e- ⇐ τ_e] 127 -------- 128 [⊢ (list- 'l e)]]) 129 130 (define-typed-syntax (case e [l:id x:id (~datum =>) e_l] ...) ≫ 131 #:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses" 132 [⊢ e ≫ e- ⇒ (~∨* [l_x : τ_x] ...)] 133 #:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses" 134 #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive" 135 [[x ≫ x- : τ_x] ⊢ e_l ≫ e_l- ⇒ τ_el] ... 136 -------- 137 [⊢ (let- ([l_e (car- e-)]) 138 (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...)) 139 ⇒ (⊔ τ_el ...)])