From f9199f6e3710018c2162f0453ae10ef164534063 Mon Sep 17 00:00:00 2001
From: AlexKnauth <alexander@knauth.org>
Date: Mon, 10 Apr 2017 20:55:23 -0700
Subject: [PATCH] Use filter-maximal for pruning redundant elements in unions

---
 turnstile/examples/stlc+union.rkt          |  8 ++--
 turnstile/examples/util/filter-maximal.rkt | 54 ++++++++++++++++++++++
 2 files changed, 58 insertions(+), 4 deletions(-)
 create mode 100644 turnstile/examples/util/filter-maximal.rkt

diff --git a/turnstile/examples/stlc+union.rkt b/turnstile/examples/stlc+union.rkt
index 2ce4e34..aaaa384 100644
--- a/turnstile/examples/stlc+union.rkt
+++ b/turnstile/examples/stlc+union.rkt
@@ -3,6 +3,8 @@
  #:except #%app #%datum + add1 sub1 *
           Int Int? ~Int Float Float? ~Float Bool ~Bool Bool?)
 
+(require (for-syntax "util/filter-maximal.rkt"))
+
 ;; Simply-Typed Lambda Calculus, plus union types
 ;; Types:
 ;; - types from and ext+stlc.rkt
@@ -45,11 +47,9 @@
 
 (define-for-syntax (prune+sort tys)
   (stx-sort 
-   (remove-duplicates 
+   (filter-maximal 
     (stx->list tys)
-    ;; remove dups keeps first element
-    ;; but we want to keep supertype
-    (lambda (x y) (typecheck? y x)))))
+    typecheck?)))
   
 (define-syntax (U stx)
   (syntax-parse stx
diff --git a/turnstile/examples/util/filter-maximal.rkt b/turnstile/examples/util/filter-maximal.rkt
new file mode 100644
index 0000000..d3901a7
--- /dev/null
+++ b/turnstile/examples/util/filter-maximal.rkt
@@ -0,0 +1,54 @@
+#lang racket/base
+
+(provide filter-maximal)
+
+(module+ test
+  (require rackunit
+           (only-in racket/list in-permutations)
+           (only-in racket/set set=? subset?)))
+
+;; filter-maximal : [Listof X] [X X -> Bool] -> [Listof X]
+;; <? is a partial ordering predicate
+(define (filter-maximal xs <?)
+  (reverse
+   (for/fold ([acc '()])
+             ([x (in-list xs)])
+     (merge-with x acc <?))))
+
+;; merge-with : X [Listof X] [X X -> Bool] -> [Listof X]
+;; <? is a partial ordering predicate
+(define (merge-with x ys <?)
+  (define (greater? y) (<? x y))
+  (cond [(ormap greater? ys) ys]
+        [else
+         (define (not-lesser? y) (not (<? y x)))
+         (cons x (filter not-lesser? ys))]))
+
+;; ----------------------------------------------------------------------------
+
+(module+ test
+  (define-check (check-filter-maximal lst <? expected)
+    (test-begin
+     (for ([p (in-permutations lst)])
+       (check set=? (filter-maximal p <?) expected))))
+
+  (check-equal? (filter-maximal '(1 2 3 2 3 2 1) <) '(3 3))
+  (check-equal? (filter-maximal '(1 2 3 2 3.0 2 1) <) '(3 3.0))
+  (check-equal? (filter-maximal '(1 2 3.0 2 3 2 1) <) '(3.0 3))
+
+  (check-equal? (filter-maximal '({} {a} {b} {c}) subset?) '({a} {b} {c}))
+  (check-equal? (filter-maximal '({b} {} {a} {c}) subset?) '({b} {a} {c}))
+  (check-equal? (filter-maximal '({c} {b} {a} {}) subset?) '({c} {b} {a}))
+
+  (check-filter-maximal '({} {a} {b}) subset? '({a} {b}))
+  (check-filter-maximal '({} {a} {b} {a b}) subset? '({a b}))
+  (check-filter-maximal '({} {a} {b} {c} {a b}) subset? '({a b} {c}))
+  (check-filter-maximal '({} {a} {b} {c} {a b} {c a} {b c}) subset?
+                        '({a b} {c a} {b c}))
+  (check-filter-maximal '({} {a} {b} {c} {a b} {c a} {b c}) subset?
+                        '({a b} {c a} {b c}))
+  (check-filter-maximal '({} {a} {b} {c} {b c d} {a b} {c a} {b c}) subset?
+                        '({a b} {c a} {b c d}))
+  (check-filter-maximal '({} {a} {b} {c} {a b c d} {a b} {c a} {b c}) subset?
+                        '({a b c d}))
+  )