From 8369574812857b24bfcde4ad5df279ab227380f9 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Mon, 14 Mar 2016 01:29:46 -0400 Subject: [PATCH] fix stlc+effect; add check-props testing form --- tapl/stlc+effect.rkt | 81 +++++++++++++++++++++++++--- tapl/tests/rackunit-typechecking.rkt | 14 +++++ tapl/tests/stlc+effect-tests.rkt | 5 ++ 3 files changed, 93 insertions(+), 7 deletions(-) diff --git a/tapl/stlc+effect.rkt b/tapl/stlc+effect.rkt index 80072ba..5b2eda1 100644 --- a/tapl/stlc+effect.rkt +++ b/tapl/stlc+effect.rkt @@ -1,6 +1,8 @@ #lang s-exp "typecheck.rkt" (extends "stlc+box.rkt" #:except ref deref := #%app λ) +(provide (for-syntax get-new-effects)) + ;; Simply-Typed Lambda Calculus, plus mutable references ;; Types: ;; - types from stlc+cons.rkt @@ -21,11 +23,14 @@ deref-locs)) (define (get-effects e tag [vs '()]) - (syntax-property (local-expand (if (null? vs) e #`(stlc+box:λ #,vs #,e)) 'expression null) tag)) + (or (syntax-property + (local-expand (if (null? vs) e #`(stlc+box:λ #,vs #,e)) 'expression null) + tag) + null)) (define (get-new-effects e [vs '()]) (get-effects e 'new vs)) (define (get-assign-effects e [vs '()]) (get-effects e 'assign vs)) (define (get-deref-effects e [vs '()]) (get-effects e 'deref vs)) - + (define (print-effects e) (printf "expr ~a\n" (syntax->datum e)) (define e+ (local-expand e 'expression null)) @@ -42,15 +47,39 @@ (define-typed-syntax #%app [(_ efn e ...) - #:with [efn- τfn] (infer+erase #'efn) - (let ([φ-news (stx-map get-new-effects #'(τfn efn e ...))] + #:with [e_fn- ty_fn fns fas fds] (infer+erase/eff #'efn) + #:with tyns (get-new-effects #'ty_fn) + #:with tyas (get-assign-effects #'ty_fn) + #:with tyds (get-deref-effects #'ty_fn) + #:with (~→ τ_in ... τ_out) #'ty_fn + #:with ([e_arg- τ_arg ns as ds] ...) (infers+erase/eff #'(e ...)) +; #:with [e_fn- (τ_in ... τ_out)] (⇑ e_fn as →) + #:fail-unless (stx-length=? #'(τ_arg ...) #'(τ_in ...)) + (mk-app-err-msg stx #:expected #'(τ_in ...) + #:given #'(τ_arg ...) + #:note "Wrong number of arguments.") + #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...)) + (mk-app-err-msg stx #:expected #'(τ_in ...) + #:given #'(τ_arg ...)) + (assign-type/eff #'(#%app e_fn- e_arg- ...) #'τ_out + (stx-flatten #'(fns tyns . (ns ...))) + (stx-flatten #'(fas tyas . (as ...))) + (stx-flatten #'(fds tyds . (ds ...)))) + #;(let ([φ-news (stx-map get-new-effects #'(τfn efn e ...))] [φ-assigns (stx-map get-assign-effects #'(τfn efn e ...))] [φ-derefs (stx-map get-deref-effects #'(τfn efn e ...))]) (add-effects #'(stlc+box:#%app efn e ...) (foldl loc-union (set) φ-news) (foldl loc-union (set) φ-assigns) (foldl loc-union (set) φ-derefs)))]) + (define-typed-syntax λ + [(_ bvs:type-ctx e) + #:with [xs- e- τ_res ns as ds] (infer/ctx+erase/eff #'bvs #'e) + (assign-type #'(λ xs- e-) + (add-effects #'(→ bvs.type ... τ_res) #'ns #'as #'ds))]) + +#;(define-typed-syntax λ [(_ bvs:type-ctx e) #:with (xs- e- τ_res) (infer/ctx+erase #'bvs #'e) (let ([φ-news (get-new-effects #'e-)] @@ -60,12 +89,50 @@ #'(λ xs- e-) (add-effects #'(→ bvs.type ... τ_res) φ-news φ-assigns φ-derefs)))]) +(define-type-constructor Ref) + +(begin-for-syntax + (define (infer+erase/eff e) + (define/with-syntax [e- ty] (infer+erase e)) + (list + #'e- #'ty + (get-new-effects #'e-) (get-assign-effects #'e-) (get-deref-effects #'e-))) + (define (infers+erase/eff es) + (stx-map infer+erase/eff es)) + (define (infer/ctx+erase/eff bvs e) + (define/with-syntax [xs- e- ty] (infer/ctx+erase bvs e)) + (list #'xs- #'e- #'ty + (get-new-effects #'e-) (get-assign-effects #'e-) (get-deref-effects #'e-))) + (define (assign-type/eff e ty news assigns derefs) + (assign-type (add-effects e news assigns derefs) ty))) + (define-typed-syntax ref [(_ e) - (syntax-property #'(stlc+box:ref e) 'new (set (syntax-position stx)))]) + #:with (e- τ ns as ds) (infer+erase/eff #'e) + (assign-type/eff #'(box e-) #'(Ref τ) + (cons (syntax-position stx) #'ns) #'as #'ds)]) (define-typed-syntax deref [(_ e) - (syntax-property #'(stlc+box:deref e) 'deref (set (syntax-position stx)))]) + #:with (e- (~Ref ty) ns as ds) (infer+erase/eff #'e) + (assign-type/eff #'(unbox e-) #'ty + #'ns #'as (cons (syntax-position stx) #'ds))]) (define-typed-syntax := [(_ e_ref e) - (syntax-property #'(stlc+box::= e_ref e) 'assign (set (syntax-position stx)))]) \ No newline at end of file + ;#:with (e_ref- (τ1)) (⇑ e_ref as Ref) + #:with [e_ref- (~Ref ty1) ns1 as1 ds1] (infer+erase/eff #'e_ref) + #:with [e- ty2 ns2 as2 ds2] (infer+erase/eff #'e) + #:when (typecheck? #'ty1 #'ty2) + (assign-type/eff #'(set-box! e_ref- e-) #'Unit + (stx-append #'ns1 #'ns2) + (cons (syntax-position stx) (stx-append #'as1 #'as2)) + (stx-append #'ds1 #'ds2))]) +;(define-typed-syntax ref +; [(_ e) +; (syntax-property #'(stlc+box:ref e) 'new (set (syntax-position stx)))]) +;(define-typed-syntax deref +; [(_ e) +; (syntax-property #'(stlc+box:deref e) 'deref (set (syntax-position stx)))]) +;(define-typed-syntax := +; [(_ e_ref e) +; (syntax-property #'(stlc+box::= e_ref e) 'assign (set (syntax-position stx)))]) + diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt index a0b1261..e189d24 100644 --- a/tapl/tests/rackunit-typechecking.rkt +++ b/tapl/tests/rackunit-typechecking.rkt @@ -31,6 +31,20 @@ (type->str #'τ) (type->str #'τ-expected)) #'(void)])) +;; for checking properties other than types +(define-syntax (check-props stx) + (syntax-parse stx #:datum-literals (: ⇒ ->) + [(_ prop e : v ... (~optional (~seq (~or ⇒ ->) v2) #:defaults ([v2 #'e]))) + #:with props (or (syntax-property (expand/df #'e) (syntax->datum #'prop)) + #'()) + #:fail-unless (set=? (apply set (syntax->datum #'(v ...))) + (apply set (syntax->datum #'props))) + (format + "Expression ~a [loc ~a:~a:~a] does not have prop ~a, actual: ~a" + (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e) (syntax-position #'e) + (syntax->datum #'(v ...)) (syntax->datum #'props)) + (syntax/loc stx (check-equal? e v2))])) + (define-syntax (check-not-type stx) (syntax-parse stx #:datum-literals (:) [(_ e : not-τ) diff --git a/tapl/tests/stlc+effect-tests.rkt b/tapl/tests/stlc+effect-tests.rkt index ae8bb84..6b7821f 100644 --- a/tapl/tests/stlc+effect-tests.rkt +++ b/tapl/tests/stlc+effect-tests.rkt @@ -1,6 +1,11 @@ #lang s-exp "../stlc+effect.rkt" (require "rackunit-typechecking.rkt") +(check-props new (ref 11) : 90) +(check-props deref (deref (ref 11)) : 124) +(check-props new (deref (ref 11)) : 172) +(check-props new ((λ ([x : Int]) (ref x)) 21) : 222) + (define x (ref 10)) (check-type x : (Ref Int)) (check-type (deref x) : Int ⇒ 10)