implication works

original commit: 2d88d698c20722f59f82e0dd2352e1e1cd067234

collects/tests/typed-scheme/succeed/simple-implies.ss

@@ -3,8 +3,10 @@
 ;; Example 13
 (define: x : Any 7)
 (define: z : (U Number String) 7)
-(cond [(and (number? x) (string? z)) (add1 x)]
-      [(number? x) (add1 z)]
-      [else 0])
+(if (and (number? x) (string? z))
+    (add1 x)
+    (if (number? x)
+        (add1 z)
+        0))
 
 ;(and (number? x) (string? z))

collects/typed-scheme/typecheck/tc-envops.ss

@@ -65,7 +65,7 @@
 ;; sets the flag box to #f if anything becomes (U)
 (d/c (env+ env fs flag)
   (env? (listof Filter/c) (box/c #t). -> . env?)
-  (define-values (imps atoms) (combine-props fs (env-props env) flag))
+  (define-values (imps atoms) (debug combine-props fs (env-props env) flag))
   (for/fold ([Γ (replace-props env imps)]) ([f atoms])
     (match f
       [(Bot:) (set-box! flag #f) (env-map (lambda (x) (cons (car x) (Un))) Γ)]

collects/typed-scheme/typecheck/tc-metafunctions.ss

@@ -118,6 +118,21 @@
             [(AndFilter: ps) (loop derived-props derived-atoms (append ps (cdr worklist)))]
             [(TypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
             [(NotTypeFilter: _ _ _) (loop derived-props (cons p derived-atoms) (cdr worklist))]
+            [(OrFilter: ps) 
+             (let ([new-or
+                    (let or-loop ([ps ps] [result null])
+                      (cond 
+                        [(null? ps) (apply -or result)]
+                        [(for/or ([other-p (in-list (append derived-props derived-atoms))])
+                             (opposite? (car ps) other-p))
+                         (or-loop (cdr ps) result)]
+                        [(for/or ([other-p (in-list derived-atoms)])
+                             (implied-atomic? (car ps) other-p))
+                         -top]
+                        [else (or-loop (cdr ps) (cons (car ps) result))]))])
+               (if (OrFilter? new-or)
+                   (loop (cons new-or derived-props) derived-atoms (cdr worklist))
+                   (loop derived-props derived-atoms (cons new-or (cdr worklist)))))]
             [(Top:) (loop derived-props derived-atoms (cdr worklist))]
             [(Bot:) (set-box! flag #f) (values derived-props derived-atoms)]
             [_ (loop (cons p derived-props) derived-atoms (cdr worklist))])))))

collects/typed-scheme/types/convenience.ss

@@ -6,6 +6,7 @@
 	 (types comparison printer union subtype utils)
          scheme/list scheme/match scheme/promise
          (for-syntax syntax/parse scheme/base)
+         unstable/debug
          (for-template scheme/base))
 
 (provide (all-defined-out)
@@ -97,23 +98,34 @@
               [(_ _) #f])))
 
 (define (-or . args) 
+  (define (distribute args)
+    (define-values (ands others) (partition AndFilter? args))
+    (if (null? ands)
+        (make-OrFilter others)
+        (match-let ([(AndFilter: elems) (car ands)])
+          (apply -and (for/list ([a (in-list elems)])
+                        (apply -or a (append (cdr ands) others)))))))
   (let loop ([fs args] [result null])
     (if (null? fs)
         (match result
           [(list) -bot]
           [(list f) f]
-          [(list f1 f2) 
-           (if (opposite? f1 f2)
-               -top
-               (if (filter-equal? f1 f2)
-                   f1
-                   (make-OrFilter (list f1 f2))))]
-          [_ (make-OrFilter result)])
+          [(or (list f1 (AndFilter: fs))
+               (list (AndFilter: fs) f1))
+           (apply -and (for/list ([f (in-list fs)]) (-or f1 f)))]
+          [_ (distribute result)])
         (match (car fs)
           [(and t (Top:)) t]
-          [(OrFilter: fs*) (loop (cdr fs) (append fs* result))]
+          [(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]
           [(Bot:) (loop (cdr fs) result)]
-          [t (loop (cdr fs) (cons t result))]))))
+          [t 
+           (cond [(for/or ([f (in-list (append (cdr fs) result))])
+                    (opposite? f t))
+                  -top]
+                 [(for/or ([f (in-list result)]) (or (filter-equal? f t) (implied-atomic? t f)))
+                  (loop (cdr fs) result)]
+                 [else
+                  (loop (cdr fs) (cons t result))])]))))
 
 (define (-and . args) 
   (let loop ([fs args] [result null])