whyml: refresh unmodified subregions in abstract parameters

TODO

@@ -11,10 +11,6 @@ WhyML
     Should they be always reset at the last arrow? What if they are
     already reset at some earlier arrows, should we reset them again?
 
-  - in "val" and "any", when a region rho is written into, but some
-    subregion rho' of rho is not, should we reset rho' under rho?
-    In Mlw_typing or in Mlw_expr?
-
   - current WP does not respect the lexical scope. In the program
 
       let r = create 0 in

src/whyml/mlw_pretty.ml

@@ -116,7 +116,7 @@ let print_effect fmt eff =
   let print_reset r = function
     | None -> print_reg "fresh" r
     | Some u ->
-        fprintf fmt "{reset %a@ under %a}@ " print_regty r print_regty u
+        fprintf fmt "{refresh %a@ under %a}@ " print_regty r print_regty u
   in
   Sreg.iter (print_reg "read") eff.eff_reads;
   Sreg.iter (print_reg "write") eff.eff_writes;

src/whyml/mlw_ty.ml

@@ -520,8 +520,13 @@ let eff_is_empty e =
   Sexn.is_empty e.eff_ghostx &&
   Mreg.is_empty e.eff_resets
 
-let join_reset _key v1 v2 =
-  Some (if option_eq reg_equal v1 v2 then v1 else None)
+let join_reset _key v1 v2 = match v1, v2 with
+  | Some r1, Some r2 ->
+      if reg_equal r1 r2 then Some v1 else
+      if reg_occurs r1 r2.reg_ity.ity_vars then Some v2 else
+      if reg_occurs r2 r1.reg_ity.ity_vars then Some v1 else
+      Some None
+  | _ -> Some None
 
 let eff_union x y = {
   eff_reads  = Sreg.union x.eff_reads  y.eff_reads;
@@ -559,6 +564,12 @@ let eff_reset e r = { e with eff_resets = Mreg.add r None e.eff_resets }
 
 exception IllegalAlias of region
 
+let eff_refresh e r u =
+  if not (reg_occurs r u.reg_ity.ity_vars) then
+    invalid_arg "Mlw_ty.eff_refresh";
+  let reset = Mreg.singleton r (Some u) in
+  { e with eff_resets = Mreg.union join_reset e.eff_resets reset }
+
 let eff_assign e ?(ghost=false) r ty =
   let e = eff_write e ~ghost r in
   let sub = ity_match ity_subst_empty r.reg_ity ty in

src/whyml/mlw_ty.mli

@@ -217,6 +217,7 @@ val eff_write : effect -> ?ghost:bool -> region -> effect
 val eff_raise : effect -> ?ghost:bool -> xsymbol -> effect
 val eff_reset : effect -> region -> effect
 
+val eff_refresh : effect -> region -> region -> effect
 val eff_assign : effect -> ?ghost:bool -> region -> ity -> effect
 
 val eff_remove_raise : effect -> xsymbol -> effect

src/whyml/mlw_typing.ml

@@ -817,6 +817,15 @@ let rec type_c lenv gh svs vars dtyc =
         and add_ity ity eff = Sreg.fold add_reg ity.ity_vars.vars_reg eff in
         add_ity v.vtv_ity eff
     | VTarrow _ -> eff in
+  (* refresh every unmodified subregion of a modified region *)
+  let writes = Sreg.union eff.eff_writes eff.eff_ghostw in
+  let check u eff =
+    let rec sub_reg r eff =
+      if Sreg.mem r writes then eff else sub_vars r (eff_refresh eff r u)
+    and sub_vars r eff = Sreg.fold sub_reg r.reg_ity.ity_vars.vars_reg eff in
+    sub_vars u eff in
+  let eff = Sreg.fold check writes eff in
+  (* create the spec *)
   let spec = {
     c_pre     = create_pre lenv dtyc.dc_pre;
     c_effect  = eff;