whyml: fix cloning of letrec

src/whyml/mlw_expr.ml

@@ -323,6 +323,16 @@ type psymbol = {
   ps_subst : ity_subst;
 }
 
+module Psym = WeakStructMake (struct
+  type t = psymbol
+  let tag ps = ps.ps_name.id_tag
+end)
+
+module Sps = Psym.S
+module Mps = Psym.M
+module Hps = Psym.H
+module Wps = Psym.W
+
 let ps_equal : psymbol -> psymbol -> bool = (==)
 
 let create_psymbol_real ~poly id vta varm =
@@ -339,10 +349,15 @@ let create_psymbol_mono = create_psymbol_real ~poly:false
 
 (** specification *)
 
+let varmap_union = Mid.set_union
+
 let add_pv_vars pv m = Mid.add pv.pv_vs.vs_name pv.pv_vars m
 let add_vs_vars vs _ m = add_pv_vars (restore_pv vs) m
 let add_t_vars vss m = Mvs.fold add_vs_vars vss m
 
+let add_ps_vars ps m =
+  Mid.add ps.ps_name ps.ps_vars (varmap_union ps.ps_varm m)
+
 let pre_vars f vsset = Mvs.set_union vsset f.t_vars
 let post_vars f vsset = Mvs.set_union vsset f.t_vars
 let xpost_vars = Mexn.fold (fun _ -> post_vars)
@@ -394,6 +409,14 @@ let create_psymbol id vta =
   vta_check ps.ps_vars vta;
   ps
 
+let create_psymbol_extra id vta pvs pss =
+  let varm = vta_varmap vta in
+  let varm = Spv.fold add_pv_vars pvs varm in
+  let varm = Sps.fold add_ps_vars pss varm in
+  let ps = create_psymbol_poly id vta varm in
+  vta_check ps.ps_vars vta;
+  ps
+
 (** program expressions *)
 
 type assertion_kind = Aassert | Aassume | Acheck
@@ -483,7 +506,6 @@ let vta_of_expr e = match e.e_vty with
   | VTvalue _ -> Loc.error ?loc:e.e_loc (ArrowExpected e)
   | VTarrow vta -> vta
 
-let varmap_union = Mid.set_union
 let add_e_vars e m = varmap_union e.e_varm m
 
 (* check admissibility of consecutive events *)
@@ -541,8 +563,8 @@ let e_value pv =
   mk_expr (Evalue pv) (VTvalue pv.pv_vtv) eff_empty varm
 
 let e_arrow ps vta =
+  let varm = add_ps_vars ps Mid.empty in
   let sbs = vta_vars_match ps.ps_subst ps.ps_vta vta in
-  let varm = Mid.add ps.ps_name ps.ps_vars ps.ps_varm in
   let vta = vta_full_inst sbs ps.ps_vta in
   mk_expr (Earrow ps) (VTarrow vta) eff_empty varm
 

src/whyml/mlw_expr.mli

@@ -109,10 +109,17 @@ type psymbol = private {
      in ps_vars to itself *)
 }
 
+module Mps : Map.S with type key = psymbol
+module Sps : Mps.Set
+module Hps : Hashtbl.S with type key = psymbol
+module Wps : Hashweak.S with type key = psymbol
+
 val ps_equal : psymbol -> psymbol -> bool
 
 val create_psymbol : preid -> vty_arrow -> psymbol
 
+val create_psymbol_extra : preid -> vty_arrow -> Spv.t -> Sps.t -> psymbol
+
 (** program expressions *)
 
 type assertion_kind = Aassert | Aassume | Acheck

src/whyml/mlw_module.ml

@@ -446,39 +446,32 @@ let clone_export uc m inst =
         Hid.add psh ps.ps_name (PS nps);
         add_pdecl uc (create_val_decl (LetA nps))
     | PDrec { rec_defn = rdl } ->
-      (* FIXME: the resulting psymbols are as polymorphic as
-         their ps_vta allow them to be. If the definition body
-         brings in some external symbol S and fixes some region
-         in the psymbol's type, but S does not occur in the spec,
-         then the cloned psymbol will be overgeneralized.
-         Three fixes are possible:
-           1. Prohibit global regions in psymbol type signatures.
-              This is what previous implementation of WhyML did.
-           2. Let Mlw_expr.create_psymbol take an additional varmap
-              as an argument and add those variables to ps.ps_varm.
-              Can this be abused in any way?
-           3. Require that (vta_varmap ps.ps_vta) fixes exactly
-              the same regions as ps.ps_varm. At the moment, we
-              only have inclusion, since ps.ps_varm is guaranteed
-              to be a superset of (vta_varmap ps.ps_vta). If this
-              requirement is satisfied, we can always set ps_varm
-              to be the varmap of ps_vta. But what about resets?
-              Consider:
-                  let r <rho> = ref 0 in
-                  let f x = ... r <- x ... in
-                  { reset rho }
-                  f 5
-              The reference r appears in f.ps_varm, and thus the
-              last expression (f 5) would be rejected as freshness
-              violation. This is correct, otherwise the effect of
-              (f 5) could modify the values of unrelated variables.
-              This is correct even if r does not occur in f.ps_vta,
-              and therefore we cannot forget about r in f.ps_varm.
-              We could require that r appears in the spec of f, as
-              we do for abstract parameters, but is this reasonable? *)
+        let add_id id _ (pvs,pss) =
+          try match Hid.find psh id with
+            | PV pv -> Spv.add pv pvs, pss
+            | PS ps -> pvs, Sps.add ps pss
+            | _ -> assert false
+          with Not_found ->
+            let exn = Invalid_argument "Mlw_module.clone_export" in
+            begin match (Mid.find_exn exn id extras).pd_node with
+              | PDval (LetV pv) | PDlet { let_sym = LetV pv } ->
+                  Spv.add pv pvs, pss
+              | PDval (LetA ps) | PDlet { let_sym = LetA ps } ->
+                  pvs, Sps.add ps pss
+              | PDrec { rec_defn = rdl } ->
+                  let rec down = function
+                    | { fun_ps = ps }::_ when id_equal ps.ps_name id -> ps
+                    | _::rdl -> down rdl
+                    | [] -> assert false in
+                  pvs, Sps.add (down rdl) pss
+              | PDtype _ | PDdata _ | PDexn _ -> assert false
+            end in
         let conv_rd uc { fun_ps = ps } =
+          let id = id_clone ps.ps_name in
           let vta = conv_vta !mvs ps.ps_vta in
-          let nps = create_psymbol (id_clone ps.ps_name) vta in
+          (* we must retrieve all pvsymbols and psymbols in ps.ps_varm *)
+          let pvs,pss = Mid.fold add_id ps.ps_varm (Spv.empty,Sps.empty) in
+          let nps = create_psymbol_extra id vta pvs pss in
           Hid.add psh ps.ps_name (PS nps);
           add_pdecl uc (create_val_decl (LetA nps)) in
         List.fold_left conv_rd uc rdl