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

Update structure types to have constructor ids.

Browse Source 
Use constructor to generate better contracts for poly structs.

original commit: 41e469d7aefd9aab480594caaba62dd7019ec0fd
This commit is contained in:
Sam Tobin-Hochstadt 2010-04-14 15:06:14 -04:00
parent ce7df53455
commit 6890aab175
14 changed files with 99 additions and 58 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
collects/tests/typed-scheme/succeed/provide-poly-struct.ss Normal file
View File

@ -0,0 +1,12 @@
#lang scheme/load
(module m typed-scheme
(define-struct: (A) x ([v : A]))
(provide make-x x-v))
(module n scheme
(require 'm)
(x-v (make-x 1)))
(require 'm)
(require 'n)

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

@ -112,10 +112,11 @@
[(-values (list -Number)) (-values (list Univ))]
[(-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) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null #'values)) . -> . (-lst a)))
((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values))
. -> . (-lst (-pair -Number (-v a))))]
[(-poly (a) ((-struct 'bar #f (list -Number a) null #'values) . -> . (-lst a)))
((-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values) . -> . (-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))))]

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

@ -37,10 +37,14 @@
[(-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))) null))
(-struct 'heap-node #f
(list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty)))
null #'values))
(-base 'heap-empty))
(Un (-mu heap-node
(-struct 'heap-node #f (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))) null))
(-struct 'heap-node #f
(list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty)))
null #'values))
(-base 'heap-empty))]))
(define-go

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

@ -1,10 +1,10 @@
#lang scheme/base
(provide (all-defined-out))
(require "../utils/utils.ss")
(require "type-env.ss"
(require "../utils/utils.ss"
"type-env.ss"
"type-name-env.ss"
"type-alias-env.ss"
unstable/struct
(rep type-rep object-rep filter-rep rep-utils)
(for-template (rep type-rep object-rep filter-rep)
(types union)
@ -25,11 +25,12 @@
[(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 acc-ids)
[(Struct: name parent flds proc poly? pred-id cert acc-ids maker-id)
`(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))))]
(list ,@(for/list ([a acc-ids]) `(quote-syntax ,a)))
(quote-syntax ,maker-id))]
[(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*))]

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

@ -160,25 +160,33 @@
#;#'class?
#'(class/c (name fcn-cnt) ... (init [by-name-init by-name-cnt] ...)))]
[(Value: '()) #'null?]
[(Struct: nm par flds proc poly? pred? cert acc-ids)
[(Struct: nm par flds proc poly? pred? cert acc-ids maker-id)
(cond
[(assf (λ (t) (type-equal? t ty)) structs-seen)
=>
(lambda (pr)
(cdr pr))]
cdr]
[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?))])]
[poly?
(with-syntax* ([(rec blame val) (generate-temporaries '(rec blame val))]
[maker maker-id]
[cnt-name nm]
[(fld-cnts ...)
(for/list ([fty flds]
[f-acc acc-ids])
#`(((contract-projection
#,(t->c fty #:seen (cons (cons ty #'(recursive-contract rec)) structs-seen)))
blame)
(#,f-acc val)))])
#`(letrec ([rec
(make-contract
#:name 'cnt-name
#:first-order #,pred?
#:projection
(lambda (blame)
(lambda (val)
(maker fld-cnts ...))))])
rec))]
[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)))]

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

@ -196,7 +196,7 @@
;; name : symbol
;; parent : Struct
;; flds : Listof[Type]
;; flds : Listof[Cons[Type,Bool]] type and mutability
;; proc : Function Type
;; poly? : is this a polymorphic type?
;; pred-id : identifier for the predicate of the struct
@ -204,22 +204,34 @@
(dt Struct ([name symbol?]
[parent (or/c #f Struct? Name?)]
[flds (listof Type/c)]
#;
[flds (listof (cons/c Type/c boolean?))]
[proc (or/c #f Function?)]
[poly? boolean?]
[pred-id identifier?]
[cert procedure?]
[acc-ids (listof identifier?)])
[acc-ids (listof identifier?)]
[maker-id 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)))]
[#:frees (combine-frees (map free-vars* (append (if proc (list proc) null)
(if parent (list parent) null)
flds #;(map car flds))))
(combine-frees (map free-idxs* (append (if proc (list proc) null)
(if parent (list parent) null)
flds #;(map car flds))))]
[#:fold-rhs (*Struct name
(and parent (type-rec-id parent))
(map type-rec-id flds)
#;
(for/list ([(t m?) (in-pairs (in-list flds))])
(cons (type-rec-id t) m?))
(and proc (type-rec-id proc))
poly?
pred-id
cert
acc-ids)]
acc-ids
maker-id)]
[#:key #f])
;; A structure type descriptor

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

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

@ -11,7 +11,7 @@
(types resolve)
(only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props)
scheme/contract scheme/match
mzlib/trace unstable/debug
mzlib/trace unstable/debug unstable/struct
(typecheck tc-metafunctions)
(for-syntax scheme/base))
@ -44,12 +44,15 @@
(make-Syntax (update t (make-NotTypeFilter u rst x)))]
;; struct ops
[((Struct: nm par flds proc poly pred cert acc-ids)
[((Struct: nm par flds proc poly pred cert acc-ids maker-id)
(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 acc-ids)]
[((Struct: nm par flds proc poly pred cert acc-ids)
(make-Struct nm par
(replace-nth flds idx
(lambda (e) (update e (make-TypeFilter u rst x))))
proc poly pred cert acc-ids maker-id)]
[((Struct: nm par flds proc poly pred cert acc-ids maker-id)
(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 acc-ids)]
(make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids maker-id)]
;; 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]))
@ -99,7 +99,7 @@
(define-values (struct-type-id 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) getters)]
[sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier) getters (or maker* maker))]
[external-fld-types/no-parent types]
[external-fld-types fld-types])
(if type-only

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

@ -77,7 +77,7 @@
(define make-promise-ty
(let ([s (string->uninterned-symbol "Promise")])
(lambda (t)
(make-Struct s #f (list t) #f #f #'promise? values (list #'values)))))
(make-Struct s #f (list t) #f #f #'promise? values (list #'values) #'values))))
(define -Listof (-poly (list-elem) (make-Listof list-elem)))
@ -256,8 +256,8 @@
(define (make-arr-dots dom rng dty dbound)
(make-arr* dom rng #:drest (cons dty dbound)))
(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 (-struct name parent flds accs constructor [proc #f] [poly #f] [pred #'dummy] [cert values])
(make-Struct name parent flds proc poly pred cert accs constructor))
(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))

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

@ -50,18 +50,18 @@
[(or (list (Pair: _ _) _)
(list _ (Pair: _ _)))
#f]
[(or (list (Value: '()) (Struct: n _ flds _ _ _ _ _))
(list (Struct: n _ flds _ _ _ _ _) (Value: '())))
[(or (list (Value: '()) (Struct: n _ flds _ _ _ _ _ _))
(list (Struct: n _ flds _ _ _ _ _ _) (Value: '())))
#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

@ -306,22 +306,22 @@
[(s (Union: es)) (or (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)
(fail! s t))]
;; 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