From c09650db513a322a869bfbe6570db93f0d361407 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 29 Jul 2022 00:15:05 -0400
Subject: [PATCH] refactor(cc): continue de-functorizing

---
 src/cc/Sidekick_cc.ml               | 13 +++++++++++++
 src/cc/Sidekick_cc.mli              | 28 +++++++---------------------
 src/cc/plugin/sidekick_cc_plugin.ml |  5 ++---
 3 files changed, 22 insertions(+), 24 deletions(-)

diff --git a/src/cc/Sidekick_cc.ml b/src/cc/Sidekick_cc.ml
index 7648562c..9b272403 100644
--- a/src/cc/Sidekick_cc.ml
+++ b/src/cc/Sidekick_cc.ml
@@ -3,7 +3,20 @@ module View = View
 
 module type ARG = Sigs.ARG
 module type S = Sigs.S
+module type DYN_MONOID_PLUGIN = Sigs.DYN_MONOID_PLUGIN
 module type MONOID_PLUGIN_ARG = Sigs.MONOID_PLUGIN_ARG
 module type MONOID_PLUGIN_BUILDER = Sigs.MONOID_PLUGIN_BUILDER
 
 module Make (A : ARG) : S = Core_cc.Make (A)
+
+module Base : S = Make (struct
+  let view_as_cc (t : Term.t) : _ View.t =
+    let f, args = Term.unfold_app t in
+    match Term.view f, args with
+    | _, [ _; t; u ] when Term.is_eq f -> View.Eq (t, u)
+    | _ ->
+      (match Term.view t with
+      | Term.E_app (f, a) -> View.App_ho (f, a)
+      | Term.E_const c -> View.App_fun (c, Iter.empty)
+      | _ -> View.Opaque t)
+end)
diff --git a/src/cc/Sidekick_cc.mli b/src/cc/Sidekick_cc.mli
index 0eb9def5..9c7da989 100644
--- a/src/cc/Sidekick_cc.mli
+++ b/src/cc/Sidekick_cc.mli
@@ -4,26 +4,12 @@ open Sidekick_core
 module View = View
 
 module type ARG = Sigs.ARG
-
-module type S = sig
-  include Sigs.S
-
-  val create :
-    ?stat:Stat.t -> ?size:[ `Small | `Big ] -> Term.store -> Proof_trace.t -> t
-  (** Create a new congruence closure.
-
-      @param term_store used to be able to create new terms. All terms
-      interacting with this congruence closure must belong in this term state
-      as well. *)
-
-  (**/**)
-
-  module Debug_ : sig
-    val pp : t Fmt.printer
-    (** Print the whole CC *)
-  end
-
-  (**/**)
-end
+module type S = Sigs.S
+module type DYN_MONOID_PLUGIN = Sigs.DYN_MONOID_PLUGIN
+module type MONOID_PLUGIN_ARG = Sigs.MONOID_PLUGIN_ARG
+module type MONOID_PLUGIN_BUILDER = Sigs.MONOID_PLUGIN_BUILDER
 
 module Make (_ : ARG) : S
+
+module Base : S
+(** Basic implementation following terms' shape *)
diff --git a/src/cc/plugin/sidekick_cc_plugin.ml b/src/cc/plugin/sidekick_cc_plugin.ml
index 0563977e..39327e1e 100644
--- a/src/cc/plugin/sidekick_cc_plugin.ml
+++ b/src/cc/plugin/sidekick_cc_plugin.ml
@@ -1,3 +1,4 @@
+open Sidekick_core
 open Sidekick_cc
 
 module type EXTENDED_PLUGIN_BUILDER = sig
@@ -23,8 +24,6 @@ module Make (M : MONOID_PLUGIN_ARG) :
   module Cls_tbl = Backtrackable_tbl.Make (E_node)
   module Expl = CC.Expl
 
-  type term = CC.term
-
   module type DYN_PL_FOR_M = DYN_MONOID_PLUGIN with module M = M
 
   type t = (module DYN_PL_FOR_M)
@@ -63,7 +62,7 @@ module Make (M : MONOID_PLUGIN_ARG) :
       else
         None
 
-    let on_new_term cc n (t : term) : CC.Handler_action.t list =
+    let on_new_term cc n (t : Term.t) : CC.Handler_action.t list =
       (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*)
       let acts = ref [] in
       let maybe_m, l = M.of_term cc n t in