From 615f245027619dc3a1d7aac13e9bbb3ce391393e Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 20 Oct 2020 02:37:11 -0700
Subject: [PATCH] [sledge] Replace RecRecord uninterpreted function symbol with
 Ancestor term

Summary:
References from a record to one of its ancestor records are used to
represent cyclic or recursive record values. While the current
interpretation is weak, these logically are part of the record theory
and should be interpreted with the rest of the record terms.

Reviewed By: jvillard

Differential Revision: D24306091

fbshipit-source-id: 41553741d
---
 sledge/src/fol.ml         | 14 +++++++++-----
 sledge/src/ses/funsym.ml  |  2 --
 sledge/src/ses/funsym.mli |  1 -
 3 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml
index 55232e6a6..037f156ce 100644
--- a/sledge/src/fol.ml
+++ b/sledge/src/fol.ml
@@ -33,6 +33,7 @@ type trm =
   | Select of {idx: int; rcd: trm}
   | Update of {idx: int; rcd: trm; elt: trm}
   | Record of trm array
+  | Ancestor of int
   | Tuple of trm array
   | Project of {ary: int; idx: int; tup: trm}
   | Apply of Funsym.t * trm
@@ -76,6 +77,7 @@ let _Concat es = Concat es
 let _Select idx rcd = Select {idx; rcd}
 let _Update idx rcd elt = Update {idx; rcd; elt}
 let _Record es = Record es
+let _Ancestor i = Ancestor i
 let _Tuple es = Tuple es
 let _Project ary idx tup = Project {ary; idx; tup}
 let _Apply f a = Apply (f, a)
@@ -455,6 +457,7 @@ let rec ppx_t strength fs trm =
     | Select {idx; rcd} -> pf "%a[%i]" pp rcd idx
     | Update {idx; rcd; elt} -> pf "[%a@ @[| %i → %a@]]" pp rcd idx pp elt
     | Record xs -> pf "{%a}" (ppx_record strength) xs
+    | Ancestor i -> pf "(ancestor %i)" i
     | Tuple xs -> pf "(%a)" (Array.pp ",@ " (ppx_t strength)) xs
     | Project {ary; idx; tup} -> pf "proj(%i,%i)(%a)" ary idx pp tup
     | Apply (f, Tuple [||]) -> pf "%a" Funsym.pp f
@@ -537,7 +540,7 @@ let pp = ppx (fun _ -> None)
 let rec fold_vars_t e ~init ~f =
   match e with
   | Var _ as v -> f init (Var.of_ v)
-  | Z _ | Q _ -> init
+  | Z _ | Q _ | Ancestor _ -> init
   | Neg x
    |Mulq (_, x)
    |Splat x
@@ -626,7 +629,7 @@ let rec map_trms_f ~f b =
 let rec map_vars_t ~f e =
   match e with
   | Var _ as v -> (f (Var.of_ v) : var :> trm)
-  | Z _ | Q _ -> e
+  | Z _ | Q _ | Ancestor _ -> e
   | Neg x -> map1 (map_vars_t ~f) e _Neg x
   | Add (x, y) -> map2 (map_vars_t ~f) e _Add x y
   | Sub (x, y) -> map2 (map_vars_t ~f) e _Sub x y
@@ -871,6 +874,7 @@ module Term = struct
   let select ~rcd ~idx = ap1t (_Select idx) rcd
   let update ~rcd ~idx ~elt = ap2t (_Update idx) rcd elt
   let record elts = apNt (fun es -> _Record (Array.of_list es)) elts
+  let ancestor i = `Trm (_Ancestor i)
 
   (* tuples *)
 
@@ -1098,10 +1102,10 @@ let rec t_to_ses : trm -> Ses.Term.t = function
       Ses.Term.update ~rcd:(t_to_ses rcd) ~idx ~elt:(t_to_ses elt)
   | Record es ->
       Ses.Term.record (IArray.of_array (Array.map ~f:t_to_ses es))
+  | Ancestor i -> Ses.Term.rec_record i
   | Apply (Mul, Tuple [|x; y|]) -> Ses.Term.mul (t_to_ses x) (t_to_ses y)
   | Apply (Div, Tuple [|x; y|]) -> Ses.Term.div (t_to_ses x) (t_to_ses y)
   | Apply (Rem, Tuple [|x; y|]) -> Ses.Term.rem (t_to_ses x) (t_to_ses y)
-  | Apply (RecRecord i, Tuple [||]) -> Ses.Term.rec_record i
   | Apply (BitAnd, Tuple [|x; y|]) ->
       Ses.Term.and_ (t_to_ses x) (t_to_ses y)
   | Apply (BitOr, Tuple [|x; y|]) -> Ses.Term.or_ (t_to_ses x) (t_to_ses y)
@@ -1265,7 +1269,7 @@ and of_ses : Ses.Term.t -> exp =
       update ~rcd:(of_ses rcd) ~idx ~elt:(of_ses elt)
   | ApN (Record, elts) ->
       record (Array.map ~f:of_ses (IArray.to_array elts))
-  | RecRecord i -> uap0 (RecRecord i)
+  | RecRecord i -> ancestor i
   | Apply (sym, args) ->
       apply sym (Array.map ~f:of_ses (IArray.to_array args))
 
@@ -1641,7 +1645,7 @@ module Term_of_Llair = struct
         update ~rcd:(exp rcd) ~idx ~elt:(exp elt)
     | ApN (Record, _, elts) ->
         record (Array.map ~f:exp (IArray.to_array elts))
-    | RecRecord (i, _) -> uap0 (RecRecord i)
+    | RecRecord (i, _) -> ancestor i
     | Ap1 (Splat, _, byt) -> splat (exp byt)
 end
 
diff --git a/sledge/src/ses/funsym.ml b/sledge/src/ses/funsym.ml
index 365530544..c11c07ee4 100644
--- a/sledge/src/ses/funsym.ml
+++ b/sledge/src/ses/funsym.ml
@@ -11,7 +11,6 @@ type t =
   | Mul
   | Div
   | Rem
-  | RecRecord of int
   | BitAnd
   | BitOr
   | BitXor
@@ -29,7 +28,6 @@ let pp ppf f =
   | Mul -> pf "@<1>×"
   | Div -> pf "/"
   | Rem -> pf "%%"
-  | RecRecord i -> pf "(rec_record %i)" i
   | BitAnd -> pf "&&"
   | BitOr -> pf "||"
   | BitXor -> pf "xor"
diff --git a/sledge/src/ses/funsym.mli b/sledge/src/ses/funsym.mli
index 9f8d68b89..01d090076 100644
--- a/sledge/src/ses/funsym.mli
+++ b/sledge/src/ses/funsym.mli
@@ -17,7 +17,6 @@ type t =
   | Rem
       (** Remainder of division, satisfies [a = b * div a b + rem a b] and
           for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
-  | RecRecord of int
   | BitAnd  (** Bitwise logical And *)
   | BitOr  (** Bitwise logical inclusive Or *)
   | BitXor  (** Bitwise logical eXclusive or *)