From a61aef0339cd5ed36a7edd8dd58346acd868b3b9 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 12 Feb 2010 21:57:58 +0000 Subject: [PATCH] Generate proper contracts for polymorphic struct types. Document `Nothing'. svn: r18074 original commit: 90c8fcff1194799ed6f522e7554d49571b1f3074 --- .../typed-scheme/unit-tests/subtype-tests.ss | 8 ++--- .../unit-tests/type-equal-tests.ss | 4 +-- collects/typed-scheme/env/init-envs.ss | 7 +++-- collects/typed-scheme/infer/infer-unit.ss | 2 +- .../typed-scheme/private/type-contract.ss | 30 +++++++++++++++---- collects/typed-scheme/rep/type-rep.ss | 6 ++-- collects/typed-scheme/ts-reference.scrbl | 2 ++ collects/typed-scheme/typecheck/tc-app.ss | 2 +- collects/typed-scheme/typecheck/tc-envops.ss | 8 ++--- collects/typed-scheme/typecheck/tc-structs.ss | 4 +-- collects/typed-scheme/types/abbrev.ss | 6 ++-- collects/typed-scheme/types/printer.ss | 4 +-- .../typed-scheme/types/remove-intersect.ss | 12 ++++---- collects/typed-scheme/types/subtype.ss | 10 +++---- 14 files changed, 66 insertions(+), 39 deletions(-) diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss index bb3be770..a179c83f 100644 --- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss @@ -113,10 +113,10 @@ [(-values (list -Number)) (-values (list Univ))] - [(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a))) . -> . (-lst a))) - ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))))) . -> . (-lst (-pair -Number (-v a))))] - [(-poly (a) ((-struct 'bar #f (list -Number a)) . -> . (-lst a))) - ((-struct 'bar #f (list -Number (-pair -Number (-v a)))) . -> . (-lst (-pair -Number (-v a))))] + [(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null)) . -> . (-lst a))) + ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null)) . -> . (-lst (-pair -Number (-v a))))] + [(-poly (a) ((-struct 'bar #f (list -Number a) null) . -> . (-lst a))) + ((-struct 'bar #f (list -Number (-pair -Number (-v a))) null) . -> . (-lst (-pair -Number (-v a))))] [(-poly (a) (a . -> . (make-Listof a))) ((-v b) . -> . (make-Listof (-v b)))] [(-poly (a) (a . -> . (make-Listof a))) ((-pair -Number (-v b)) . -> . (make-Listof (-pair -Number (-v b))))] diff --git a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss index 57aaa478..b262c348 100644 --- a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss @@ -37,10 +37,10 @@ [(-mu x (Un -Number -Symbol x)) (-mu y (Un -Number -Symbol y))] ;; found bug [FAIL (Un (-mu heap-node - (-struct 'heap-node #f (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))))) + (-struct 'heap-node #f (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))) null)) (-base 'heap-empty)) (Un (-mu heap-node - (-struct 'heap-node #f (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))))) + (-struct 'heap-node #f (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))) null)) (-base 'heap-empty))])) (define-go diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index 73d1a9a1..6f0bf6c7 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -25,8 +25,11 @@ [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))] [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))] [(Name: stx) `(make-Name (quote-syntax ,stx))] - [(Struct: name parent flds proc poly? pred-id cert) - `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))] + [(Struct: name parent flds proc poly? pred-id cert acc-ids) + `(make-Struct ,(sub name) ,(sub parent) + ,(sub flds) ,(sub proc) ,(sub poly?) + (quote-syntax ,pred-id) (syntax-local-certifier) + (list ,@(for/list ([a acc-ids]) `(quote-syntax ,a))))] [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))] [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))] [(Refinement: parent pred cert) `(make-Refinement ,(sub parent) diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss index eb2ce093..265371b1 100644 --- a/collects/typed-scheme/infer/infer-unit.ss +++ b/collects/typed-scheme/infer/infer-unit.ss @@ -322,7 +322,7 @@ (cg S e))) (fail! S T))] - [((Struct: nm p flds proc _ _ _) (Struct: nm p flds* proc* _ _ _)) + [((Struct: nm p flds proc _ _ _ _) (Struct: nm p flds* proc* _ _ _ _)) (let-values ([(flds flds*) (cond [(and proc proc*) (values (cons proc flds) (cons proc* flds*))] diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index 89c690ad..3a2fb917 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -51,9 +51,10 @@ (define (type->contract ty fail #:out [out? #f] #:typed-side [from-typed? #t]) (define vars (make-parameter '())) (let/ec exit - (let loop ([ty ty] [pos? #t] [from-typed? from-typed?]) - (define (t->c t) (loop t pos? from-typed?)) - (define (t->c/neg t) (loop t (not pos?) (not from-typed?))) + (let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null]) + (define (t->c t #:seen [structs-seen structs-seen]) (loop t pos? from-typed? structs-seen)) + (define (t->c/neg t #:seen [structs-seen structs-seen]) (loop t (not pos?) (not from-typed?) structs-seen)) + (trace t->c) (match ty [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))] ;; any/c doesn't provide protection in positive position @@ -79,6 +80,7 @@ (define (f a) (define-values (dom* opt-dom* rngs* rst) (match a + ;; functions with no filters or objects [(arr: dom (Values: (list (Result: rngs (LFilterSet: '() '()) (LEmpty:)) ...)) rst #f kws) (let-values ([(mand-kws opt-kws) (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws)] [(conv) (match-lambda [(Keyword: kw kty _) (list kw (t->c/neg kty))])]) @@ -86,6 +88,7 @@ (append-map conv opt-kws) (map t->c rngs) (and rst (t->c/neg rst))))] + ;; functions with filters or objects [(arr: dom (Values: (list (Result: rngs _ _) ...)) rst #f '()) (if (and out? pos?) (values (map t->c/neg dom) @@ -140,8 +143,25 @@ [(Instance: _) #'(is-a?/c object%)] [(Class: _ _ _) #'(subclass?/c object%)] [(Value: '()) #'null?] - [(Struct: _ _ _ _ #f pred? cert) - #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))] + [(Struct: nm par flds proc poly? pred? cert acc-ids) + (cond + [(assf (λ (t) (type-equal? t ty)) structs-seen) + => + (lambda (pr) + (cdr pr))] + [proc (exit (fail))] + [poly? + (with-syntax* ([(x rec) (generate-temporaries '(x rec))] + [(fld-cnts ...) + (for/list ([fty flds] + [f-acc acc-ids]) + #`(#,(t->c fty #:seen (cons (cons ty #'rec) structs-seen)) + (#,f-acc x)))]) + #`(flat-rec-contract + rec + '#,(syntax-e pred?) + (lambda (x) (and fld-cnts ...))))] + [else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])] [(Syntax: (Base: 'Symbol _)) #'identifier?] [(Syntax: t) #`(syntax/c #,(t->c t))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index 9bcb03c9..1627f7af 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -207,7 +207,8 @@ [proc (or/c #f Function?)] [poly? boolean?] [pred-id identifier?] - [cert procedure?]) + [cert procedure?] + [acc-ids (listof identifier?)]) [#:intern (list name parent flds proc)] [#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds))) (combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))] @@ -217,7 +218,8 @@ (and proc (type-rec-id proc)) poly? pred-id - cert)] + cert + acc-ids)] [#:key #f]) ;; the supertype of all of these values diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl index 9ad4989c..33cf0ded 100644 --- a/collects/typed-scheme/ts-reference.scrbl +++ b/collects/typed-scheme/ts-reference.scrbl @@ -46,6 +46,8 @@ These types represent primitive Scheme data. Note that @scheme[Integer] represe @defidform[Any]{Any Scheme value. All other types are subtypes of @scheme[Any].} +@defidform[Nothing]{The type with no members.} + The following base types are parameteric in their type arguments. @defform[(Listof t)]{Homogenous @rtech{lists} of @scheme[t]} diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 6dcd92ac..ccb0cb5e 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -708,7 +708,7 @@ (lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected)))) t argtys expected)] ;; procedural structs - [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _))) _) + [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _))) _) (tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty) (cons ftype0 argtys) expected)] ;; parameters are functions too [((tc-result1: (Param: in out)) (list)) (ret out)] diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index 34a2280e..e2ee9b83 100644 --- a/collects/typed-scheme/typecheck/tc-envops.ss +++ b/collects/typed-scheme/typecheck/tc-envops.ss @@ -38,12 +38,12 @@ (make-Pair t (update s (make-NotTypeFilter u rst x)))] ;; struct ops - [((Struct: nm par flds proc poly pred cert) + [((Struct: nm par flds proc poly pred cert acc-ids) (TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x)) - (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))) proc poly pred cert)] - [((Struct: nm par flds proc poly pred cert) + (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))) proc poly pred cert )] + [((Struct: nm par flds proc poly pred cert acc-ids) (NotTypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x)) - (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert)] + (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids)] ;; otherwise [(t (TypeFilter: u (list) _)) diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss index 337444f3..cbbdd5bb 100644 --- a/collects/typed-scheme/typecheck/tc-structs.ss +++ b/collects/typed-scheme/typecheck/tc-structs.ss @@ -76,7 +76,7 @@ ;; Option[Struct-Ty] -> Listof[Type] (define (get-parent-flds p) (match p - [(Struct: _ _ flds _ _ _ _) flds] + [(Struct: _ _ flds _ _ _ _ _) flds] [(Name: n) (get-parent-flds (lookup-type-name n))] [#f null])) @@ -98,7 +98,7 @@ (define-values (maker pred getters setters) (struct-names nm flds setters?)) (let* ([name (syntax-e nm)] [fld-types (append parent-field-types types)] - [sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier))] + [sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier) getters)] [external-fld-types/no-parent types] [external-fld-types fld-types]) (if type-only diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index ca5ca183..617d2693 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -76,7 +76,7 @@ (define make-promise-ty (let ([s (string->uninterned-symbol "Promise")]) (lambda (t) - (make-Struct s #f (list t) #f #f #'promise? values)))) + (make-Struct s #f (list t) #f #f #'promise? values (list #'values))))) (define -Listof (-poly (list-elem) (make-Listof list-elem))) @@ -252,8 +252,8 @@ (define (make-arr-dots dom rng dty dbound) (make-arr* dom rng #:drest (cons dty dbound))) -(define (-struct name parent flds [proc #f] [poly #f] [pred #'dummy] [cert values]) - (make-Struct name parent flds proc poly pred cert)) +(define (-struct name parent flds accs [proc #f] [poly #f] [pred #'dummy] [cert values]) + (make-Struct name parent flds proc poly pred cert accs)) (define (-filter t [p null] [i 0]) (make-LTypeFilter t p i)) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index f84d5b6c..2092712c 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -166,8 +166,8 @@ (fp "~a" (cons 'List (tuple-elems t)))] [(Base: n cnt) (fp "~a" n)] [(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))] - [(Struct: 'Promise par (list fld) proc _ _ _) (fp "(Promise ~a)" fld)] - [(Struct: nm par flds proc _ _ _) + [(Struct: 'Promise par (list fld) proc _ _ _ _) (fp "(Promise ~a)" fld)] + [(Struct: nm par flds proc _ _ _ _) (fp "#(struct:~a ~a" nm flds) (when proc (fp " ~a" proc)) diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss index ebcd2938..a9680bb9 100644 --- a/collects/typed-scheme/types/remove-intersect.ss +++ b/collects/typed-scheme/types/remove-intersect.ss @@ -50,15 +50,15 @@ [(or (list (Pair: _ _) _) (list _ (Pair: _ _))) #f] - [(list (Struct: n _ flds _ _ _ _) - (Struct: n _ flds* _ _ _ _)) + [(list (Struct: n _ flds _ _ _ _ _) + (Struct: n _ flds* _ _ _ _ _)) (for/and ([f flds] [f* flds*]) (overlap f f*))] ;; n and n* must be different, so there's no overlap - [(list (Struct: n #f flds _ _ _ _) - (Struct: n* #f flds* _ _ _ _)) + [(list (Struct: n #f flds _ _ _ _ _) + (Struct: n* #f flds* _ _ _ _ _)) #f] - [(list (Struct: n p flds _ _ _ _) - (Struct: n* p* flds* _ _ _ _)) + [(list (Struct: n p flds _ _ _ _ _) + (Struct: n* p* flds* _ _ _ _ _)) (and (= (length flds) (length flds*)) (for/and ([f flds] [f* flds*]) (overlap f f*)))] [else #t])]))) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 2d44c649..936646a4 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -304,22 +304,22 @@ [((Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)] [(s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)] ;; subtyping on immutable structs is covariant - [((Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _)) + [((Struct: nm _ flds #f _ _ _ _) (Struct: nm _ flds* #f _ _ _ _)) (subtypes* A0 flds flds*)] - [((Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _)) + [((Struct: nm _ flds proc _ _ _ _) (Struct: nm _ flds* proc* _ _ _ _)) (subtypes* A0 (cons proc flds) (cons proc* flds*))] - [((Struct: _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s))))) + [((Struct: _ _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s))))) A0] [((Box: _) (BoxTop:)) A0] [((Vector: _) (VectorTop:)) A0] [((MPair: _ _) (MPairTop:)) A0] [((Hashtable: _ _) (HashtableTop:)) A0] ;; subtyping on structs follows the declared hierarchy - [((Struct: nm (? Type? parent) flds proc _ _ _) other) + [((Struct: nm (? Type? parent) flds proc _ _ _ _) other) ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other) (subtype* A0 parent other)] ;; Promises are covariant - [((Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)] + [((Struct: 'Promise _ (list t) _ _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _ _)) (subtype* A0 t t*)] ;; subtyping on values is pointwise [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] ;; trivial case for Result