From 3e7aeed230dc92c76d5bb5792de7c8d30f830db4 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Fri, 4 Sep 2020 13:37:39 -0700 Subject: [PATCH] [sledge] Improve: Sh.fold_dnf to use iter vs list Reviewed By: ngorogiannis Differential Revision: D23459526 fbshipit-source-id: 6cd172e56 --- sledge/nonstdlib/iter.ml | 3 +++ sledge/nonstdlib/iter.mli | 2 ++ sledge/src/sh.ml | 10 +++++----- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/sledge/nonstdlib/iter.ml b/sledge/nonstdlib/iter.ml index 6462aefe4..351631fcc 100644 --- a/sledge/nonstdlib/iter.ml +++ b/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 diff --git a/sledge/nonstdlib/iter.mli b/sledge/nonstdlib/iter.mli index 661d049f9..8b9342150 100644 --- a/sledge/nonstdlib/iter.mli +++ b/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 diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 1f7006b36..c03670370 100644 --- a/sledge/src/sh.ml +++ b/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]