Theory: add_clone_internal

This is a one-call function that exports add_clone_unsafe to Pmodule,
allowing it to add Clone declarations to underlying theories without
additional checks.

src/core/theory.ml

@@ -720,6 +720,15 @@ let clone_export uc th inst =
 let clone_theory add_td acc th inst =
   clone_theory (cl_init th inst) add_td acc th inst
 
+let add_clone_unsafe uc th tsm lsm prm =
+  let sm = {sm_ts = tsm; sm_ls = lsm; sm_pr = prm} in
+  add_tdecl uc (mk_tdecl (Clone (th, sm)))
+
+let add_clone_internal =
+  let used = ref false in fun () -> if !used
+    then invalid_arg "Theory.add_clone_internal"
+    else begin used := true; add_clone_unsafe end
+
 (** Meta properties *)
 
 let get_meta_arg_type = function

src/core/theory.mli

@@ -179,6 +179,9 @@ val clone_theory : ('a -> tdecl -> 'a) -> 'a -> theory -> th_inst -> 'a
 
 val clone_export : theory_uc -> theory -> th_inst -> theory_uc
 
+val add_clone_internal : unit -> theory_uc -> theory ->
+  tysymbol Mts.t -> lsymbol Mls.t -> prsymbol Mpr.t -> theory_uc
+
 (** {2 Meta} *)
 
 val create_meta : meta -> meta_arg list -> tdecl

src/mlw/pmodule.ml

@@ -550,9 +550,14 @@ let clone_pdecl inst cl uc d = match d.pd_node with
   | PDpure ->
       List.fold_left (clone_decl inst cl) uc d.pd_pure
 
+let theory_add_clone = Theory.add_clone_internal ()
+
 let add_clone uc mi =
-  (* TODO: add TDclone to the muc_theory *)
-  { uc with muc_units = Uclone mi :: uc.muc_units }
+  let tuc = theory_add_clone uc.muc_theory mi.mi_mod.mod_theory
+    (Mts.map (fun s -> s.its_ts) mi.mi_ts) mi.mi_ls mi.mi_pr in
+  { uc with
+      muc_theory = tuc;
+      muc_units  = Uclone mi :: uc.muc_units }
 
 let clone_export uc m inst =
   let check_local id =