whyml: several API simplifications

- get rid of val_decl, the psymbol/pvsymbol is enough
- get rid of vtv_vars, keep the varset in pvsymbol
- include fresh regions in pd_news (will serve for clone)

src/whyml/mlw_decl.ml

@@ -42,7 +42,7 @@ type pdecl = {
 and pdecl_node =
   | PDtype of itysymbol
   | PDdata of data_decl list
-  | PDval  of val_decl
+  | PDval  of let_sym
   | PDlet  of let_defn
   | PDrec  of rec_defn
   | PDexn  of xsymbol
@@ -175,11 +175,21 @@ let check_vars vars =
     raise (UnboundTypeVar (Stv.choose vars.vars_tv))
 
 let letvar_news = function
-  | LetV pv -> check_vars pv.pv_vtv.vtv_vars; Sid.singleton pv.pv_vs.vs_name
+  | LetV pv -> check_vars pv.pv_vars; Sid.singleton pv.pv_vs.vs_name
   | LetA ps -> check_vars ps.ps_vars; Sid.singleton ps.ps_name
 
+let rec new_regs old_vars news vars =
+  let add_reg r s =
+    let s = if reg_occurs r old_vars then s else Sid.add r.reg_name s in
+    new_regs old_vars s r.reg_ity.ity_vars in
+  Sreg.fold add_reg vars.vars_reg news
+
 let create_let_decl ld =
+  let vars = vars_merge ld.let_expr.e_varm vars_empty in
   let news = letvar_news ld.let_sym in
+  let news = match ld.let_sym with
+    | LetA ps -> new_regs vars news ps.ps_vars
+    | LetV pv -> new_regs vars news pv.pv_vars in
 (*
   let syms = syms_varmap Sid.empty ld.let_expr.e_vars in
   let syms = syms_effect syms ld.let_expr.e_effect in
@@ -189,7 +199,6 @@ let create_let_decl ld =
   mk_decl (PDlet ld) (*syms*) news
 
 let create_rec_decl ({ rec_defn = rdl } as d) =
-  if rdl = [] then raise Decl.EmptyDecl;
   let add_rd s { fun_ps = p } = check_vars p.ps_vars; news_id s p.ps_name in
   let news = List.fold_left add_rd Sid.empty rdl in
 (*
@@ -207,13 +216,18 @@ let create_rec_decl ({ rec_defn = rdl } as d) =
 *)
   mk_decl (PDrec d) (*syms*) news
 
-let create_val_decl vd =
-  let news = letvar_news vd.val_sym in
+let create_val_decl lv =
+  let news = letvar_news lv in
+  let news = match lv with
+    | LetV { pv_vtv = { vtv_mut = Some _ }} ->
+        Loc.errorm "abstract parameters cannot be mutable"
+    | LetV pv -> new_regs vars_empty news pv.pv_vars
+    | LetA _ -> news in
 (*
   let syms = syms_type_v Sid.empty vd.val_spec in
   let syms = syms_varmap syms vd.val_vars in
 *)
-  mk_decl (PDval vd) (*syms*) news
+  mk_decl (PDval lv) (*syms*) news
 
 let create_exn_decl xs =
   let news = Sid.singleton xs.xs_name in

src/whyml/mlw_decl.mli

@@ -43,7 +43,7 @@ type pdecl = private {
 and pdecl_node = private
   | PDtype of itysymbol
   | PDdata of data_decl list
-  | PDval  of val_decl
+  | PDval  of let_sym
   | PDlet  of let_defn
   | PDrec  of rec_defn
   | PDexn  of xsymbol
@@ -58,7 +58,7 @@ val create_data_decl : pre_data_decl list -> pdecl
 
 val create_ty_decl : itysymbol -> pdecl
 
-val create_val_decl : val_decl -> pdecl
+val create_val_decl : let_sym -> pdecl
 
 val create_let_decl : let_defn -> pdecl
 

src/whyml/mlw_expr.ml

@@ -48,9 +48,8 @@ let create_psymbol_real ~poly id vta varm =
     ps_vars  = vars;
     ps_subst = vars_freeze vars; }
 
-let create_psymbol_poly   = create_psymbol_real ~poly:true
-let create_psymbol_mono   = create_psymbol_real ~poly:false
-let create_psymbol id vta = create_psymbol_poly id vta Mid.empty
+let create_psymbol_poly = create_psymbol_real ~poly:true
+let create_psymbol_mono = create_psymbol_real ~poly:false
 
 (** program/logic symbols *)
 
@@ -96,16 +95,7 @@ exception RdOnlyPLS of lsymbol
 
 (** specification *)
 
-type let_sym =
-  | LetV of pvsymbol
-  | LetA of psymbol
-
-type val_decl = {
-  val_sym  : let_sym;
-  val_vty  : vty;
-}
-
-let add_pv_vars pv m = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_vars m
+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 pre_vars f vsset = Mvs.set_union vsset f.t_vars
@@ -124,15 +114,13 @@ let spec_varmap varm spec =
   Mvs.fold (fun vs _ m -> add_vs_vars vs m) vsset varm
 
 let rec vta_varmap vta =
-  let varm = vty_varmap vta.vta_result in
+  let varm = match vta.vta_result with
+    | VTarrow a -> vta_varmap a
+    | VTvalue _ -> Mid.empty in
   let varm = spec_varmap varm vta.vta_spec in
   let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
   List.fold_left del_pv varm vta.vta_args
 
-and vty_varmap = function
-  | VTarrow a -> vta_varmap a
-  | VTvalue _ -> Mid.empty
-
 let eff_check vars result e =
   let check vars r = if not (reg_occurs r vars) then
     Loc.errorm "every external effect must be mentioned in specification" in
@@ -147,28 +135,19 @@ let eff_check vars result e =
     Mreg.iter reset e.eff_resets
 
 let rec vta_check vars vta =
-  let add_arg vars pv = vars_union vars pv.pv_vtv.vtv_vars in
+  let add_arg vars pv = vars_union vars pv.pv_vars in
   let vars = List.fold_left add_arg vars vta.vta_args in
   if vta.vta_spec.c_variant <> [] || vta.vta_spec.c_letrec <> 0 then
     Loc.errorm "variants are not allowed in a parameter declaration";
   eff_check vars vta.vta_result vta.vta_spec.c_effect;
-  vty_check vars vta.vta_result
-
-and vty_check vars = function
+  match vta.vta_result with
   | VTarrow a -> vta_check vars a
-  | VTvalue v -> if v.vtv_mut <> None then
-      Loc.errorm "abstract parameters cannot produce mutable values"
-
-let create_val id vty = match vty with
-  | VTvalue v ->
-      let pv = create_pvsymbol id v in
-      vty_check vars_empty vty;
-      { val_sym = LetV pv; val_vty = vty }
-  | VTarrow a ->
-      let varm = vta_varmap a in
-      let ps = create_psymbol_poly id a varm in
-      vta_check ps.ps_vars a;
-      { val_sym = LetA ps; val_vty = vty }
+  | VTvalue _ -> ()
+
+let create_psymbol id vta =
+  let ps = create_psymbol_poly id vta (vta_varmap vta) in
+  vta_check ps.ps_vars vta;
+  ps
 
 (** patterns *)
 
@@ -351,6 +330,10 @@ type for_bounds = pvsymbol * for_direction * pvsymbol
 
 type invariant = term
 
+type let_sym =
+  | LetV of pvsymbol
+  | LetA of psymbol
+
 type expr = {
   e_node   : expr_node;
   e_vty    : vty;
@@ -532,7 +515,10 @@ let create_fun_defn id lam letrec recsyms =
   let varm = Mid.set_diff varm recsyms in
   let del_pv m pv = Mid.remove pv.pv_vs.vs_name m in
   let varm = List.fold_left del_pv varm lam.l_args in
-  let vta = vty_arrow lam.l_args ~spec e.e_vty in
+  let vty = match e.e_vty with
+    | VTvalue ({ vtv_mut = Some _ } as vtv) -> VTvalue (vtv_unmut vtv)
+    | vty -> vty in
+  let vta = vty_arrow lam.l_args ~spec vty in
   { fun_ps     = create_psymbol_poly id vta varm;
     fun_lambda = lam; }
 
@@ -702,14 +688,12 @@ let e_assign me e = on_value (e_assign_real me) e
 let e_ghost e =
   mk_expr (Eghost e) (vty_ghostify e.e_vty) e.e_effect e.e_varm
 
+let pv_dummy = create_pvsymbol (id_fresh "dummy") (vty_value ity_unit)
+
 let e_any spec vty =
-  let varm = spec_varmap (vty_varmap vty) spec in
-  let vars = vars_merge varm vars_empty in
-  spec_check spec vty;
-  if spec.c_variant <> [] || spec.c_letrec <> 0 then
-    Loc.errorm "variants are not allowed in a parameter declaration";
-  eff_check vars vty spec.c_effect;
-  vty_check vars vty;
+  let vta = vty_arrow [pv_dummy] ~spec vty in
+  let varm = vta_varmap vta in
+  vta_check (vars_merge varm vars_empty) vta;
   mk_expr (Eany spec) vty spec.c_effect varm
 
 let e_const t =

src/whyml/mlw_expr.mli

@@ -78,19 +78,6 @@ val create_plsymbol : ?hidden:bool -> ?rdonly:bool ->
 exception HiddenPLS of lsymbol
 exception RdOnlyPLS of lsymbol
 
-(** specification *)
-
-type let_sym =
-  | LetV of pvsymbol
-  | LetA of psymbol
-
-type val_decl = private {
-  val_sym  : let_sym;
-  val_vty  : vty;
-}
-
-val create_val : Ident.preid -> vty -> val_decl
-
 (** patterns *)
 
 type ppattern = private {
@@ -126,6 +113,10 @@ type for_bounds = pvsymbol * for_direction * pvsymbol
 
 type invariant = term
 
+type let_sym =
+  | LetV of pvsymbol
+  | LetA of psymbol
+
 type expr = private {
   e_node   : expr_node;
   e_vty    : vty;

src/whyml/mlw_module.ml

@@ -311,7 +311,7 @@ let add_pdecl uc d =
       let defn cl = List.map constructor cl in
       let dl = List.map (fun (its,cl) -> its.its_pure, defn cl) dl in
       add_to_theory Theory.add_data_decl uc dl
-  | PDval { val_sym = lv } | PDlet { let_sym = lv } ->
+  | PDval lv | PDlet { let_sym = lv } ->
       add_let uc lv
   | PDrec rdl ->
       List.fold_left add_rec uc rdl.rec_defn

src/whyml/mlw_pretty.ml

@@ -391,7 +391,9 @@ let print_data_decl fst fmt (ts,csl) =
     (print_head fst) ts (print_list newline print_constr) csl;
   forget_tvs_regs ()
 
-let print_val_decl fmt { val_sym = lv ; val_vty = vty } =
+let print_val_decl fmt lv =
+  let vty = match lv with
+    | LetV pv -> VTvalue pv.pv_vtv | LetA ps -> VTarrow ps.ps_vta in
   fprintf fmt "@[<hov 2>val (%a) :@ %a@]" print_lv lv print_type_v vty;
   (* FIXME: don't forget global regions *)
   forget_tvs_regs ()

src/whyml/mlw_ty.ml

@@ -726,31 +726,26 @@ type vty_value = {
   vtv_ity   : ity;
   vtv_ghost : bool;
   vtv_mut   : region option;
-  vtv_vars  : varset;
 }
 
 let vty_value ?(ghost=false) ?mut ity =
-  let vars = ity.ity_vars in
-  let vars = match mut with
-    | Some r ->
-        ity_equal_check ity r.reg_ity;
-        { vars with vars_reg = Sreg.add r vars.vars_reg }
-    | None ->
-        vars
-  in {
-    vtv_ity   = ity;
+  Util.option_iter (fun r -> ity_equal_check ity r.reg_ity) mut;
+  { vtv_ity   = ity;
     vtv_ghost = ghost;
-    vtv_mut   = mut;
-    vtv_vars  = vars;
-  }
+    vtv_mut   = mut }
+
+let vtv_vars {vtv_ity = {ity_vars = vars}; vtv_mut = mut} = match mut with
+  | Some r -> { vars with vars_reg = Sreg.add r vars.vars_reg }
+  | None   -> vars
 
 let vtv_unmut vtv =
   if vtv.vtv_mut = None then vtv else
     vty_value ~ghost:vtv.vtv_ghost vtv.vtv_ity
 
 type pvsymbol = {
-  pv_vs  : vsymbol;
-  pv_vtv : vty_value;
+  pv_vs   : vsymbol;
+  pv_vtv  : vty_value;
+  pv_vars : varset;
 }
 
 module PVsym = WeakStructMake (struct
@@ -768,6 +763,7 @@ let pv_equal : pvsymbol -> pvsymbol -> bool = (==)
 let create_pvsymbol id vtv = {
   pv_vs   = create_vsymbol id (ty_of_ity vtv.vtv_ity);
   pv_vtv  = vtv;
+  pv_vars = vtv_vars vtv;
 }
 
 let create_pvsymbol, restore_pv =
@@ -793,11 +789,11 @@ and vty_arrow = {
 }
 
 let rec vta_vars vta =
-  let add_arg vars pv = vars_union vars pv.pv_vtv.vtv_vars in
+  let add_arg vars pv = vars_union vars pv.pv_vars in
   List.fold_left add_arg (vty_vars vta.vta_result) vta.vta_args
 
 and vty_vars = function
-  | VTvalue vtv -> vtv.vtv_vars
+  | VTvalue vtv -> vtv_vars vtv
   | VTarrow vta -> vta_vars vta
 
 let vty_ghost = function
@@ -822,18 +818,19 @@ let vty_arrow_unsafe argl ~spec ~ghost vty = {
 }
 
 let vty_arrow argl ?spec ?(ghost=false) vty =
-  (* we accept a mutable vty_value as a result to simplify Mlw_expr,
-     but drop it in the signature: only projections return mutables *)
-  let vty = match vty with
-    | VTvalue v -> VTvalue (vtv_unmut v)
-    | VTarrow _ -> vty in
-  (* the arguments must be all distinct and at least one must be given *)
-  if argl = [] then invalid_arg "Mlw.vty_arrow";
+  let exn = Invalid_argument "Mlw.vty_arrow" in
+  (* the arguments must be all distinct *)
+  if argl = [] then raise exn;
   let add_arg pvs pv =
     (* mutable arguments are rejected outright *)
-    if pv.pv_vtv.vtv_mut <> None then invalid_arg "Mlw.vty_arrow";
-    Spv.add_new (Invalid_argument "Mlw.vty_arrow") pv pvs in
+    if pv.pv_vtv.vtv_mut <> None then raise exn;
+    Spv.add_new exn pv pvs in
   ignore (List.fold_left add_arg Spv.empty argl);
+  (* only projections may return mutable values *)
+  begin match vty with
+    | VTvalue { vtv_mut = Some _ } -> raise exn
+    | _ -> ()
+  end;
   let spec = match spec with
     | Some spec -> spec_check spec vty; spec
     | None -> spec_empty (ty_of_vty vty) in
@@ -882,8 +879,8 @@ let vta_full_inst sbs vta =
 (* remove from the given arrow every effect that is covered
    neither by the arrow's vta_vars nor by the given varmap *)
 let rec vta_filter varm vars vta =
-  let add_m pv m = Mid.add pv.pv_vs.vs_name pv.pv_vtv.vtv_vars m in
-  let add_s pv s = vars_union pv.pv_vtv.vtv_vars s in
+  let add_m pv m = Mid.add pv.pv_vs.vs_name pv.pv_vars m in
+  let add_s pv s = vars_union pv.pv_vars s in
   let varm = List.fold_right add_m vta.vta_args varm in
   let vars = List.fold_right add_s vta.vta_args vars in
   let vty = match vta.vta_result with

src/whyml/mlw_ty.mli

@@ -256,7 +256,6 @@ type vty_value = private {
   vtv_ity   : ity;
   vtv_ghost : bool;
   vtv_mut   : region option;
-  vtv_vars  : varset;
 }
 
 val vty_value : ?ghost:bool -> ?mut:region -> ity -> vty_value
@@ -264,8 +263,9 @@ val vty_value : ?ghost:bool -> ?mut:region -> ity -> vty_value
 val vtv_unmut : vty_value -> vty_value (* remove mutability *)
 
 type pvsymbol = private {
-  pv_vs  : vsymbol;
-  pv_vtv : vty_value;
+  pv_vs   : vsymbol;
+  pv_vtv  : vty_value;
+  pv_vars : varset;
 }
 
 module Mpv : Map.S with type key = pvsymbol

src/whyml/mlw_typing.ml

@@ -860,7 +860,7 @@ and type_v lenv gh svs vars = function
   | DSpecA (bl,tyc) ->
       let lenv, pvl = binders lenv bl in
       let add_pv (vars,svs) pv =
-        vars_union vars pv.pv_vtv.vtv_vars, Svs.add pv.pv_vs svs in
+        vars_union vars pv.pv_vars, Svs.add pv.pv_vs svs in
       let vars, svs = List.fold_left add_pv (vars,svs) pvl in
       let spec, vty = type_c lenv gh svs vars tyc in
       VTarrow (vty_arrow pvl ~spec vty)
@@ -1550,15 +1550,17 @@ let add_module lib path mm mt m =
     | Dparam (id, gh, tyv) ->
         let tyv, _ = dtype_v (create_denv uc) tyv in
         let tyv = type_v (create_lenv uc) gh Svs.empty vars_empty tyv in
-        let vd = create_val (Denv.create_user_id id) tyv in
-        begin match vd.val_sym with
-          | LetA { ps_vta = { vta_ghost = true }} when not gh ->
-              errorm ~loc "%s must be a ghost function" id.id
-          | LetV { pv_vtv = { vtv_ghost = true }} when not gh ->
-              errorm ~loc "%s must be a ghost variable" id.id
-          | _ -> ()
-        end;
-        let pd = create_val_decl vd in
+        let lv = match tyv with
+          | VTvalue v ->
+              if v.vtv_ghost && not gh then
+                errorm ~loc "%s must be a ghost variable" id.id;
+              LetV (create_pvsymbol (Denv.create_user_id id) v)
+          | VTarrow a ->
+              if a.vta_ghost && not gh then
+                errorm ~loc "%s must be a ghost function" id.id;
+              LetA (create_psymbol (Denv.create_user_id id) a)
+        in
+        let pd = create_val_decl lv in
         add_pdecl_with_tuples uc pd
     (* TODO: this is made obsolete by Duseclone, remove later *)
     | Duse (qid, use_imp_exp, use_as) ->

src/whyml/mlw_wp.ml

@@ -550,6 +550,7 @@ and wp_abstract env c_eff c_q c_xq q xq =
     let xq = Mexn.set_inter xq exns in
     let c_xq = Mexn.set_inter c_xq exns in
     let mexn = Mexn.inter quantify_xpost c_xq xq in
+    (* FIXME? This wp_ands is asymmetric in Pgm_wp *)
     wp_ands ~sym:true (f :: Mexn.values mexn)
   in
   backstep proceed c_q c_xq
@@ -680,4 +681,4 @@ let wp_rec env km th rdl =
   in
   List.fold_left2 add_one th rdl.rec_defn fl
 
-let wp_val _env _km th _vd = th
+let wp_val _env _km th _lv = th

src/whyml/mlw_wp.mli

@@ -42,6 +42,6 @@ val remove_old : Term.term -> Term.term
 
 (** Weakest preconditions *)
 
-val wp_val: Env.env -> known_map -> theory_uc -> val_decl -> theory_uc
+val wp_val: Env.env -> known_map -> theory_uc -> let_sym  -> theory_uc
 val wp_let: Env.env -> known_map -> theory_uc -> let_defn -> theory_uc
 val wp_rec: Env.env -> known_map -> theory_uc -> rec_defn -> theory_uc