perf(cc): more inlining; remove dead code

src/cc/CC.ml

@@ -180,14 +180,15 @@ let add_signature self (s : signature) (n : e_node) : unit =
   on_backtrack self (fun () -> Sig_tbl.remove self.signatures_tbl s);
   Sig_tbl.add self.signatures_tbl s n
 
-let push_pending self t : unit =
+let[@inline] push_pending self t : unit =
   Log.debugf 50 (fun k -> k "(@[<hv1>cc.push-pending@ %a@])" E_node.pp t);
   Vec.push self.pending t
 
-let push_action self (a : Handler_action.t) : unit =
+let[@inline] push_action self (a : Handler_action.t) : unit =
   Vec.push self.combine (CT_act a)
 
-let push_action_l self (l : _ list) : unit = List.iter (push_action self) l
+let[@inline] push_action_l self (l : _ list) : unit =
+  List.iter (push_action self) l
 
 let merge_classes self t u e : unit =
   if t != u && not (same_class t u) then (
@@ -544,7 +545,7 @@ and task_pending_ self (n : e_node) : unit =
     )
   | Some s0 ->
     (* update the signature by using [find] on each sub-e_node *)
-    let s = update_sig s0 in
+    let s = (update_sig [@inlined]) s0 in
     (match find_signature self s with
     | None ->
       (* add to the signature table [sig(n) --> n] *)

src/cc/Sidekick_cc.ml

@@ -1,4 +1,5 @@
-module View = View
+open Sidekick_core
+module View = CC_view
 module E_node = E_node
 module Expl = Expl
 module Signature = Signature

src/cc/Sidekick_cc.mli

@@ -4,7 +4,7 @@ module type DYN_MONOID_PLUGIN = Sigs_plugin.DYN_MONOID_PLUGIN
 module type MONOID_PLUGIN_ARG = Sigs_plugin.MONOID_PLUGIN_ARG
 module type MONOID_PLUGIN_BUILDER = Sigs_plugin.MONOID_PLUGIN_BUILDER
 
-module View = View
+module View = Sidekick_core.CC_view
 module E_node = E_node
 module Expl = Expl
 module Signature = Signature

src/cc/signature.ml

@@ -19,14 +19,7 @@ let equal (s1 : t) s2 : bool =
     E_node.equal a1 a2 && E_node.equal b1 b2 && E_node.equal c1 c2
   | Eq (a1, b1), Eq (a2, b2) -> E_node.equal a1 a2 && E_node.equal b1 b2
   | Opaque u1, Opaque u2 -> E_node.equal u1 u2
-  | Bool _, _
+  | (Bool _ | App_fun _ | App_ho _ | If _ | Eq _ | Opaque _ | Not _), _ -> false
-  | App_fun _, _
-  | App_ho _, _
-  | If _, _
-  | Eq _, _
-  | Opaque _, _
-  | Not _, _ ->
-    false
 
 let hash (s : t) : int =
   let module H = CCHash in
@@ -40,7 +33,7 @@ let hash (s : t) : int =
     H.combine4 60 (E_node.hash a) (E_node.hash b) (E_node.hash c)
   | Not u -> H.combine2 70 (E_node.hash u)
 
-let pp out = function
+let[@inline never] pp out = function
   | Bool b -> Fmt.bool out b
   | App_fun (f, []) -> Const.pp out f
   | App_fun (f, l) ->

src/cc/sigs.ml

@@ -1,4 +0,0 @@
-(** Main types for congruence closure *)
-
-open Sidekick_core
-module View = View

src/core/CC_view.ml

@@ -8,7 +8,7 @@ type ('f, 't, 'ts) t =
   | Opaque of 't
 (* do not enter *)
 
-let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
+let[@inline] map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
   match v with
   | Bool b -> Bool b
   | App_fun (f, args) -> App_fun (f_f f, f_ts args)
@@ -18,7 +18,7 @@ let map_view ~f_f ~f_t ~f_ts (v : _ t) : _ t =
   | Eq (a, b) -> Eq (f_t a, f_t b)
   | Opaque t -> Opaque (f_t t)
 
-let iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
+let[@inline] iter_view ~f_f ~f_t ~f_ts (v : _ t) : unit =
   match v with
   | Bool _ -> ()
   | App_fun (f, args) ->