stlc+effect.rkt (3294B)
1 #lang turnstile/lang 2 (extends "stlc+box.rkt" #:except Ref ref deref := #%app λ) 3 4 ;; Simply-Typed Lambda Calculus, plus mutable references 5 ;; Types: 6 ;; - types from stlc+cons.rkt 7 ;; - Ref constructor 8 ;; Terms: 9 ;; - terms from stlc+cons.rkt 10 ;; - ref deref := 11 12 (provide Ref #%app λ ref deref :=) 13 14 (define-syntax-rule (locs loc ...) 15 '(loc ...)) 16 (begin-for-syntax 17 (define-syntax ~locs 18 (pattern-expander 19 (syntax-parser 20 [(locs loc:id ...) 21 #:with tmp (generate-temporary 'locs) 22 #'(~and tmp 23 (~parse ((~literal quote) (loc ...)) 24 (stx-or #'tmp #'(quote ()))))]))) 25 26 (define (stx-truth? a) 27 (and a (not (and (syntax? a) (false? (syntax-e a)))))) 28 (define (stx-or a b) 29 (cond [(stx-truth? a) a] 30 [else b]))) 31 32 33 (define-typed-syntax #%app 34 [(_ efn e ...) ≫ 35 [⊢ efn ≫ e_fn- 36 (⇒ : (~→ τ_in ... τ_out) 37 (⇒ ν (~locs tyns ...)) 38 (⇒ := (~locs tyas ...)) 39 (⇒ ! (~locs tyds ...))) 40 (⇒ ν (~locs fns ...)) 41 (⇒ := (~locs fas ...)) 42 (⇒ ! (~locs fds ...))] 43 #:fail-unless (stx-length=? #'[e ...] #'[τ_in ...]) 44 (num-args-fail-msg #'efn #'[τ_in ...] #'[e ...]) 45 [⊢ e ≫ e_arg- 46 (⇐ : τ_in) 47 (⇒ ν (~locs ns ...)) 48 (⇒ := (~locs as ...)) 49 (⇒ ! (~locs ds ...))] ... 50 -------- 51 [⊢ (#%app- e_fn- e_arg- ...) 52 (⇒ : τ_out) 53 (⇒ ν (locs fns ... tyns ... ns ... ...)) 54 (⇒ := (locs fas ... tyas ... as ... ...)) 55 (⇒ ! (locs fds ... tyds ... ds ... ...))]]) 56 57 (define-typed-syntax (λ bvs:type-ctx e) ≫ 58 [[bvs.x ≫ x- : bvs.type] ... 59 ⊢ e ≫ e- 60 (⇒ : τ_res) 61 (⇒ ν (~locs ns ...)) 62 (⇒ := (~locs as ...)) 63 (⇒ ! (~locs ds ...))] 64 -------- 65 [⊢ (λ- (x- ...) e-) 66 (⇒ : (→ bvs.type ... τ_res) 67 (⇒ ν (locs ns ...)) 68 (⇒ := (locs as ...)) 69 (⇒ ! (locs ds ...)))]) 70 71 (define-type-constructor Ref) 72 73 (define-typed-syntax ref 74 [(_ e) ≫ 75 [⊢ e ≫ e- 76 (⇒ : τ) 77 (⇒ ν (~locs ns ...)) 78 (⇒ := (~locs as ...)) 79 (⇒ ! (~locs ds ...))] 80 -------- 81 [⊢ (#%app- box- e-) 82 (⇒ : (Ref τ)) 83 (⇒ ν (locs #,(syntax-position this-syntax) ns ...)) 84 (⇒ := (locs as ...)) 85 (⇒ ! (locs ds ...))]]) 86 (define-typed-syntax deref 87 [(_ e) ≫ 88 [⊢ e ≫ e- 89 (⇒ : (~Ref ty)) 90 (⇒ ν (~locs ns ...)) 91 (⇒ := (~locs as ...)) 92 (⇒ ! (~locs ds ...))] 93 -------- 94 [⊢ (#%app- unbox- e-) 95 (⇒ : ty) 96 (⇒ ν (locs ns ...)) 97 (⇒ := (locs as ...)) 98 (⇒ ! (locs #,(syntax-position this-syntax) ds ...))]]) 99 (define-typed-syntax := #:literals (:=) 100 [(_ e_ref e) ≫ 101 [⊢ e_ref ≫ e_ref- 102 (⇒ : (~Ref ty)) 103 (⇒ ν (~locs ns1 ...)) 104 (⇒ := (~locs as1 ...)) 105 (⇒ ! (~locs ds1 ...))] 106 [⊢ e ≫ e- 107 (⇐ : ty) 108 (⇒ ν (~locs ns2 ...)) 109 (⇒ := (~locs as2 ...)) 110 (⇒ ! (~locs ds2 ...))] 111 -------- 112 [⊢ (#%app- set-box!- e_ref- e-) 113 (⇒ : Unit) 114 (⇒ ν (locs ns1 ... ns2 ...)) 115 (⇒ := (locs #,(syntax-position this-syntax) as1 ... as2 ...)) 116 (⇒ ! (locs ds1 ... ds2 ...))]]) 117