handle subtyping for varargs functions

svn: r13962

original commit: 147cac076ca959adfb754a778979621a37d5ce73
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-05 00:09:43 +00:00
parent 5f9dbd695a
commit ee917a791e
3 changed files with 37 additions and 16 deletions

View File

@ -33,8 +33,6 @@
(B Univ)
(Sym Univ)
(-Void Univ)
#;(Sym Dyn)
#;(Dyn N)
[N N]
[(Un (-pair Univ (-lst Univ)) (-val '())) (-lst Univ)]
[(-pair N (-pair N (-pair (-val 'foo) (-val '())))) (-lst Univ)]
@ -113,6 +111,8 @@
(cl-> [() (-pair N (-v b))]
[(N) (-pair N (-v b))])]
[(-values (list N)) (-values (list Univ))]
[(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list N a))) . -> . (-lst a)))
((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list N (-pair N (-v a))))) . -> . (-lst (-pair N (-v a))))]
[(-poly (a) ((-struct 'bar #f (list N a)) . -> . (-lst a)))

View File

@ -122,17 +122,30 @@
(define (arr-subtype*/no-fail A0 s t)
(with-handlers
([exn:subtype? (lambda _ #f)])
(match (list s t)
(match* (s t)
;; top for functions is above everything
[(list _ (top-arr:)) A0]
[(list (arr: s1 s2 #f #f s-kws)
(arr: t1 t2 #f #f t-kws))
[(_ (top-arr:)) A0]
[((arr: s1 s2 #f #f s-kws)
(arr: t1 t2 #f #f t-kws))
(subtype-seq A0
(subtypes* t1 s1)
(kw-subtypes* t-kws s-kws)
(subtype* s2 t2))]
;; FIXME - handle varargs
[else
[((arr: s-dom s-rng s-rest #f s-kws)
(arr: t-dom t-rng #f #f t-kws))
(subtype-seq A0
(subtypes*/varargs t-dom s-dom s-rest)
(kw-subtypes* t-kws s-kws)
(subtype* s-rng t-rng))]
[((arr: s-dom s-rng s-rest #f s-kws)
(arr: t-dom t-rng t-rest #f t-kws))
(subtype-seq A0
(subtypes*/varargs t-dom s-dom s-rest)
(subtype* t-rest s-rest)
(kw-subtypes* t-kws s-kws)
(subtype* s-rng t-rng))]
;; FIXME - handle dotted varargs
[(_ _)
(fail! s t)])))
(define (subtypes/varargs args dom rst)
@ -283,6 +296,9 @@
[(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
;; subtyping on values is pointwise
[(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)]
;; trivial case for Result
[(list (Result: t f o) (Result: t* f o))
(subtype* A0 t t*)]
;; single values shouldn't actually happen, but they're just like the type
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]

View File

@ -29,20 +29,25 @@ at least theoretically.
(begin
(define-require-syntax (nm stx)
(syntax-parse stx
[(_ id:identifier ...)
[(form id:identifier ...)
(with-syntax ([(id* ...)
(map (lambda (id)
(datum->syntax
id
`(file
,(path->string
(build-path (collection-path "typed-scheme"
#,(symbol->string (syntax-e #'nm)))
(string-append (symbol->string (syntax-e id))
".ss"))))
,(datum->syntax
#f
(path->string
(build-path (collection-path "typed-scheme"
#,(symbol->string (syntax-e #'nm)))
(string-append (symbol->string (syntax-e id))
".ss")))
id id))
id id))
(syntax->list #'(id ...)))])
(syntax/loc stx (combine-in id* ...)))]))
(syntax-property (syntax/loc stx (combine-in id* ...))
'disappeared-use
#'form))]))
(define-provide-syntax (nm-out stx)
(syntax-parse stx
[(_ id:identifier ...)
@ -183,7 +188,7 @@ at least theoretically.
[(_ val)
#'(? (lambda (x) (equal? val x)))])))
(define-for-syntax printing? #f)
(define-for-syntax printing? #t)
(define-syntax-rule (defprinter t ...)
(begin