[sledge] Refactor: Move eq_concat out of Term

Summary:
`Term.eq_concat` is not primitive and complicates the `Term`
interface. Move it to a couple clients as a convenience wrapper.

Reviewed By: jvillard

Differential Revision: D21721026

fbshipit-source-id: 0d74aa251

sledge/src/exec.ml

@@ -33,6 +33,11 @@ let fresh_seg ~loc ?bas ?len ?siz ?arr ?(xs = Var.Set.empty) us =
 
 let null_eq ptr = Sh.pure (Term.eq Term.zero ptr)
 
+let eq_concat (siz, arr) ms =
+  Term.(
+    eq (memory ~siz ~arr)
+      (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)))
+
 (* Overwritten variables renaming and remaining modified variables. [ws] are
    the written variables; [rs] are the variables read or in the
    precondition; [us] are the variables to which ghosts must be chosen
@@ -167,7 +172,7 @@ let memmov_foot us dst src len =
   let siz_dst_mid_src, us, xs = fresh_var "m" us xs in
   let arr_dst_mid_src, us, xs = fresh_var "a" us xs in
   let eq_mem_dst_mid_src =
-    Term.eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src
+    eq_concat (siz_dst_mid_src, arr_dst_mid_src) mem_dst_mid_src
   in
   let seg =
     Sh.seg
@@ -192,7 +197,7 @@ let memmov_dn_spec us dst src len =
   let siz_mid_src_src, us, xs = fresh_var "m" us xs in
   let arr_mid_src_src, _, xs = fresh_var "a" us xs in
   let eq_mem_mid_src_src =
-    Term.eq_concat (siz_mid_src_src, arr_mid_src_src) mem_mid_src_src
+    eq_concat (siz_mid_src_src, arr_mid_src_src) mem_mid_src_src
   in
   let post =
     Sh.and_ eq_mem_mid_src_src
@@ -217,7 +222,7 @@ let memmov_up_spec us dst src len =
   let siz_src_src_mid, us, xs = fresh_var "m" us xs in
   let arr_src_src_mid, _, xs = fresh_var "a" us xs in
   let eq_mem_src_src_mid =
-    Term.eq_concat (siz_src_src_mid, arr_src_src_mid) mem_src_src_mid
+    eq_concat (siz_src_src_mid, arr_src_src_mid) mem_src_src_mid
   in
   let post =
     Sh.and_ eq_mem_src_src_mid

sledge/src/sh_test.ml

@@ -41,6 +41,11 @@ let%test_module _ =
     let x = Term.var x_
     let y = Term.var y_
 
+    let eq_concat (siz, arr) ms =
+      Term.(
+        eq (memory ~siz ~arr)
+          (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)))
+
     let of_eqs l =
       List.fold ~init:emp ~f:(fun q (a, b) -> and_ (Term.eq a b) q) l
 
@@ -147,12 +152,12 @@ let%test_module _ =
         exists
           ~$[a_; c_; d_; e_]
           (star
-             (pure (Term.eq_concat (!16, e) [|(!8, a); (!8, d)|]))
+             (pure (eq_concat (!16, e) [|(!8, a); (!8, d)|]))
              (or_
                 (pure (Term.dq x !0))
                 (exists
                    (Var.Set.of_list [b_])
-                   (pure (Term.eq_concat (!8, a) [|(!4, c); (!4, b)|])))))
+                   (pure (eq_concat (!8, a) [|(!4, c); (!4, b)|])))))
       in
       pp_raw q ;
       let q' = simplify q in

sledge/src/solver.ml

@@ -132,6 +132,11 @@ end
 
 open Goal
 
+let eq_concat (siz, arr) ms =
+  Term.(
+    eq (memory ~siz ~arr)
+      (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms)))
+
 let fresh_var name vs zs ~wrt =
   let v, wrt = Var.fresh name ~wrt in
   let vs = Var.Set.add vs v in
@@ -244,7 +249,7 @@ let excise_seg_sub_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg o_n
   let com = Sh.star (Sh.seg {msg with siz= n; arr= a0}) com in
   let min =
     Sh.and_
-      (Term.eq_concat (o, a) [|(n, a0); (o_n, a1)|])
+      (eq_concat (o, a) [|(n, a0); (o_n, a1)|])
       (Sh.star
          (Sh.seg {loc= Term.add k n; bas= b; len= m; siz= o_n; arr= a1})
          (Sh.rem_seg msg min))
@@ -285,7 +290,7 @@ let excise_seg_min_prefix ({us; com; min; xs; sub; zs} as goal) msg ssg n_o
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq_concat (n, a') [|(o, a); (n_o, a1')|])
+            (eq_concat (n, a') [|(o, a); (n_o, a1')|])
             (Sh.star
                (Sh.seg
                   {loc= Term.add l o; bas= b'; len= m'; siz= n_o; arr= a1'})
@@ -322,7 +327,7 @@ let excise_seg_sub_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Term.eq_concat (o, a) [|(l_k, a0); (n, a1)|])
+      (eq_concat (o, a) [|(l_k, a0); (n, a1)|])
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.rem_seg msg min))
@@ -367,7 +372,7 @@ let excise_seg_sub_infix ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Term.eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|])
+      (eq_concat (o, a) [|(l_k, a0); (n, a1); (ko_ln, a2)|])
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.star
@@ -415,7 +420,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
   in
   let min =
     Sh.and_
-      (Term.eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|])
+      (eq_concat (o, a) [|(l_k, a0); (ko_l, a1)|])
       (Sh.star
          (Sh.seg {loc= k; bas= b; len= m; siz= l_k; arr= a0})
          (Sh.rem_seg msg min))
@@ -424,7 +429,7 @@ let excise_seg_min_skew ({us; com; min; xs; sub; zs} as goal) msg ssg l_k
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
+            (eq_concat (n, a') [|(ko_l, a1); (ln_ko, a2')|])
             (Sh.star
                (Sh.seg {loc= ko; bas= b'; len= m'; siz= ln_ko; arr= a2'})
                (Sh.rem_seg ssg sub))))
@@ -460,7 +465,7 @@ let excise_seg_min_suffix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq_concat (n, a') [|(k_l, a0'); (o, a)|])
+            (eq_concat (n, a') [|(k_l, a0'); (o, a)|])
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.rem_seg ssg sub))))
@@ -500,7 +505,7 @@ let excise_seg_min_infix ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
+            (eq_concat (n, a') [|(k_l, a0'); (o, a); (ln_ko, a2')|])
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.star
@@ -542,7 +547,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
   in
   let min =
     Sh.and_
-      (Term.eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|])
+      (eq_concat (o, a) [|(ln_k, a1); (ko_ln, a2)|])
       (Sh.star
          (Sh.seg {loc= ln; bas= b; len= m; siz= ko_ln; arr= a2})
          (Sh.rem_seg msg min))
@@ -551,7 +556,7 @@ let excise_seg_sub_skew ({us; com; min; xs; sub; zs} as goal) msg ssg k_l
     Sh.and_ (Term.eq b b')
       (Sh.and_ (Term.eq m m')
          (Sh.and_
-            (Term.eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
+            (eq_concat (n, a') [|(k_l, a0'); (ln_k, a1)|])
             (Sh.star
                (Sh.seg {loc= l; bas= b'; len= m'; siz= k_l; arr= a0'})
                (Sh.rem_seg ssg sub))))

sledge/src/term.ml

@@ -973,10 +973,6 @@ let select ~rcd ~idx = norm1 (Select idx) rcd
 let update ~rcd ~idx ~elt = norm2 (Update idx) rcd elt
 let rec_record i = simp_rec_record i |> check invariant
 
-let eq_concat (siz, arr) ms =
-  eq (memory ~siz ~arr)
-    (concat (Array.map ~f:(fun (siz, arr) -> memory ~siz ~arr) ms))
-
 let rec binary mk x y = mk (of_exp x) (of_exp y)
 
 and ubinary mk typ x y =

sledge/src/term.mli

@@ -226,7 +226,6 @@ val splat : t -> t
 val memory : siz:t -> arr:t -> t
 val extract : agg:t -> off:t -> len:t -> t
 val concat : t array -> t
-val eq_concat : t * t -> (t * t) array -> t
 
 (* records (struct / array values) *)
 val record : t iarray -> t