[sledge] Switch from Base.List to Containers.List

Reviewed By: ngorogiannis

Differential Revision: D24306101

fbshipit-source-id: a653f793d

sledge/cli/domain_itv.ml

@@ -278,7 +278,7 @@ let call ~summaries ~globals:_ ~actuals ~areturn ~formals ~freturn:_
     let mangle r =
       Llair.Reg.program (Llair.Reg.typ r) ("__tmp__" ^ Llair.Reg.name r)
     in
-    let args = List.zip_exn formals actuals in
+    let args = List.combine_exn formals actuals in
     let q' =
       List.fold args ~init:q ~f:(fun q (f, a) -> assign (mangle f) a q)
     in

sledge/cli/frontend.ml

@@ -469,8 +469,8 @@ and xlate_value ?(inline = false) stk :
         (pre, Exp.record typ (IArray.of_list args))
     | ConstantStruct -> (
         let typ = xlate_type x (Llvm.type_of llv) in
-        match List.findi llv stk with
+        match List.find_idx ~f:(( == ) llv) stk with
-        | Some i -> ([], Exp.rec_record i typ)
+        | Some (i, _) -> ([], Exp.rec_record i typ)
         | None ->
             let stk = llv :: stk in
             let len = Llvm.num_operands llv in

sledge/cli/version.ml

@@ -31,7 +31,7 @@ let build_info =
         ( Build_info.Statically_linked_library.name lib
         , version_to_string
             (Build_info.Statically_linked_library.version lib) ) )
-    |> List.sort ~compare:[%compare: string * string]
+    |> List.sort ~cmp:[%compare: string * string]
   in
   let max_length =
     List.fold_left libs ~init:0 ~f:(fun n (name, _) ->

sledge/nonstdlib/NS.mli

@@ -127,8 +127,6 @@ include module type of Iter.Import
 
 (** Containers *)
 
-type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
-
 module Option = Option
 include module type of Option.Infix
 

sledge/nonstdlib/NS0.ml

@@ -119,8 +119,6 @@ let map_endo map t ~f =
 
 (** Containers *)
 
-type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
-
 (* from upcoming Stdlib *)
 module Either = struct
   type ('a, 'b) t = Left of 'a | Right of 'b

sledge/nonstdlib/iArray.ml

@@ -45,6 +45,8 @@ let fold_map xs ~init ~f =
   let a, ys = Array.fold_map (i2a xs) ~init ~f in
   (a, a2i ys)
 
+type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
+
 let fold_map_until xs ~init ~f ~finish =
   With_return.with_return (fun {return} ->
       finish

sledge/nonstdlib/iArray.mli

@@ -43,6 +43,8 @@ val contains_dup : compare:('a -> 'a -> int) -> 'a t -> bool
 val fold_map :
   'a t -> init:'accum -> f:('accum -> 'a -> 'accum * 'b) -> 'accum * 'b t
 
+type ('a, 'b) continue_or_stop = Continue of 'a | Stop of 'b
+
 val fold_map_until :
      'a t
   -> init:'accum

sledge/nonstdlib/iter.ml

@@ -13,3 +13,40 @@ end
 
 let pop seq =
   match head seq with Some x -> Some (x, drop 1 seq) | None -> None
+
+let contains_dup (type elt) seq ~cmp =
+  let module S = CCSet.Make (struct
+    type t = elt
+
+    let compare = cmp
+  end) in
+  let exception Found_dup in
+  try
+    fold ~init:S.empty seq ~f:(fun elts x ->
+        let elts' = S.add x elts in
+        if elts' == elts then raise_notrace Found_dup else elts' )
+    |> ignore ;
+    false
+  with Found_dup -> true
+
+let fold_opt seq ~init ~f =
+  let state = ref init in
+  let exception Stop in
+  try
+    seq (fun x ->
+        match f !state x with
+        | Some s -> state := s
+        | None -> raise_notrace Stop ) ;
+    Some !state
+  with Stop -> None
+
+let fold_until (type res) seq ~init ~f ~finish =
+  let state = ref init in
+  let exception Stop of res in
+  try
+    seq (fun x ->
+        match f !state x with
+        | `Continue s -> state := s
+        | `Stop r -> raise_notrace (Stop r) ) ;
+    finish !state
+  with Stop r -> r

sledge/nonstdlib/iter.mli

@@ -12,3 +12,16 @@ module Import : sig
 end
 
 val pop : 'a iter -> ('a * 'a iter) option
+val contains_dup : 'a iter -> cmp:('a -> 'a -> int) -> bool
+
+val fold_opt : 'a t -> init:'s -> f:('s -> 'a -> 's option) -> 's option
+(** [fold_option t ~init ~f] is a short-circuiting version of [fold] that
+    runs in the [Option] monad. If [f] returns [None], [None] is returned
+    without any additional invocations of [f]. *)
+
+val fold_until :
+     'a t
+  -> init:'s
+  -> f:('s -> 'a -> [`Continue of 's | `Stop of 'b])
+  -> finish:('s -> 'b)
+  -> 'b

sledge/nonstdlib/list.ml

@@ -6,91 +6,81 @@
  *)
 
 open! NS0
-include Base.List
+include ContainersLabels.List
 
-exception Not_found_s = Base.Sexp.Not_found_s
+type 'a t = 'a list [@@deriving compare, equal, hash, sexp]
 
-let rec pp ?pre ?suf sep pp_elt fs = function
+let hd_exn = hd
-  | [] -> ()
+let hd = function [] -> None | hd :: _ -> Some hd
-  | x :: xs ->
+let tl_exn = tl
-      Option.iter ~f:(Format.fprintf fs) pre ;
+let tl = function [] -> None | _ :: tl -> Some tl
-      pp_elt fs x ;
+let pop_exn = function x :: xs -> (x, xs) | [] -> raise Not_found
-      ( match xs with
+let exists xs ~f = exists ~f xs
-      | [] -> ()
+let for_all xs ~f = for_all ~f xs
-      | xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ;
+let find_exn xs ~f = find ~f xs
-      Option.iter ~f:(Format.fprintf fs) suf
+let find xs ~f = find_opt ~f xs
-
+let find_map xs ~f = find_map ~f xs
-let findi x xs =
+let find_map_exn xs ~f = Option.get_exn (find_map xs ~f)
-  let rec findi_ i xs =
-    match xs with
-    | [] -> None
-    | x' :: _ when x == x' -> Some i
-    | _ :: xs -> findi_ (i + 1) xs
-  in
-  findi_ 0 xs
-
-let pop_exn = function
-  | x :: xs -> (x, xs)
-  | [] -> raise (Not_found_s (Atom __LOC__))
 
-let find_map_remove xs ~f =
+let remove_one_exn ~eq x xs =
-  let rec find_map_remove_ ys = function
+  let rec remove_ ys = function
-    | [] -> None
+    | [] -> raise Not_found
-    | x :: xs -> (
+    | z :: xs -> if eq x z then rev_append ys xs else remove_ (z :: ys) xs
-      match f x with
-      | Some x' -> Some (x', rev_append ys xs)
-      | None -> find_map_remove_ (x :: ys) xs )
   in
-  find_map_remove_ [] xs
+  remove_ [] xs
 
-let fold_option xs ~init ~f =
+let remove_one ~eq x xs =
-  let@ {return} = With_return.with_return in
+  try Some (remove_one_exn ~eq x xs) with Not_found -> None
-  Some
-    (fold xs ~init ~f:(fun acc elt ->
-         match f acc elt with Some res -> res | None -> return None ))
 
+let remove ~eq x xs = remove ~eq ~key:x xs
+let map xs ~f = map ~f xs
 let map_endo t ~f = map_endo map t ~f
 
-let rev_map_unzip xs ~f =
+let rev_map_split xs ~f =
-  fold xs ~init:([], []) ~f:(fun (ys, zs) x ->
+  fold_left xs ~init:([], []) ~f:(fun (ys, zs) x ->
       let y, z = f x in
       (y :: ys, z :: zs) )
 
-let remove_exn ?(equal = ( == )) xs x =
+let combine_exn = combine
-  let rec remove_ ys = function
+
-    | [] -> raise (Not_found_s (Atom __LOC__))
+let combine xs ys =
-    | z :: xs ->
+  try Some (combine_exn xs ys) with Invalid_argument _ -> None
-        if equal x z then rev_append ys xs else remove_ (z :: ys) xs
+
-  in
+let fold xs ~init ~f = fold_left ~f ~init xs
-  remove_ [] xs
 
-let remove ?equal xs x =
+let reduce xs ~f =
-  try Some (remove_exn ?equal xs x) with Not_found_s _ -> None
+  match xs with [] -> None | x :: xs -> Some (fold xs ~init:x ~f)
 
-let rec rev_init n ~f =
+let fold2_exn xs ys ~init ~f = fold_left2 ~f ~init xs ys
-  if n = 0 then []
+let group_succ ~eq xs = group_succ ~eq:(fun y x -> eq x y) xs
-  else
-    let n = n - 1 in
-    let xs = rev_init n ~f in
-    f n :: xs
 
-let symmetric_diff ~compare xs ys =
+let symmetric_diff ~cmp xs ys =
   let rec symmetric_diff_ xxs yys : _ Either.t list =
     match (xxs, yys) with
     | x :: xs, y :: ys ->
-        let ord = compare x y in
+        let ord = cmp x y in
         if ord = 0 then symmetric_diff_ xs ys
         else if ord < 0 then Left x :: symmetric_diff_ xs yys
         else Right y :: symmetric_diff_ xxs ys
     | xs, [] -> map ~f:Either.left xs
     | [], ys -> map ~f:Either.right ys
   in
-  symmetric_diff_ (sort ~compare xs) (sort ~compare ys)
+  symmetric_diff_ (sort ~cmp xs) (sort ~cmp ys)
+
+let rec pp ?pre ?suf sep pp_elt fs = function
+  | [] -> ()
+  | x :: xs ->
+      Option.iter ~f:(Format.fprintf fs) pre ;
+      pp_elt fs x ;
+      ( match xs with
+      | [] -> ()
+      | xs -> Format.fprintf fs "%( %)%a" sep (pp sep pp_elt) xs ) ;
+      Option.iter ~f:(Format.fprintf fs) suf
 
-let pp_diff ~compare sep pp_elt fs (xs, ys) =
+let pp_diff ~cmp sep pp_elt fs (xs, ys) =
   let pp_diff_elt fs (elt : _ Either.t) =
     match elt with
     | Left x -> Format.fprintf fs "-- %a" pp_elt x
     | Right y -> Format.fprintf fs "++ %a" pp_elt y
   in
-  pp sep pp_diff_elt fs (symmetric_diff ~compare xs ys)
+  pp sep pp_diff_elt fs (symmetric_diff ~cmp xs ys)

sledge/nonstdlib/list.mli

@@ -6,7 +6,9 @@
  *)
 
 open! NS0
-include module type of Base.List
+include module type of ContainersLabels.List
+
+type 'a t = 'a list [@@deriving compare, equal, hash, sexp]
 
 val pp :
      ?pre:(unit, unit) fmt
@@ -17,39 +19,43 @@ val pp :
 (** Pretty-print a list. *)
 
 val pp_diff :
-     compare:('a -> 'a -> int)
+     cmp:('a -> 'a -> int)
   -> (unit, unit) fmt
   -> 'a pp
   -> ('a list * 'a list) pp
 
-val findi : 'a -> 'a t -> int option
+val hd : 'a t -> 'a option
-(** [findi x xs] is [Some i] when [nth xs i == x], otherwise [None]. *)
+val hd_exn : 'a t -> 'a
-
+val tl : 'a t -> 'a t option
+val tl_exn : 'a t -> 'a t
 val pop_exn : 'a list -> 'a * 'a list
+val exists : 'a t -> f:('a -> bool) -> bool
+val for_all : 'a t -> f:('a -> bool) -> bool
+val find : 'a t -> f:('a -> bool) -> 'a option
+val find_exn : 'a t -> f:('a -> bool) -> 'a
+val find_map : 'a t -> f:('a -> 'b option) -> 'b option
+val find_map_exn : 'a t -> f:('a -> 'b option) -> 'b
 
-val find_map_remove :
+val remove_one_exn : eq:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
-  'a list -> f:('a -> 'b option) -> ('b * 'a list) option
+(** Returns the input list without the first element [eq]ual to the
+    argument, or raise [Not_found] if no such element exists. *)
 
-val fold_option :
+val remove_one : eq:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list option
-  'a t -> init:'accum -> f:('accum -> 'a -> 'accum option) -> 'accum option
+val remove : eq:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
-(** [fold_option t ~init ~f] is a short-circuiting version of [fold] that
+val map : 'a t -> f:('a -> 'b) -> 'b t
-    runs in the [Option] monad. If [f] returns [None], that value is
-    returned without any additional invocations of [f]. *)
 
 val map_endo : 'a t -> f:('a -> 'a) -> 'a t
-(** Like map, but specialized to require [f] to be an endofunction, which
+(** Like [map], but specialized to require [f] to be an endofunction, which
     enables preserving [==] if [f] preserves [==] of every element. *)
 
-val rev_map_unzip : 'a t -> f:('a -> 'b * 'c) -> 'b list * 'c list
+val rev_map_split : 'a t -> f:('a -> 'b * 'c) -> 'b list * 'c list
-(** [rev_map_unzip ~f xs] is [unzip (rev_map ~f xs)] but more efficient. *)
+(** [rev_map_split ~f xs] is [split (rev_map ~f xs)] but more efficient. *)
-
-val remove_exn : ?equal:('a -> 'a -> bool) -> 'a list -> 'a -> 'a list
-(** Returns the input list without the first element [equal] to the
-    argument, or raise [Not_found_s] if no such element exists. [equal]
-    defaults to physical equality. *)
 
-val remove : ?equal:('a -> 'a -> bool) -> 'a list -> 'a -> 'a list option
+val combine : 'a t -> 'b t -> ('a * 'b) t option
-val rev_init : int -> f:(int -> 'a) -> 'a list
+val combine_exn : 'a t -> 'b t -> ('a * 'b) t
+val fold : 'a list -> init:'s -> f:('s -> 'a -> 's) -> 's
+val reduce : 'a t -> f:('a -> 'a -> 'a) -> 'a option
+val fold2_exn : 'a t -> 'b t -> init:'s -> f:('s -> 'a -> 'b -> 's) -> 's
 
 val symmetric_diff :
-  compare:('a -> 'a -> int) -> 'a t -> 'a t -> ('a, 'a) Either.t t
+  cmp:('a -> 'a -> int) -> 'a t -> 'a t -> ('a, 'a) Either.t t

sledge/report/sledge_report.ml

@@ -75,11 +75,11 @@ let add_gcs base_gcs gcs row =
   else List.fold ~f:(add_gc base_gcs) ~init:row gcs
 
 let add_status base_status row status =
-  if List.mem ~equal:Report.equal_status row.status status then row
+  if List.mem ~eq:Report.equal_status status row.status then row
   else
     match base_status with
     | Some base_status
-      when not (List.mem ~equal:Report.equal_status base_status status) ->
+      when not (List.mem ~eq:Report.equal_status status base_status) ->
         { row with
           status= status :: row.status
         ; status_deltas=
@@ -151,7 +151,7 @@ let combine name b_result c_result =
                 ; peak_size= ave_floats peaks }
         in
         let status =
-          Some (List.dedup_and_sort ~compare:Report.compare_status statuses)
+          Some (List.sort_uniq ~cmp:Report.compare_status statuses)
         in
         (times, gcs, status)
     | None -> (None, None, None)

sledge/src/fol.ml

@@ -1273,7 +1273,7 @@ module Context = struct
     List.pp "@ @<2>∧ "
       (fun fs (rep, cls) ->
         Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep (ppx_cls x)
-          (List.sort ~compare:Term.compare cls) )
+          (List.sort ~cmp:Term.compare cls) )
       fs (Term.Map.to_alist clss)
 
   let pp fs r = ppx_classes (fun _ -> None) fs (classes r)

sledge/src/llair/llair.ml

@@ -460,7 +460,7 @@ module Func = struct
         if is_undefined func then Format.fprintf fs " #%i@]" sort_index
         else
           let cfg =
-            List.sort ~compare:Block.compare (List.tl_exn (entry_cfg func))
+            List.sort ~cmp:Block.compare (List.tl_exn (entry_cfg func))
           in
           Format.fprintf fs " { #%i %a@;<1 4>@[<v>%a@ %a@]%t%a@]@ }"
             sort_index Loc.pp name.loc pp_cmnd cmnd Term.pp term
@@ -475,8 +475,9 @@ module Func = struct
     | Pointer {elt= Function {return; _}; _} ->
         assert (
           not
-            (List.contains_dup (entry_cfg func) ~compare:(fun b1 b2 ->
+            (Iter.contains_dup
-                 String.compare b1.lbl b2.lbl )) ) ;
+               (Iter.of_list (entry_cfg func))
+               ~cmp:(fun b1 b2 -> String.compare b1.lbl b2.lbl)) ) ;
         assert (
           Bool.equal (Option.is_some return) (Option.is_some func.freturn)
         ) ;
@@ -615,5 +616,5 @@ module Program = struct
       globals
       (List.pp "@\n@\n" Func.pp)
       ( String.Map.data functions
-      |> List.sort ~compare:(fun x y -> compare_block x.entry y.entry) )
+      |> List.sort ~cmp:(fun x y -> compare_block x.entry y.entry) )
 end

sledge/src/ses/equality.ml

@@ -383,13 +383,13 @@ let pp_diff fs (r, s) =
 
 let ppx_cls x = List.pp "@ = " (Term.ppx x)
 let pp_cls = ppx_cls (fun _ -> None)
-let pp_diff_cls = List.pp_diff ~compare:Term.compare "@ = " Term.pp
+let pp_diff_cls = List.pp_diff ~cmp:Term.compare "@ = " Term.pp
 
 let ppx_classes x fs clss =
   List.pp "@ @<2>∧ "
     (fun fs (rep, cls) ->
       Format.fprintf fs "@[%a@ = %a@]" (Term.ppx x) rep (ppx_cls x)
-        (List.sort ~compare:Term.compare cls) )
+        (List.sort ~cmp:Term.compare cls) )
     fs (Term.Map.to_alist clss)
 
 let pp_classes fs r = ppx_classes (fun _ -> None) fs (classes r)
@@ -903,17 +903,14 @@ let solve_class us us_xs ~key:rep ~data:cls (classes, subst) =
       Subst.pp subst]
   ;
   let cls, cls_not_ito_us_xs =
-    List.partition_tf
+    List.partition
       ~f:(fun e -> Var.Set.is_subset (Term.fv e) ~of_:us_xs)
       (rep :: cls)
   in
   let cls, subst = solve_interp_eqs us (cls, subst) in
   let cls, subst = solve_uninterp_eqs us (cls, subst) in
   let cls = List.rev_append cls_not_ito_us_xs cls in
-  let cls =
+  let cls = List.remove ~eq:Term.equal (Subst.norm subst rep) cls in
-    List.remove ~equal:Term.equal cls (Subst.norm subst rep)
-    |> Option.value ~default:cls
-  in
   let classes =
     if List.is_empty cls then Term.Map.remove classes rep
     else Term.Map.set classes ~key:rep ~data:cls
@@ -959,7 +956,8 @@ let solve_concat_extracts_eq r x =
 let solve_concat_extracts r us x (classes, subst, us_xs) =
   match
     List.filter_map (solve_concat_extracts_eq r x) ~f:(fun rev_extracts ->
-        List.fold_option rev_extracts ~init:[] ~f:(fun suffix e ->
+        Iter.fold_opt (Iter.of_list rev_extracts) ~init:[]
+          ~f:(fun suffix e ->
             let+ rep_ito_us =
               List.fold (cls_of r e) ~init:None ~f:(fun rep_ito_us trm ->
                   match rep_ito_us with
@@ -969,7 +967,8 @@ let solve_concat_extracts r us x (classes, subst, us_xs) =
                   | _ -> rep_ito_us )
             in
             Term.sized ~siz:(Term.seq_size_exn e) ~seq:rep_ito_us :: suffix ) )
-    |> List.min_elt ~compare:[%compare: Term.t list]
+    |> Iter.of_list
+    |> Iter.min ~lt:(fun xs ys -> [%compare: Term.t list] xs ys < 0)
   with
   | Some extracts ->
       let concat = Term.concat (Array.of_list extracts) in
@@ -1036,7 +1035,7 @@ let solve_for_vars vss r =
           || fail "@[%a@ = %a@ not entailed by@ @[%a@]@]" Term.pp key
                Term.pp data pp_classes r () ) ;
         assert (
-          List.fold_until vss ~init:us
+          Iter.fold_until (Iter.of_list vss) ~init:us
             ~f:(fun us xs ->
               let us_xs = Var.Set.union us xs in
               let ks = Term.fv key in
@@ -1046,8 +1045,8 @@ let solve_for_vars vss r =
                 && Var.Set.is_subset ds ~of_:us_xs
                 && ( Var.Set.is_subset ds ~of_:us
                    || not (Var.Set.is_subset ks ~of_:us) )
-              then Stop true
+              then `Stop true
-              else Continue us_xs )
+              else `Continue us_xs )
             ~finish:(fun _ -> false) ) )]
 
 let elim xs r = {r with rep= Subst.remove xs r.rep}

sledge/src/sh.ml

@@ -106,7 +106,7 @@ let rec var_strength_ xs m q =
   let m =
     List.fold ~init:m_stem q.djns ~f:(fun m djn ->
         let ms = List.map ~f:(fun dj -> snd (var_strength_ xs m dj)) djn in
-        List.reduce_balanced ms ~f:(fun m1 m2 ->
+        List.reduce ms ~f:(fun m1 m2 ->
             Var.Map.merge_skewed m1 m2 ~combine:(fun ~key:_ s1 s2 ->
                 match (s1, s2) with
                 | `Anonymous, `Anonymous -> `Anonymous
@@ -175,19 +175,18 @@ let pp_heap x ?pre ctx fs heap =
     | Some const -> (Term.sub e (Term.rational const), const)
     | None -> (e, Q.zero)
   in
-  let compare s1 s2 =
+  let cmp s1 s2 =
     [%compare: Term.t * (Term.t * Q.t)]
       (Context.normalize ctx s1.bas, bas_off (Context.normalize ctx s1.loc))
       (Context.normalize ctx s2.bas, bas_off (Context.normalize ctx s2.loc))
   in
-  let break s1 s2 =
+  let eq s1 s2 =
-    (not (Term.equal s1.bas s2.bas))
+    Term.equal s1.bas s2.bas
-    || (not (Term.equal s1.len s2.len))
+    && Term.equal s1.len s2.len
-    || not
+    && Context.implies ctx (Formula.eq (Term.add s1.loc s1.siz) s2.loc)
-         (Context.implies ctx (Formula.eq (Term.add s1.loc s1.siz) s2.loc))
   in
   let heap = List.map heap ~f:(map_seg ~f:(Context.normalize ctx)) in
-  let blocks = List.group ~break (List.sort ~compare heap) in
+  let blocks = List.group_succ ~eq (List.sort ~cmp heap) in
   List.pp ?pre "@ * " (pp_block x) fs blocks
 
 let pp_us ?(pre = ("" : _ fmt)) ?vs () fs us =
@@ -569,7 +568,8 @@ let seg pt =
 (** Update *)
 
 let rem_seg seg q =
-  {q with heap= List.remove_exn q.heap seg} |> check invariant
+  {q with heap= List.remove_one_exn ~eq:( == ) seg q.heap}
+  |> check invariant
 
 let filter_heap ~f q =
   {q with heap= List.filter q.heap ~f} |> check invariant
@@ -692,7 +692,7 @@ let rec propagate_context_ ancestor_vs ancestor_ctx q =
   exists xs
     (List.fold djns ~init:ancestor_stem ~f:(fun q' djn ->
          let dj_ctxs, djn =
-           List.rev_map_unzip djn ~f:(fun dj ->
+           List.rev_map_split djn ~f:(fun dj ->
                let dj = propagate_context_ ancestor_vs ancestor_ctx dj in
                (dj.ctx, dj) )
          in

sledge/src/solver.ml

@@ -653,7 +653,8 @@ let excise_dnf : Sh.t -> Var.Set.t -> Sh.t -> Sh.t option =
  fun minuend xs subtrahend ->
   let dnf_minuend = Sh.dnf minuend in
   let dnf_subtrahend = Sh.dnf subtrahend in
-  List.fold_option dnf_minuend
+  Iter.fold_opt
+    (Iter.of_list dnf_minuend)
     ~init:(Sh.false_ (Var.Set.union minuend.us xs))
     ~f:(fun remainders minuend ->
       [%trace]