Undo the last four commits. Never listen to people

coming to you late in the evening and talking French.

src/core/pretty.ml

@@ -43,11 +43,18 @@ let iprinter,tprinter,lprinter,pprinter =
   create_ident_printer bl ~sanitizer:lsanitize,
   create_ident_printer bl ~sanitizer:usanitize
 
+let thash = Hid.create 63
+let lhash = Hid.create 63
+let phash = Hid.create 63
+
 let forget_all () =
   forget_all iprinter;
   forget_all tprinter;
   forget_all lprinter;
-  forget_all pprinter
+  forget_all pprinter;
+  Hid.clear thash;
+  Hid.clear lhash;
+  Hid.clear phash
 
 let tv_set = ref Sid.empty
 
@@ -77,9 +84,11 @@ let print_th fmt th =
   fprintf fmt "%s" n
 
 let print_ts fmt ts =
+  Hid.replace thash ts.ts_name ts;
   fprintf fmt "%s" (id_unique tprinter ts.ts_name)
 
 let print_ls fmt ls =
+  Hid.replace lhash ls.ls_name ls;
   let n = if ls.ls_constr
     then id_unique lprinter ~sanitizer:String.capitalize ls.ls_name
     else id_unique lprinter ls.ls_name
@@ -87,6 +96,7 @@ let print_ls fmt ls =
   fprintf fmt "%s" n
 
 let print_pr fmt pr =
+  Hid.replace phash pr.pr_name pr;
   fprintf fmt "%s" (id_unique pprinter pr.pr_name)
 
 (** Types *)
@@ -302,6 +312,18 @@ let print_prop_decl fmt (k,pr,f) =
     print_pr pr print_fmla f;
   forget_tvs ()
 
+let print_inst fmt (id1,id2) =
+  if Hid.mem thash id2 then
+    let n = id_unique tprinter id1 in
+    fprintf fmt "type %s = %a" n print_ts (Hid.find thash id2)
+  else if Hid.mem lhash id2 then
+    let n = id_unique lprinter id1 in
+    fprintf fmt "logic %s = %a" n print_ls (Hid.find lhash id2)
+  else if Hid.mem phash id2 then
+    let n = id_unique pprinter id1 in
+    fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
+  else assert false
+
 let print_decl fmt d = match d.d_node with
   | Dtype tl  -> print_list newline print_type_decl fmt tl
   | Dlogic ll -> print_list newline print_logic_decl fmt ll
@@ -313,6 +335,9 @@ let print_tdecl fmt = function
       print_decl fmt d
   | Use th ->
       fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
+  | Clone (th,inst) ->
+      fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
+        print_th th (print_list comma print_inst) inst
 
 let print_decls fmt dl =
   fprintf fmt "@[<hov>%a@\n@]" (print_list newline2 print_decl) dl

src/core/task.ml

@@ -40,19 +40,11 @@ let cloned_from cl i1 i2 =
   try i1 = i2 || Sid.mem i2 (Mid.find i1 cl.cl_map)
   with Not_found -> false
 
-let merge_clone =
-  let add m id s acc =
-    let s =
-      try Sid.union s (Mid.find id m)
-      with Not_found -> s
-    in
-    Mid.add id s acc
-  in
+let add_clone =
   let r = ref 0 in
-  fun cl th ->
-    if Mid.is_empty th.th_clone then cl else
-    { cl_map = Mid.fold (add cl.cl_map) th.th_clone cl.cl_map;
-      cl_tag = (incr r; !r) }
+  fun cl th sl ->
+    incr r;
+    { cl_map = merge_clone cl.cl_map th sl; cl_tag = !r }
 
 
 (** Known identifiers *)
@@ -215,11 +207,13 @@ let rec use_export names acc td =
     | Use th when Sid.mem th.th_name used ->
         acc
     | Use th ->
-        let names = Some Spr.empty in
         let used = Sid.add th.th_name used in
-        let cl = merge_clone cl th in
         let acc = used, cl, res, task in
+        let names = Some Spr.empty in
         List.fold_left (use_export names) acc th.th_decls
+    | Clone (th,sl) ->
+        let cl = add_clone cl th sl in
+        used, cl, res, task
     | Decl d ->
         begin match d.d_node with
           | Dprop (Pgoal,pr,_)

src/core/theory.ml

@@ -89,6 +89,7 @@ type theory = {
 and tdecl =
   | Decl  of decl
   | Use   of theory
+  | Clone of theory * (ident * ident) list
 
 and clone_map = Sid.t Mid.t
 
@@ -221,6 +222,11 @@ let merge_clone cl th sl =
   in
   List.fold_left (add th.th_clone) cl sl
 
+let add_clone uc th sl =
+  let decls = Clone (th,sl) :: uc.uc_decls in
+  let clone = merge_clone uc.uc_clone th sl in
+  { uc with uc_decls = decls; uc_clone = clone }
+
 
 (** Clone *)
 
@@ -423,22 +429,6 @@ let cl_add_decl cl inst d = match d.d_node with
       let pr',f' = cl_new_prop cl (pr,f) in
       Some (create_prop_decl k' pr' f')
 
-let clone_fold add_tdecl v th inst =
-  let cl = cl_init th inst in
-  let add acc td = match td with
-    | Decl d ->
-        begin match cl_add_decl cl inst d with
-          | Some d -> add_tdecl acc (Decl d)
-          | None   -> acc
-        end
-    | Use _ ->
-        add_tdecl acc td
-  in
-  let (res,clmap) = List.fold_left add v th.th_decls in
-  let add_idid id id' acc = (id,id') :: acc in
-  let sl = Hid.fold add_idid cl.id_table [] in
-  res, merge_clone clmap th sl
-
 let cl_add_tdecl cl inst uc td = match td with
   | Decl d ->
       let decls = match cl_add_decl cl inst d with
@@ -448,6 +438,8 @@ let cl_add_tdecl cl inst uc td = match td with
       { uc with uc_decls = decls }
   | Use _ ->
       { uc with uc_decls = td :: uc.uc_decls }
+  | Clone (th,sl) ->
+      add_clone uc th sl
 
 let clone_export uc th inst =
   let cl = cl_init th inst in
@@ -456,8 +448,7 @@ let clone_export uc th inst =
 
   let add_idid id id' acc = (id,id') :: acc in
   let sl = Hid.fold add_idid cl.id_table [] in
-  let cm = merge_clone uc.uc_clone th sl in
-  let uc = { uc with uc_clone = cm } in
+  let uc = add_clone uc th sl in
 
   let add_local id' () acc = Sid.add id' acc in
   let lc = Hid.fold add_local cl.nw_local uc.uc_local in

src/core/theory.mli

@@ -54,6 +54,7 @@ type theory = private {
 and tdecl = private
   | Decl  of decl
   | Use   of theory
+  | Clone of theory * (ident * ident) list
 
 and clone_map = Sid.t Mid.t
 
@@ -87,8 +88,7 @@ val empty_inst : th_inst
 val use_export   : theory_uc -> theory -> theory_uc
 val clone_export : theory_uc -> theory -> th_inst -> theory_uc
 
-val clone_fold   : (('a * clone_map) -> tdecl -> ('a * clone_map)) ->
-        ('a * clone_map) -> theory -> th_inst -> ('a * clone_map)
+val merge_clone  : clone_map -> theory -> (ident * ident) list -> clone_map
 
 (* exceptions *)