Skip to content
This repository

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse code

Fix filter conjunction constructor. Closes CTYP-23

  • Loading branch information...
commit 87040592b383436bf37bd3908727335f3d29e2b3 1 parent 9f5b432
Ambrose Bonnaire-Sergeant authored March 25, 2013
126  src/main/clojure/clojure/core/typed/filter_ops.clj
@@ -306,69 +306,71 @@
306 306
 
307 307
 
308 308
 ;  A ^ (B v ...) -> (simplify A (B v ...))
309  
-(defn -and [& args]
310  
-             ;flatten direct internal AndFilters
311  
-  (let [flat (apply concat
312  
-                    (for [fl args]
313  
-                      (if (AndFilter? fl)
314  
-                        (:fs fl)
315  
-                        [fl])))
316  
-        fs (set flat)]
317  
-    (cond
318  
-      (empty? fs) -bot
319  
-      (fs -bot) -bot
320  
-      (or (= 1 (count fs))
321  
-          (= 1 (count (disj fs -top)))) (or (first (disj fs -top))
322  
-                                            (first fs))
323  
-      :else (->AndFilter (disj fs -top)))))
324  
-
325 309
 ;(defn -and [& args]
326  
-;  {:pre [(every? Filter? args)]
327  
-;   :post [(Filter? %)]}
328  
-;  (letfn [(mk [& fs]
329  
-;            {:pre [(every? Filter? fs)]
330  
-;             :post [(Filter? %)]}
331  
-;            (cond
332  
-;              (empty? fs) -top
333  
-;              (= 1 (count fs)) (first fs)
334  
-;              :else (->AndFilter fs)))]
335  
-;    (loop [fs (set args)
336  
-;           result nil]
337  
-;      (if (empty? fs)
338  
-;        (cond
339  
-;          (empty? result) -top
340  
-;          (= 1 (count result)) (first result)
341  
-;          ;; don't think this is useful here
342  
-;          (= 2 (count result)) (let [[f1 f2] result]
343  
-;                                 (if (opposite? f1 f2)
344  
-;                                   -bot
345  
-;                                   (if (= f1 f2)
346  
-;                                     f1
347  
-;                                     (apply mk (compact [f1 f2] false)))))
348  
-;          :else
349  
-;           ;; first, remove anything implied by the atomic propositions
350  
-;           ;; We commonly see: (And (Or P Q) (Or P R) (Or P S) ... P), which this fixes
351  
-;          (let [{atomic true not-atomic false} (group-by atomic-filter? result)
352  
-;                not-atomic* (for [p not-atomic
353  
-;                                  :when (some (fn [a] (implied-atomic? p a)) atomic)]
354  
-;                              p)]
355  
-;             ;; `compact' takes care of implications between atomic props
356  
-;            (apply mk (compact (concat not-atomic* atomic) false))))
357  
-;        (let [ffs (first fs)]
358  
-;          (cond
359  
-;            (BotFilter? ffs) ffs
360  
-;            (AndFilter? ffs) (let [fs* (:fs ffs)]
361  
-;                               (recur (next fs) (concat fs* result)))
362  
-;            (TopFilter? ffs) (recur (next fs) result)
363  
-;            :else (let [t ffs]
364  
-;                    (cond
365  
-;                      (some (fn [f] (opposite? f ffs)) (concat (rest fs) result)) 
366  
-;                      -bot
367  
-;                      (some (fn [f] (or (= f t)
368  
-;                                        (implied-atomic? t f))) result) 
369  
-;                      (recur (rest fs) result)
370  
-;                      :else
371  
-;                      (recur (rest fs) (cons t result))))))))))
  310
+;             ;flatten direct internal AndFilters
  311
+;  (let [flat (apply concat
  312
+;                    (for [fl args]
  313
+;                      (if (AndFilter? fl)
  314
+;                        (:fs fl)
  315
+;                        [fl])))
  316
+;        fs (set flat)]
  317
+;    (cond
  318
+;      (empty? fs) -bot
  319
+;      (fs -bot) -bot
  320
+;      (or (= 1 (count fs))
  321
+;          (= 1 (count (disj fs -top)))) (or (first (disj fs -top))
  322
+;                                            (first fs))
  323
+;      :else (->AndFilter (disj fs -top)))))
  324
+
  325
+(declare implied-atomic?)
  326
+
  327
+(defn -and [& args]
  328
+  {:pre [(every? Filter? args)]
  329
+   :post [(Filter? %)]}
  330
+  (letfn [(mk [& fs]
  331
+            {:pre [(every? Filter? fs)]
  332
+             :post [(Filter? %)]}
  333
+            (cond
  334
+              (empty? fs) -top
  335
+              (= 1 (count fs)) (first fs)
  336
+              :else (->AndFilter (set fs))))]
  337
+    (loop [fs (set args)
  338
+           result nil]
  339
+      (if (empty? fs)
  340
+        (cond
  341
+          (empty? result) -top
  342
+          (= 1 (count result)) (first result)
  343
+          ;; don't think this is useful here
  344
+          (= 2 (count result)) (let [[f1 f2] result]
  345
+                                 (if (opposite? f1 f2)
  346
+                                   -bot
  347
+                                   (if (= f1 f2)
  348
+                                     f1
  349
+                                     (apply mk (compact [f1 f2] false)))))
  350
+          :else
  351
+           ;; first, remove anything implied by the atomic propositions
  352
+           ;; We commonly see: (And (Or P Q) (Or P R) (Or P S) ... P), which this fixes
  353
+          (let [{atomic true not-atomic false} (group-by atomic-filter? result)
  354
+                not-atomic* (for [p not-atomic
  355
+                                  :when (some (fn [a] (implied-atomic? p a)) atomic)]
  356
+                              p)]
  357
+             ;; `compact' takes care of implications between atomic props
  358
+            (apply mk (compact (concat not-atomic* atomic) false))))
  359
+        (let [ffs (first fs)]
  360
+          (cond
  361
+            (BotFilter? ffs) ffs
  362
+            (AndFilter? ffs) (let [fs* (:fs ffs)]
  363
+                               (recur (next fs) (concat fs* result)))
  364
+            (TopFilter? ffs) (recur (next fs) result)
  365
+            :else (let [t ffs]
  366
+                    (cond
  367
+                      (some (fn [f] (opposite? f ffs)) (concat (rest fs) result)) 
  368
+                      -bot
  369
+                      (some (fn [f] (or (= f t)
  370
+                                        (implied-atomic? t f))) result) 
  371
+                      (recur (rest fs) result)
  372
+                      :else
  373
+                      (recur (rest fs) (cons t result))))))))))
372 374
 
373 375
 (defn -FS [+ -]
374 376
   {:pre [(Filter? +)
3  src/test/clojure/clojure/core/typed/test/core.clj
@@ -1216,8 +1216,7 @@
1216 1216
                      (adder [_ i] (Accumulator. (+ t i))))))))
1217 1217
 ;;;;
1218 1218
 
1219  
-;TODO CTYP-23
1220  
-#_(deftest let-filter-unscoping-test
  1219
+(deftest let-filter-unscoping-test
1221 1220
   (is (cf (fn [a]
1222 1221
             (and (< 1 2) a))
1223 1222
           [(U nil Number) -> Any :filters {:then (is Number 0)}])))

0 notes on commit 8704059

Please sign in to comment.
Something went wrong with that request. Please try again.