From 1c43a7fe3d7db72391599177f6bb2fc05c045c1d Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Tue, 2 Feb 2021 04:33:07 -0800
Subject: [PATCH] [sledge] Simplify Context.Subst.compose1

Summary: It is no longer necessary to test for constant terms.

Reviewed By: jvillard

Differential Revision: D25883720

fbshipit-source-id: 4b10740ae
---
 sledge/src/fol/context.ml | 18 ++++++++----------
 1 file changed, 8 insertions(+), 10 deletions(-)

diff --git a/sledge/src/fol/context.ml b/sledge/src/fol/context.ml
index 4d516a9c6..c6ca7c6b3 100644
--- a/sledge/src/fol/context.ml
+++ b/sledge/src/fol/context.ml
@@ -88,16 +88,14 @@ end = struct
 
   (** compose a substitution with a mapping *)
   let compose1 ~key ~data r =
-    match (key : Trm.t) with
-    | Z _ | Q _ -> r
-    | _ when Trm.equal key data -> r
-    | _ ->
-        assert (
-          Option.for_all ~f:(Trm.equal key) (Trm.Map.find key r)
-          || fail "domains intersect: %a" Trm.pp key () ) ;
-        let s = Trm.Map.singleton key data in
-        let r' = Trm.Map.map_endo ~f:(norm s) r in
-        Trm.Map.add ~key ~data r'
+    if Trm.equal key data then r
+    else (
+      assert (
+        Option.for_all ~f:(Trm.equal key) (Trm.Map.find key r)
+        || fail "domains intersect: %a" Trm.pp key () ) ;
+      let s = Trm.Map.singleton key data in
+      let r' = Trm.Map.map_endo ~f:(norm s) r in
+      Trm.Map.add ~key ~data r' )
 
   (** add an identity entry if the term is not already present *)
   let extend e s =