commit 8369574812857b24bfcde4ad5df279ab227380f9
parent 6a85e067190c9c08158fb8c734377d4d3be7a9a7
Author: Stephen Chang <stchang216@gmail.com>
Date: Mon, 14 Mar 2016 01:29:46 -0400
fix stlc+effect; add check-props testing form
Diffstat:
3 files changed, 93 insertions(+), 8 deletions(-)
diff --git 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,16 +47,40 @@
(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-)]
[φ-assigns (get-assign-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
@@ -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
@@ -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)
