whyml: forcefully reset fresh regions

TODO

@@ -5,12 +5,6 @@ WhyML
     "false" would be a poor choice, as it could introduce inconsistency
     in the WPs of the caller. Should we allow unhandled exceptions at all?
 
-  - should we produce the WPs for the modules loaded from loadpath?
-
-  - should the API ensure that every psymbol resets the new regions?
-    Should they be always reset at the last arrow? What if they are
-    already reset at some earlier arrows, should we reset them again?
-
   - current WP does not respect the lexical scope. In the program
 
       let r = create 0 in

src/whyml/mlw_decl.ml

@@ -131,15 +131,15 @@ let create_data_decl tdl =
     let vtvs = List.map (fun (pv,_) -> pv.pv_vtv) al in
     let tvs = List.fold_right Stv.add its.its_args Stv.empty in
     let regs = List.fold_right Sreg.add its.its_regs Sreg.empty in
-    let check_tv tv =
-      if not (Stv.mem tv tvs) then raise (UnboundTypeVar tv); true in
-    let check_reg r =
-      if not (Sreg.mem r regs) then raise (UnboundRegion r); true in
+    let check_vars { vars_tv = atvs; vars_reg = aregs } =
+      if not (Stv.subset atvs tvs) then
+        raise (UnboundTypeVar (Stv.choose (Stv.diff atvs tvs)));
+      if not (Sreg.subset aregs regs) then
+        raise (UnboundRegion (Sreg.choose (Sreg.diff aregs regs))) in
     let check_arg vtv = match vtv.vtv_mut with
-      | None -> ity_v_all check_tv check_reg vtv.vtv_ity
-      | Some r -> check_reg r
-    in
-    ignore (List.for_all check_arg vtvs);
+      | Some r -> if not (Sreg.mem r regs) then raise (UnboundRegion r)
+      | None -> check_vars vtv.vtv_ity.ity_vars in
+    List.iter check_arg vtvs;
     (* build the constructor ps *)
     let hidden = its.its_abst in
     let rdonly = its.its_priv in
@@ -179,10 +179,9 @@ let letvar_news = function
   | LetA ps -> check_vars ps.ps_vars; Sid.singleton ps.ps_name
 
 let new_regs old_vars news vars =
-  let rec add_reg r acc = add_regs r.reg_ity.ity_vars.vars_reg acc
-  and add_regs regs acc = Sreg.fold add_reg regs (Sreg.union regs acc) in
-  let old_regs = add_regs old_vars.vars_reg Sreg.empty in
-  let regs = add_regs vars.vars_reg Sreg.empty in
+  let on_reg r acc = Sreg.union r.reg_ity.ity_vars.vars_reg acc in
+  let old_regs = reg_fold on_reg old_vars old_vars.vars_reg in
+  let regs = reg_fold on_reg vars vars.vars_reg in
   let regs = Sreg.diff regs old_regs in
   Sreg.fold (fun r s -> news_id s r.reg_name) regs news
 

src/whyml/mlw_expr.ml

@@ -394,6 +394,13 @@ let eff_check vars result e =
     let reset = reset (vars_union vars (vty_vars result)) in
     Mreg.iter reset e.eff_resets
 
+let vtv_check vars eff vtv =
+  let on_reg r =
+    if not (reg_occurs r vars) &&
+      (try Mreg.find r eff.eff_resets <> None with Not_found -> true)
+    then Loc.errorm "every fresh region in the result must be reset" in
+  reg_iter on_reg vtv.vtv_ity.ity_vars
+
 let rec vta_check vars vta =
   let add_arg vars pv = vars_union vars pv.pv_vars in
   let vars = List.fold_left add_arg vars vta.vta_args in
@@ -402,7 +409,7 @@ let rec vta_check vars vta =
   eff_check vars vta.vta_result vta.vta_spec.c_effect;
   match vta.vta_result with
   | VTarrow a -> vta_check vars a
-  | VTvalue _ -> ()
+  | VTvalue v -> vtv_check vars vta.vta_spec.c_effect v
 
 let create_psymbol id vta =
   let ps = create_psymbol_poly id vta (vta_varmap vta) in
@@ -524,7 +531,7 @@ let check_reset e varm =
       let rec check_reg reg =
         reg_equal r reg || match u with
           | Some u when reg_equal u reg -> false
-          | _ -> ity_v_any Util.ffalse check_reg reg.reg_ity
+          | _ -> Sreg.exists check_reg reg.reg_ity.ity_vars.vars_reg
       in
       if Sreg.exists check_reg s.vars_reg then
         Loc.error ?loc:e.e_loc (StaleRegion (e,r,id))

src/whyml/mlw_ty.ml

@@ -137,10 +137,6 @@ let create_varset tvs regs = {
   vars_reg = regs;
 }
 
-let rec reg_occurs r vars =
-  let check r r' = reg_equal r r' || reg_occurs r r'.reg_ity.ity_vars in
-  Sreg.exists (check r) vars.vars_reg
-
 (* value type symbols *)
 
 module Itsym = WeakStructMake (struct
@@ -260,26 +256,30 @@ let rec ity_v_map fnv fnr ity = match ity.ity_node with
   | Ityapp (f,tl,rl) ->
       ity_app_unsafe f (List.map (ity_v_map fnv fnr) tl) (List.map fnr rl)
 
-let rec ity_v_fold fnv fnr acc ity = match ity.ity_node with
-  | Ityvar v ->
-      fnv acc v
-  | Itypur (_,tl) ->
-      List.fold_left (ity_v_fold fnv fnr) acc tl
-  | Ityapp (_,tl,rl) ->
-      List.fold_left (ity_v_fold fnv fnr) (List.fold_left fnr acc rl) tl
-
-let ity_v_all prv prr ity =
-  try ity_v_fold (all_fn prv) (all_fn prr) true ity with FoldSkip -> false
-
-let ity_v_any prv prr ity =
-  try ity_v_fold (any_fn prv) (any_fn prr) false ity with FoldSkip -> true
-
 let ity_subst_unsafe mv mr ity =
   ity_v_map (fun v -> Mtv.find v mv) (fun r -> Mreg.find r mr) ity
 
 let ity_closed ity = Stv.is_empty ity.ity_vars.vars_tv
 let ity_pure ity = Sreg.is_empty ity.ity_vars.vars_reg
 
+let rec reg_fold fn vars acc =
+  let on_reg r acc = reg_fold fn r.reg_ity.ity_vars (fn r acc) in
+  Sreg.fold on_reg vars.vars_reg acc
+
+let rec reg_all fn vars =
+  let on_reg r = fn r && reg_all fn r.reg_ity.ity_vars in
+  Sreg.for_all on_reg vars.vars_reg
+
+let rec reg_any fn vars =
+  let on_reg r = fn r || reg_any fn r.reg_ity.ity_vars in
+  Sreg.exists on_reg vars.vars_reg
+
+let rec reg_iter fn vars =
+  let rec on_reg r = fn r; reg_iter fn r.reg_ity.ity_vars in
+  Sreg.iter on_reg vars.vars_reg
+
+let reg_occurs r vars = reg_any (reg_equal r) vars
+
 (* smart constructors *)
 
 exception BadItyArity of itysymbol * int * int
@@ -450,11 +450,13 @@ let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
   (* all type variables *)
   let sargs = List.fold_right Stv.add args Stv.empty in
   (* all type variables in [regs] must be in [args] *)
-  let check tv = Stv.mem tv sargs || raise (UnboundTypeVar tv) in
-  List.iter (fun r -> ignore (ity_v_all check Util.ttrue r.reg_ity)) regs;
+  let check dtvs = if not (Stv.subset dtvs sargs) then
+    raise (UnboundTypeVar (Stv.choose (Stv.diff dtvs sargs))) in
+  List.iter (fun r -> check r.reg_ity.ity_vars.vars_tv) regs;
   (* all regions in [def] must be in [regs] *)
-  let check r = Sreg.mem r sregs || raise (UnboundRegion r) in
-  ignore (option_map (ity_v_all Util.ttrue check) def);
+  let check dregs = if not (Sreg.subset dregs sregs) then
+    raise (UnboundRegion (Sreg.choose (Sreg.diff dregs sregs))) in
+  Util.option_iter (fun d -> check d.ity_vars.vars_reg) def;
   (* if a type is an alias then it cannot be abstract or private *)
   if abst && def <> None then Loc.errorm "A type alias cannot be abstract";
   if priv && def <> None then Loc.errorm "A type alias cannot be private";
@@ -951,6 +953,13 @@ let rec vta_filter varm vars vta =
     let rst = (eff_filter vars rst).eff_resets in
     let eff = { spec.c_effect with eff_resets = rst } in
     { spec with c_effect = eff } in
+  (* we must also reset every fresh region in the value *)
+  let spec = match vta.vta_result with
+    | VTvalue v ->
+        let on_reg r e = if reg_occurs r vars then e else eff_reset e r in
+        let eff = reg_fold on_reg v.vtv_ity.ity_vars spec.c_effect in
+        { spec with c_effect = eff }
+    | VTarrow _ -> spec in
   vty_arrow_unsafe vta.vta_args ~ghost:vta.vta_ghost ~spec vty
 
 let vta_filter varm vta =

src/whyml/mlw_ty.mli

@@ -88,8 +88,6 @@ val ity_hash : ity -> int
 val reg_equal : region -> region -> bool
 val reg_hash : region -> int
 
-val reg_occurs : region -> varset -> bool
-
 exception BadItyArity of itysymbol * int * int
 exception BadRegArity of itysymbol * int * int
 exception DuplicateRegion of region
@@ -133,16 +131,21 @@ val its_clone : Theory.symbol_map -> itysymbol Mits.t * region Mreg.t
 
 val ity_v_map : (tvsymbol -> ity) -> (region -> region) -> ity -> ity
 
-val ity_v_fold :
-  ('a -> tvsymbol -> 'a) -> ('a -> region -> 'a) -> 'a -> ity -> 'a
-
-val ity_v_all : (tvsymbol -> bool) -> (region -> bool) -> ity -> bool
-val ity_v_any : (tvsymbol -> bool) -> (region -> bool) -> ity -> bool
-
 val ity_closed : ity -> bool
 val ity_pure : ity -> bool
 
-val ts_unit : tysymbol
+(* these functions attend the sub-regions *)
+
+val reg_fold : (region -> 'a -> 'a) -> varset -> 'a -> 'a
+val reg_any  : (region -> bool) -> varset -> bool
+val reg_all  : (region -> bool) -> varset -> bool
+val reg_iter : (region -> unit) -> varset -> unit
+
+val reg_occurs : region -> varset -> bool
+
+(* built-in types *)
+
+val ts_unit : tysymbol (* the same as [Ty.ts_tuple 0] *)
 val ty_unit : ty
 
 val ity_int : ity

src/whyml/mlw_typing.ml

@@ -807,18 +807,14 @@ let rec type_c lenv gh svs vars dtyc =
   (* reset every new region in the result *)
   let eff = match vty with
     | VTvalue v ->
-        let rec add_reg r eff =
-          if reg_occurs r vars then eff else eff_reset (add_ity r.reg_ity eff) r
-        and add_ity ity eff = Sreg.fold add_reg ity.ity_vars.vars_reg eff in
-        add_ity v.vtv_ity eff
+        let on_reg r e = if reg_occurs r vars then e else eff_reset e r in
+        reg_fold on_reg v.vtv_ity.ity_vars 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 on_reg r e = if Sreg.mem r writes then e else eff_refresh e r u in
+    reg_fold on_reg u.reg_ity.ity_vars eff in
   let eff = Sreg.fold check writes eff in
   (* create the spec *)
   let spec = {
@@ -1148,7 +1144,7 @@ let add_types ~wp uc tdl =
       let d = Mstr.find x def in
       let add_tv acc id =
         let e = Loc.Located (id.id_loc, DuplicateTypeVar id.id) in
-        let tv = create_tvsymbol (Denv.create_user_id id) in
+        let tv = Typing.create_user_tv id.id in
         Mstr.add_new e id.id tv acc in
       let vars = List.fold_left add_tv Mstr.empty d.td_params in
       let vl = List.map (fun id -> Mstr.find id.id vars) d.td_params in