From 6a83901a8bd60ccea014f84238a378749573beb2 Mon Sep 17 00:00:00 2001
From: Sam Tobin-Hochstadt <samth@racket-lang.org>
Date: Sun, 18 Oct 2009 01:10:00 +0000
Subject: [PATCH] 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
---
 .../typed-scheme/unit-tests/subtype-tests.ss  |  2 ++
 collects/typed-scheme/private/base-env.ss     | 22 ++++++++++++++++++-
 collects/typed-scheme/typecheck/tc-if.ss      |  6 +++++
 collects/typed-scheme/types/subtype.ss        | 18 +++++++++++++++
 4 files changed, 47 insertions(+), 1 deletion(-)

diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
index 3725582e68..c84dcce50c 100644
--- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
+++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss
@@ -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 
diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss
index 993206c07c..edd2bec2d7 100644
--- a/collects/typed-scheme/private/base-env.ss
+++ b/collects/typed-scheme/private/base-env.ss
@@ -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)]
diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss
index b465898128..9a73b8bbb8 100644
--- a/collects/typed-scheme/typecheck/tc-if.ss
+++ b/collects/typed-scheme/typecheck/tc-if.ss
@@ -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"
diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss
index 909e22dbec..3bbb1d6d68 100644
--- a/collects/typed-scheme/types/subtype.ss
+++ b/collects/typed-scheme/types/subtype.ss
@@ -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))