lin+tup.rkt (3277B)
1 #lang turnstile/lang 2 (extends "lin.rkt") 3 4 (provide (type-out ⊗) tup let*) 5 (begin-for-syntax (provide in-cad*rs 6 list-destructure-syntax)) 7 8 (define-type-constructor ⊗ #:arity >= 2) 9 10 (begin-for-syntax 11 (define (num-tuple-fail-msg σs xs) 12 (format "wrong number of tuple elements: expected ~a, got ~a" 13 (stx-length xs) 14 (stx-length σs))) 15 16 (current-linear-type? (or/c ⊗? (current-linear-type?)))) 17 18 19 (define-typed-syntax tup 20 [(_ e1 e2 ...+) ≫ 21 [⊢ e1 ≫ e1- ⇒ σ1] 22 [⊢ e2 ≫ e2- ⇒ σ2] ... 23 -------- 24 [⊢ (list- e1- e2- ...) ⇒ (⊗ σ1 σ2 ...)]]) 25 26 27 (define-typed-syntax let* 28 ; normal let* recursive bindings 29 [(_ ([x:id e_rhs] . xs) . body) ≫ 30 [⊢ e_rhs ≫ e_rhs- ⇒ σ] 31 [[x ≫ x- : σ] ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out] 32 #:do [(linear-out-of-scope! #'([x- : σ]))] 33 -------- 34 [⊢ (let- ([x- e_rhs-]) e_body-) ⇒ σ_out]] 35 36 ; tuple unpacking with (let* ([(x ...) tup]) ...) 37 [(_ ([(x:id ...) e_rhs] . xs) . body) ≫ 38 [⊢ e_rhs ≫ e_rhs- ⇒ (~⊗ σ ...)] 39 #:fail-unless (stx-length=? #'[σ ...] #'[x ...]) 40 (num-tuple-fail-msg #'[σ ...] #'[x ...]) 41 42 [[x ≫ x- : σ] ... ⊢ (let* xs . body) ≫ e_body- ⇒ σ_out] 43 #:do [(linear-out-of-scope! #'([x- : σ] ...))] 44 45 #:with tmp (generate-temporary #'e_tup) 46 #:with destr (list-destructure-syntax #'[x- ...] #'tmp #:unsafe? #t 47 #'e_body-) 48 -------- 49 [⊢ (let- ([tmp e_rhs-]) destr) ⇒ σ_out]] 50 51 [(_ () e) ≫ 52 -------- 53 [≻ e]] 54 55 [(_ () e ...+) ≫ 56 -------- 57 [≻ (lin:begin e ...)]]) 58 59 60 61 (require racket/unsafe/ops) 62 63 ;; generate infinite sequence of cad*r syntax, e.g. 64 ;; (car e) (cadr e) (caddr e) ... 65 (define-for-syntax (in-cad*rs e #:unsafe? [unsafe? #f]) 66 (make-do-sequence 67 (λ () 68 (values (λ (s) 69 (if unsafe? 70 (quasisyntax/loc e (unsafe-car #,s)) 71 (quasisyntax/loc e (car #,s)))) 72 (λ (s) 73 (if unsafe? 74 (quasisyntax/loc e (unsafe-cdr #,s)) 75 (quasisyntax/loc e (cdr #,s)))) 76 e 77 #f #f #f)))) 78 79 80 ;; (list-destructure-syntax #'(x y z ...) #'rhs #'body) 81 ;; = 82 ;; (let ([x (car rhs)] 83 ;; [y (cadr rhs)] 84 ;; [z (caddr rhs)] 85 ;; ...) 86 ;; body) 87 (define-for-syntax (list-destructure-syntax xs rhs body #:unsafe? [unsafe? #f]) 88 (with-syntax ([binds (for/list ([c (in-cad*rs rhs #:unsafe? unsafe?)] 89 [x (in-syntax xs)]) 90 (list x c))] 91 [body body]) 92 (syntax/loc rhs 93 (let- binds body)))) 94 95 96 97 (module+ test 98 (begin-for-syntax 99 (require rackunit) 100 (check-equal? (for/list ([c (in-cad*rs #'x)] 101 [i (in-range 4)]) 102 (syntax->datum c)) 103 '[(car x) 104 (car (cdr x)) 105 (car (cdr (cdr x))) 106 (car (cdr (cdr (cdr x))))]) 107 108 (check-equal? (syntax->datum 109 (list-destructure-syntax #'[x y] #'lst #'z #:unsafe? #t)) 110 '(let- ([x (unsafe-car lst)] 111 [y (unsafe-car (unsafe-cdr lst))]) 112 z))))