WhyML: weakest preconditions in progress

src/whyml/mlw_module.ml

@@ -281,12 +281,23 @@ let add_rec uc { rec_ps = ps } =
 let add_exn uc xs =
   add_symbol add_ps xs.xs_name (XS xs) uc
 
+let pdecl_vc km th d = match d.pd_node with
+  | PDtype _ | PDdata _ | PDexn _ -> th
+  | PDval lv -> Mlw_wp.wp_val km th lv
+  | PDlet ld -> Mlw_wp.wp_let km th ld
+  | PDrec rdl -> Mlw_wp.wp_rec km th rdl
+
 let add_pdecl uc d =
   let uc = { uc with
     muc_decls = d :: uc.muc_decls;
     muc_known = known_add_decl (Theory.get_known uc.muc_theory) uc.muc_known d;
     muc_local = Sid.union uc.muc_local d.pd_news }
   in
+  let uc =
+    if Debug.test_flag Typing.debug_type_only then uc else
+    let th = pdecl_vc uc.muc_known uc.muc_theory d in
+    { uc with muc_theory = th }
+  in
   match d.pd_node with
   | PDtype its ->
       let uc = add_type uc its in

src/whyml/mlw_wp.ml

@@ -54,3 +54,38 @@ let e_setmark = e_lapp fs_setmark [] (ity_pur ts_mark [])
 
 let vs_old = create_vsymbol (id_fresh "'old") ty_mark
 let vs_now = create_vsymbol (id_fresh "'now") ty_mark
+
+(** Weakest preconditions *)
+
+let ty_of_vty = function
+  | VTvalue vtv -> ty_of_ity vtv.vtv_ity
+  | VTarrow _   -> ty_unit
+
+let default_exn_post xs _ =
+  let vs = create_vsymbol (id_fresh "result") (ty_of_ity xs.xs_ity) in
+  create_post vs t_true
+
+let default_post vty ef =
+  let vs = create_vsymbol (id_fresh "result") (ty_of_vty vty) in
+  create_post vs t_true,
+  Mexn.mapi default_exn_post ef.eff_raises
+
+let rec wp_expr _km _lkm _e _q =
+  assert false (*TODO*)
+
+let wp_close _km _lkm _ef _f =
+  assert false (*TODO*)
+
+let wp km lkm e =
+  let f = wp_expr km lkm e (default_post e.e_vty e.e_effect) in
+  wp_close km lkm e.e_effect f
+
+let wp_val _km th _lv =
+  th
+
+let wp_let _km th _ld =
+  th
+
+let wp_rec _km th _rdl =
+  th
+

src/whyml/mlw_wp.mli

@@ -19,8 +19,10 @@
 (**************************************************************************)
 
 open Why3
+open Theory
 open Mlw_ty
 open Mlw_ty.T
+open Mlw_decl
 open Mlw_expr
 
 (** WP-only builtins *)
@@ -35,3 +37,9 @@ val th_mark : Theory.theory
 
 val fs_setmark : Term.lsymbol
 val e_setmark  : expr
+
+(** Weakest preconditions *)
+
+val wp_val: known_map -> theory_uc -> val_decl -> theory_uc
+val wp_let: known_map -> theory_uc -> let_defn -> theory_uc
+val wp_rec: known_map -> theory_uc -> rec_defn list -> theory_uc