Don't error for branches with wrong number of results where return type is Bot.

Allow case-lambda to be subtype of equiv union type.
Add types for path?, fold-files, assert

svn: r16357
This commit is contained in:
Sam Tobin-Hochstadt 2009-10-18 01:10:00 +00:00
parent ba959a9b24
commit 6a83901a8b
4 changed files with 47 additions and 1 deletions

View File

@ -125,6 +125,8 @@
;; polymorphic function types should be subtypes of the function top
[(-poly (a) (a . -> . a)) top-func]
[(cl->* (-Number . -> . -String) (-Boolean . -> . -String)) ((Un -Number -Boolean) . -> . -String)]
))
(define-go

View File

@ -7,6 +7,7 @@
scheme/unsafe/ops
(only-in rnrs/lists-6 fold-left)
'#%paramz
"extra-procs.ss"
(only-in '#%kernel [apply kernel:apply])
scheme/promise
(only-in string-constants/private/only-once maybe-print-message)
@ -85,7 +86,9 @@
[(-Port) -Sexp]
[() -Sexp])]
[ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))]
[andmap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))]
[andmap (-polydots (a c b) (cl->*
;(make-pred-ty (list (make-pred-ty (list a) B d) (-lst a)) B (-lst d))
(->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c)))]
[newline (cl-> [() -Void]
[(-Port) -Void])]
[not (-> Univ B)]
@ -638,6 +641,9 @@
[find-system-path (Sym . -> . -Path)]
[object-name (Univ . -> . Univ)]
[path? (make-pred-ty -Path)]
;; scheme/cmdline
[parse-command-line
@ -707,6 +713,20 @@
[string->some-system-path
(-String (Un (-val 'unix) (-val 'windows)) . -> . -Path)]
;; scheme/file
[fold-files
(-poly
(a)
(let ([funarg* (-Path (one-of/c 'file 'dir 'link) a . -> . (-values (list a Univ)))]
[funarg (-Path (one-of/c 'file 'dir 'link) a . -> . a)])
(cl->*
(funarg a . -> . a)
(funarg a (-opt -Pathlike) . -> . a)
(funarg a (-opt -Pathlike) Univ . -> . a)
(funarg* a . -> . a)
(funarg* a (-opt -Pathlike) . -> . a)
(funarg* a (-opt -Pathlike) Univ . -> . a))))]
;; scheme/math
[sgn (-Real . -> . -Real)]

View File

@ -53,6 +53,12 @@
(if expected
(check-below r expected)
r))]
;; special case if one of the branches is unreachable
[(and (= 1 (length us)) (type-equal? (car us) (Un)))
(if expected (check-below (ret ts fs2 os2)) (ret ts fs2 os2))]
[(and (= 1 (length ts)) (type-equal? (car ts) (Un)))
(if expected (check-below (ret us fs3 os3)) (ret us fs3 os3))]
;; otherwise, error
[else
(tc-error/expr #:return (ret (or expected Err))
"Expected the same number of values from both branches of if expression, but got ~a and ~a"

View File

@ -179,6 +179,18 @@
;(trace subtypes*/varargs)
(define (combine-arrs arrs)
(match arrs
[(list (arr: dom1 rng1 #f #f '()) (arr: dom rng #f #f '()) ...)
(cond
[(null? dom) (make-arr dom1 rng1 #f #f '())]
((not (apply = (length dom1) (map length dom)))
#f)
((not (foldl type-equal? rng1 rng))
#f)
[else (make-arr (apply map (lambda args (make-Union args)) (cons dom1 dom)) rng1 #f #f '())])]
[_ #f]))
;; the algorithm for recursive types transcribed directly from TAPL, pg 305
;; List[(cons Number Number)] type type -> List[(cons Number Number)]
@ -218,6 +230,12 @@
[(list (Value: (? string? n)) (Base: 'String _)) A0]
;; tvars are equal if they are the same variable
[(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))]
;; special-case for case-lambda/union
[(list (Function: arr1) (Function: (list arr2)))
(when (null? arr1) (fail! s t))
(or (arr-subtype*/no-fail A0 (combine-arrs arr1) arr2)
(supertype-of-one/arr A0 arr2 arr1)
(fail! s t))]
;; case-lambda
[(list (Function: arr1) (Function: arr2))
(when (null? arr1) (fail! s t))