From 5ea2f20cad173f17c8bba86dca4120127077deba Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Sun, 21 Feb 2021 13:17:13 -0800
Subject: [PATCH] [sledge] Optimize by inlining functors

Summary:
Inline functor applications, principally those involved in the
representation of (arithmetic) terms. This enables direct calls to
functions in the result of functor applications, instead of indirect
via an offset from the start of the module block resulting from the
functor appication. This also then enables further inlining
opportunities.

Reviewed By: jvillard

Differential Revision: D26338016

fbshipit-source-id: 27b770fa3
---
 sledge/nonstdlib/NSMap.ml       | 3 ++-
 sledge/nonstdlib/NSSet.ml       | 3 ++-
 sledge/nonstdlib/comparer.ml    | 4 ++++
 sledge/nonstdlib/hashSet.ml     | 2 +-
 sledge/nonstdlib/hashTable.ml   | 2 +-
 sledge/nonstdlib/multiset.ml    | 1 +
 sledge/src/control.ml           | 1 +
 sledge/src/domain_relation.ml   | 1 +
 sledge/src/fol/arithmetic.ml    | 2 ++
 sledge/src/fol/propositional.ml | 1 +
 sledge/src/fol/subst.ml         | 1 +
 11 files changed, 17 insertions(+), 4 deletions(-)

diff --git a/sledge/nonstdlib/NSMap.ml b/sledge/nonstdlib/NSMap.ml
index 6abcf14fb..b25093270 100644
--- a/sledge/nonstdlib/NSMap.ml
+++ b/sledge/nonstdlib/NSMap.ml
@@ -11,7 +11,7 @@ include NSMap_intf
 module Make (Key : sig
   type t [@@deriving compare, sexp_of]
 end) : S with type key = Key.t = struct
-  module M = Stdlib.Map.Make (Key)
+  module M = Stdlib.Map.Make [@inlined] (Key)
 
   type key = Key.t
   type 'a t = 'a M.t [@@deriving compare, equal]
@@ -249,3 +249,4 @@ end) : S with type key = Key.t = struct
     let sd = Iter.to_list (symmetric_diff ~eq x y) in
     List.pp ~pre ~suf sep pp_diff_elt fs sd
 end
+[@@inline]
diff --git a/sledge/nonstdlib/NSSet.ml b/sledge/nonstdlib/NSSet.ml
index 47e699f0f..e75fd1230 100644
--- a/sledge/nonstdlib/NSSet.ml
+++ b/sledge/nonstdlib/NSSet.ml
@@ -11,7 +11,7 @@ include NSSet_intf
 module Make (Elt : sig
   type t [@@deriving compare, sexp_of]
 end) : S with type elt = Elt.t = struct
-  module S = Stdlib.Set.Make (Elt)
+  module S = Stdlib.Set.Make [@inlined] (Elt)
 
   type elt = Elt.t
   type t = S.t [@@deriving compare, equal]
@@ -138,3 +138,4 @@ end) : S with type elt = Elt.t = struct
       if not (is_empty gain) then Format.fprintf fs "++ %a" pp gain
   end
 end
+[@@inline]
diff --git a/sledge/nonstdlib/comparer.ml b/sledge/nonstdlib/comparer.ml
index 651e26adb..577bcab79 100644
--- a/sledge/nonstdlib/comparer.ml
+++ b/sledge/nonstdlib/comparer.ml
@@ -36,6 +36,7 @@ struct
 
   let comparer = Ord.compare
 end
+[@@inlined]
 
 module Counterfeit (Ord : sig
   type t [@@deriving compare]
@@ -46,6 +47,7 @@ struct
 
   let comparer = Ord.compare
 end
+[@@inlined]
 
 module Apply (F : sig
   type ('a, 'compare_a) t [@@deriving compare]
@@ -64,6 +66,7 @@ struct
 
   let comparer = compare
 end
+[@@inlined]
 
 module Apply1 (F : sig
   type ('a, 'b, 'compare_a) t [@@deriving compare]
@@ -84,3 +87,4 @@ struct
 
   let comparer = compare
 end
+[@@inlined]
diff --git a/sledge/nonstdlib/hashSet.ml b/sledge/nonstdlib/hashSet.ml
index 29cc77a2c..817b4f194 100644
--- a/sledge/nonstdlib/hashSet.ml
+++ b/sledge/nonstdlib/hashSet.ml
@@ -8,7 +8,7 @@
 include CCHashSet
 
 module Make (E : ELEMENT) = struct
-  include CCHashSet.Make (E)
+  include CCHashSet.Make [@inlined] (E)
 
   let update s e ~f =
     let eo = find s e in
diff --git a/sledge/nonstdlib/hashTable.ml b/sledge/nonstdlib/hashTable.ml
index 00656694c..e3b70351d 100644
--- a/sledge/nonstdlib/hashTable.ml
+++ b/sledge/nonstdlib/hashTable.ml
@@ -12,7 +12,7 @@ open! NS0
 include HashTable_intf
 
 module Make (Key : HashedType) = struct
-  include CCHashtbl.Make (Key)
+  include CCHashtbl.Make [@inlined] (Key)
 
   let create ?(size = 0) () = create size
   let set tbl ~key ~data = replace tbl key data
diff --git a/sledge/nonstdlib/multiset.ml b/sledge/nonstdlib/multiset.ml
index 289c2a289..7d5636bfb 100644
--- a/sledge/nonstdlib/multiset.ml
+++ b/sledge/nonstdlib/multiset.ml
@@ -112,3 +112,4 @@ struct
   let for_all m ~f = M.for_alli ~f:(fun ~key ~data -> f key data) m
   let fold m s ~f = M.fold ~f:(fun ~key ~data -> f key data) m s
 end
+[@@inline]
diff --git a/sledge/src/control.ml b/sledge/src/control.ml
index 19a08e855..eba954a91 100644
--- a/sledge/src/control.ml
+++ b/sledge/src/control.ml
@@ -559,3 +559,4 @@ module Make (Opts : Domain_intf.Opts) (Dom : Domain_intf.Dom) = struct
         | [] -> map
         | _ -> Llair.Function.Map.add ~key ~data map )
 end
+[@@inlined]
diff --git a/sledge/src/domain_relation.ml b/sledge/src/domain_relation.ml
index bfedc807e..dcde0dd50 100644
--- a/sledge/src/domain_relation.ml
+++ b/sledge/src/domain_relation.ml
@@ -115,3 +115,4 @@ module Make (State_domain : State_domain_sig) = struct
     let+ next = State_domain.apply_summary current summ in
     (entry, next)
 end
+[@@inlined]
diff --git a/sledge/src/fol/arithmetic.ml b/sledge/src/fol/arithmetic.ml
index e46203fdb..c920c3b49 100644
--- a/sledge/src/fol/arithmetic.ml
+++ b/sledge/src/fol/arithmetic.ml
@@ -399,4 +399,6 @@ struct
               solve_for_mono Sum.empty c m p
           | _ -> None )
   end
+  [@@inline]
 end
+[@@inline]
diff --git a/sledge/src/fol/propositional.ml b/sledge/src/fol/propositional.ml
index db1519b71..5558c83a7 100644
--- a/sledge/src/fol/propositional.ml
+++ b/sledge/src/fol/propositional.ml
@@ -258,3 +258,4 @@ struct
     let trms p = Iter.from_labelled_iter (iter_trms p)
   end
 end
+[@@inline]
diff --git a/sledge/src/fol/subst.ml b/sledge/src/fol/subst.ml
index 9b454c2fc..1a9aa6402 100644
--- a/sledge/src/fol/subst.ml
+++ b/sledge/src/fol/subst.ml
@@ -76,3 +76,4 @@ module Make (Var : VAR) = struct
 
   let apply sub v = Map.find v sub |> Option.value ~default:v
 end
+[@@inline]