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

Generate proper contracts for polymorphic struct types.

Browse Source 
Document `Nothing'.

svn: r18074

original commit: 90c8fcff1194799ed6f522e7554d49571b1f3074
This commit is contained in:
Sam Tobin-Hochstadt 2010-02-12 21:57:58 +00:00
parent b2ea0474f2
commit a61aef0339
14 changed files with 66 additions and 39 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
collects/tests/typed-scheme/unit-tests/subtype-tests.ss
View File

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

4
collects/tests/typed-scheme/unit-tests/type-equal-tests.ss
View File

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

7
collects/typed-scheme/env/init-envs.ss vendored
View File

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

2
collects/typed-scheme/infer/infer-unit.ss
View File

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

30
collects/typed-scheme/private/type-contract.ss
View File

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

6
collects/typed-scheme/rep/type-rep.ss
View File

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

2
collects/typed-scheme/ts-reference.scrbl
View File

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

2
collects/typed-scheme/typecheck/tc-app.ss
View File

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

8
collects/typed-scheme/typecheck/tc-envops.ss
View File

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

4
collects/typed-scheme/typecheck/tc-structs.ss
View File

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

6
collects/typed-scheme/types/abbrev.ss
View File

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

4
collects/typed-scheme/types/printer.ss
View File

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

12
collects/typed-scheme/types/remove-intersect.ss
View File

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

10
collects/typed-scheme/types/subtype.ss
View File

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