Revert "Ity: give every region a vsymbol to use in VCs"

This reverts commit e368d43a.

src/mlw/dexpr.ml

@@ -256,7 +256,7 @@ let rec print_dity pur pri fmt = function
   | Dvar {contents = Dsim (d,_)} ->
       Format.fprintf fmt "[%a]" (print_dity true 0) d
   | Dvar {contents = Dreg (Dapp (s,tl,rl),{tv_name = id})}
-  | Durg (Dapp (s,tl,rl),{reg_vs = {vs_name = id}}) ->
+  | Durg (Dapp (s,tl,rl),{reg_name = id}) ->
       Format.fprintf fmt
         (protect_on (pri > 1 && (tl <> [] || rl <> [])) "%a%a%a@ @@%s")
         Pretty.print_ts s.its_ts (print_args (print_dity pur 2)) tl

src/mlw/ity.ml

@@ -49,7 +49,7 @@ and ity_node =
     (** type variable and its purity status *)
 
 and region = {
-  reg_vs   : vsymbol;
+  reg_name : ident;
   reg_its  : itysymbol;
   reg_args : ity list;
   reg_regs : ity list;
@@ -73,7 +73,7 @@ end)
 
 module Reg = MakeMSHW (struct
   type t = region
-  let tag reg = reg.reg_vs.vs_name.id_tag
+  let tag reg = reg.reg_name.id_tag
 end)
 
 module PVsym = MakeMSHW (struct
@@ -110,12 +110,12 @@ let pv_equal  : pvsymbol  -> pvsymbol  -> bool = (==)
 
 let its_hash its = id_hash its.its_ts.ts_name
 let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
-let reg_hash reg = id_hash reg.reg_vs.vs_name
+let reg_hash reg = id_hash reg.reg_name
 let pv_hash  pv  = id_hash pv.pv_vs.vs_name
 
 let its_compare its1 its2 = id_compare its1.its_ts.ts_name its2.its_ts.ts_name
 let ity_compare ity1 ity2 = Pervasives.compare (ity_hash ity1) (ity_hash ity2)
-let reg_compare reg1 reg2 = id_compare reg1.reg_vs.vs_name reg2.reg_vs.vs_name
+let reg_compare reg1 reg2 = id_compare reg1.reg_name reg2.reg_name
 let pv_compare  pv1  pv2  = id_compare pv1.pv_vs.vs_name pv2.pv_vs.vs_name
 
 module Hsity = Hashcons.Make (struct
@@ -156,8 +156,8 @@ let mk_ity node = {
   ity_tag  = Weakhtbl.dummy_tag;
 }
 
-let mk_reg v s tl rl = {
-  reg_vs   = v;
+let mk_reg name s tl rl = {
+  reg_name = id_register name;
   reg_its  = s;
   reg_args = tl;
   reg_regs = rl;
@@ -193,10 +193,6 @@ let rec ty_of_ity ity = match ity.ity_node with
       ty_app s.its_ts (List.map ty_of_ity tl)
   | Ityvar (v,_) -> ty_var v
 
-let mk_reg id s tl rl =
-  let ty = ty_app s.its_ts (List.map ty_of_ity tl) in
-  mk_reg (create_vsymbol id ty) s tl rl
-
 (* generic traversal functions *)
 
 let dfold fn acc l1 l2 =
@@ -511,7 +507,7 @@ let its_inst_regs fresh_reg s tl =
     try sbs, Mreg.find r sbs.isb_reg with Not_found ->
     let sbs, tl = Lists.map_fold_left ity_inst sbs r.reg_args in
     let sbs, rl = Lists.map_fold_left ity_inst sbs r.reg_regs in
-    let ity = fresh_reg r.reg_vs.vs_name r.reg_its tl rl in
+    let ity = fresh_reg (id_clone r.reg_name) r.reg_its tl rl in
     { sbs with isb_reg = Mreg.add r ity sbs.isb_reg }, ity in
   Lists.map_fold_left reg_inst (its_match_args s tl) s.its_regions
 
@@ -522,12 +518,12 @@ let its_match_smart fresh_reg s tl rl =
   else its_inst_regs fresh_reg s tl
 
 let create_region id s tl rl =
-  let fresh id s tl rl = ity_reg (mk_reg (id_clone id) s tl rl) in
+  let fresh id s tl rl = ity_reg (mk_reg id s tl rl) in
   let sbs, rl = its_match_smart fresh s tl rl in
   create_region_raw sbs id s tl rl
 
 let ity_app s tl rl =
-  let fresh id s tl rl = ity_reg (mk_reg (id_clone id) s tl rl) in
+  let fresh id s tl rl = ity_reg (mk_reg id s tl rl) in
   let sbs, rl = its_match_smart fresh s tl rl in
   ity_app_raw sbs (id_fresh "rho") s tl rl
 
@@ -1289,10 +1285,10 @@ let rprinter = create_ident_printer []
 let xprinter = create_ident_printer []
   ~sanitizer:(sanitizer char_to_ualpha char_to_alnumus)
 
-let forget_reg r = forget_id rprinter r.reg_vs.vs_name
+let forget_reg r = forget_id rprinter r.reg_name
 
 let print_reg_name fmt r =
-  fprintf fmt "@@%s" (id_unique rprinter r.reg_vs.vs_name)
+  fprintf fmt "@@%s" (id_unique rprinter r.reg_name)
 
 let print_args pr fmt tl = if tl <> [] then
   fprintf fmt "@ %a" (Pp.print_list Pp.space pr) tl

src/mlw/ity.mli

@@ -48,7 +48,7 @@ and ity_node = private
     (** type variable and its purity status *)
 
 and region = private {
-  reg_vs   : vsymbol;
+  reg_name : ident;
   reg_its  : itysymbol;
   reg_args : ity list;
   reg_regs : ity list;

src/mlw/pmodule.ml

@@ -415,20 +415,21 @@ and clone_reg cl reg =
      with all top-level pvsymbols (local or external) before
      descending into a let_defn. *)
   try Mreg.find reg cl.rn_table with Not_found ->
-  let id = id_clone reg.reg_vs.vs_name in
   let tl = List.map (clone_ity cl) reg.reg_args in
   let rl = List.map (clone_ity 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 its tl rl
+    | Some its ->
+        create_region (id_clone reg.reg_name) its tl rl
     | None -> (* creative indentation *)
     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
         let rl = List.map (ity_full_inst sbs) r.reg_regs in
-        create_region id r.reg_its tl rl
+        create_region (id_clone reg.reg_name) r.reg_its tl rl
     | Some _ -> assert false
-    | None -> create_region id reg.reg_its tl rl
+    | None ->
+        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

src/mlw/vc.ml

@@ -59,7 +59,7 @@ let name_regions kn wr mvs =
   let mreg = Mvs.fold fill mvs Mreg.empty in
   let complete r nm _ = if nm <> None then nm else
     let ty = ty_app r.reg_its.its_ts (List.map ty_of_ity r.reg_args) in
-    Some (t_var (create_vsymbol (id_clone r.reg_vs.vs_name) ty)) in
+    Some (t_var (create_vsymbol (id_clone r.reg_name) ty)) in
   Mreg.merge complete mreg aff
 
 let rec havoc kn wr mreg t ity =