[sledge] Optimize Context.Subst.compose1

Summary:
Trade a bit more code for lowering complexity from linear to
logarithmic.

Reviewed By: jvillard

Differential Revision: D25756569

fbshipit-source-id: 83ad575fe

sledge/src/fol/context.ml

@@ -118,16 +118,17 @@ end = struct
       assert (r' == r || not (equal r' r))]
 
   (** compose a substitution with a mapping *)
-  let compose1 ~key ~data s =
+  let compose1 ~key ~data r =
     match (key : Trm.t) with
-    | Z _ | Q _ -> s
+    | Z _ | Q _ -> r
+    | _ when Trm.equal key data -> r
     | _ ->
-        if Trm.equal key data then s
+        assert (
-        else (
+          (not (Trm.Map.mem key r))
-          assert (
+          || fail "domains intersect: %a" Trm.pp key () ) ;
-            (not (Trm.Map.mem key s))
+        let s = Trm.Map.singleton key data in
-            || fail "domains intersect: %a" Trm.pp key () ) ;
+        let r' = Trm.Map.map_endo ~f:(norm s) r in
-          compose s (Trm.Map.singleton key data) )
+        Trm.Map.add ~key ~data r'
 
   (** add an identity entry if the term is not already present *)
   let extend e s =