suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

For classes, always check expected type against synthesized

Browse Source 
This also enables depth subtyping for class types, which
was needed to get the tests to pass
This commit is contained in:
Asumu Takikawa 2013-08-02 13:11:59 -04:00
parent 37c313e9b3
commit 008e18a6b4
3 changed files with 104 additions and 84 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

173
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
View File

@ -160,15 +160,15 @@
(define (check-class form [expected #f]) (define (check-class form [expected #f])
(match (and expected (resolve expected)) (match (and expected (resolve expected))
[(tc-result1: (and self-class-type (Class: _ _ _ _ _))) [(tc-result1: (and self-class-type (Class: _ _ _ _ _)))
(do-check form #t self-class-type)] (do-check form self-class-type)]
[(tc-result1: (Poly-names: ns body-type)) [(tc-result1: (Poly-names: ns body-type))
(check-class form (ret body-type))] (check-class form (ret body-type))]
[#f (do-check form #f #f)] [#f (do-check form #f)]
[_ (check-below (do-check form #f #f) expected)])) [_ (check-below (do-check form #f) expected)]))
;; Syntax Boolean Option<Type> -> Type ;; Syntax Boolean Option<Type> -> Type
;; Do the actual type-checking ;; Do the actual type-checking
(define (do-check form expected? self-class-type) (define (do-check form expected)
(syntax-parse form (syntax-parse form
;; Inspect the expansion of the class macro for the pieces that ;; Inspect the expansion of the class macro for the pieces that
;; we need to type-check like superclass, methods, top-level ;; we need to type-check like superclass, methods, top-level
@ -178,19 +178,17 @@
;; FIXME: maybe should check the property on this expression ;; FIXME: maybe should check the property on this expression
;; as a sanity check too ;; as a sanity check too
(define super-type (tc-expr #'cls.superclass-expr)) (define super-type (tc-expr #'cls.superclass-expr))
(define-values (super-inits super-fields (define-values (super-row super-inits super-fields
super-methods super-augments) super-methods super-augments)
(match super-type (match super-type
;; FIXME: should handle the case where the super class is [(tc-result1: (Class: super-row super-inits super-fields
;; polymorphic
[(tc-result1: (Class: _ super-inits super-fields
super-methods super-augments)) super-methods super-augments))
(values super-inits super-fields super-methods super-augments)] (values super-row super-inits super-fields
super-methods super-augments)]
[(tc-result1: t) [(tc-result1: t)
(tc-error/expr "expected a superclass but got value of type ~a" t (tc-error/expr "expected a superclass but got value of type ~a" t
#:stx #'cls.superclass-expr) #:stx #'cls.superclass-expr)
;; FIXME: is this the right thing to do? (values #f null null null null)]))
(values null null null null)]))
;; Define sets of names for use later ;; Define sets of names for use later
(define super-init-names (list->set (dict-keys super-inits))) (define super-init-names (list->set (dict-keys super-inits)))
(define super-field-names (list->set (dict-keys super-fields))) (define super-field-names (list->set (dict-keys super-fields)))
@ -294,19 +292,19 @@
name)) name))
;; Type for self in method calls ;; Type for self in method calls
(define self-type (define self-type
(if self-class-type (infer-self-type super-row
(make-Instance self-class-type) expected
(infer-self-type internals-table internals-table
optional-inits optional-inits
internal-external-mapping internal-external-mapping
remaining-super-inits remaining-super-inits
super-fields super-fields
super-methods super-methods
super-augments super-augments
this%-init-internals this%-init-internals
this%-field-internals this%-field-internals
this%-public-internals this%-public-internals
this%-pubment-internals))) this%-pubment-internals))
(match-define (Instance: (Class: _ inits fields methods augments)) (match-define (Instance: (Class: _ inits fields methods augments))
self-type) self-type)
;; trawl the body for the local name table ;; trawl the body for the local name table
@ -374,14 +372,12 @@
(check-private-methods meth-stxs this%-private-names (check-private-methods meth-stxs this%-private-names
private-method-types self-type)) private-method-types self-type))
(define final-class-type (define final-class-type
(if expected? (merge-types
self-class-type self-type
(merge-types checked-method-types
self-type checked-pubment-types))
checked-method-types
checked-pubment-types)))
(check-method-presence-and-absence (check-method-presence-and-absence
final-class-type expected
this%-init-names this%-field-names this%-init-names this%-field-names
this%-public-names this%-override-names this%-public-names this%-override-names
this%-inherit-names this%-inherit-names
@ -390,13 +386,15 @@
remaining-super-inits super-field-names remaining-super-inits super-field-names
super-method-names super-method-names
super-augment-names) super-augment-names)
(when expected
(check-below final-class-type expected))
final-class-type])) final-class-type]))
;; check-method-presence-and-absence : Type Set<Symbol> * 12 -> Void ;; check-method-presence-and-absence : Type Set<Symbol> * 12 -> Void
;; use the internal class: information to check whether clauses ;; use the internal class: information to check whether clauses
;; exist or are absent appropriately ;; exist or are absent appropriately
(define (check-method-presence-and-absence (define (check-method-presence-and-absence
class-type this%-init-names this%-field-names expected this%-init-names this%-field-names
this%-public-names this%-override-names this%-public-names this%-override-names
this%-inherit-names this%-inherit-names
this%-pubment-names this%-augment-names this%-pubment-names this%-augment-names
@ -404,30 +402,31 @@
remaining-super-inits super-field-names remaining-super-inits super-field-names
super-method-names super-method-names
super-augment-names) super-augment-names)
(match-define (Class: _ inits fields methods augments) class-type) (when expected
(define exp-init-names (list->set (dict-keys inits))) (match-define (Class: _ inits fields methods augments) expected)
(define exp-field-names (list->set (dict-keys fields))) (define exp-init-names (list->set (dict-keys inits)))
(define exp-method-names (list->set (dict-keys methods))) (define exp-field-names (list->set (dict-keys fields)))
(define exp-augment-names (list->set (dict-keys augments))) (define exp-method-names (list->set (dict-keys methods)))
(define exp-optional-inits (define exp-augment-names (list->set (dict-keys augments)))
(for/set ([(name val) (in-dict inits)] (define exp-optional-inits
#:when (cadr val)) (for/set ([(name val) (in-dict inits)]
name)) #:when (cadr val))
(check-same (set-union this%-init-names name))
(list->set (dict-keys remaining-super-inits))) (check-same (set-union this%-init-names
exp-init-names (list->set (dict-keys remaining-super-inits)))
"initialization argument") exp-init-names
(check-same (set-union this%-public-names super-method-names) "initialization argument")
exp-method-names (check-same (set-union this%-public-names super-method-names)
"public method") exp-method-names
(check-same (set-union this%-field-names super-field-names) "public method")
exp-field-names (check-same (set-union this%-field-names super-field-names)
"public field") exp-field-names
(check-same (set-union this%-pubment-names super-augment-names) "public field")
exp-augment-names (check-same (set-union this%-pubment-names super-augment-names)
"public augmentable method") exp-augment-names
(check-same optional-external exp-optional-inits "public augmentable method")
"optional init argument") (check-same optional-external exp-optional-inits
"optional init argument"))
(check-exists super-method-names this%-override-names (check-exists super-method-names this%-override-names
"override method") "override method")
(check-exists super-augment-names this%-augment-names (check-exists super-augment-names this%-augment-names
@ -448,7 +447,7 @@
(match-define (match-define
(Instance: (Instance:
(and class-type (and class-type
(Class: #f inits fields methods augments))) (Class: row-var inits fields methods augments)))
self-type) self-type)
(define (make-new-methods methods method-types) (define (make-new-methods methods method-types)
(for/fold ([methods methods]) (for/fold ([methods methods])
@ -459,7 +458,7 @@
(when (and old-type (not (subtype (car type) (car old-type)))) (when (and old-type (not (subtype (car type) (car old-type))))
(int-err "merge-types: actual type not a subtype of annotated type")) (int-err "merge-types: actual type not a subtype of annotated type"))
(dict-set methods name type))) (dict-set methods name type)))
(make-Class #f inits fields (make-Class row-var inits fields
(make-new-methods methods method-types) (make-new-methods methods method-types)
(make-new-methods augments pubment-types))) (make-new-methods augments pubment-types)))
@ -943,40 +942,52 @@
[else (hash-set table name type)])] [else (hash-set table name type)])]
[_ table]))) [_ table])))
;; infer-self-type : Dict<Symbol, Type> Set<Symbol> Dict<Symbol, Symbol> ;; infer-self-type : RowVar Class Dict<Symbol, Type> Set<Symbol> Dict<Symbol, Symbol>
;; Inits Fields Methods ;; Inits Fields Methods
;; Set<Symbol> * 4 -> Type ;; Set<Symbol> * 4 -> Type
;; Construct a self object type based on the registered types ;; Construct a self object type based on all type annotations
;; from : inside the class body. ;; and the expected type
(define (infer-self-type internals-table optional-inits (define (infer-self-type super-row
expected
internals-table optional-inits
internal-external-mapping internal-external-mapping
super-inits super-fields super-methods super-inits super-fields super-methods
super-augments super-augments
inits fields publics augments) inits fields publics augments)
(define (make-type-dict names supers [inits? #f] (define (make-type-dict names supers maybe-expected [inits? #f]
#:default-type [default-type Univ]) #:default-type [default-type Univ])
(for/fold ([type-dict supers]) (for/fold ([type-dict supers])
([name names]) ([name names])
(define external (dict-ref internal-external-mapping name)) (define external (dict-ref internal-external-mapping name))
(cond [(dict-ref internals-table name #f) => (define (update-dict type)
(λ (type) (define entry
(define entry (if inits?
(if inits? (list type (set-member? optional-inits name))
(list type (set-member? optional-inits name)) (list type)))
(list type))) (dict-set type-dict external entry))
(dict-set type-dict external entry))] ;; A type is assigned for each member in this order:
[else ;; (1) a type annotation from the user
(dict-set type-dict external ;; (2) the expected type
(if inits? ;; (3) Any or Procedure
(list default-type (set-member? optional-inits name)) (cond [(dict-ref internals-table name #f) => update-dict]
(list default-type)))]))) [(and maybe-expected
(define init-types (make-type-dict inits super-inits #t)) (dict-ref maybe-expected name #f))
(define field-types (make-type-dict fields super-fields)) => (compose update-dict car)]
(define public-types (make-type-dict publics super-methods [default-type => update-dict])))
(define-values (expected-inits expected-fields
expected-publics expected-augments)
(match expected
[(Class: _ inits fields publics augments)
(values inits fields publics augments)]
[_ (values #f #f #f #f)]))
(define init-types (make-type-dict inits super-inits expected-inits #t))
(define field-types (make-type-dict fields super-fields expected-fields))
(define public-types (make-type-dict publics super-methods expected-publics
#:default-type top-func)) #:default-type top-func))
(define augment-types (make-type-dict augments super-augments (define augment-types (make-type-dict
#:default-type top-func)) augments super-augments expected-augments
(make-Instance (make-Class #f init-types field-types #:default-type top-func))
(make-Instance (make-Class super-row init-types field-types
public-types augment-types))) public-types augment-types)))
;; fixup-method-type : Function Type -> Function ;; fixup-method-type : Function Type -> Function

6
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/subtype.rkt
View File

@ -594,6 +594,8 @@
(subtype-clause? field-map field-map*))] (subtype-clause? field-map field-map*))]
[((Class: row inits fields methods augments) [((Class: row inits fields methods augments)
(Class: row* inits* fields* methods* augments*)) (Class: row* inits* fields* methods* augments*))
;; TODO: should the result be folded instead?
(define sub (curry subtype* A))
;; check that each of inits, fields, methods, etc. are ;; check that each of inits, fields, methods, etc. are
;; equal by sorting and checking type equality ;; equal by sorting and checking type equality
(define (equal-clause? clause clause* [inits? #f]) (define (equal-clause? clause clause* [inits? #f])
@ -607,7 +609,7 @@
(match-define (list (list names* types*) ...) clause*) (match-define (list (list names* types*) ...) clause*)
(and (= (length names) (length names*)) (and (= (length names) (length names*))
(andmap equal? names names*) (andmap equal? names names*)
(andmap equal? types types*))] (andmap sub types types*))]
[else [else
(match-define (list (list names types opt?) ...) (match-define (list (list names types opt?) ...)
clause) clause)
@ -615,7 +617,7 @@
clause*) clause*)
(and (= (length names) (length names*)) (and (= (length names) (length names*))
(andmap equal? names names*) (andmap equal? names names*)
(andmap equal? types types*) (andmap sub types types*)
(andmap equal? opt? opt?*))]))) (andmap equal? opt? opt?*))])))
;; There is no non-trivial width subtyping on class types, but it's ;; There is no non-trivial width subtyping on class types, but it's
;; possible for two "equal" class types to look different ;; possible for two "equal" class types to look different

9
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/class-tests.rkt
View File

@ -1037,5 +1037,12 @@
(class object% (class object%
(super-new) (super-new)
(: x Real) (: x Real)
(field [x : Integer 0]))))) (field [x : Integer 0])))
;; fails, expected type and annotation don't match
(check-err #:exn #rx"Expected \\(Class \\(field \\(x String"
(: c% (Class (field [x String])))
(define c%
(class object% (super-new)
(field [x : Integer 5]))))))