better names for region variables in singleton mutable types

src/programs/pgm_typing.ml

@@ -1196,21 +1196,18 @@ let declare_global ls pv =
   Pgm_wp.declare_global_regions pv;
   Hls.add globals ls pv
 
-let rec fmla_effect ef f =
-  TermTF.t_map_fold term_effect fmla_effect ef f
-
-and term_effect ef t = match t.t_node with
+let rec term_effect ef t = match t.t_node with
   | Term.Tapp (ls, []) when Hls.mem globals ls ->
       let pv = Hls.find globals ls in
       E.add_glob pv ef, t_var pv.pv_pure
   | _ ->
-      TermTF.t_map_fold term_effect fmla_effect ef t
+      t_map_fold term_effect ef t
 
 let post_effect ef ((v, q), ql) =
   let exn_effect ef (e, (x, q)) =
-    let ef, q = fmla_effect ef q in ef, (e, (x, q))
+    let ef, q = term_effect ef q in ef, (e, (x, q))
   in
-  let ef, q = fmla_effect ef q in
+  let ef, q = term_effect ef q in
   let ef, ql = map_fold_left exn_effect ef ql in
   ef, ((v, q), ql)
 (* TODO? *)
@@ -1254,7 +1251,7 @@ let rec type_v env = function
 
 and type_c env c =
   let ef = effect c.ic_effect in
-  let ef, p = fmla_effect ef c.ic_pre in
+  let ef, p = term_effect ef c.ic_pre in
   let ef, q = post_effect ef c.ic_post in
   (* saturate effect with exceptions appearing in q *)
   let ef = List.fold_left (fun ef (e, _) -> E.add_raise e ef) ef (snd q) in
@@ -1456,7 +1453,7 @@ and expr_desc gl env loc ty = function
   | IEloop (a, e1) ->
       let e1 = expr gl env e1 in
       let ef = e1.expr_effect in
-      let ef, inv = option_map_fold fmla_effect ef a.loop_invariant in
+      let ef, inv = option_map_fold term_effect ef a.loop_invariant in
       let ef, var = match a.loop_variant with
         | Some (t, ls) -> let ef, t = term_effect ef t in ef, Some (t, ls)
         | None         -> ef, None
@@ -1532,11 +1529,11 @@ and expr_desc gl env loc ty = function
       let env, x = add_local env x (tpure v1.pv_pure.vs_ty) in
       let e3 = expr gl env e3 in
       let ef = e3.expr_effect in
-      let ef, inv = option_map_fold fmla_effect ef inv in
+      let ef, inv = option_map_fold term_effect ef inv in
       Efor (x, v1, d, v2, inv, e3), type_v_unit gl, ef
 
   | IEassert (k, f) ->
-      let ef, f = fmla_effect E.empty f in
+      let ef, f = term_effect E.empty f in
       Eassert (k, f), tpure ty, ef
   | IElabel (lab, e1) ->
       let e1 = expr gl env e1 in
@@ -1549,7 +1546,7 @@ and triple gl env (p, e, q) =
   let e = expr gl env e in
   let q = saturation e.expr_loc e.expr_effect q in
   let ef = e.expr_effect in
-  let ef, p = fmla_effect ef p in
+  let ef, p = term_effect ef p in
   let ef, q = post_effect ef q in
   (* eprintf "triple: p = %a ef = %a@." Pretty.print_fmla p E.print ef; *)
   let e = { e with expr_effect = ef } in

src/programs/pgm_wp.ml

@@ -91,7 +91,7 @@ let rec wp_forall env v f =
   match cl with
     | [ls] ->
         let s = ty_match Mtv.empty (of_option ls.ls_value) ty in
-        let mk_v ty = create_vsymbol (id_fresh "x") (ty_inst s ty) in
+        let mk_v ty = create_vsymbol (id_clone v.vs_name) (ty_inst s ty) in
         let vl = List.map mk_v ls.ls_args in
         let t = fs_app ls (List.map t_var vl) ty in
         List.fold_right (wp_forall env) vl (t_let_close_simp v t f)
@@ -267,22 +267,33 @@ let rec update env mreg x ty =
 *)
 let quantify env rm ef f =
   let sreg = ef.E.writes in
-  (* mreg: rho -> rho' *)
-  let mreg =
-    let add r m =
-      let r' = create_vsymbol (id_clone r.R.r_tv.tv_name) (purify r.R.r_ty) in
-      Mreg.add r r' m
-    in
-    Sreg.fold add sreg Mreg.empty
-  in
   (* all program variables involving these regions *)
   let vars =
-    let add r _ s =
+    let add r s =
       try Spv.union (Mreg.find r rm) s with Not_found -> assert false
     in
-    Mreg.fold add mreg Spv.empty
+    Sreg.fold add sreg Spv.empty
+  in
+  (* mreg: rho -> rho' *)
+  let mreg =
+    let add r m =
+      let vars = Mreg.find r rm in
+      let test x acc = match x.pv_effect.vs_ty.ty_node with
+        | Tyapp (ts,{ ty_node = Tyvar tv }::_) when tv_equal tv r.R.r_tv ->
+            let mt = get_mtsymbol ts in
+            if mt.mt_regions = 1 then
+              Some x.pv_effect.vs_name
+            else acc
+        | Tyapp _ -> acc
+        | Tyvar _ -> assert false
+      in
+      let id = Spv.fold test vars None in
+      let id = id_clone (default_option r.R.r_tv.tv_name id) in
+      let r' = create_vsymbol id (purify r.R.r_ty) in
+      Mtv.add r.R.r_tv r' m
+    in
+    Sreg.fold add sreg Mtv.empty
   in
-  let mreg = Mreg.fold (fun r x -> Mtv.add r.R.r_tv x) mreg Mtv.empty in
   (* s: v -> v' and vv': pv -> v', update_v *)
   (****
   let mreg, s, vv' =