[sledge] Factor primitive map function out of Sh.apply_subst

Reviewed By: ngorogiannis

Differential Revision: D19282638

fbshipit-source-id: 8bef3be4e

sledge/src/symbheap/sh.ml

@@ -25,8 +25,32 @@ and disjunction = starjunction list
 
 type t = starjunction [@@deriving compare, equal, sexp]
 
-let map_seg {loc; bas; len; siz; arr} ~f =
+(** Traversals *)
-  {loc= f loc; bas= f bas; len= f len; siz= f siz; arr= f arr}
+
+let map_seg ~f h =
+  let loc = f h.loc in
+  let bas = f h.bas in
+  let len = f h.len in
+  let siz = f h.siz in
+  let arr = f h.arr in
+  if
+    loc == h.loc && bas == h.bas && len == h.len && siz == h.siz
+    && arr == h.arr
+  then h
+  else {loc; bas; len; siz; arr}
+
+let map ~f_sjn ~f_cong ~f_trm ({us= _; xs= _; cong; pure; heap; djns} as q)
+    =
+  let cong = f_cong cong in
+  let pure = List.map_preserving_phys_equal pure ~f:f_trm in
+  let heap = List.map_preserving_phys_equal heap ~f:(map_seg ~f:f_trm) in
+  let djns =
+    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}
 
 let fold_terms_seg {loc; bas; len; siz; arr} ~init ~f =
   let f b s = f s b in
@@ -44,6 +68,8 @@ let fold_vars fold_vars {us= _; xs= _; cong; pure; heap; djns} ~init ~f =
   |> fun init ->
   List.fold ~init djns ~f:(fun init -> List.fold ~init ~f:fold_vars)
 
+(** Pretty-printing *)
+
 let var_strength q =
   let rec var_strength_ xs m q =
     let xs = Set.union xs q.xs in
@@ -256,33 +282,12 @@ let rec simplify {us; xs; cong; pure; heap; djns} =
 
 (** Quantification and Vocabulary *)
 
-let rename_seg sub ({loc; bas; len; siz; arr} as h) =
-  let loc = Term.rename sub loc in
-  let bas = Term.rename sub bas in
-  let len = Term.rename sub len in
-  let siz = Term.rename sub siz in
-  let arr = Term.rename sub arr in
-  ( if
-    loc == h.loc && bas == h.bas && len == h.len && siz == h.siz
-    && arr == h.arr
-  then h
-  else {loc; bas; len; siz; arr} )
-  |> check (fun h' ->
-         assert (Set.disjoint (fv_seg h') (Var.Subst.domain sub)) )
-
 (** primitive application of a substitution, ignores us and xs, may violate
     invariant *)
-let rec apply_subst sub ({us= _; xs= _; cong; pure; heap; djns} as q) =
+let rec apply_subst sub q =
-  let cong = Equality.rename cong sub in
+  map q ~f_sjn:(rename sub)
-  let pure = List.map_preserving_phys_equal pure ~f:(Term.rename sub) in
+    ~f_cong:(fun r -> Equality.rename r sub)
-  let heap = List.map_preserving_phys_equal heap ~f:(rename_seg sub) in
+    ~f_trm:(Term.rename sub)
-  let djns =
-    List.map_preserving_phys_equal djns ~f:(fun d ->
-        List.map_preserving_phys_equal d ~f:(fun q -> rename sub q) )
-  in
-  ( if cong == q.cong && pure == q.pure && heap == q.heap && djns == q.djns
-  then q
-  else {q with cong; pure; heap; djns} )
   |> check (fun q' -> assert (Set.disjoint (fv q') (Var.Subst.domain sub)))
 
 and rename sub q =

sledge/src/symbheap/sh_test.ml

@@ -7,7 +7,8 @@
 
 let%test_module _ =
   ( module struct
-    (* let () = Trace.init ~margin:68 ~config:all () *)
+    (* let () =
+     *   Trace.init ~margin:160 ~config:(Result.ok_exn (Trace.parse "+Sh")) () *)
 
     let () = Trace.init ~margin:68 ~config:Trace.none ()
     let pp = Format.printf "@\n%a@." Sh.pp