From e0312f1274211f76ba731689177e0dbecbb62103 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 12 Jan 2021 04:24:39 -0800
Subject: [PATCH] [sledge] Add fast path for applying an empty substitution

Reviewed By: jvillard

Differential Revision: D25756576

fbshipit-source-id: 401eab0c0
---
 sledge/src/fol/context.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 462d1f14f..e558e077b 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -681,11 +681,13 @@ let fold_uses_of r t s ~f =
 let apply_subst wrt s r =
   [%Trace.call fun {pf} -> pf "%a@ %a" Subst.pp s pp r]
   ;
-  Trm.Map.fold (classes r) empty ~f:(fun ~key:rep ~data:cls r ->
-      let rep' = Subst.subst_ s rep in
-      List.fold cls r ~f:(fun trm r ->
-          let trm' = Subst.subst_ s trm in
-          and_eq_ ~wrt trm' rep' r ) )
+  ( if Subst.is_empty s then r
+  else
+    Trm.Map.fold (classes r) empty ~f:(fun ~key:rep ~data:cls r ->
+        let rep' = Subst.subst_ s rep in
+        List.fold cls r ~f:(fun trm r ->
+            let trm' = Subst.subst_ s trm in
+            and_eq_ ~wrt trm' rep' r ) ) )
   |> extract_xs
   |>
   [%Trace.retn fun {pf} (xs, r') ->