lin+cons.rkt (2051B)
1 #lang turnstile/lang 2 (extends "lin+tup.rkt") 3 4 (provide (type-out MList MList0) 5 cons nil match-list) 6 7 (define-type-constructor MList #:arity = 1) 8 (define-base-type MList0) 9 10 (begin-for-syntax 11 (current-linear-type? (or/c MList? MList0? (current-linear-type?)))) 12 13 14 (define-typed-syntax cons 15 #:datum-literals (@) 16 17 ; implicit memory location created 18 [(_ e e_rest) ≫ 19 [⊢ e ≫ e- ⇒ σ] 20 [⊢ e_rest ≫ e_rest- ⇐ (MList σ)] 21 -------- 22 [⊢ (#%app- mcons- e- e_rest-) ⇒ (MList σ)]] 23 24 ; with memory location given 25 [(_ e e_rest @ e_loc) ≫ 26 [⊢ e ≫ e- ⇒ σ] 27 [⊢ e_rest ≫ e_rest- ⇐ (MList σ)] 28 [⊢ e_loc ≫ e_loc- ⇐ MList0] 29 #:with tmp (generate-temporary #'e_loc) 30 -------- 31 [⊢ (let- ([tmp e_loc-]) 32 (set-mcar!- tmp e-) 33 (set-mcdr!- tmp e_rest-) 34 tmp) 35 ⇒ (MList σ)]]) 36 37 38 (define-typed-syntax nil 39 [(_ {ty:type}) ≫ 40 -------- 41 [⊢ '() ⇒ (MList ty.norm)]] 42 [(_) ⇐ (~MList σ) ≫ 43 -------- 44 [⊢ '()]]) 45 46 47 (define-typed-syntax match-list 48 #:datum-literals (cons nil @) 49 [(_ e_list 50 (~or [(cons x+:id xs+:id @ l+:id) e_cons+] 51 [(nil) e_nil+]) ...) ≫ 52 #:with [(l x xs e_cons)] #'[(l+ x+ xs+ e_cons+) ...] 53 #:with [e_nil] #'[e_nil+ ...] 54 55 ; list 56 [⊢ e_list ≫ e_list- ⇒ (~MList σ)] 57 #:with σ_xs ((current-type-eval) #'(MList σ)) 58 #:with σ_l ((current-type-eval) #'MList0) 59 60 #:mode (make-linear-branch-mode 2) 61 (; cons branch 62 #:submode (branch-nth 0) 63 ([[x ≫ x- : σ] 64 [xs ≫ xs- : σ_xs] 65 [l ≫ l- : σ_l] 66 ⊢ e_cons ≫ e_cons- ⇒ σ_out] 67 #:do [(linear-out-of-scope! #'([x- : σ] [xs- : σ_xs] [l- : σ_l]))]) 68 69 ; nil branch 70 #:submode (branch-nth 1) 71 ([⊢ [e_nil ≫ e_nil- ⇐ σ_out]])) 72 73 -------- 74 [⊢ (let- ([l- e_list-]) 75 (if- (null? l-) 76 e_nil- 77 (let- ([x- (mcar- l-)] 78 [xs- (mcdr- l-)]) 79 e_cons-))) 80 ⇒ σ_out]])