From 194127eb4bb9ba4ad18acaa835eb5d722dbfbc9c Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 27 Oct 2020 12:16:51 -0700
Subject: [PATCH] [sledge] Move additional Fol representation operations to Trm
 and Fml

Summary:
Operations over the core representation are more useful in the core
representation modules.

Reviewed By: ngorogiannis

Differential Revision: D24532340

fbshipit-source-id: f1eab822d
---
 sledge/nonstdlib/NS.ml  |  22 ++++++
 sledge/nonstdlib/NS.mli |  10 +++
 sledge/src/fml.ml       |  57 ++++++++++++++
 sledge/src/fml.mli      |   4 +
 sledge/src/fol.ml       | 160 ++++++----------------------------------
 sledge/src/fol.mli      |   2 +-
 sledge/src/trm.ml       |  21 ++++++
 sledge/src/trm.mli      |   1 +
 8 files changed, 140 insertions(+), 137 deletions(-)

diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml
index 88c647667..1ffc2501e 100644
--- a/sledge/nonstdlib/NS.ml
+++ b/sledge/nonstdlib/NS.ml
@@ -8,6 +8,28 @@
 (** Global namespace intended to be opened in each source file *)
 
 include NS0
+
+(** Map-and-construct operations that preserve physical equality *)
+
+let map1 f e cons x =
+  let x' = f x in
+  if x == x' then e else cons x'
+
+let map2 f e cons x y =
+  let x' = f x in
+  let y' = f y in
+  if x == x' && y == y' then e else cons x' y'
+
+let map3 f e cons x y z =
+  let x' = f x in
+  let y' = f y in
+  let z' = f z in
+  if x == x' && y == y' && z == z' then e else cons x' y' z'
+
+let mapN f e cons xs =
+  let xs' = Array.map_endo ~f xs in
+  if xs' == xs then e else cons xs'
+
 module Array = Array
 module Float = Float
 module HashSet = HashSet
diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli
index 3c3b8f95a..aec1d2473 100644
--- a/sledge/nonstdlib/NS.mli
+++ b/sledge/nonstdlib/NS.mli
@@ -80,6 +80,16 @@ val snd3 : _ * 'b * _ -> 'b
 val trd3 : _ * _ * 'c -> 'c
 (** Third projection from a triple. *)
 
+(** Map-and-construct operations that preserve physical equality *)
+
+val map1 : ('a -> 'a) -> 'b -> ('a -> 'b) -> 'a -> 'b
+val map2 : ('a -> 'a) -> 'b -> ('a -> 'a -> 'b) -> 'a -> 'a -> 'b
+
+val map3 :
+  ('a -> 'a) -> 'b -> ('a -> 'a -> 'a -> 'b) -> 'a -> 'a -> 'a -> 'b
+
+val mapN : ('a -> 'a) -> 'b -> ('a array -> 'b) -> 'a array -> 'b
+
 (** Pretty-printing *)
 
 (** Pretty-printer for argument type. *)
diff --git a/sledge/src/fml.ml b/sledge/src/fml.ml
index 0b85b566a..658c741b1 100644
--- a/sledge/src/fml.ml
+++ b/sledge/src/fml.ml
@@ -14,6 +14,46 @@ type set = Set.t
 
 include Prop.Fml
 
+let pp_boxed fs fmt =
+  Format.pp_open_box fs 2 ;
+  Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
+
+let ppx strength fs fml =
+  let pp_t = Trm.ppx strength in
+  let rec pp fs fml =
+    let pf fmt = pp_boxed fs fmt in
+    let pp_arith op x =
+      let a, c = Trm.Arith.split_const (Trm.Arith.trm x) in
+      pf "(%a@ @<2>%s %a)" Q.pp (Q.neg c) op (Trm.Arith.ppx strength) a
+    in
+    let pp_join sep pos neg =
+      pf "(%a%t%a)" (Set.pp ~sep pp) pos
+        (fun ppf ->
+          if (not (Set.is_empty pos)) && not (Set.is_empty neg) then
+            Format.fprintf ppf sep )
+        (Set.pp ~sep (fun fs fml -> pp fs (_Not fml)))
+        neg
+    in
+    match fml with
+    | Tt -> pf "tt"
+    | Not Tt -> pf "ff"
+    | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y
+    | Not (Eq (x, y)) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y
+    | Eq0 x -> pp_arith "=" x
+    | Not (Eq0 x) -> pp_arith "≠" x
+    | Pos x -> pp_arith "<" x
+    | Not (Pos x) -> pp_arith "≥" x
+    | Not x -> pf "@<1>¬%a" pp x
+    | And {pos; neg} -> pp_join "@ @<2>∧ " pos neg
+    | Or {pos; neg} -> pp_join "@ @<2>∨ " pos neg
+    | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y
+    | Cond {cnd; pos; neg} ->
+        pf "@[<hv 1>(%a@ ? %a@ : %a)@]" pp cnd pp pos pp neg
+    | Lit (p, xs) -> pf "%a(%a)" Ses.Predsym.pp p (Array.pp ",@ " pp_t) xs
+  in
+  pp fs fml
+
+let pp = ppx (fun _ -> None)
 let tt = mk_Tt ()
 let ff = _Not tt
 let bool b = if b then tt else ff
@@ -79,4 +119,21 @@ let _Eq x y =
         _Eq (Trm._Sized x (Trm.seq_size_exn a)) a
     | _ -> sort_eq x y
 
+let map_pos_neg f e cons ~pos ~neg =
+  map2 (Set.map ~f) e (fun pos neg -> cons ~pos ~neg) pos neg
+
+let rec map_trms b ~f =
+  match b with
+  | Tt -> b
+  | Eq (x, y) -> map2 f b _Eq x y
+  | Eq0 x -> map1 f b _Eq0 x
+  | Pos x -> map1 f b _Pos x
+  | Not x -> map1 (map_trms ~f) b _Not x
+  | And {pos; neg} -> map_pos_neg (map_trms ~f) b _And ~pos ~neg
+  | Or {pos; neg} -> map_pos_neg (map_trms ~f) b _Or ~pos ~neg
+  | Iff (x, y) -> map2 (map_trms ~f) b _Iff x y
+  | Cond {cnd; pos; neg} -> map3 (map_trms ~f) b _Cond cnd pos neg
+  | Lit (p, xs) -> mapN f b (_Lit p) xs
+
+let map_vars b ~f = map_trms ~f:(Trm.map_vars ~f) b
 let vars p = Iter.flat_map ~f:Trm.vars (trms p)
diff --git a/sledge/src/fml.mli b/sledge/src/fml.mli
index 8200ad58b..275f7298e 100644
--- a/sledge/src/fml.mli
+++ b/sledge/src/fml.mli
@@ -11,10 +11,14 @@ open Propositional_intf
 include FORMULA with type trm := Trm.t
 module Set : FORMULA_SET with type elt := t with type t = set
 
+val ppx : Var.t Var.strength -> t pp
+val pp : t pp
 val tt : t
 val ff : t
 val bool : bool -> t
 val _Eq0 : Trm.t -> t
 val _Pos : Trm.t -> t
 val _Eq : Trm.t -> Trm.t -> t
+val map_vars : t -> f:(Var.t -> Var.t) -> t
+val map_trms : t -> f:(Trm.t -> Trm.t) -> t
 val vars : t -> Var.t iter
diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 1b636cfe0..134db085c 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -12,9 +12,8 @@ type var = Var.t
 type trm = Trm.t [@@deriving compare, equal, sexp]
 type fml = Fml.t [@@deriving compare, equal, sexp]
 
-(*
- * Conditional terms
- *)
+let map_pos_neg f e cons ~pos ~neg =
+  map2 (Set.map ~f) e (fun pos neg -> cons ~pos ~neg) pos neg
 
 (** Conditional terms, denoting functions from structures to values, taking
     the form of trees with internal nodes labeled with formulas and leaves
@@ -22,64 +21,17 @@ type fml = Fml.t [@@deriving compare, equal, sexp]
 type cnd = [`Ite of fml * cnd * cnd | `Trm of trm]
 [@@deriving compare, equal, sexp]
 
-(*
- * Expressions
- *)
-
 (** Expressions, which are partitioned into terms, conditional terms, and
     formulas. *)
 type exp = [cnd | `Fml of fml] [@@deriving compare, equal, sexp]
 
-(*
- * Representation operations
- *)
-
-(** pp *)
-
 let pp_boxed fs fmt =
   Format.pp_open_box fs 2 ;
   Format.kfprintf (fun fs -> Format.pp_close_box fs ()) fs fmt
 
-let ppx_f strength fs fml =
+let ppx_cnd strength fs ct =
   let pp_t = Trm.ppx strength in
-  let rec pp fs fml =
-    let pf fmt = pp_boxed fs fmt in
-    let pp_arith op x =
-      let a, c = Arith.split_const (Arith.trm x) in
-      pf "(%a@ @<2>%s %a)" Q.pp (Q.neg c) op (Arith.ppx strength) a
-    in
-    let pp_join sep pos neg =
-      pf "(%a%t%a)" (Fml.Set.pp ~sep pp) pos
-        (fun ppf ->
-          if (not (Fml.Set.is_empty pos)) && not (Fml.Set.is_empty neg) then
-            Format.fprintf ppf sep )
-        (Fml.Set.pp ~sep (fun fs fml -> pp fs (_Not fml)))
-        neg
-    in
-    match (fml : fml) with
-    | Tt -> pf "tt"
-    | Not Tt -> pf "ff"
-    | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y
-    | Not (Eq (x, y)) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y
-    | Eq0 x -> pp_arith "=" x
-    | Not (Eq0 x) -> pp_arith "≠" x
-    | Pos x -> pp_arith "<" x
-    | Not (Pos x) -> pp_arith "≥" x
-    | Not x -> pf "@<1>¬%a" pp x
-    | And {pos; neg} -> pp_join "@ @<2>∧ " pos neg
-    | Or {pos; neg} -> pp_join "@ @<2>∨ " pos neg
-    | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y
-    | Cond {cnd; pos; neg} ->
-        pf "@[<hv 1>(%a@ ? %a@ : %a)@]" pp cnd pp pos pp neg
-    | Lit (p, xs) -> pf "%a(%a)" Ses.Predsym.pp p (Array.pp ",@ " pp_t) xs
-  in
-  pp fs fml
-
-let pp_f = ppx_f (fun _ -> None)
-
-let ppx_c strength fs ct =
-  let pp_t = Trm.ppx strength in
-  let pp_f = ppx_f strength in
+  let pp_f = Fml.ppx strength in
   let rec pp fs ct =
     let pf fmt = pp_boxed fs fmt in
     match ct with
@@ -89,89 +41,11 @@ let ppx_c strength fs ct =
   pp fs ct
 
 let ppx strength fs = function
-  | #cnd as c -> ppx_c strength fs c
-  | `Fml f -> ppx_f strength fs f
+  | #cnd as c -> ppx_cnd strength fs c
+  | `Fml f -> Fml.ppx strength fs f
 
 let pp = ppx (fun _ -> None)
 
-(** map *)
-
-let map1 f e cons x =
-  let x' = f x in
-  if x == x' then e else cons x'
-
-let map2 f e cons x y =
-  let x' = f x in
-  let y' = f y in
-  if x == x' && y == y' then e else cons x' y'
-
-let map3 f e cons x y z =
-  let x' = f x in
-  let y' = f y in
-  let z' = f z in
-  if x == x' && y == y' && z == z' then e else cons x' y' z'
-
-let mapN f e cons xs =
-  let xs' = Array.map_endo ~f xs in
-  if xs' == xs then e else cons xs'
-
-let map_pos_neg f e cons ~pos ~neg =
-  let pos' = Fml.Set.map ~f pos in
-  let neg' = Fml.Set.map ~f neg in
-  if pos' == pos && neg' == neg then e else cons ~pos:pos' ~neg:neg'
-
-(** map_trms *)
-
-let rec map_trms_f ~f b =
-  match b with
-  | Tt -> b
-  | Eq (x, y) -> map2 f b _Eq x y
-  | Eq0 x -> map1 f b _Eq0 x
-  | Pos x -> map1 f b _Pos x
-  | Not x -> map1 (map_trms_f ~f) b _Not x
-  | And {pos; neg} -> map_pos_neg (map_trms_f ~f) b _And ~pos ~neg
-  | Or {pos; neg} -> map_pos_neg (map_trms_f ~f) b _Or ~pos ~neg
-  | Iff (x, y) -> map2 (map_trms_f ~f) b _Iff x y
-  | Cond {cnd; pos; neg} -> map3 (map_trms_f ~f) b _Cond cnd pos neg
-  | Lit (p, xs) -> mapN f b (_Lit p) xs
-
-(** map_vars *)
-
-let rec map_vars_t ~f e =
-  match e with
-  | Var _ as v -> (f (Var.of_ v) : var :> trm)
-  | Z _ | Q _ -> e
-  | Arith a ->
-      let a' = Arith.map ~f:(map_vars_t ~f) a in
-      if a == a' then e else _Arith a'
-  | Splat x -> map1 (map_vars_t ~f) e _Splat x
-  | Sized {seq; siz} -> map2 (map_vars_t ~f) e _Sized seq siz
-  | Extract {seq; off; len} -> map3 (map_vars_t ~f) e _Extract seq off len
-  | Concat xs -> mapN (map_vars_t ~f) e _Concat xs
-  | Select {idx; rcd} -> map1 (map_vars_t ~f) e (_Select idx) rcd
-  | Update {idx; rcd; elt} -> map2 (map_vars_t ~f) e (_Update idx) rcd elt
-  | Record xs -> mapN (map_vars_t ~f) e _Record xs
-  | Ancestor _ -> e
-  | Apply (g, xs) -> mapN (map_vars_t ~f) e (_Apply g) xs
-
-let map_vars_f ~f = map_trms_f ~f:(map_vars_t ~f)
-
-let rec map_vars_c ~f c =
-  match c with
-  | `Ite (cnd, thn, els) ->
-      let cnd' = map_vars_f ~f cnd in
-      let thn' = map_vars_c ~f thn in
-      let els' = map_vars_c ~f els in
-      if cnd' == cnd && thn' == thn && els' == els then c
-      else `Ite (cnd', thn', els')
-  | `Trm t ->
-      let t' = map_vars_t ~f t in
-      if t' == t then c else `Trm t'
-
-let map_vars ~f = function
-  | `Fml p -> `Fml (map_vars_f ~f p)
-  | #cnd as c -> (map_vars_c ~f c :> exp)
-
 (*
  * Core construction functions
  *
@@ -413,7 +287,21 @@ module Term = struct
 
   (** Transform *)
 
-  let map_vars = map_vars
+  let rec map_vars_c ~f c =
+    match c with
+    | `Ite (cnd, thn, els) ->
+        let cnd' = Fml.map_vars ~f cnd in
+        let thn' = map_vars_c ~f thn in
+        let els' = map_vars_c ~f els in
+        if cnd' == cnd && thn' == thn && els' == els then c
+        else `Ite (cnd', thn', els')
+    | `Trm t ->
+        let t' = Trm.map_vars ~f t in
+        if t' == t then c else `Trm t'
+
+  let map_vars ~f = function
+    | `Fml p -> `Fml (Fml.map_vars ~f p)
+    | #cnd as c -> (map_vars_c ~f c :> exp)
 
   let fold_map_vars e s0 ~f =
     let s = ref s0 in
@@ -441,8 +329,8 @@ module Formula = struct
 
   let inject f = `Fml f
   let project = function `Fml f -> Some f | #cnd as c -> project_out_fml c
-  let ppx = ppx_f
-  let pp = pp_f
+  let ppx = Fml.ppx
+  let pp = Fml.pp
 
   (* constants *)
 
@@ -492,7 +380,7 @@ module Formula = struct
 
   (** Transform *)
 
-  let map_vars = map_vars_f
+  let map_vars = Fml.map_vars
 
   let rec map_terms ~f b =
     let lift_map1 : (exp -> exp) -> t -> (trm -> t) -> trm -> t =
diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli
index 3ac8dee92..2299c0c99 100644
--- a/sledge/src/fol.mli
+++ b/sledge/src/fol.mli
@@ -134,7 +134,7 @@ and Formula : sig
   (** Transform *)
 
   val map_terms : f:(Term.t -> Term.t) -> t -> t
-  val map_vars : f:(Var.t -> Var.t) -> t -> t
+  val map_vars : t -> f:(Var.t -> Var.t) -> t
   val fold_map_vars : t -> 's -> f:(Var.t -> 's -> Var.t * 's) -> t * 's
   val rename : Var.Subst.t -> t -> t
 end
diff --git a/sledge/src/trm.ml b/sledge/src/trm.ml
index 99accecb5..836457e2a 100644
--- a/sledge/src/trm.ml
+++ b/sledge/src/trm.ml
@@ -370,6 +370,27 @@ include Trm
 let zero = _Z Z.zero
 let one = _Z Z.one
 
+(** Transform *)
+
+let rec map_vars e ~f =
+  match e with
+  | Var _ as v -> (f (Var.of_ v) : Var.t :> t)
+  | Z _ | Q _ -> e
+  | Arith a ->
+      let a' = Arith.map ~f:(map_vars ~f) a in
+      if a == a' then e else _Arith a'
+  | Splat x -> map1 (map_vars ~f) e _Splat x
+  | Sized {seq; siz} -> map2 (map_vars ~f) e _Sized seq siz
+  | Extract {seq; off; len} -> map3 (map_vars ~f) e _Extract seq off len
+  | Concat xs -> mapN (map_vars ~f) e _Concat xs
+  | Select {idx; rcd} -> map1 (map_vars ~f) e (_Select idx) rcd
+  | Update {idx; rcd; elt} -> map2 (map_vars ~f) e (_Update idx) rcd elt
+  | Record xs -> mapN (map_vars ~f) e _Record xs
+  | Ancestor _ -> e
+  | Apply (g, xs) -> mapN (map_vars ~f) e (_Apply g) xs
+
+(** Traverse *)
+
 let rec iter_vars e ~f =
   match e with
   | Var _ as v -> f (Var.of_ v)
diff --git a/sledge/src/trm.mli b/sledge/src/trm.mli
index cdac07569..d6f29b74a 100644
--- a/sledge/src/trm.mli
+++ b/sledge/src/trm.mli
@@ -62,3 +62,4 @@ val seq_size : t -> t option
 val vars : t -> Var.t iter
 val zero : t
 val one : t
+val map_vars : t -> f:(Var.t -> Var.t) -> t