whyml: various fixes

examples/programs/mergesort_list.mlw

@@ -9,7 +9,7 @@ module M
   use import list.Append
   use import list.Permut
 
-  let split l0 =
+  let split (l0 : list 'a) =
     {  length l0 >= 2 }
     let rec split_aux (l1 : list 'a) l2 l variant { length l } =
       { length l2 = length l1 \/ length l2 = length l1 + 1 }

src/whyml/mlw_dty.ml

@@ -50,14 +50,16 @@ and rvar =
   | Rtvs  of tvsymbol * dity * region Lazy.t
   | Rval  of dreg
 
-let rec ity_of_dity = function
+let rec ity_of_dity ?(strict=true) = function
+  | Dvar { contents = Dtvs _ } when strict ->
+      Loc.errorm "undefined type variable"
   | Dvar { contents = Dtvs tv } -> ity_var tv
-  | Dvar { contents = Dval dty } -> ity_of_dity dty
+  | Dvar { contents = Dval dty } -> ity_of_dity ~strict dty
   | Duvar tv -> ity_var tv
   | Dits (its,dl,rl) ->
-      ity_app its (List.map ity_of_dity dl) (List.map reg_of_dreg rl)
+      ity_app its (List.map (ity_of_dity ~strict) dl) (List.map reg_of_dreg rl)
   | Dts (ts,dl) ->
-      ity_pur ts (List.map ity_of_dity dl)
+      ity_pur ts (List.map (ity_of_dity ~strict) dl)
 
 and reg_of_dreg = function
   | Rreg (r,_) -> r
@@ -193,15 +195,16 @@ and unify_reg r1 r2 =
     | _ -> raise Exit
 
 let unify ~weak d1 d2 =
-  try unify ~weak d1 d2
-  with Exit -> raise (TypeMismatch (ity_of_dity d1, ity_of_dity d2))
+  try unify ~weak d1 d2 with Exit -> raise (TypeMismatch
+    (ity_of_dity ~strict:false d1, ity_of_dity ~strict:false d2))
 
 let unify_weak d1 d2 = unify ~weak:true d1 d2
 let unify d1 d2 = unify ~weak:false d1 d2
 
 type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
 
-let vty_of_dvty (argl,res) =
+let vty_of_dvty ?(strict=true) (argl,res) =
+  let ity_of_dity dity = ity_of_dity ~strict dity in
   let vtv = VTvalue (vty_value (ity_of_dity res)) in
   let conv a = create_pvsymbol (id_fresh "x") (vty_value (ity_of_dity a)) in
   if argl = [] then vtv else VTarrow (vty_arrow (List.map conv argl) vtv)

src/whyml/mlw_dty.mli

@@ -46,8 +46,8 @@ val ts_app: tysymbol -> dity list -> dity
 val unify: dity -> dity -> unit
 val unify_weak: dity -> dity -> unit (* don't unify regions *)
 
-val ity_of_dity: dity -> ity
-val vty_of_dvty: dvty -> vty
+val ity_of_dity: ?strict:bool -> dity -> ity
+val vty_of_dvty: ?strict:bool -> dvty -> vty
   (** use with care, only once unification is done *)
 
 val specialize_scheme: tvars -> dvty -> dvty

src/whyml/mlw_expr.ml

@@ -525,8 +525,10 @@ let create_fun_defn id lam letrec recsyms =
     fun_lambda = lam; }
 
 let e_rec rdl e =
-  let add_varm m rd = varmap_union m rd.fun_ps.ps_varm in
-  let varm = List.fold_left add_varm e.e_varm rdl.rec_defn in
+  let add_rd m { fun_ps = ps } =
+    (* psymbols defined in rdl can't occur in ps.ps_varm *)
+    varmap_union (Mid.remove ps.ps_name m) ps.ps_varm in
+  let varm = List.fold_left add_rd e.e_varm rdl.rec_defn in
   mk_expr (Erec (rdl,e)) e.e_vty e.e_effect varm
 
 let on_value fn e = match e.e_node with

src/whyml/mlw_typing.ml

@@ -109,6 +109,19 @@ let ht_tuple   = Hashtbl.create 3
 let ts_tuple n = Hashtbl.replace ht_tuple n (); ts_tuple n
 let fs_tuple n = Hashtbl.replace ht_tuple n (); fs_tuple n
 
+let rec check_at f0 =
+  let rec check f = match f.t_node with
+    | Term.Tapp (ls, _) when ls_equal ls fs_at ->
+        let d = Mvs.set_diff f.t_vars f0.t_vars in
+        if not (Mvs.is_empty d) then errorm ?loc:f.t_loc
+          "locally bound variable %a under `at'"
+          Pretty.print_vs (fst (Mvs.choose d))
+        else true
+    | _ ->
+        t_all check f
+  in
+  ignore (check f0)
+
 let count_term_tuples t =
   let syms_ts _ ts = match is_ts_tuple_id ts.ts_name with
     | Some n -> Hashtbl.replace ht_tuple n () | _ -> () in
@@ -662,6 +675,7 @@ let create_post lenv x ty f =
   let f = Typing.type_fmla lenv.th_old log_denv log_vars f in
   let f = remove_old f in
   count_term_tuples f;
+  check_at f;
   create_post res f
 
 let create_xpost lenv x xs f = create_post lenv x (ty_of_ity xs.xs_ity) f
@@ -670,11 +684,13 @@ let create_post lenv x vty f = create_post lenv x (ty_of_vty vty) f
 let create_pre lenv f =
   let f = Typing.type_fmla lenv.th_at lenv.log_denv lenv.log_vars f in
   count_term_tuples f;
+  check_at f;
   f
 
 let create_variant lenv (t,r) =
   let t = Typing.type_term lenv.th_at lenv.log_denv lenv.log_vars t in
   count_term_tuples t;
+  check_at t;
   t, r
 
 let add_local x lv lenv = match lv with
@@ -980,12 +996,19 @@ and expr_lam lenv gh (bl, var, p, de, q, xq) =
   let e = e_ghostify gh (expr lenv de) in
   if not gh && vty_ghost e.e_vty then
     errorm ~loc:de.de_loc "ghost body in a non-ghost function";
+  let xq =
+    let dummy_xpost xs () =
+      let v = create_vsymbol (id_fresh "dummy") (ty_of_ity xs.xs_ity) in
+      Mlw_ty.create_post v t_false in
+    let xq = xpost lenv xq in
+    let xs = Sexn.union e.e_effect.eff_raises e.e_effect.eff_ghostx in
+    Mexn.set_union xq (Mexn.mapi dummy_xpost (Mexn.set_diff xs xq)) in
   { l_args = pvl;
     l_variant = List.map (create_variant lenv) var;
     l_pre = create_pre lenv p;
     l_expr = e;
     l_post = create_post lenv "result" e.e_vty q;
-    l_xpost = xpost lenv xq; }
+    l_xpost = xq; }
 
 (** Type declaration *)
 

src/whyml/mlw_wp.ml

@@ -564,12 +564,10 @@ and wp_abstract env c_eff c_q c_xq q xq =
 and wp_lambda env lr l =
   let lab = fresh_mark () in
   let args = List.map (fun pv -> pv.pv_vs) l.l_args in
-  let env = if lr = 0 then env else
+  let env = if lr = 0 || l.l_variant = [] then env else
     let lab = t_var lab in
-    let t_at_lab v = fs_app fs_at [t_var v; lab] v.vs_ty in
-    let add_arg v sbs = Mvs.add v (t_at_lab v) sbs in
-    let sbs = List.fold_right add_arg args Mvs.empty in
-    let tl = List.map (fun (t,_) -> t_subst sbs t) l.l_variant in
+    let t_at_lab (t,_) = t_app fs_at [t; lab] t.t_ty in
+    let tl = List.map t_at_lab l.l_variant in
     { env with letrec_var = Mint.add lr tl env.letrec_var }
   in
   let q = old_mark lab (wp_expl expl_post l.l_post) in
@@ -638,7 +636,7 @@ let rec unabsurd f = match f.t_node with
 
 let add_wp_decl name f uc =
   (* prepare a proposition symbol *)
-  let s = "WP_parameter_" ^ name.id_string in
+  let s = "WP_parameter " ^ name.id_string in
   let lab = Ident.create_label ("expl:parameter " ^ name.id_string) in
   let label = Slab.add lab name.id_label in
   let id = id_fresh ~label ?loc:name.id_loc s in