[sledge] Improve: Sh.fold_dnf to use iter vs list

Reviewed By: ngorogiannis

Differential Revision: D23459526

fbshipit-source-id: 6cd172e56

sledge/nonstdlib/iter.ml

@@ -10,3 +10,6 @@ include IterLabels
 module Import = struct
   type 'a iter = 'a t
 end
+
+let pop seq =
+  match head seq with Some x -> Some (x, drop 1 seq) | None -> None

sledge/nonstdlib/iter.mli

@@ -10,3 +10,5 @@ include module type of IterLabels
 module Import : sig
   type 'a iter = 'a t
 end
+
+val pop : 'a iter -> ('a * 'a iter) option

sledge/src/sh.ml

@@ -605,17 +605,17 @@ let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts =
     let djns = sjn.djns in
     let sjn = {sjn with djns= []} in
     split_case
-      (List.rev_append djns pending_splits)
+      (Iter.append (Iter.of_list djns) pending_splits)
       (xs, conj sjn conjuncts)
       disjuncts
   and split_case pending_splits (xs, conjuncts) disjuncts =
-    match pending_splits with
-    | split :: pending_splits ->
+    match Iter.pop pending_splits with
+    | Some (split, pending_splits) ->
         List.fold split ~init:disjuncts ~f:(fun disjuncts sjn ->
             add_disjunct pending_splits sjn (xs, conjuncts) disjuncts )
-    | [] -> disj (xs, conjuncts) disjuncts
+    | None -> disj (xs, conjuncts) disjuncts
   in
-  add_disjunct [] sjn (xs, conjuncts) disjuncts
+  add_disjunct Iter.empty sjn (xs, conjuncts) disjuncts
 
 let dnf q =
   [%Trace.call fun {pf} -> pf "%a" pp q]