Ity: give every region a vsymbol to use in VCs

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_name = id}) ->
+  | Durg (Dapp (s,tl,rl),{reg_vs = {vs_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

@@ -46,7 +46,7 @@ and ity_node =
     (** type variable and its purity status *)
 
 and region = {
-  reg_name : ident;
+  reg_vs   : vsymbol;
   reg_its  : itysymbol;
   reg_args : ity list;
   reg_regs : ity list;
@@ -70,7 +70,7 @@ end)
 
 module Reg = MakeMSHW (struct
   type t = region
-  let tag reg = reg.reg_name.id_tag
+  let tag reg = reg.reg_vs.vs_name.id_tag
 end)
 
 module PVsym = MakeMSHW (struct
@@ -107,12 +107,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_name
+let reg_hash reg = id_hash reg.reg_vs.vs_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_name reg2.reg_name
+let reg_compare reg1 reg2 = id_compare reg1.reg_vs.vs_name reg2.reg_vs.vs_name
 let pv_compare  pv1  pv2  = id_compare pv1.pv_vs.vs_name pv2.pv_vs.vs_name
 
 exception NonUpdatable of itysymbol * ity
@@ -162,8 +162,8 @@ let mk_ity node = {
   ity_tag  = Weakhtbl.dummy_tag;
 }
 
-let mk_reg name s tl rl = {
-  reg_name = id_register name;
+let mk_reg v s tl rl = {
+  reg_vs   = v;
   reg_its  = s;
   reg_args = (check_its_args s tl; tl);
   reg_regs = rl;
@@ -201,6 +201,10 @@ 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 =
@@ -488,7 +492,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 (id_clone r.reg_name) r.reg_its tl rl in
+    let ity = fresh_reg r.reg_vs.vs_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
 
@@ -499,12 +503,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 s tl rl) in
+  let fresh id s tl rl = ity_reg (mk_reg (id_clone 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 s tl rl) in
+  let fresh id s tl rl = ity_reg (mk_reg (id_clone 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
 
@@ -1193,10 +1197,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_name
+let forget_reg r = forget_id rprinter r.reg_vs.vs_name
 
 let print_reg_name fmt r =
-  fprintf fmt "@@%s" (id_unique rprinter r.reg_name)
+  fprintf fmt "@@%s" (id_unique rprinter r.reg_vs.vs_name)
 
 let print_args pr fmt tl = if tl <> [] then
   fprintf fmt "@ %a" (Pp.print_list Pp.space pr) tl

src/mlw/ity.mli

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

src/mlw/pmodule.ml

@@ -423,21 +423,20 @@ 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_clone reg.reg_name) its tl rl
+    | Some its -> create_region id 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_clone reg.reg_name) r.reg_its tl rl
+        create_region id r.reg_its tl rl
     | Some _ -> assert false
-    | None ->
-        create_region (id_clone reg.reg_name) reg.reg_its tl rl
+    | None -> create_region id reg.reg_its tl rl
     end in
   cl.rn_table <- Mreg.add reg r cl.rn_table;
   r