New function [Misc.trim] (unused on master).

src/misc.ml

@@ -347,6 +347,36 @@ let levels cmp xs =
       let ys1, yss = levels1 cmp x1 xs in
       ys1 :: yss
 
+(* Suppose [ys] is a list of elements that are pairwise incomparable
+   with respect to the partial order [<=], and [x] is a new element.
+   Then, [insert (<=) x ys] is the list obtained by inserting [x] and
+   removing any non-maximal elements; so it is again a list of pairwise
+   incomparable elements. *)
+
+let insert (<=) x ys =
+  (* If [x] is subsumed by some element [y] of [ys], then there is nothing
+     to do. In particular, no element [y] of [ys] can be subsumed by [x],
+     since the elements of [ys] are pairwise incomparable. *)
+  if List.exists (fun y -> x <= y) ys then
+    ys
+  (* Or [x] must be inserted, and any element [y] of [ys] that is subsumed
+     by [x] must be removed. *)
+  else
+    x :: List.filter (fun y -> not (y <= x)) ys
+
+(* Suppose [xs] is an arbitrary list of elements. Then [trim (<=) xs] is the
+   sublist of the elements of [xs] that are maximal with respect to the
+   partial order [<=]. In other words, it is a sublist where every element
+   that is less than some other element has been removed. *)
+
+(* One might wish to define [trim] using [List.filter] to keep just the
+   maximal elements, but it is not so easy to say "keep an element only
+   if it is not subsumed by some *other* element of the list". Instead,
+   we iterate [insert]. *)
+
+let trim (<=) xs =
+  List.fold_right (insert (<=)) xs []
+
 let rec dup1 cmp x ys =
   match ys with
   | [] ->

src/misc.mli

@@ -167,6 +167,13 @@ val best: ('a -> 'a -> bool) -> 'a list -> 'a option
 
 val levels: ('a -> 'a -> int) -> 'a list -> 'a list list
 
+(* Suppose [xs] is an arbitrary list of elements. Then [trim (<=) xs] is the
+   sublist of the elements of [xs] that are maximal with respect to the
+   partial order [<=]. In other words, it is a sublist where every element
+   that is less than some other element has been removed. *)
+
+val trim: ('a -> 'a -> bool) -> 'a list -> 'a list
+
 (* Assuming that the list [xs] is sorted with respect to the ordering [cmp],
    [dup cmp xs] returns a duplicate element of the list [xs], if one exists. *)