fix: remove some module aliases for 4.08

src/cc/Sidekick_cc.ml

@@ -13,17 +13,16 @@ module type ARG = Sidekick_core.CC_ARG
 module type S = Sidekick_core.CC_S
 
 module Make(CC_A: ARG) = struct
-  module CC_A = CC_A
-  module A = CC_A.A
-  type term = A.Term.t
-  type term_state = A.Term.state
-  type lit = CC_A.Lit.t
-  type fun_ = A.Fun.t
-  type proof = A.Proof.t
-  type actions = CC_A.Actions.t
+  module A = CC_A
+  type term = A.A.Term.t
+  type term_state = A.A.Term.state
+  type lit = A.Lit.t
+  type fun_ = A.A.Fun.t
+  type proof = A.A.Proof.t
+  type actions = A.Actions.t
 
-  module T = A.Term
-  module Fun = A.Fun
+  module T = A.A.Term
+  module Fun = A.A.Fun
   module Lit = CC_A.Lit
 
   module Bits : sig
@@ -353,7 +352,7 @@ module Make(CC_A: ARG) = struct
     Vec.clear cc.combine;
     List.iter (fun f -> f cc e) cc.on_conflict;
     Stat.incr cc.count_conflict;
-    CC_A.Actions.raise_conflict acts e A.Proof.default
+    CC_A.Actions.raise_conflict acts e A.A.Proof.default
 
   let[@inline] all_classes cc : repr Iter.t =
     T_tbl.values cc.tbl

src/cc/Sidekick_cc.mli

@@ -3,4 +3,4 @@
 module type ARG = Sidekick_core.CC_ARG
 module type S = Sidekick_core.CC_S
 
-module Make(CC_A: ARG) : S with module CC_A = CC_A
+module Make(A: ARG) : S with module A = A

src/core/Sidekick_core.ml

@@ -124,14 +124,13 @@ module type CC_ARG = sig
 end
 
 module type CC_S = sig
-  module CC_A : CC_ARG
-  module A = CC_A.A
-  type term_state = A.Term.state
-  type term = A.Term.t
-  type fun_ = A.Fun.t
-  type lit = CC_A.Lit.t
-  type proof = A.Proof.t
-  type actions = CC_A.Actions.t
+  module A : CC_ARG 
+  type term_state = A.A.Term.state
+  type term = A.A.Term.t
+  type fun_ = A.A.Fun.t
+  type lit = A.Lit.t
+  type proof = A.A.Proof.t
+  type actions = A.Actions.t
 
   type t
   (** Global state of the congruence closure *)
@@ -303,7 +302,7 @@ end
 module type SOLVER_INTERNAL = sig
   module A : TERM_PROOF 
   module CC_A : CC_ARG with module A = A
-  module CC : CC_S with module CC_A = CC_A
+  module CC : CC_S with module A = CC_A
 
   type ty = A.Ty.t
   type term = A.Term.t
@@ -314,9 +313,6 @@ module type SOLVER_INTERNAL = sig
   type t
   type solver = t
 
-  module Expl = CC.Expl
-  module N = CC.N
-
   val tst : t -> term_state
 
   val cc : t -> CC.t
@@ -401,31 +397,31 @@ module type SOLVER_INTERNAL = sig
   (** Add the given (signed) bool term to the SAT solver, so it gets assigned
       a boolean value *)
 
-  val cc_raise_conflict_expl : t -> actions -> Expl.t -> 'a
+  val cc_raise_conflict_expl : t -> actions -> CC.Expl.t -> 'a
   (** Raise a conflict with the given congruence closure explanation.
       it must be a theory tautology that [expl ==> absurd].
       To be used in theories. *)
 
-  val cc_find : t -> N.t -> N.t
+  val cc_find : t -> CC.N.t -> CC.N.t
   (** Find representative of the node *)
 
-  val cc_merge : t -> actions -> N.t -> N.t -> Expl.t -> unit
+  val cc_merge : t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit
   (** Merge these two nodes in the congruence closure, given this explanation.
       It must be a theory tautology that [expl ==> n1 = n2].
       To be used in theories. *)
 
-  val cc_merge_t : t -> actions -> term -> term -> Expl.t -> unit
+  val cc_merge_t : t -> actions -> term -> term -> CC.Expl.t -> unit
   (** Merge these two terms in the congruence closure, given this explanation.
       See {!cc_merge} *)
 
-  val cc_add_term : t -> term -> N.t
+  val cc_add_term : t -> term -> CC.N.t
   (** Add/retrieve congruence closure node for this term.
       To be used in theories *)
 
-  val on_cc_merge : t -> (CC.t -> actions -> N.t -> N.t -> Expl.t -> unit) -> unit
+  val on_cc_merge : t -> (CC.t -> actions -> CC.N.t -> CC.N.t -> CC.Expl.t -> unit) -> unit
   (** Callback for when two classes containing data for this key are merged *)
 
-  val on_cc_new_term : t -> (CC.t -> N.t -> term -> unit) -> unit
+  val on_cc_new_term : t -> (CC.t -> CC.N.t -> term -> unit) -> unit
   (** Callback to add data on terms when they are added to the congruence
       closure *)
 
@@ -473,8 +469,6 @@ module type SOLVER = sig
   module Solver_internal : SOLVER_INTERNAL with module A = A and module CC_A = CC_A
   (** Internal solver, available to theories.  *)
 
-  module Lit = Solver_internal.Lit
-
   type t
   type solver = t
   type term = A.Term.t
@@ -539,7 +533,7 @@ module type SOLVER = sig
     val hash : t -> int
     val pp : t CCFormat.printer
 
-    val formula : t -> Lit.t
+    val formula : t -> lit
     val sign : t -> bool
   end
 

src/smtlib/Process.ml

@@ -406,7 +406,7 @@ end
 module Solver = Sidekick_msat_solver.Make(Solver_arg)
 
 module Check_cc = struct
-  module Lit = Solver.Lit
+  module Lit = Solver.Solver_internal.Lit
   module SI = Solver.Solver_internal
   module CC = Solver.Solver_internal.CC
   module MCC = Sidekick_mini_cc.Make(Solver_arg)

src/th-bool-static/Sidekick_th_bool_static.ml

@@ -34,17 +34,15 @@ end
 
 module type S = sig
   module A : ARG
-  module T = A.S.A.Term
-  module SI = A.S.Solver_internal
 
   type state
 
-  val create : T.state -> state
+  val create : A.S.A.Term.state -> state
 
-  val simplify : state -> SI.simplify_hook
+  val simplify : state -> A.S.Solver_internal.simplify_hook
   (** Simplify given term *)
 
-  val cnf : state -> SI.preprocess_hook
+  val cnf : state -> A.S.Solver_internal.preprocess_hook
   (** add clauses for the booleans within the term. *)
 
   val theory : A.S.theory
@@ -54,7 +52,7 @@ module Make(A : ARG) : S with module A = A = struct
   module A = A
   module Ty = A.S.A.Ty
   module T = A.S.A.Term
-  module Lit = A.S.Lit
+  module Lit = A.S.Solver_internal.Lit
   module SI = A.S.Solver_internal
 
   type state = {