[sledge] Rename `*_preserves_phys_equal` to `*_endo` and clarify docs

Summary:
Rename and clarify documentation to indicate that the stronger
specification wrt physical equality is due to requiring the mapped
function to be an endofunction.

Reviewed By: jvillard

Differential Revision: D20863524

fbshipit-source-id: 74dabeb5c

sledge/lib/import/iArray.ml

@@ -51,7 +51,7 @@ let fold_map_until xs ~init ~f ~finish =
              | Continue x -> x
              | Stop x -> return x )) )
 
-let map_preserving_phys_equal xs ~f =
+let map_endo xs ~f =
   let change = ref false in
   let xs' =
     map xs ~f:(fun x ->

sledge/lib/import/iArray.mli

@@ -49,8 +49,8 @@ val fold_map_until :
   -> finish:('accum * 'b t -> 'final)
   -> 'final
 
-val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t
+val map_endo : 'a t -> f:('a -> 'a) -> 'a t
-(** Like map, but preserves [phys_equal] if [f] preserves [phys_equal] of
+(** Like map, but specialized to require [f] to be an endofunction, which
-    every element. *)
+    enables preserving [==] if [f] preserves [==] of every element. *)
 
 val combine_adjacent : f:('a -> 'a -> 'a option) -> 'a t -> 'a t

sledge/lib/import/list.ml

@@ -39,7 +39,7 @@ let fold_option xs ~init ~f =
     (fold xs ~init ~f:(fun acc elt ->
          match f acc elt with Some res -> res | None -> return None ))
 
-let map_preserving_phys_equal map t ~f =
+let map_endo map t ~f =
   let change = ref false in
   let t' =
     map t ~f:(fun x ->
@@ -49,7 +49,7 @@ let map_preserving_phys_equal map t ~f =
   in
   if !change then t' else t
 
-let filter_map_preserving_phys_equal filter_map t ~f =
+let filter_map_endo filter_map t ~f =
   let change = ref false in
   let t' =
     filter_map t ~f:(fun x ->
@@ -61,10 +61,8 @@ let filter_map_preserving_phys_equal filter_map t ~f =
   in
   if !change then t' else t
 
-let filter_map_preserving_phys_equal t ~f =
+let filter_map_endo t ~f = filter_map_endo filter_map t ~f
-  filter_map_preserving_phys_equal filter_map t ~f
+let map_endo t ~f = map_endo map t ~f
-
-let map_preserving_phys_equal t ~f = map_preserving_phys_equal map t ~f
 
 let rev_map_unzip xs ~f =
   fold xs ~init:([], []) ~f:(fun (ys, zs) x ->

sledge/lib/import/list.mli

@@ -33,13 +33,13 @@ val fold_option :
     runs in the [Option] monad. If [f] returns [None], that value is
     returned without any additional invocations of [f]. *)
 
-val map_preserving_phys_equal : 'a t -> f:('a -> 'a) -> 'a t
+val map_endo : 'a t -> f:('a -> 'a) -> 'a t
-(** Like map, but preserves [phys_equal] if [f] preserves [phys_equal] of
+(** Like map, but specialized to require [f] to be an endofunction, which
-    every element. *)
+    enables preserving [==] if [f] preserves [==] of every element. *)
 
-val filter_map_preserving_phys_equal : 'a t -> f:('a -> 'a option) -> 'a t
+val filter_map_endo : 'a t -> f:('a -> 'a option) -> 'a t
-(** Like filter_map, but preserves [phys_equal] if [f] preserves
+(** Like filter_map, but specialized to require [f] to be an endofunction,
-    [phys_equal] of every element. *)
+    which enables preserving [==] if [f] preserves [==] of every element. *)
 
 val rev_map_unzip : 'a t -> f:('a -> 'b * 'c) -> 'b list * 'c list
 (** [rev_map_unzip ~f xs] is [unzip (rev_map ~f xs)] but more efficient. *)

sledge/lib/sh.ml

@@ -56,17 +56,14 @@ let map ~f_sjn ~f_cong ~f_trm ({us; xs= _; cong; pure; heap; djns} as q) =
   try
     let cong = f_cong cong in
     let pure =
-      List.filter_map_preserving_phys_equal pure ~f:(fun e ->
+      List.filter_map_endo pure ~f:(fun e ->
           let e' = f_trm e in
           if Term.is_false e' then raise Unsat
           else if Term.is_true e' then None
           else Some e' )
     in
-    let heap = List.map_preserving_phys_equal heap ~f:(map_seg ~f:f_trm) in
+    let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in
-    let djns =
+    let djns = List.map_endo djns ~f:(List.map_endo ~f:f_sjn) in
-      List.map_preserving_phys_equal djns
-        ~f:(List.map_preserving_phys_equal ~f:f_sjn)
-    in
     if cong == q.cong && pure == q.pure && heap == q.heap && djns == q.djns
     then q
     else {q with cong; pure; heap; djns}
@@ -595,8 +592,7 @@ let is_false = function
 let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) =
   let heap = emp.heap in
   let djns =
-    List.map_preserving_phys_equal djns ~f:(fun djn ->
+    List.map_endo djns ~f:(fun djn -> List.map_endo djn ~f:pure_approx)
-        List.map_preserving_phys_equal djn ~f:pure_approx )
   in
   if heap == q.heap && djns == q.djns then q
   else {us; xs; cong; pure; heap; djns} |> check invariant

sledge/lib/term.ml

@@ -1048,7 +1048,7 @@ let map e ~f =
     if x' == x && y' == y && z' == z then e else norm3 op x' y' z'
   in
   let mapN op ~f xs =
-    let xs' = IArray.map_preserving_phys_equal ~f xs in
+    let xs' = IArray.map_endo ~f xs in
     if xs' == xs then e else normN op xs'
   in
   let map_qset mk ~f args =
@@ -1064,7 +1064,7 @@ let map e ~f =
   | ApN (op, xs) -> mapN op ~f xs
   | RecN (_, xs) ->
       assert (
-        xs == IArray.map_preserving_phys_equal ~f xs
+        xs == IArray.map_endo ~f xs
         || fail "Term.map does not support updating subterms of RecN." () ) ;
       e
   | Var _ | Label _ | Nondet _ | Float _ | Integer _ -> e