cloning: preserve ts-to-ts instances

the previous commit loses information when the target type symbol
is an existing type alias. This commit preserves symbol-to-symbol
instances.

src/core/pretty.ml

@@ -420,11 +420,14 @@ let print_logic_decl      = print_logic_decl true
 let print_next_ind_decl   = print_ind_decl Ind false
 let print_ind_decl fmt s  = print_ind_decl s true fmt
 
-let print_inst_ts fmt (ts1,ty2) =
+let print_inst_ty fmt (ts1,ty2) =
   fprintf fmt "type %a%a = %a" print_ts ts1
     (print_list_pre space print_tv) ts1.ts_args
     print_ty ty2; forget_tvs ()
 
+let print_inst_ts fmt (ts1,ts2) =
+  fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2
+
 let print_inst_ls fmt (ls1,ls2) =
   fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
 
@@ -460,12 +463,14 @@ let print_tdecl fmt td = match td.td_node with
       fprintf fmt "@[<hov 2>(* use %a *)@]" print_qt th
   | Clone (th,sm) ->
       let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
+      let ym = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ty [] in
       let lm = Mls.fold (fun x y a -> (x,y)::a) sm.sm_ls [] in
       let pm = Mpr.fold (fun x y a -> (x,y)::a) sm.sm_pr [] in
-      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]"
-        print_qt th (print_list comma print_inst_ts) tm
-                    (print_list comma print_inst_ls) lm
-                    (print_list comma print_inst_pr) pm
+      fprintf fmt "@[<hov 2>(* clone %a with %a%a%a%a *)@]"
+        print_qt th (print_list_suf comma print_inst_ts) tm
+                    (print_list_suf comma print_inst_ty) ym
+                    (print_list_suf comma print_inst_ls) lm
+                    (print_list_suf comma print_inst_pr) pm
   | Meta (m,al) ->
       fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
         m.meta_name (print_list comma print_meta_arg) al

src/core/theory.ml

@@ -171,7 +171,8 @@ and tdecl_node =
   | Meta  of meta * meta_arg list
 
 and symbol_map = {
-  sm_ts : ty Mts.t;
+  sm_ty : ty Mts.t;
+  sm_ts : tysymbol Mts.t;
   sm_ls : lsymbol Mls.t;
   sm_pr : prsymbol Mpr.t;
 }
@@ -192,7 +193,8 @@ module Hstdecl = Hashcons.Make (struct
     | _,_ -> false
 
   let eq_smap sm1 sm2 =
-    Mts.equal ty_equal sm1.sm_ts sm2.sm_ts &&
+    Mts.equal ty_equal sm1.sm_ty sm2.sm_ty &&
+    Mts.equal ts_equal sm1.sm_ts sm2.sm_ts &&
     Mls.equal ls_equal sm1.sm_ls sm2.sm_ls &&
     Mpr.equal pr_equal sm1.sm_pr sm2.sm_pr
 
@@ -206,6 +208,7 @@ module Hstdecl = Hashcons.Make (struct
     | _,_ -> false
 
   let hs_cl_ty _ ty acc = Hashcons.combine acc (ty_hash ty)
+  let hs_cl_ts _ ts acc = Hashcons.combine acc (ts_hash ts)
   let hs_cl_ls _ ls acc = Hashcons.combine acc (ls_hash ls)
   let hs_cl_pr _ pr acc = Hashcons.combine acc (pr_hash pr)
 
@@ -218,9 +221,10 @@ module Hstdecl = Hashcons.Make (struct
     | MAint i -> Hashtbl.hash i
 
   let hs_smap sm h =
-    Mts.fold hs_cl_ty sm.sm_ts
-      (Mls.fold hs_cl_ls sm.sm_ls
-        (Mpr.fold hs_cl_pr sm.sm_pr h))
+    Mts.fold hs_cl_ty sm.sm_ty
+      (Mts.fold hs_cl_ts sm.sm_ts
+        (Mls.fold hs_cl_ls sm.sm_ls
+          (Mpr.fold hs_cl_pr sm.sm_pr h)))
 
   let hash td = match td.td_node with
     | Decl d -> d_hash d
@@ -312,7 +316,8 @@ let known_ty kn ty =
   ty_s_fold (fun () ts -> known_id kn ts.ts_name) () ty
 
 let known_clone kn sm =
-  Mts.iter (fun _ ty -> known_ty kn ty) sm.sm_ts;
+  Mts.iter (fun _ ty -> known_ty kn ty) sm.sm_ty;
+  Mts.iter (fun _ ts -> known_id kn ts.ts_name) sm.sm_ts;
   Mls.iter (fun _ ls -> known_id kn ls.ls_name) sm.sm_ls;
   Mpr.iter (fun _ pr -> known_id kn pr.pr_name) sm.sm_pr
 
@@ -446,12 +451,14 @@ let use_export uc th =
 (** Clone *)
 
 type th_inst = {
-  inst_ts : ty Mts.t; (* old to new *)
+  inst_ty : ty Mts.t;
+  inst_ts : tysymbol Mts.t;
   inst_ls : lsymbol Mls.t;
   inst_pr : prop_kind Mpr.t;
 }
 
 let empty_inst = {
+  inst_ty = Mts.empty;
   inst_ts = Mts.empty;
   inst_ls = Mls.empty;
   inst_pr = Mpr.empty;
@@ -461,13 +468,15 @@ exception CannotInstantiate of ident
 
 type clones = {
   cl_local : Sid.t;
-  mutable ts_table : ty Mts.t;
+  mutable ty_table : ty Mts.t;
+  mutable ts_table : tysymbol Mts.t;
   mutable ls_table : lsymbol Mls.t;
   mutable pr_table : prsymbol Mpr.t;
 }
 
 let empty_clones th = {
   cl_local = th.th_local;
+  ty_table = Mts.empty;
   ts_table = Mts.empty;
   ls_table = Mls.empty;
   pr_table = Mpr.empty;
@@ -475,35 +484,28 @@ let empty_clones th = {
 
 (* populate the clone structure *)
 
-let rec sm_trans_ty tsm ty = match ty.ty_node with
+let rec sm_trans_ty tym tsm ty = match ty.ty_node with
   | Tyapp (ts, tyl) ->
-      let tyl = List.map (sm_trans_ty tsm) tyl in
+      let tyl = List.map (sm_trans_ty tym tsm) tyl in
       begin match Mts.find_opt ts tsm with
+      | Some ts -> ty_app ts tyl
+      | None -> begin match Mts.find_opt ts tym with
       | Some ty -> ty_inst (ts_match_args ts tyl) ty
       | None -> ty_app ts tyl
-      end
+      end end
   | Tyvar _ -> ty
 
-let cl_trans_ty cl ty = sm_trans_ty cl.ts_table ty
-
-let sm_find_ts tsm ({ts_args = tvl} as ts) =
-  let check v ty = match ty.ty_node with
-    | Tyvar u -> tv_equal u v
-    | _ -> false in
-  match (Mts.find ts tsm).ty_node with
-  | Tyapp (ts, tyl) when Lists.equal check tvl tyl -> ts
-  | _ -> raise Not_found
+let cl_trans_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty
 
 let cl_find_ts cl ts =
   if not (Sid.mem ts.ts_name cl.cl_local) then ts else
-  try sm_find_ts cl.ts_table ts with Not_found -> raise EmptyDecl
+  try Mts.find ts cl.ts_table with Not_found -> raise EmptyDecl
 
 let cl_clone_ts cl ts =
   (* cl_clone_ts is only called for local non-instantiated symbols *)
   let td' = Opt.map (cl_trans_ty cl) ts.ts_def in
   let ts' = create_tysymbol (id_clone ts.ts_name) ts.ts_args td' in
-  let ty' = ty_app ts' (List.map ty_var ts.ts_args) in
-  cl.ts_table <- Mts.add ts ty' cl.ts_table;
+  cl.ts_table <- Mts.add ts ts' cl.ts_table;
   ts'
 
 let cl_find_ls cl ls =
@@ -533,11 +535,17 @@ let cl_clone_pr cl pr =
 exception NonLocal of ident
 exception BadInstance of ident
 
-let cl_init_ts cl ({ts_name = id} as ts) ty =
+let cl_init_ty cl ({ts_name = id} as ts) ty =
   if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
   let stv = Stv.of_list ts.ts_args in
   if not (ty_v_all (fun v -> Stv.mem v stv) ty) then raise (BadInstance id);
-  cl.ts_table <- Mts.add ts ty cl.ts_table
+  cl.ty_table <- Mts.add ts ty cl.ty_table
+
+let cl_init_ts cl ({ts_name = id} as ts) ts' =
+  if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
+  if List.length ts.ts_args <> List.length ts'.ts_args then
+    raise (BadInstance id);
+  cl.ts_table <- Mts.add ts ts' cl.ts_table
 
 let cl_init_ls cl ({ls_name = id} as ls) ls' =
   if not (Sid.mem id cl.cl_local) then raise (NonLocal id);
@@ -559,6 +567,7 @@ let cl_init_pr cl {pr_name = id} _ =
 
 let cl_init th inst =
   let cl = empty_clones th in
+  Mts.iter (cl_init_ty cl) inst.inst_ty;
   Mts.iter (cl_init_ts cl) inst.inst_ts;
   Mls.iter (cl_init_ls cl) inst.inst_ls;
   Mpr.iter (cl_init_pr cl) inst.inst_pr;
@@ -644,7 +653,8 @@ let cl_marg cl = function
   | a -> a
 
 let cl_smap cl sm = {
-  sm_ts = Mts.map (cl_trans_ty cl) sm.sm_ts;
+  sm_ty = Mts.map (cl_trans_ty cl) sm.sm_ty;
+  sm_ts = Mts.map (cl_find_ts cl) sm.sm_ts;
   sm_ls = Mls.map (cl_find_ls cl) sm.sm_ls;
   sm_pr = Mpr.map (cl_find_pr cl) sm.sm_pr}
 
@@ -681,6 +691,7 @@ let clone_theory cl add_td acc th inst =
   in
   let acc = List.fold_left add acc th.th_decls in
   let sm = {
+    sm_ty = cl.ty_table;
     sm_ts = cl.ts_table;
     sm_ls = cl.ls_table;
     sm_pr = cl.pr_table}
@@ -693,7 +704,7 @@ let clone_export uc th inst =
 
   let f_ts p ts =
     if Mid.mem ts.ts_name th.th_local then
-    try let ts = sm_find_ts cl.ts_table ts in
+    try let ts = Mts.find ts cl.ts_table in
         store_path uc p ts.ts_name; Some ts
     with Not_found -> None else Some ts in
   let f_ls p ls =
@@ -724,8 +735,7 @@ 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
+let add_clone_unsafe uc th sm =
   add_tdecl uc (mk_tdecl (Clone (th, sm)))
 
 let add_clone_internal =
@@ -764,13 +774,13 @@ let add_meta uc s al = add_tdecl uc (create_meta s al)
 let clone_meta tdt th sm = match tdt.td_node with
   | Meta (t,al) ->
       let find_ts ts = if Mid.mem ts.ts_name th.th_local
-        then sm_find_ts sm.sm_ts ts else ts in
+        then Mts.find ts sm.sm_ts else ts in
       let find_ls ls = if Mid.mem ls.ls_name th.th_local
         then Mls.find ls sm.sm_ls else ls in
       let find_pr pr = if Mid.mem pr.pr_name th.th_local
         then Mpr.find pr sm.sm_pr else pr in
       let cl_marg = function
-        | MAty ty -> MAty (sm_trans_ty sm.sm_ts ty)
+        | MAty ty -> MAty (sm_trans_ty sm.sm_ty sm.sm_ts ty)
         | MAts ts -> MAts (find_ts ts)
         | MAls ls -> MAls (find_ls ls)
         | MApr pr -> MApr (find_pr pr)

src/core/theory.mli

@@ -95,14 +95,15 @@ and tdecl = private {
   td_tag  : int;
 }
 
-and tdecl_node = private
+and tdecl_node =
   | Decl  of decl
   | Use   of theory
   | Clone of theory * symbol_map
   | Meta  of meta * meta_arg list
 
-and symbol_map = private {
-  sm_ts : ty Mts.t;
+and symbol_map = {
+  sm_ty : ty Mts.t;
+  sm_ts : tysymbol Mts.t;
   sm_ls : lsymbol Mls.t;
   sm_pr : prsymbol Mpr.t;
 }
@@ -166,7 +167,8 @@ val use_export : theory_uc -> theory -> theory_uc
 (** {2 Clone} *)
 
 type th_inst = {
-  inst_ts : ty Mts.t; (* old to new *)
+  inst_ty : ty Mts.t;
+  inst_ts : tysymbol Mts.t;
   inst_ls : lsymbol Mls.t;
   inst_pr : prop_kind Mpr.t;
 }
@@ -179,8 +181,7 @@ 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 ->
-  ty Mts.t -> lsymbol Mls.t -> prsymbol Mpr.t -> theory_uc
+val add_clone_internal : unit -> theory_uc -> theory -> symbol_map -> theory_uc
 
 (** {2 Meta} *)
 

src/mlw/pmodule.ml

@@ -109,7 +109,8 @@ and mod_unit =
 
 and mod_inst = {
   mi_mod : pmodule;
-  mi_ts  : ity Mts.t;
+  mi_ty  : ity Mts.t;
+  mi_ts  : itysymbol Mts.t;
   mi_ls  : lsymbol Mls.t;
   mi_pr  : prsymbol Mpr.t;
   mi_pv  : pvsymbol Mpv.t;
@@ -344,7 +345,8 @@ let add_pdecl ~vc uc d =
 
 type clones = {
   cl_local : Sid.t;
-  mutable ts_table : ity Mts.t;
+  mutable ty_table : ity Mts.t;
+  mutable ts_table : itysymbol Mts.t;
   mutable ls_table : lsymbol Mls.t;
   mutable pr_table : prsymbol Mpr.t;
   mutable rn_table : region Mreg.t;
@@ -355,6 +357,7 @@ type clones = {
 
 let empty_clones m = {
   cl_local = m.mod_local;
+  ty_table = Mts.empty;
   ts_table = Mts.empty;
   ls_table = Mls.empty;
   pr_table = Mpr.empty;
@@ -366,28 +369,26 @@ let empty_clones m = {
 
 (* populate the clone structure *)
 
-let rec sm_trans_ty tsm ty = match ty.ty_node with
+let rec sm_trans_ty tym tsm ty = match ty.ty_node with
   | Tyapp (s, tl) ->
-      let tl = List.map (sm_trans_ty tsm) tl in
+      let tl = List.map (sm_trans_ty tym tsm) tl in
       begin match Mts.find_opt s tsm with
+      | Some its -> ty_app its.its_ts tl
+      | None -> begin match Mts.find_opt s tym with
       | Some ity -> ty_inst (ts_match_args s tl) (ty_of_ity ity)
       | None -> ty_app s tl
-      end
+      end end
   | Tyvar _ -> ty
 
-let cl_trans_ty cl ty = sm_trans_ty cl.ts_table ty
+let cl_trans_ty cl ty = sm_trans_ty cl.ty_table cl.ts_table ty
 
-let sm_find_ts tsm ({ts_args = vl} as s) =
-  let check v ty = match ty.ty_node with
-    | Tyvar u -> tv_equal u v
-    | _ -> false in
-  match (ty_of_ity (Mts.find s tsm)).ty_node with
-  | Tyapp (s, tl) when Lists.equal check vl tl -> s
-  | _ -> raise Not_found
+let cl_find_its cl its =
+  if not (Sid.mem its.its_ts.ts_name cl.cl_local) then its
+  else Mts.find its.its_ts cl.ts_table
 
-let cl_find_ts cl s =
-  if not (Sid.mem s.ts_name cl.cl_local) then s else
-  sm_find_ts cl.ts_table s
+let cl_find_ts cl ts =
+  if not (Sid.mem ts.ts_name cl.cl_local) then ts
+  else (Mts.find ts cl.ts_table).its_ts
 
 let rec cl_trans_ity cl ity = match ity.ity_node with
   | Ityreg r ->
@@ -396,15 +397,19 @@ let rec cl_trans_ity cl ity = match ity.ity_node with
       let tl = List.map (cl_trans_ity cl) tl in
       let rl = List.map (cl_trans_reg cl) rl in
       begin match Mts.find_opt s.its_ts cl.ts_table with
+      | Some its -> ity_app its tl rl
+      | None -> begin match Mts.find_opt s.its_ts cl.ty_table with
       | Some ity -> ity_full_inst (its_match_regs s tl rl) ity
       | None -> ity_app s tl rl
-      end
+      end end
   | Itypur (s, tl) ->
       let tl = List.map (cl_trans_ity cl) tl in
       begin match Mts.find_opt s.its_ts cl.ts_table with
+      | Some its -> ity_pur its tl
+      | None -> begin match Mts.find_opt s.its_ts cl.ty_table with
       | Some ity -> ity_full_inst (its_match_args s tl) (ity_purify ity)
       | None -> ity_pur s tl
-      end
+      end end
   | Ityvar _ -> ity
 
 and cl_trans_reg cl reg =
@@ -417,6 +422,9 @@ and cl_trans_reg cl reg =
   let tl = List.map (cl_trans_ity cl) reg.reg_args in
   let rl = List.map (cl_trans_reg cl) reg.reg_regs in
   let r = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with
+    | Some its ->
+        create_region (id_clone reg.reg_name) its tl rl
+    | None -> begin match Mts.find_opt reg.reg_its.its_ts cl.ty_table with
     | Some {ity_node = Ityreg r} ->
         let sbs = its_match_regs reg.reg_its tl rl in
         let tl = List.map (ity_full_inst sbs) r.reg_args in
@@ -424,7 +432,8 @@ and cl_trans_reg cl reg =
         create_region (id_clone reg.reg_name) r.reg_its tl rl
     | Some _ -> assert false
     | None ->
-        create_region (id_clone reg.reg_name) reg.reg_its tl rl in
+        create_region (id_clone reg.reg_name) reg.reg_its tl rl
+    end in
   cl.rn_table <- Mreg.add reg r cl.rn_table;
   r
 
@@ -521,9 +530,14 @@ let clone_decl inst cl uc d = match d.d_node with
       let d = create_prop_decl k' pr' (cl_trans_fmla cl f) in
       add_pdecl ~vc:false uc (create_pure_decl d)
 
+let clone_type_decl _inst _cl _tdl = assert false
 let clone_pdecl inst cl uc d = match d.pd_node with
-  | PDtype _tdl -> assert false (* TODO *)
-  | PDlet _ld -> assert false (* TODO *)
+  | PDtype tdl ->
+      let tdl = clone_type_decl inst cl tdl in
+      if tdl = [] then uc else
+      add_pdecl ~vc:false uc (create_type_decl tdl)
+  | PDlet _ld ->
+      assert false (* TODO *)
   | PDexn xs ->
       let ity = cl_trans_ity cl xs.xs_ity in
       let xs' = create_xsymbol (id_clone xs.xs_name) ity in
@@ -535,10 +549,13 @@ let clone_pdecl inst cl uc d = match d.pd_node with
 let theory_add_clone = Theory.add_clone_internal ()
 
 let add_clone uc mi =
-  let tuc = theory_add_clone uc.muc_theory mi.mi_mod.mod_theory
-              (Mts.map ty_of_ity mi.mi_ts) mi.mi_ls mi.mi_pr in
+  let sm = {
+    sm_ty = Mts.map ty_of_ity mi.mi_ty;
+    sm_ts = Mts.map (fun s -> s.its_ts) mi.mi_ts;
+    sm_ls = mi.mi_ls;
+    sm_pr = mi.mi_pr } in
   { uc with
-      muc_theory = tuc;
+      muc_theory = theory_add_clone uc.muc_theory mi.mi_mod.mod_theory sm;
       muc_units  = Uclone mi :: uc.muc_units }
 
 let clone_export uc m inst =
@@ -553,7 +570,8 @@ let clone_export uc m inst =
     | Uuse m -> use_export uc m
     | Uclone mi ->
         begin try add_clone uc { mi_mod = mi.mi_mod;
-          mi_ts = Mts.map (cl_trans_ity cl) mi.mi_ts;
+          mi_ty = Mts.map (cl_trans_ity cl) mi.mi_ty;
+          mi_ts = Mts.map (cl_find_its cl) mi.mi_ts;
           mi_ls = Mls.map (cl_find_ls cl) mi.mi_ls;
           mi_pr = Mpr.map (cl_find_pr cl) mi.mi_pr;
           mi_pv = Mpv.map (cl_find_pv cl) mi.mi_pv;
@@ -575,6 +593,7 @@ let clone_export uc m inst =
   let uc = List.fold_left add_unit uc m.mod_units in
   let mi = {
     mi_mod = m;
+    mi_ty  = cl.ty_table;
     mi_ts  = cl.ts_table;
     mi_ls  = cl.ls_table;
     mi_pr  = cl.pr_table;

src/mlw/pmodule.mli

@@ -60,9 +60,10 @@ and mod_unit =
   | Umeta  of meta * meta_arg list
   | Uscope of string * bool * mod_unit list
 
-and mod_inst = private {
+and mod_inst = {
   mi_mod : pmodule;
-  mi_ts  : ity Mts.t;
+  mi_ty  : ity Mts.t;
+  mi_ts  : itysymbol Mts.t;
   mi_ls  : lsymbol Mls.t;
   mi_pr  : prsymbol Mpr.t;
   mi_pv  : pvsymbol Mpv.t;

src/parser/typing.ml

@@ -981,17 +981,30 @@ let type_inst ({muc_theory = tuc} as _muc) {mod_theory = t} s =
     | CStsym (p,[],PTtyapp (q,[])) ->
         let ts1 = find_tysymbol_ns t.th_export p in
         let ts2 = find_tysymbol tuc q in
-        let ty2 = ty_app ts2 (List.map ty_var ts1.ts_args) in
+        if Mts.mem ts1 s.inst_ty then Loc.error ~loc:(qloc p)
+          (ClashSymbol ts1.ts_name.id_string);
         { s with inst_ts = Loc.try4 ~loc:(qloc p) Mts.add_new
-            (ClashSymbol ts1.ts_name.id_string) ts1 ty2 s.inst_ts }
+            (ClashSymbol ts1.ts_name.id_string) ts1 ts2 s.inst_ts }
     | CStsym (p,tvl,pty) ->
         let ts1 = find_tysymbol_ns t.th_export p in
         let tvl = List.map (fun id -> tv_of_string id.id_str) tvl in
         let ts2 = Loc.try3 ~loc:(qloc p) create_tysymbol
           (id_clone ts1.ts_name) tvl (Some (ty_of_pty tuc pty)) in
         let ty2 = ty_app ts2 (List.map ty_var ts1.ts_args) in
-        { s with inst_ts = Loc.try4 ~loc:(qloc p) Mts.add_new
-            (ClashSymbol ts1.ts_name.id_string) ts1 ty2 s.inst_ts }
+        let check v ty = match ty.ty_node with
+          | Tyvar u -> tv_equal u v | _ -> false in
+        begin match ty2.ty_node with
+        | Tyapp (ts2, tyl) when Lists.equal check tvl tyl ->
+            if Mts.mem ts1 s.inst_ty then Loc.error ~loc:(qloc p)
+              (ClashSymbol ts1.ts_name.id_string);
+            { s with inst_ts = Loc.try4 ~loc:(qloc p) Mts.add_new
+                (ClashSymbol ts1.ts_name.id_string) ts1 ts2 s.inst_ts }
+        | _ ->
+            if Mts.mem ts1 s.inst_ts then Loc.error ~loc:(qloc p)
+              (ClashSymbol ts1.ts_name.id_string);
+            { s with inst_ty = Loc.try4 ~loc:(qloc p) Mts.add_new
+                (ClashSymbol ts1.ts_name.id_string) ts1 ty2 s.inst_ty }
+        end
     | CSfsym (p,q) ->
         let ls1 = find_fsymbol_ns t.th_export p in
         let ls2 = find_fsymbol tuc q in

src/printer/why3printer.ml

@@ -342,11 +342,14 @@ let print_decl fmt d = match d.d_node with
   | Dind (s, il) -> print_list_next nothing (print_ind_decl s) fmt il
   | Dprop p   -> print_prop_decl fmt p
 
-let print_inst_ts fmt (ts1,ty2) =
+let print_inst_ty fmt (ts1,ty2) =
   fprintf fmt "type %a%a = %a" print_ts ts1
     (print_list_pre space print_tv) ts1.ts_args
     print_ty ty2; forget_tvs ()
 
+let print_inst_ts fmt (ts1,ts2) =
+  fprintf fmt "type %a = %a" print_ts ts1 print_ts ts2
+
 let print_inst_ls fmt (ls1,ls2) =
   fprintf fmt "%s %a = %a" (ls_kind ls1) print_ls ls1 print_ls ls2
 
@@ -374,12 +377,14 @@ let print_tdecl fmt td = match td.td_node with
       fprintf fmt "@[<hov 2>(* use %a *)@]@\n@\n" print_qt th
   | Clone (th,sm) ->
       let tm = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ts [] in
+      let ym = Mts.fold (fun x y a -> (x,y)::a) sm.sm_ty [] in
       let lm = Mls.fold (fun x y a -> (x,y)::a) sm.sm_ls [] in
       let pm = Mpr.fold (fun x y a -> (x,y)::a) sm.sm_pr [] in
-      fprintf fmt "@[<hov 2>(* clone %a with %a,@ %a,@ %a *)@]@\n@\n"
-        print_qt th (print_list comma print_inst_ts) tm
-                    (print_list comma print_inst_ls) lm
-                    (print_list comma print_inst_pr) pm
+      fprintf fmt "@[<hov 2>(* clone %a with %a%a%a%a *)@]"
+        print_qt th (print_list_suf comma print_inst_ts) tm
+                    (print_list_suf comma print_inst_ty) ym
+                    (print_list_suf comma print_inst_ls) lm
+                    (print_list_suf comma print_inst_pr) pm
   | Meta (m,al) ->
       fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
         m.meta_name (print_list comma print_meta_arg) al