whyml: check program variables and symbols in declarations

src/whyml/mlw_decl.ml

@@ -298,7 +298,17 @@ let merge_known kn1 kn2 =
   in
   Mid.union check_known kn1 kn2
 
-let known_add_decl _lkn0 kn0 decl =
+let pd_vars pd = match pd.pd_node with
+  | PDval (LetV _) -> Sid.empty
+  | PDval (LetA ps) -> Mid.map (fun _ -> ()) ps.ps_varm
+  | PDlet ld -> Mid.map (fun _ -> ()) ld.let_expr.e_varm
+  | PDrec rd ->
+      let add_rd s fd = Mid.set_union s fd.fun_ps.ps_varm in
+      let varm = List.fold_left add_rd Mid.empty rd.rec_defn in
+      Mid.map (fun _ -> ()) varm
+  | PDtype _ | PDdata _ | PDexn _ -> Sid.empty
+
+let known_add_decl lkn0 kn0 decl =
   let kn = Mid.map (const decl) decl.pd_news in
   let check id decl0 _ =
     if pd_equal decl0 decl
@@ -306,13 +316,10 @@ let known_add_decl _lkn0 kn0 decl =
     else raise (RedeclaredIdent id)
   in
   let kn = Mid.union check kn0 kn in
-(*
-  let unk = Mid.set_diff decl.pd_syms kn in
+  let unk = Mid.set_diff (pd_vars decl) kn in
   let unk = Mid.set_diff unk lkn0 in
   if Sid.is_empty unk then kn
   else raise (UnknownIdent (Sid.choose unk))
-*)
-  kn
 
 (* TODO: known_add_decl must check pattern matches for exhaustiveness *)
 

src/whyml/mlw_module.ml

@@ -343,22 +343,29 @@ let th_unit =
   close_theory uc
 
 let xs_exit = create_xsymbol (id_fresh "%Exit") ity_unit
-let pd_exit = create_exn_decl xs_exit
-
-let mod_exit = {
-  mod_theory = close_theory (create_theory (id_fresh "Exit"));
-  mod_decls  = [pd_exit];
-  mod_export = add_ps true xs_exit.xs_name.id_string (XS xs_exit) empty_ns;
-  mod_known  = Mid.singleton xs_exit.xs_name pd_exit;
-  mod_local  = Sid.singleton xs_exit.xs_name;
-  mod_used   = Sid.empty;
-}
+
+let mod_prelude env =
+  let pd_exit = create_exn_decl xs_exit in
+  let pd_old = create_val_decl (LetV Mlw_wp.pv_old) in
+  let uc = empty_module env (id_fresh "Prelude") [] in
+  let uc = add_pdecl ~wp:false uc pd_old in
+  let uc = add_pdecl ~wp:false uc pd_exit in
+  close_module uc
+
+let mod_prelude =
+  let one_time = ref None in
+  fun env -> match !one_time with
+    | Some m -> m
+    | None ->
+        let m = mod_prelude env in
+        one_time := Some m;
+        m
 
 let create_module env ?(path=[]) n =
   let m = empty_module env n path in
   let m = use_export_theory m bool_theory in
   let m = use_export_theory m th_unit in
-  let m = use_export m mod_exit in
+  let m = use_export m (mod_prelude env) in
   m
 
 (** Clone *)

src/whyml/mlw_wp.ml

@@ -62,13 +62,13 @@ let th_mark_old =
   let uc = add_param_decl uc fs_old in
   close_theory uc
 
-let fs_now = create_lsymbol (id_fresh "'now") [] (Some ty_mark)
+let fs_now = create_lsymbol (id_fresh "%now") [] (Some ty_mark)
 let t_now = fs_app fs_now [] ty_mark
 let e_now = e_lapp fs_now [] (ity_pur ts_mark [])
 
 (* [vs_old] appears in the postconditions given to the core API,
    which expects every vsymbol to be a pure part of a pvsymbol *)
-let pv_old = create_pvsymbol (id_fresh "'old") vtv_mark
+let pv_old = create_pvsymbol (id_fresh "%old") vtv_mark
 let vs_old = pv_old.pv_vs
 let t_old  = t_var vs_old
 

src/whyml/mlw_wp.mli

@@ -38,6 +38,7 @@ val th_mark_old : Theory.theory
 
 val e_now : expr
 
+val pv_old : pvsymbol
 val remove_old : Term.term -> Term.term
 
 val full_invariant :