www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

stlc+box.rkt (796B)

      1 #lang s-exp macrotypes/typecheck
      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
     17   [(_ e)
     18    #:with [e- τ] (infer+erase #'e)
     19    (⊢ (box- e-) : (Ref τ))])
     20 (define-typed-syntax deref
     21   [(_ e)
     22    #:with [e- (~Ref τ)] (infer+erase #'e)
     23    (⊢/no-teval (unbox- e-) : τ)])
     24 (define-typed-syntax := #:literals (:=)
     25   [(_ e_ref e)
     26    #:with [e_ref- (~Ref τ1)] (infer+erase #'e_ref)
     27    #:with [e- τ2] (infer+erase #'e)
     28    #:fail-unless (typecheck? #'τ1 #'τ2)
     29                  (typecheck-fail-msg/1 #'τ1 #'τ2 #'e)
     30    (⊢ (set-box!- e_ref- e-) : Unit)])