From 62c86d5ddd246d7f6da77f6f52a2560d725bde24 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Thu, 22 Jan 2015 11:22:27 -0500 Subject: [PATCH] Added occurrence typing for private fields. This also tracks mutation of private fields to ensure that only non-mutated field types are allowed to be refined. --- .../typed-racket/rep/object-rep.rkt | 1 + .../typecheck/check-class-unit.rkt | 67 +++++++++++++++--- .../typed-racket/typecheck/tc-envops.rkt | 13 ++++ .../typed-racket/types/path-type.rkt | 5 ++ .../typed-racket/utils/mutated-vars.rkt | 16 ++++- typed-racket-test/unit-tests/class-tests.rkt | 70 ++++++++++++++++++- 6 files changed, 158 insertions(+), 14 deletions(-) diff --git a/typed-racket-lib/typed-racket/rep/object-rep.rkt b/typed-racket-lib/typed-racket/rep/object-rep.rkt index 42ac53e3..6ffb5e5d 100644 --- a/typed-racket-lib/typed-racket/rep/object-rep.rkt +++ b/typed-racket-lib/typed-racket/rep/object-rep.rkt @@ -16,6 +16,7 @@ (def-pathelem StructPE ([t Type?] [idx natural-number/c]) [#:frees (λ (f) (f t))] [#:fold-rhs (*StructPE (type-rec-id t) idx)]) +(def-pathelem FieldPE () [#:fold-rhs #:base]) (def-object Empty () [#:fold-rhs #:base]) diff --git a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt index 595f9ee9..235d9a47 100644 --- a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt @@ -12,11 +12,11 @@ syntax/stx "signatures.rkt" (private parse-type syntax-properties) - (env lexical-env tvar-env global-env type-alias-helper) + (env lexical-env tvar-env global-env type-alias-helper mvar-env) (types utils abbrev union subtype resolve generalize) (typecheck check-below internal-forms) - (utils tc-utils) - (rep type-rep) + (utils tc-utils mutated-vars) + (rep object-rep type-rep) (for-syntax racket/base) (for-template racket/base (private class-literals) @@ -261,6 +261,21 @@ ([(meth-name) meth1.form] ...) meth2.form))) +;; For detecting field mutations for occurrence typing +(define-syntax-class (field-assignment local-table) + #:literal-sets (kernel-literals) + #:attributes (sub name) + (pattern (begin (quote ((~datum declare-field-assignment) field-name:id)) + sub) + ;; Mutation tracking needs to look at the *accessor* name + ;; since the predicate check happens on a read. But the accessor + ;; is not in the mutation expression, so we need to look up the + ;; corresponding identifier. + #:attr maybe-accessor + (dict-ref local-table (syntax-e #'field-name) #f) + #:when (attribute maybe-accessor) + #:with name (car (attribute maybe-accessor)))) + ;; Syntax Option -> TCResults ;; Type-check a class form by trawling its innards ;; @@ -523,6 +538,20 @@ local-private-field-table private-field-types) + ;; Detect mutation of private fields for occurrence typing + (for ([stx (in-sequences + (in-list (stx->list (hash-ref parse-info 'initializer-body))) + (in-list method-stxs))] + ;; Avoid counting the local table, which has dummy mutations that the + ;; typed class macro inserted only for analysis. + #:when (not (tr:class:local-table-property stx))) + (find-mutated-vars stx + mvar-env + (syntax-parser + [(~var f (field-assignment local-private-field-table)) + (list #'f.sub #'f.name)] + [_ #f]))) + ;; start type-checking elements in the body (define-values (lexical-names lexical-types lexical-names/top-level lexical-types/top-level) @@ -801,12 +830,9 @@ augments #:inner? #t)) ;; construct field accessor types - (define (make-field-types field-names type-map #:private? [private? #f]) + (define (make-field-types field-names type-map) (for/lists (_1 _2) ([f (in-set field-names)]) - (define external - (if private? - f - (dict-ref internal-external-mapping f))) + (define external (dict-ref internal-external-mapping f)) (define maybe-type (dict-ref type-map external #f)) (values (-> (make-Univ) (or (and maybe-type (car maybe-type)) @@ -815,12 +841,31 @@ -Bottom) -Void)))) + (define (make-private-field-types field-names getter-ids type-map) + (for/lists (_1 _2) ([field-name (in-set field-names)] + [getter-id (in-list getter-ids)]) + (define maybe-type (dict-ref type-map field-name #f)) + (values + (make-Function + ;; This case is more complicated than for public fields because private + ;; fields support occurrence typing. The object is set as the field's + ;; accessor id, so that *its* range type is refined for occurrence typing. + (list (make-arr* (list (make-Univ)) + (or (and maybe-type (car maybe-type)) + (make-Univ)) + #:filters -no-filter + #:object + (make-Path (list (make-FieldPE)) getter-id)))) + (-> (make-Univ) (or (and maybe-type (car maybe-type)) + -Bottom) + -Void)))) + (define-values (field-get-types field-set-types) (make-field-types (hash-ref parse-info 'field-internals) fields)) (define-values (private-field-get-types private-field-set-types) - (make-field-types (hash-ref parse-info 'private-fields) - private-field-types - #:private? #t)) + (make-private-field-types (hash-ref parse-info 'private-fields) + localized-private-field-get-names + private-field-types)) (define-values (inherit-field-get-types inherit-field-set-types) (make-field-types (hash-ref parse-info 'inherit-field-internals) super-fields)) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt index 52d7a5f5..fc1ddaa3 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt @@ -56,6 +56,19 @@ [else (let ([flds* (append lhs (cons (make-fld ty* acc-id #f) (cdr rhs)))]) (make-Struct nm par flds* proc poly pred))]))] + ;; class field ops + ;; + ;; A refinement of a private field in a class is really a refinement of the + ;; return type of the accessor function for that field (rather than a variable). + ;; We cannot just refine the type of the argument to the accessor, since that + ;; is an object type that doesn't mention private fields. Thus we use the + ;; FieldPE path element as a marker to refine the result of the accessor + ;; function. + [((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _))) + (list rst ... (FieldPE:))) + (make-Function + (list (make-arr* doms (update rng ft pos? rst))))] + ;; otherwise [(t '()) (if pos? diff --git a/typed-racket-lib/typed-racket/types/path-type.rkt b/typed-racket-lib/typed-racket/types/path-type.rkt index 3c364f77..747b8145 100644 --- a/typed-racket-lib/typed-racket/types/path-type.rkt +++ b/typed-racket-lib/typed-racket/types/path-type.rkt @@ -57,6 +57,11 @@ [((PolyDots: _ body-t) _) (path-type path body-t resolved)] [((PolyRow: _ _ body-t) _) (path-type path body-t resolved)] + ;; for private fields in classes + [((Function: (list (arr: doms (Values: (list (Result: rng _ _))) _ _ _))) + (list rst ... (FieldPE:))) + (path-type rst rng)] + ;; types which need resolving [((? needs-resolving?) _) #:when (not (set-member? resolved t)) (path-type path (resolve-once t) (set-add resolved t))] diff --git a/typed-racket-lib/typed-racket/utils/mutated-vars.rkt b/typed-racket-lib/typed-racket/utils/mutated-vars.rkt index d7dd928d..49548967 100644 --- a/typed-racket-lib/typed-racket/utils/mutated-vars.rkt +++ b/typed-racket-lib/typed-racket/utils/mutated-vars.rkt @@ -5,8 +5,10 @@ ;; find and add to mapping all the set!'ed variables in form ;; if the supplied mapping is mutable, mutates it ;; default is immutability -;; syntax [table] -> table -(define (find-mutated-vars form [tbl (make-immutable-free-id-table)]) +;; syntax [table] [pred] -> table +(define (find-mutated-vars form + [tbl (make-immutable-free-id-table)] + [pred #f]) (define add (if (dict-mutable? tbl) (lambda (t i) (dict-set! t i #t) t) (lambda (t i) (dict-set t i #t)))) @@ -17,8 +19,18 @@ (loop stx tbl))) (syntax-parse stx #:literal-sets (kernel-literals) + ;; let us care about custom syntax classes + [form + #:when pred + #:attr result (pred #'form) + #:when (attribute result) + (define-values (sub name) + (values (car (attribute result)) + (cadr (attribute result)))) + (add (loop sub tbl) name)] ;; what we care about: set! [(set! v e) + #:when (not pred) (add (loop #'e tbl) #'v)] ;; forms with expression subforms [(define-values (var ...) expr) diff --git a/typed-racket-test/unit-tests/class-tests.rkt b/typed-racket-test/unit-tests/class-tests.rkt index 5de9165f..6a8f77c3 100644 --- a/typed-racket-test/unit-tests/class-tests.rkt +++ b/typed-racket-test/unit-tests/class-tests.rkt @@ -1932,4 +1932,72 @@ (define/public (m [x : Symbol 'y]) (symbol->string x) (void)))) (send (new c%) m)) - -Void])) + -Void] + ;; Next several tests are for occurrence typing on private fields + [tc-e (let () + (define c% + (class object% + (super-new) + (: x (U String #f)) + (define x "foo") + (: m (-> String)) + (define/public (m) + (if (string? x) (string-append x "bar") "baz")))) + (send (new c%) m)) + -String] + [tc-e (let () + (define c% + (class object% + (super-new) + (: x (List (U String #f))) + (define x (list "foo")) + (: m (-> String)) + (define/public (m) + (if (string? (car x)) ; car path + (string-append (car x) "bar") + "baz")))) + (send (new c%) m)) + -String] + [tc-e (class object% + (super-new) + (: x (Option String)) + (define x "foo") + ;; let-aliasing + occ. typing on fields + (let ([y x]) (if (string? y) (string-append x) ""))) + (-class)] + [tc-err (let () + (define c% + (class object% + (super-new) + (: x (U String #f)) + (define x "foo") + (set! x #f) ; prevents occ. typing + (: m (-> String)) + (define/public (m) + (if (string? x) (string-append x "bar") "baz")))) + (error "foo")) + #:msg #rx"expected: String.*given: \\(U False String\\)"] + [tc-err (let () + (define c% + (class object% + (super-new) + (: x (U String #f)) + (define x "foo") + (field [f (begin (set! x #f) "hello")]) + (: m (-> String)) + (define/public (m) + (if (string? x) (string-append x "bar") "baz")))) + (error "foo")) + #:msg #rx"expected: String.*given: \\(U False String\\)"] + [tc-err (let () + (define c% + (class object% + (super-new) + (: x (U String #f)) + (define x "foo") + (define/public (n) (set! x #f)) + (: m (-> String)) + (define/public (m) + (if (string? x) (string-append x "bar") "baz")))) + (error "foo")) + #:msg #rx"expected: String.*given: \\(U False String\\)"]))