From 9e373fb68cde5a22f6337ac71cf2511a44478659 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:26:36 -0800
Subject: [PATCH] [sledge] Generalize Context.Subst.compose to support shadowed
 bindings

Summary:
Composing two substitutions does not need to require that their
domains are disjoint.

Leave disjointness check for composing a single mapping just to check
expected usage.

Reviewed By: jvillard

Differential Revision: D25756557

fbshipit-source-id: 04e92b864
---
 sledge/nonstdlib/map.ml      | 15 +++++++++++++++
 sledge/nonstdlib/map_intf.ml |  6 ++++++
 sledge/src/fol/context.ml    | 14 ++++++--------
 3 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/sledge/nonstdlib/map.ml b/sledge/nonstdlib/map.ml
index 486ece4b6..0eec08336 100644
--- a/sledge/nonstdlib/map.ml
+++ b/sledge/nonstdlib/map.ml
@@ -63,6 +63,21 @@ end) : S with type key = Key.t = struct
     if !change then t' else t
 
   let union x y ~f = M.union f x y
+
+  let union_absent t u =
+    let change = ref false in
+    let t' =
+      M.merge
+        (fun _ v1 v2 ->
+          match v1 with
+          | Some _ -> v1
+          | None ->
+              change := true ;
+              v2 )
+        t u
+    in
+    if !change then t' else t
+
   let partition m ~f = M.partition f m
 
   let partition_map m ~f =
diff --git a/sledge/nonstdlib/map_intf.ml b/sledge/nonstdlib/map_intf.ml
index 710003d34..950fb2a6b 100644
--- a/sledge/nonstdlib/map_intf.ml
+++ b/sledge/nonstdlib/map_intf.ml
@@ -48,6 +48,12 @@ module type S = sig
       every value. *)
 
   val union : 'a t -> 'a t -> f:(key -> 'a -> 'a -> 'a option) -> 'a t
+
+  val union_absent : 'a t -> 'a t -> 'a t
+  (** [union_absent m1 m2] contains all the bindings of [m1] as well as
+      those of [m2] for keys not contained by [m1].
+      [union_absent m1 m2 == m1] if no bindings from [m2] are added. *)
+
   val partition : 'a t -> f:(key -> 'a -> bool) -> 'a t * 'a t
 
   val partition_map :
diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index ebdfe00b4..b363a6f65 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -111,13 +111,7 @@ end = struct
     [%Trace.call fun {pf} -> pf "%a@ %a" pp r pp s]
     ;
     let r' = Trm.Map.map_endo ~f:(norm s) r in
-    Trm.Map.merge_endo r' s ~f:(fun key -> function
-      | `Both (data_r, data_s) ->
-          assert (
-            Trm.equal data_s data_r
-            || fail "domains intersect: %a" Trm.pp key () ) ;
-          Some data_r
-      | `Left data | `Right data -> Some data )
+    Trm.Map.union_absent r' s
     |>
     [%Trace.retn fun {pf} r' ->
       pf "%a" pp_diff (r, r') ;
@@ -129,7 +123,11 @@ end = struct
     | Z _ | Q _ -> s
     | _ ->
         if Trm.equal key data then s
-        else compose s (Trm.Map.singleton key data)
+        else (
+          assert (
+            (not (Trm.Map.mem key s))
+            || fail "domains intersect: %a" Trm.pp key () ) ;
+          compose s (Trm.Map.singleton key data) )
 
   (** add an identity entry if the term is not already present *)
   let extend e s =