[sledge] Fix type of List.filter

Reviewed By: jvillard

Differential Revision: D25756574

fbshipit-source-id: 233ebc78a

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
 

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

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 ->
+    List.filter uses ~f:(function
-        match (use : Trm.t) with
+      | Extract {off= o} -> implies r (Fml.eq o off)
-        | Extract {off= o} -> implies r (Fml.eq o off)
+      | _ -> false )
-        | _ -> false )
   in
   let rec find_extracts full_rev_extracts rev_prefix off =
     List.fold (find_extracts_at_off off) full_rev_extracts