From 93abf301c928185ce9517f5e7f69bcf19c18030b Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 12 Jan 2021 04:28:21 -0800 Subject: [PATCH] [sledge] Fix type of List.filter Reviewed By: jvillard Differential Revision: D25756574 fbshipit-source-id: 233ebc78a --- sledge/nonstdlib/list.ml | 1 + sledge/nonstdlib/list.mli | 1 + sledge/src/fol/context.ml | 7 +++---- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/sledge/nonstdlib/list.ml b/sledge/nonstdlib/list.ml index 107c229cb..dfa484906 100644 --- a/sledge/nonstdlib/list.ml +++ b/sledge/nonstdlib/list.ml @@ -34,6 +34,7 @@ let remove_one ~eq x xs = try Some (remove_one_exn ~eq x xs) with Not_found -> None let remove ~eq x xs = remove ~eq ~key:x xs +let filter xs ~f = filter ~f xs let map xs ~f = map ~f xs let map_endo t ~f = map_endo map t ~f diff --git a/sledge/nonstdlib/list.mli b/sledge/nonstdlib/list.mli index 03a6f3a94..7372bf36b 100644 --- a/sledge/nonstdlib/list.mli +++ b/sledge/nonstdlib/list.mli @@ -43,6 +43,7 @@ val remove_one_exn : eq:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val remove_one : eq:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list option val remove : eq:('a -> 'a -> bool) -> 'a -> 'a list -> 'a list +val filter : 'a list -> f:('a -> bool) -> 'a list val map : 'a t -> f:('a -> 'b) -> 'b t val map_endo : 'a t -> f:('a -> 'a) -> 'a t diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml index f10b047bc..1a790c19e 100644 --- a/sledge/src/fol/context.ml +++ b/sledge/src/fol/context.ml @@ -1070,10 +1070,9 @@ let solve_concat_extracts_eq r x = | _ -> uses ) in let find_extracts_at_off off = - List.filter uses ~f:(fun use -> - match (use : Trm.t) with - | Extract {off= o} -> implies r (Fml.eq o off) - | _ -> false ) + List.filter uses ~f:(function + | Extract {off= o} -> implies r (Fml.eq o off) + | _ -> false ) in let rec find_extracts full_rev_extracts rev_prefix off = List.fold (find_extracts_at_off off) full_rev_extracts