[sledge] Replace uses of Base.With_return with Iterators

Summary:
Expressing the sort of short-circuit evaluation in the changed code is
conceptually more direct using iterators.

Also, when using With_return, getting usable backtraces relies on the
compiler recognizing that the `raise` in the implementation of
`Base.Exn.raise_without_backtrace` should be a `reraise`. Using
iterators avoids this potential fragility.

Reviewed By: jvillard

Differential Revision: D24306094

fbshipit-source-id: b1abe04fb

sledge/nonstdlib/NS.mli

@@ -214,4 +214,3 @@ val violates : ('a -> unit) -> 'a -> _
 (**)
 
 module Hashtbl : sig end [@@deprecated "Use HashTable instead of Hashtbl"]
-module With_return = Base.With_return

sledge/nonstdlib/NS0.ml

@@ -231,4 +231,3 @@ let violates f x =
 (** Deprecated *)
 
 module Hashtbl = struct end
-module With_return = Base.With_return

sledge/nonstdlib/iter.ml

@@ -14,6 +14,7 @@ end
 let pop seq =
   match head seq with Some x -> Some (x, drop 1 seq) | None -> None
 
+let find_map seq ~f = find_map ~f seq
 let find seq ~f = find (CCOpt.if_ f) seq
 let find_exn seq ~f = CCOpt.get_exn (find ~f seq)
 

sledge/nonstdlib/iter.mli

@@ -14,6 +14,7 @@ end
 val pop : 'a iter -> ('a * 'a iter) option
 val find : 'a t -> f:('a -> bool) -> 'a option
 val find_exn : 'a t -> f:('a -> bool) -> 'a
+val find_map : 'a iter -> f:('a -> 'b option) -> 'b 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

sledge/nonstdlib/map.ml

@@ -159,6 +159,7 @@ end) : S with type key = Key.t = struct
   let fold m ~init ~f = M.fold (fun key data acc -> f ~key ~data acc) m init
   let to_alist ?key_order:_ = M.to_list
   let data m = Iter.to_list (M.values m)
+  let to_iter = M.to_iter
 
   let to_iter2 l r =
     let seq = ref Iter.empty in

sledge/nonstdlib/map_intf.ml

@@ -116,6 +116,7 @@ module type S = sig
     ?key_order:[`Increasing | `Decreasing] -> 'a t -> (key * 'a) list
 
   val data : 'a t -> 'a list
+  val to_iter : 'a t -> (key * 'a) iter
 
   val to_iter2 :
        'a t

sledge/src/ses/equality.ml

@@ -51,6 +51,7 @@ module Subst : sig
   val extend : Term.t -> t -> t option
   val remove : Var.Set.t -> t -> t
   val map_entries : f:(Term.t -> Term.t) -> t -> t
+  val to_iter : t -> (Term.t * Term.t) iter
   val to_alist : t -> (Term.t * Term.t) list
   val partition_valid : Var.Set.t -> t -> t * Var.Set.t * t
 end = struct
@@ -70,6 +71,7 @@ end = struct
   let fold = Term.Map.fold
   let iteri = Term.Map.iteri
   let for_alli = Term.Map.for_alli
+  let to_iter = Term.Map.to_iter
   let to_alist = Term.Map.to_alist ~key_order:`Increasing
 
   (** look up a term in a substitution *)
@@ -453,10 +455,9 @@ let false_ = {true_ with sat= false}
 let lookup r a =
   ([%Trace.call fun {pf} -> pf "%a" Term.pp a]
   ;
-  let@ {return} = With_return.with_return in
-  Subst.iteri r.rep ~f:(fun ~key:b ~data:b' ->
-      if semi_congruent r a b then return b' ) ;
-  a)
+  Iter.find_map (Subst.to_iter r.rep) ~f:(fun (b, b') ->
+      Option.return_if (semi_congruent r a b) b' )
+  |> Option.value ~default:a)
   |>
   [%Trace.retn fun {pf} -> pf "%a" Term.pp]
 
@@ -508,20 +509,19 @@ let merge us a b r =
 
 (** find an unproved equation between congruent terms *)
 let find_missing r =
-  let@ {return} = With_return.with_return in
-  Subst.iteri r.rep ~f:(fun ~key:a ~data:a' ->
+  Iter.find_map (Subst.to_iter r.rep) ~f:(fun (a, a') ->
       let a_subnorm = Term.map ~f:(Subst.norm r.rep) a in
-      Subst.iteri r.rep ~f:(fun ~key:b ~data:b' ->
-          if
+      Iter.find_map (Subst.to_iter r.rep) ~f:(fun (b, b') ->
+          (* need to equate a' and b'? *)
+          let need_a'_eq_b' =
             (* optimize: do not consider both a = b and b = a *)
             Term.compare a b < 0
             (* a and b are not already equal *)
             && (not (Term.equal a' b'))
             (* a and b are congruent *)
             && semi_congruent r a_subnorm b
-          then (* need to equate a' and b' *)
-            return (Some (a', b')) ) ) ;
-  None
+          in
+          Option.return_if need_a'_eq_b' (a', b') ) )
 
 let rec close us r =
   if not r.sat then r

sledge/src/ses/term.ml

@@ -1145,9 +1145,7 @@ let iter_vars e ~f =
   iter_terms ~f:(fun e -> Option.iter ~f (Var.of_term e)) e
 
 let exists_vars e ~f =
-  With_return.with_return (fun {return} ->
-      iter_vars e ~f:(fun v -> if f v then return true) ;
-      false )
+  Iter.exists ~f (Iter.from_labelled_iter (iter_vars e))
 
 let fold_vars e ~init ~f =
   fold_terms ~f:(fun s e -> Option.fold ~f ~init:s (Var.of_term e)) ~init e