lin+var.rkt (3642B)
1 #lang turnstile/lang 2 (extends "lin.rkt") 3 (require (only-in "lin+tup.rkt" list-destructure-syntax)) 4 5 (provide ⊕ var match) 6 7 (define-internal-type-constructor ⊕/i) 8 9 (define-syntax ⊕ 10 (syntax-parser 11 [(_ (V:id t ...) ...) 12 (add-orig (mk-type #'(⊕/i- (#%app 'V t ...) ...)) 13 this-syntax)])) 14 15 (begin-for-syntax 16 (provide ⊕? ~⊕) 17 (define ⊕? ⊕/i?) 18 19 (define (fail/no-variant type V [src V]) 20 (raise-syntax-error #f 21 (format "expected type ~a does not have variant named '~a'\n" 22 (type->str type) 23 (stx->datum V)) 24 src)) 25 26 (define (num-var-args-fail-msg σs xs) 27 (format "wrong number of arguments to variant: expected ~a, got ~a" 28 (stx-length σs) 29 (stx-length xs))) 30 31 32 (define (unvariant type) 33 (syntax-parse type 34 [(~⊕/i ((~literal #%plain-app) ((~literal quote) U) τ ...) ...) 35 #'[(U τ ...) ...]])) 36 37 (define-syntax ~⊕ 38 (pattern-expander 39 (λ (stx) 40 (syntax-case stx () 41 [(_ . pat) 42 (with-syntax ([(x) (generate-temporaries #'(x))]) 43 #'(~and x (~⊕/i . _) (~parse pat (unvariant #'x))))])))) 44 45 (define (has-variant? type v) 46 (syntax-parse type 47 [(~⊕ [U . _] ...) 48 (for/or ([u (in-syntax #'[U ...])]) 49 (eq? (stx->datum u) (stx->datum v)))] 50 [_ #f])) 51 52 (define (get-variant type v) 53 (syntax-parse type 54 [(~⊕ [U τ ...] ...) 55 (for/first ([u (in-syntax #'[U ...])] 56 [ts (in-syntax #'[(τ ...) ...])] 57 #:when (eq? (stx->datum u) (stx->datum v))) 58 ts)])) 59 60 (current-linear-type? (or/c ⊕? (current-linear-type?))) 61 ) 62 63 64 (define-typed-syntax var 65 [(_ [V:id e ...]) ⇐ σ_var ≫ 66 #:when (⊕? #'σ_var) 67 #:fail-unless (has-variant? #'σ_var #'V) 68 (fail/no-variant #'σ_var #'V this-syntax) 69 #:with [σ ...] (get-variant #'σ_var #'V) 70 #:fail-unless (stx-length=? #'[σ ...] #'[e ...]) 71 (num-var-args-fail-msg #'[σ ...] #'[e ...]) 72 [⊢ e ≫ e- ⇐ σ] ... 73 -------- 74 [⊢ (list 'V e- ...)]] 75 76 [(_ [V:id e ...] (~datum as) t) ≫ 77 -------- 78 [≻ (lin:ann (var [V e ...]) : t)]]) 79 80 81 82 (define-typed-syntax match 83 [(_ e_var [(V:id x:id ...) e_bra] ...) ≫ 84 [⊢ e_var ≫ e_var- ⇒ σ_var] 85 #:fail-unless (⊕? #'σ_var) 86 (format "expected type ⊕, given ~a" (type->str #'σ_var)) 87 88 #:mode (make-linear-branch-mode (stx-length #'[e_bra ...])) 89 (#:with ([(x- ...) e_bra- σ_bra] ...) 90 (for/list ([q (in-syntax #'([V (x ...) e_bra] ...))] 91 [i (in-naturals)]) 92 (syntax-parse/typecheck q 93 [(V (x ...) e) ≫ 94 #:fail-unless (has-variant? #'σ_var #'V) 95 (fail/no-variant #'σ_var #'V) 96 97 #:with [σ ...] (get-variant #'σ_var #'V) 98 #:fail-unless (stx-length=? #'[σ ...] #'[x ...]) 99 (num-var-args-fail-msg #'[σ ...] #'[x ...]) 100 101 #:submode (branch-nth i) 102 ([[x ≫ x- : σ] ... ⊢ e ≫ e- ⇒ σ_bra] 103 #:do [(linear-out-of-scope! #'([x- : σ] ...))]) 104 -------- 105 [≻ [(x- ...) e- σ_bra]]]))) 106 107 #:with tmp (generate-temporary) 108 #:with (destr ...) (stx-map (λ (l) (apply list-destructure-syntax (stx->list l))) 109 #'[([x- ...] 110 (cdr tmp) 111 e_bra-) ...]) 112 -------- 113 [⊢ (let ([tmp e_var-]) 114 (case (car tmp) 115 [(V) destr] ... 116 [else (printf "~a\n" tmp) 117 (error '"unhandled case: " (car tmp))])) 118 ⇒ (⊔ σ_bra ...)]])