From 6fb29dac9089df7d53834b6306c00277f40f62d2 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sun, 21 Feb 2021 13:19:33 -0800
Subject: [PATCH] [sledge] Add Theory.oriented_equality type for code
 readability

Summary:
Theory.solved is a list of pairs of terms representing solved
equalities. The order of the pairs is very important, which is not
apparent from the type. This diff introduces an oriented_equality type
to make this more clear.

Reviewed By: jvillard

Differential Revision: D26451303

fbshipit-source-id: 56a49e601
---
 sledge/src/fol/context.ml | 6 +++---
 sledge/src/fol/theory.ml  | 8 +++++---
 sledge/src/fol/theory.mli | 4 +++-
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 25ac35b07..f68b4197a 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -583,7 +583,7 @@ let update_rep noninterp ~from:r ~to_:r' x =
   {x with rep; cls; use}
 
 (** add v ↦ t to x *)
-let propagate1 (v, t) x =
+let propagate1 {Theory.var= v; rep= t} x =
   [%trace]
     ~call:(fun {pf} ->
       pf "@ @[%a ↦ %a@]@ %a" Trm.pp v Trm.pp t pp_raw x ;
@@ -985,8 +985,8 @@ let rec solve_pending (s : Theory.t) soln =
       match Theory.solve a' b' {s with pending} with
       | {solved= Some solved} as s ->
           solve_pending {s with solved= Some []}
-            (List.fold solved soln ~f:(fun (trm, rep) soln ->
-                 Subst.compose1 ~key:trm ~data:rep soln ))
+            (List.fold solved soln ~f:(fun {var; rep} soln ->
+                 Subst.compose1 ~key:var ~data:rep soln ))
       | {solved= None} -> None )
   | [] -> Some soln
 
diff --git a/sledge/src/fol/theory.ml b/sledge/src/fol/theory.ml
index 454a837ba..4fe6e1eea 100644
--- a/sledge/src/fol/theory.ml
+++ b/sledge/src/fol/theory.ml
@@ -9,18 +9,20 @@
 
 (* Theory equation solver state ===========================================*)
 
+type oriented_equality = {var: Trm.t; rep: Trm.t}
+
 type t =
   { wrt: Var.Set.t
   ; no_fresh: bool
   ; fresh: Var.Set.t
-  ; solved: (Trm.t * Trm.t) list option
+  ; solved: oriented_equality list option
   ; pending: (Trm.t * Trm.t) list }
 
 let pp ppf = function
   | {solved= None} -> Format.fprintf ppf "unsat"
   | {solved= Some solved; fresh; pending} ->
       Format.fprintf ppf "%a%a : %a" Var.Set.pp_xs fresh
-        (List.pp ";@ " (fun ppf (var, rep) ->
+        (List.pp ";@ " (fun ppf {var; rep} ->
              Format.fprintf ppf "@[%a ↦ %a@]" Trm.pp var Trm.pp rep ))
         solved
         (List.pp ";@ " (fun ppf (a, b) ->
@@ -102,7 +104,7 @@ let orient e f =
 let add_solved ~var ~rep s =
   match s with
   | {solved= None} -> s
-  | {solved= Some solved} -> {s with solved= Some ((var, rep) :: solved)}
+  | {solved= Some solved} -> {s with solved= Some ({var; rep} :: solved)}
 
 let add_pending a b s = {s with pending= (a, b) :: s.pending}
 
diff --git a/sledge/src/fol/theory.mli b/sledge/src/fol/theory.mli
index 3323e10a8..ee988e78a 100644
--- a/sledge/src/fol/theory.mli
+++ b/sledge/src/fol/theory.mli
@@ -7,11 +7,13 @@
 
 (** Theory Solver *)
 
+type oriented_equality = {var: Trm.t; rep: Trm.t}
+
 type t =
   { wrt: Var.Set.t
   ; no_fresh: bool
   ; fresh: Var.Set.t
-  ; solved: (Trm.t * Trm.t) list option
+  ; solved: oriented_equality list option
   ; pending: (Trm.t * Trm.t) list }
 
 val pp : t pp