progress, fix some dumb bugs

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

@@ -0,0 +1,10 @@
+#lang typed/scheme
+
+;; 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])
+
+;(and (number? x) (string? z))

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

@@ -0,0 +1,6 @@
+#lang typed/scheme
+
+(define: x : Any 7)
+(define: (f [x : (U String Number)]) : Number
+  (if (number? x) (add1 x) (string-length x)))
+(if (let ([tmp (number? x)]) (if tmp tmp (string? x))) (f x) 0)

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)))
+  (define-values (imps atoms) (debug combine-props fs (env-props env)))
   (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-if.ss

@@ -41,9 +41,7 @@
       [else (ret (Un))]))
   (match (single-value tst)
     [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _)
-     (let*-values ([(flag+ flag-) (values (box #t) (box #t))]
-                   [(derived-imps+ derived-atoms+)
-                    (combine-props (list fs+) (env-props (lexical-env)))])
+     (let*-values ([(flag+ flag-) (values (box #t) (box #t))])
        (match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) (list fs+) flag+) (tc thn (unbox flag+)))]
                     [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) (list fs-) flag-) (tc els (unbox flag-)))])
          ;; if we have the same number of values in both cases
@@ -58,7 +56,7 @@
                                       (-FS -top -top)]
                                      [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-))
                                       (-FS (-or (-and fs+ f2+) (-and fs- f3+))
-                                           (-or (-and fs+ f2-) (-and fs- f3-)))])]
+                                           (debug -or (-and fs+ f2-) (-and fs- f3-)))])]
                                   [type (Un t2 t3)]
                                   [object (if (object-equal? o2 o3) o2 (make-Empty))])
                               ;(printf "result filter is: ~a\n" filter)

collects/typed-scheme/types/abbrev.ss

@@ -297,7 +297,12 @@
         (match result
           [(list) -bot]
           [(list f) f]
-          [(list f1 f2) (opposite? f1 f2) -top]
+          [(list f1 f2) 
+           (if (opposite? f1 f2)
+               -top
+               (if (filter-equal? f1 f2)
+                   f1
+                   (make-OrFilter (list f1 f2))))]
           [_ (make-OrFilter result)])
         (match (car fs)
           [(and t (Top:)) t]
@@ -312,7 +317,11 @@
           [(list) -top]
           [(list f) f]
           ;; don't think this is useful here
-          #;[(list f1 f2) (opposite? f1 f2) -bot]
+          [(list f1 f2) (if (opposite? f1 f2)
+                            -bot
+                            (if (filter-equal? f1 f2)
+                                f1
+                                (make-AndFilter (list f1 f2))))]
           [_ (make-AndFilter result)])
         (match (car fs)
           [(and t (Bot:)) t]