From 5574c5e07851467c0f0d7330244f86eb2b0f69d0 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sun, 25 Oct 2020 16:00:30 -0700 Subject: [PATCH] [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 | 1 - sledge/nonstdlib/NS0.ml | 1 - sledge/nonstdlib/iter.ml | 1 + sledge/nonstdlib/iter.mli | 1 + sledge/nonstdlib/map.ml | 1 + sledge/nonstdlib/map_intf.ml | 1 + sledge/src/ses/equality.ml | 22 +++++++++++----------- sledge/src/ses/term.ml | 4 +--- 8 files changed, 16 insertions(+), 16 deletions(-) diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index a263d9b92..4228701ab 100644 --- a/sledge/nonstdlib/NS.mli +++ b/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 diff --git a/sledge/nonstdlib/NS0.ml b/sledge/nonstdlib/NS0.ml index 2bda0e32f..3060325df 100644 --- a/sledge/nonstdlib/NS0.ml +++ b/sledge/nonstdlib/NS0.ml @@ -231,4 +231,3 @@ let violates f x = (** Deprecated *) module Hashtbl = struct end -module With_return = Base.With_return diff --git a/sledge/nonstdlib/iter.ml b/sledge/nonstdlib/iter.ml index fdc9ffa84..e3293fd8b 100644 --- a/sledge/nonstdlib/iter.ml +++ b/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) diff --git a/sledge/nonstdlib/iter.mli b/sledge/nonstdlib/iter.mli index 143d5a893..8f74134a2 100644 --- a/sledge/nonstdlib/iter.mli +++ b/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 diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml index c85ba7963..45d0b1437 100644 --- a/sledge/nonstdlib/map.ml +++ b/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 diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml index 67606fdaf..e9ec394cb 100644 --- a/sledge/nonstdlib/map_intf.ml +++ b/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 diff --git a/sledge/src/ses/equality.ml b/sledge/src/ses/equality.ml index 97492dbd7..12dd90fe9 100644 --- a/sledge/src/ses/equality.ml +++ b/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 diff --git a/sledge/src/ses/term.ml b/sledge/src/ses/term.ml index aa619ac76..7f0b21e0e 100644 --- a/sledge/src/ses/term.ml +++ b/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