add first steps in real solving

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) (debug combine-props fs (env-props env)))
+  (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

@@ -90,7 +90,21 @@
 
 (provide combine-props tc-results->values)
 
-(define (combine-props new-props old-props)
+(define (resolve atoms prop)
+  (for/fold ([prop prop])
+    ([a (in-list atoms)])
+    (match prop
+      [(AndFilter: ps)
+       (let loop ([ps ps] [result null])
+         (if (null? ps)
+             (-and result)
+             (let ([p (car ps)])
+               (cond [(opposite? a p) -bot]
+                     [(implied-atomic? p a) (loop (cdr ps) result)]
+                     [else (loop (cdr ps) (cons p result))]))))]
+      [_ prop])))
+
+(define (combine-props new-props old-props flag)
   (define (atomic-prop? p) (or (TypeFilter? p) (NotTypeFilter? p)))
   (define-values (new-atoms new-formulas) (partition atomic-prop? new-props))
   (let loop ([derived-props null] 
@@ -98,9 +112,12 @@
              [worklist (append old-props new-formulas)])
     (if (null? worklist)
         (values derived-props derived-atoms)
-        (let ([p (car worklist)])
+        (let* ([p (car worklist)]
+               [p (resolve derived-atoms p)])
           (match p      
             [(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))]
+            [(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/abbrev.ss

@@ -279,55 +279,6 @@
     [(Path: p i) (-not-filter t i p)]
     [_ -top]))
 
-(define (opposite? f1 f2)
-  (match* (f1 f2)
-          [((TypeFilter: t1 p1 i1)
-            (NotTypeFilter: t2 p1 i2))
-           (and (type-equal? t1 t2)                
-                (free-identifier=? i1 i2))]
-          [((NotTypeFilter: t2 p1 i2)
-            (TypeFilter: t1 p1 i1))
-           (and (type-equal? t1 t2)                
-                (free-identifier=? i1 i2))]
-          [(_ _) #f]))
-
-(define (-or . args) 
-  (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)])
-        (match (car fs)
-          [(and t (Top:)) t]
-          [(OrFilter: fs*) (loop (cdr fs) (append fs* result))]
-          [(Bot:) (loop (cdr fs) result)]
-          [t (loop (cdr fs) (cons t result))]))))
-
-(define (-and . args) 
-  (let loop ([fs args] [result null])
-    (if (null? fs)
-        (match result
-          [(list) -top]
-          [(list f) f]
-          ;; don't think this is useful here
-          [(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]
-          [(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
-          [(Top:) (loop (cdr fs) result)]
-          [t (loop (cdr fs) (cons t result))]))))
 
 (d/c (-not-filter t i [p null])
      (c:->* (Type/c name-ref/c) ((listof PathElem?)) Filter/c)

collects/typed-scheme/types/convenience.ss

@@ -68,3 +68,68 @@
 (define Syntax-Sexp (-Sexpof Any-Syntax))
 
 (define Ident (-Syntax -Symbol))
+
+(define (opposite? f1 f2)
+  (match* (f1 f2)
+          [((TypeFilter: t1 p1 i1)
+            (NotTypeFilter: t2 p1 i2))
+           (and (free-identifier=? i1 i2)
+                (subtype t1 t2))]
+          [((NotTypeFilter: t2 p1 i2)
+            (TypeFilter: t1 p1 i1))
+           (and (free-identifier=? i1 i2)
+                (subtype t1 t2))]
+          [(_ _) #f]))
+
+;; is f1 implied by f2?
+(define (implied-atomic? f1 f2)
+  (if (filter-equal? f1 f2)
+      #t
+      (match* (f1 f2)
+              [((TypeFilter: t1 p1 i1)
+                (TypeFilter: t2 p1 i2))
+               (and (free-identifier=? i1 i2)
+                    (subtype t1 t2))]
+              [((NotTypeFilter: t2 p1 i2)
+                (NotTypeFilter: t1 p1 i1))
+               (and (free-identifier=? i1 i2)
+                    (subtype t1 t2))]
+              [(_ _) #f])))
+
+(define (-or . args) 
+  (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)])
+        (match (car fs)
+          [(and t (Top:)) t]
+          [(OrFilter: fs*) (loop (cdr fs) (append fs* result))]
+          [(Bot:) (loop (cdr fs) result)]
+          [t (loop (cdr fs) (cons t result))]))))
+
+(define (-and . args) 
+  (let loop ([fs args] [result null])
+    (if (null? fs)
+        (match result
+          [(list) -top]
+          [(list f) f]
+          ;; don't think this is useful here
+          [(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]
+          [(AndFilter: fs*) (loop (cdr fs) (append fs* result))]
+          [(Top:) (loop (cdr fs) result)]
+          [t (loop (cdr fs) (cons t result))]))))