stlc+effect.rkt (4178B)
1 #lang s-exp macrotypes/typecheck 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 (for-syntax get-new-effects) 13 Ref 14 #%app λ ref deref :=) 15 16 (begin-for-syntax 17 (define (add-news e locs) (syntax-property e 'ν locs)) 18 (define (add-assigns e locs) (syntax-property e ':= locs)) 19 (define (add-derefs e locs) (syntax-property e '! locs)) 20 (define (add-effects e new-locs assign-locs deref-locs) 21 (add-derefs 22 (add-assigns 23 (add-news e new-locs) 24 assign-locs) 25 deref-locs)) 26 27 (define (get-effects e tag [vs '()]) 28 (or (syntax-property 29 (local-expand 30 (if (null? vs) e #`(stlc+box:λ #,vs #,e)) 'expression null) 31 tag) 32 null)) 33 (define (get-new-effects e [vs '()]) (get-effects e 'ν vs)) 34 (define (get-assign-effects e [vs '()]) (get-effects e ':= vs)) 35 (define (get-deref-effects e [vs '()]) (get-effects e '! vs)) 36 37 (define (print-effects e) 38 (printf "expr ~a\n" (syntax->datum e)) 39 (define e+ (local-expand e 'expression null)) 40 (printf "new locs: ~a\n" (syntax-property e+ 'ν)) 41 (printf "deref locs: ~a\n" (syntax-property e+ '!)) 42 (printf "assign locs: ~a\n" (syntax-property e+ ':=))) 43 44 (define (loc-union locs1 locs2) 45 (cond 46 [(not locs1) locs2] 47 [(not locs2) locs1] 48 [else (set-union locs1 locs2)]))) 49 50 51 (define-typed-syntax #%app 52 [(_ efn e ...) 53 #:with [e_fn- ty_fn fns fas fds] (infer+erase/eff #'efn) 54 #:with tyns (get-new-effects #'ty_fn) 55 #:with tyas (get-assign-effects #'ty_fn) 56 #:with tyds (get-deref-effects #'ty_fn) 57 #:with (~→ τ_in ... τ_out) #'ty_fn 58 #:with ([e_arg- τ_arg ns as ds] ...) (infers+erase/eff #'(e ...)) 59 #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...)) 60 (num-args-fail-msg #'efn #'(τ_in ...) #'(e ...)) 61 #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) 62 (typecheck-fail-msg/multi 63 #'(τ_in ...) #'(τ_arg ...) #'(e ...)) 64 (assign-type/eff #'(#%app- e_fn- e_arg- ...) #'τ_out 65 (stx-flatten #'(fns tyns . (ns ...))) 66 (stx-flatten #'(fas tyas . (as ...))) 67 (stx-flatten #'(fds tyds . (ds ...))))]) 68 69 (define-typed-syntax λ 70 [(_ bvs:type-ctx e) 71 #:with [xs- e- τ_res ns as ds] (infer/ctx+erase/eff #'bvs #'e) 72 (assign-type #'(λ- xs- e-) 73 (add-effects #'(→ bvs.type ... τ_res) #'ns #'as #'ds))]) 74 75 (define-type-constructor Ref) 76 77 (begin-for-syntax 78 (define (infer+erase/eff e) 79 (define/with-syntax [e- ty] (infer+erase e)) 80 (list 81 #'e- #'ty 82 (get-new-effects #'e-) 83 (get-assign-effects #'e-) 84 (get-deref-effects #'e-))) 85 (define (infers+erase/eff es) 86 (stx-map infer+erase/eff es)) 87 (define (infer/ctx+erase/eff bvs e) 88 (define/with-syntax [xs- e- ty] (infer/ctx+erase bvs e)) 89 (list #'xs- #'e- #'ty 90 (get-new-effects #'e-) 91 (get-assign-effects #'e-) 92 (get-deref-effects #'e-))) 93 (define (assign-type/eff e ty news assigns derefs) 94 (assign-type (add-effects e news assigns derefs) ty))) 95 96 (define-typed-syntax ref 97 [(_ e) 98 #:with [e- τ ns as ds] (infer+erase/eff #'e) 99 (assign-type/eff #'(#%app- box- e-) #'(Ref τ) 100 (cons (syntax-position stx) #'ns) #'as #'ds)]) 101 (define-typed-syntax deref 102 [(_ e) 103 #:with [e- (~Ref ty) ns as ds] (infer+erase/eff #'e) 104 (assign-type/eff #'(#%app- unbox- e-) #'ty 105 #'ns #'as (cons (syntax-position stx) #'ds))]) 106 (define-typed-syntax := #:literals (:=) 107 [(_ e_ref e) 108 #:with [e_ref- (~Ref ty1) ns1 as1 ds1] (infer+erase/eff #'e_ref) 109 #:with [e- ty2 ns2 as2 ds2] (infer+erase/eff #'e) 110 #:fail-unless (typecheck? #'ty1 #'ty2) 111 (typecheck-fail-msg/1 #'ty1 #'ty2 #'e) 112 (assign-type/eff #'(#%app- set-box!- e_ref- e-) #'Unit 113 (stx-append #'ns1 #'ns2) 114 (cons (syntax-position stx) (stx-append #'as1 #'as2)) 115 (stx-append #'ds1 #'ds2))])