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.
This commit is contained in:
Asumu Takikawa 2015-01-22 11:22:27 -05:00
parent 177d1a7f68
commit 62c86d5ddd
6 changed files with 158 additions and 14 deletions

View File

@ -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])

View File

@ -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> -> 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))

View File

@ -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?

View File

@ -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))]

View File

@ -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)

View File

@ -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\\)"]))