From d6c8f6aafd76bb7965fcf3db8f2ecdce1aa11384 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:26:49 -0800
Subject: [PATCH] [sledge] Add fast path to Context.Subst.compose for empty

Reviewed By: jvillard

Differential Revision: D25756568

fbshipit-source-id: 7f1856279
---
 sledge/src/fol/context.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index a4ab7b8ee..2ad3a0798 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -110,8 +110,10 @@ end = struct
   let compose r s =
     [%Trace.call fun {pf} -> pf "%a@ %a" pp r pp s]
     ;
-    let r' = Trm.Map.map_endo ~f:(norm s) r in
-    Trm.Map.union_absent r' s
+    ( if is_empty s then r
+    else
+      let r' = Trm.Map.map_endo ~f:(norm s) r in
+      Trm.Map.union_absent r' s )
     |>
     [%Trace.retn fun {pf} r' ->
       pf "%a" pp_diff (r, r') ;