stlc+box.rkt (644B)
1 #lang turnstile/lang 2 (extends "stlc+cons.rkt") 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 ref deref :=) 13 14 (define-type-constructor Ref) 15 16 (define-typed-syntax (ref e) ≫ 17 [⊢ e ≫ e- ⇒ τ] 18 -------- 19 [⊢ (box- e-) ⇒ (Ref τ)]) 20 21 (define-typed-syntax (deref e) ≫ 22 [⊢ e ≫ e- ⇒ (~Ref τ)] 23 -------- 24 [⊢ (unbox- e-) ⇒ τ]) 25 26 (define-typed-syntax (:= e_ref e) ≫ 27 [⊢ e_ref ≫ e_ref- ⇒ (~Ref τ)] 28 [⊢ e ≫ e- ⇐ τ] 29 -------- 30 [⊢ (set-box!- e_ref- e-) ⇒ Unit]) 31