Simplify and document compact.

original commit: e8c14839e11847066bda841d5027b992b89fb253

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/filter-ops.rkt

@@ -78,46 +78,41 @@
 ;; compact : (Listof prop) bool -> (Listof prop)
 ;; props : propositions to compress
 ;; or? : is this an OrFilter (alternative is AndFilter)
+;;
+;; This combines all the TypeFilters at the same path into one TypeFilter. If it is an OrFilter the
+;; combination is done using Un, otherwise, restrict. The reverse is done for NotTypeFilters. If it is
+;; an OrFilter this simplifies to -top if any of the atomic filters simplified to -top, and removes
+;; any -bot values. The reverse is done if this is an AndFilter.
+;;
 (define/cond-contract (compact props or?)
      ((c:listof Filter/c) boolean? . c:-> . (c:listof Filter/c))
   (define tf-map (make-hash))
   (define ntf-map (make-hash))
-  ;; props: the propositions we're processing
-  ;; others: props that are neither TF or NTF
-  (let loop ([props props] [others null])
-    (if (null? props)
-        (append others
-                (for/list ([v (in-dict-values tf-map)]) v)
-                (for/list ([v (in-dict-values ntf-map)]) v))
-        (match (car props)
-          [(and f (TypeFilter: t1 p) (? (lambda _ or?)))
-           (hash-update! tf-map
-                         p
-                         (match-lambda [(TypeFilter: t2 _) (-filter (Un t1 t2) p)]
-                                       [p (int-err "got something that isn't a typefilter ~a" p)])
-                         f)
-           (loop (cdr props) others)]
-          [(and f (TypeFilter: t1 p) (? (lambda _ (not or?))))
-           (match (hash-ref tf-map p #f)
-             [(TypeFilter: (? (lambda (t2) (not (overlap t1 t2)))) _)
-              ;; we're in an And, and we got two types for the same path that do not overlap
-              (list -bot)]
-             [(TypeFilter: t2 _)
-              (hash-set! tf-map p
-                         (-filter (restrict t1 t2) p))
-              (loop (cdr props) others)]
-             [#f
-              (hash-set! tf-map  p
-                         (-filter t1 p))
-              (loop (cdr props) others)])]
-          [(and f (NotTypeFilter: t1 p) (? (lambda _ (not or?))))
-           (hash-update! ntf-map p
-                         (match-lambda [(NotTypeFilter: t2 _)
-                                        (-not-filter (Un t1 t2) p)]
-                                       [p (int-err "got something that isn't a nottypefilter ~a" p)])
-                         f)
-           (loop (cdr props) others)]
-          [p (loop (cdr props) (cons p others))]))))
+  (define (restrict-update dict t1 p)
+    (hash-update! dict p (λ (t2) (restrict t1 t2)) Univ))
+  (define (union-update dict t1 p)
+    (hash-update! dict p (λ (t2) (Un t1 t2)) -Bottom))
+
+  (define-values (atomics others) (partition atomic-filter? props))
+  (for ([prop (in-list atomics)])
+    (match prop
+      [(TypeFilter: t1 p)
+       ((if or? union-update restrict-update) tf-map t1 p) ]
+      [(NotTypeFilter: t1 p)
+       ((if or? restrict-update union-update) ntf-map t1 p) ]))
+  (define raw-results
+    (append others
+            (for/list ([(k v) (in-hash tf-map)]) (-filter v k))
+            (for/list ([(k v) (in-hash ntf-map)]) (-not-filter v k))))
+  (if or?
+      (if (member -top raw-results)
+          (list -top)
+          (filter-not Bot? raw-results))
+      (if (member -bot raw-results)
+          (list -bot)
+          (filter-not Top? raw-results))))
+
+
 
 ;; invert-filter: Filter/c -> Filter/c
 ;; Logically inverts a filter.
@@ -146,7 +141,7 @@
   (define mk
     (case-lambda [() -bot]
                  [(f) f]
-                 [fs (make-OrFilter fs)]))
+                 [fs (make-OrFilter (sort fs filter<?))]))
   (define (distribute args)
     (define-values (ands others) (partition AndFilter? args))
     (if (null? ands)
@@ -156,10 +151,7 @@
                         (apply -or a (append (cdr ands) others)))))))
   (let loop ([fs args] [result null])
     (if (null? fs)
-        (match result
-          [(list) -bot]
-          [(list f) f]
-          [_ (distribute (compact result #t))])
+        (distribute (compact result #t))
         (match (car fs)
           [(and t (Top:)) t]
           [(OrFilter: fs*) (loop (append fs* (cdr fs)) result)]
@@ -179,7 +171,7 @@
   (define mk
     (case-lambda [() -top]
                  [(f) f]
-                 [fs (make-AndFilter fs)]))
+                 [fs (make-AndFilter (sort fs filter<?))]))
   (define (flatten-ands fs)
     (let loop ([fs fs] [results null])
       (match fs
@@ -194,26 +186,7 @@
     (partition TypeFilter? filters))
   (let loop ([fs (append type-filters not-type-filters other-args)] [result null])
     (if (null? fs)
-        (match result
-          [(list) -top]
-          [(list f) f]
-          ;; don't think this is useful here
-          [(list f1 f2) (if (contradictory? f1 f2)
-                            -bot
-                            (if (filter-equal? f1 f2)
-                                f1
-                                (apply mk (compact (list f1 f2) #f))))]
-          [_
-           ;; first, remove anything implied by the atomic propositions
-           ;; We commonly see: (And (Or P Q) (Or P R) (Or P S) ... P), which this fixes
-           (let-values ([(atomic not-atomic) (partition atomic-filter? result)])
-             (define not-atomic*
-               (for/list ([p (in-list not-atomic)]
-                          #:unless (for/or ([a (in-list atomic)])
-                                     (implied-atomic? p a)))
-                 p))
-             ;; `compact' takes care of implications between atomic props
-             (apply mk (compact (append not-atomic* atomic) #f)))])
+        (apply mk (compact result #f))
         (match (car fs)
           [(and t (Bot:)) t]
           [(Top:) (loop (cdr fs) result)]