whyml: patterns in postconditions

src/parser/parser.mly

@@ -148,9 +148,9 @@ end
     { pe_reads = r1 @ r2; pe_writes = w1 @ w2; pe_raises = x1 @ x2 }
 
   let spec p (q,xq) ef vl = {
-    sp_pre     = [p];
-    sp_post    = [q];
-    sp_xpost   = [xq];
+    sp_pre     = p;
+    sp_post    = q;
+    sp_xpost   = xq;
     sp_effect  = ef;
     sp_variant = vl;
   }
@@ -1138,7 +1138,7 @@ expr:
 | GHOST expr
    { mk_expr (Eghost $2) }
 | ABSTRACT expr post
-   { mk_expr (Eabstract($2, spec (mk_pp PPtrue) $3 empty_effect [])) }
+   { mk_expr (Eabstract($2, spec [] $3 empty_effect [])) }
 | label expr %prec prec_named
    { mk_expr (Enamed ($1, $2)) }
 ;
@@ -1148,7 +1148,7 @@ triple:
   { (* add_init_label *) $2, spec $1 $3 empty_effect [] }
 | expr %prec prec_triple
   { (* add_init_label *) $1,
-    spec (mk_pp PPtrue) (mk_pp PPtrue, []) empty_effect [] }
+    spec [] ([], []) empty_effect [] }
 ;
 
 expr_arg:
@@ -1303,7 +1303,7 @@ simple_type_v:
 
 type_c:
 | type_v
-    { $1, spec (mk_pp PPtrue) (mk_pp PPtrue, []) empty_effect [] }
+    { $1, spec [] ([], []) empty_effect [] }
 | pre type_v effects post
     { $2, spec $1 $4 $3 [] }
 ;
@@ -1311,7 +1311,7 @@ type_c:
 /* for ANY */
 simple_type_c:
 | simple_type_v
-    { $1, spec (mk_pp PPtrue) (mk_pp PPtrue, []) empty_effect [] }
+    { $1, spec [] ([], []) empty_effect [] }
 | pre type_v effects post
     { $2, spec $1 $4 $3 [] }
 ;
@@ -1322,11 +1322,16 @@ annotation:
 ;
 
 pre:
-| annotation { $1 }
+| annotation { [$1] }
 ;
 
 post:
-| annotation list0_post_exn { $1, $2 }
+| normal_post list0_post_exn { [floc_i 1, [$1]], [floc_i 2, $2] }
+;
+
+normal_post:
+| annotation
+    { mk_pat (PPpvar (mk_id "result" (floc ()))), $1 }
 ;
 
 list0_post_exn:
@@ -1340,7 +1345,8 @@ list1_post_exn:
 ;
 
 post_exn:
-| BAR uqualid ARROW annotation { $2, $4 }
+| BAR uqualid ARROW annotation
+    { $2, mk_pat (PPpvar (mk_id "result" (floc_i 2))), $4 }
 ;
 
 effects:

src/parser/ptree.ml

@@ -196,14 +196,14 @@ type effect = {
   pe_raises : qualid list;
 }
 
-type pre = lexpr list
-type post = lexpr list
-type xpost = (qualid * lexpr) list list
+type pre = lexpr
+type post = loc * (pattern * lexpr) list
+type xpost = loc * (qualid * pattern * lexpr) list
 
 type spec = {
-  sp_pre     : pre;
-  sp_post    : post;
-  sp_xpost   : xpost;
+  sp_pre     : pre list;
+  sp_post    : post list;
+  sp_xpost   : xpost list;
   sp_effect  : effect;
   sp_variant : variant list;
 }

src/programs/pgm_typing.ml

@@ -310,12 +310,26 @@ let rec lexpr_conj = function
   | [l] -> l
   | l :: ll -> { l with pp_desc = PPbinop (l, PPand, lexpr_conj ll) }
 
+let get_post l =
+  let conv = function
+    | _, [{pat_desc = PPpvar { id = "result" }}, le] -> le
+    | loc, _ -> Loc.errorm ~loc "Patterns in postconditions \
+        are not supported in this version of WhyML" in
+  lexpr_conj (List.map conv l)
+
 let get_xpost = function
   | [] -> []
-  | [l] -> l
+  | [loc, l] ->
+      let conv (xs, p, le) = match p.pat_desc with
+        | PPpvar { id = "result" } -> xs, le
+        | _ -> Loc.errorm ~loc "Patterns in postconditions \
+              are not supported in this version of WhyML" in
+      List.map conv l
   | _ :: _ -> Loc.errorm "Multiple exceptional postconditions \
       are not supported in this version of WhyML"
 
+let dpost uc sp = dpost uc (get_post sp.sp_post, get_xpost sp.sp_xpost)
+
 let rec dutype_v env = function
   | Ptree.Tpure pt ->
       DUTpure (dtype ~user:true env pt)
@@ -328,8 +342,7 @@ and dutype_c env (ty,sp) =
   { duc_result_type = dutype_v env ty;
     duc_effect      = dueffect env sp.Ptree.sp_effect;
     duc_pre         = lexpr_conj sp.Ptree.sp_pre;
-    duc_post        = dpost env.uc
-      (lexpr_conj sp.Ptree.sp_post, get_xpost sp.Ptree.sp_xpost);
+    duc_post        = dpost env.uc sp;
   }
 
 and dubinder env ({id=x; id_loc=loc} as id, gh, v) =
@@ -748,7 +761,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
       DEany c, dpurify_utype_v c.duc_result_type
   | Ptree.Eabstract(e1,q) ->
       let e1 = dexpr ~ghost ~userloc env e1 in
-      let q = dpost env.uc (lexpr_conj q.sp_post, get_xpost q.sp_xpost) in
+      let q = dpost env.uc q in
       DEabstract(e1, q), e1.dexpr_type
   | Ptree.Eghost _ ->
       no_ghost true;
@@ -782,7 +795,7 @@ and dletrec ~ghost ~userloc env dl =
 and dtriple ~ghost ~userloc env (e, sp) =
   let v = dvariants env sp.sp_variant in
   let e = dexpr ~ghost ~userloc env e in
-  let q = dpost env.uc (lexpr_conj sp.sp_post, get_xpost sp.sp_xpost) in
+  let q = dpost env.uc sp in
   v, (lexpr_conj sp.sp_pre, e, q)
 
 (*** regions tables ********************************************************)

src/whyml/mlw_dtree.ml

@@ -28,8 +28,8 @@ type ident = Ptree.ident
 
 type ghost = bool
 
-type dpre = Ptree.pre
-type dpost = Ptree.post
+type dpre = Ptree.lexpr list
+type dpost = (string * Ptree.lexpr) list
 type dxpost = dpost Mexn.t
 type dvariant = Ptree.lexpr * Term.lsymbol option
 type dinvariant = Ptree.lexpr list

src/whyml/mlw_typing.ml

@@ -370,13 +370,26 @@ let deff_of_peff uc pe =
     deff_writes = pe.pe_writes;
     deff_raises = List.map (find_xsymbol uc) pe.pe_raises; }
 
-exception DuplicateException of xsymbol
+let mk_dpost loc = function
+  | [] -> assert false
+  | [{ pat_desc = PPpvar { id = x }}, f] -> x, f
+  | l ->
+      let x = "result" in
+      let v = { id = x; id_loc = loc; id_lab = [] } in
+      let v = { pp_desc = Ptree.PPvar (Qident v); pp_loc = loc } in
+      x, { pp_desc = PPmatch (v,l); pp_loc = loc }
+
+let dpost ql = List.map (fun (loc, ql) -> mk_dpost loc ql) ql
 
 let dxpost uc ql =
-  let add_exn m (q,f) =
+  let add_exn (q,pat,f) m =
     let xs = find_xsymbol uc q in
-    Mexn.add_new (DuplicateException xs) xs [f] m in
-  let exn_map ql = List.fold_left add_exn Mexn.empty ql in
+    Mexn.change (function
+      | Some l -> Some ((pat,f) :: l)
+      | None   -> Some ((pat,f) :: [])) xs m in
+  let exn_map (loc,ql) =
+    let m = List.fold_right add_exn ql Mexn.empty in
+    Mexn.map (fun ql -> [mk_dpost loc ql]) m in
   let add_map ql m =
     Mexn.union (fun _ l r -> Some (l @ r)) (exn_map ql) m in
   List.fold_right add_map ql Mexn.empty
@@ -386,7 +399,7 @@ let dvariant uc var =
 
 let dspec uc sp = {
   ds_pre     = sp.sp_pre;
-  ds_post    = sp.sp_post;
+  ds_post    = dpost sp.sp_post;
   ds_xpost   = dxpost uc sp.sp_xpost;
   ds_effect  = deff_of_peff uc sp.sp_effect;
   ds_variant = dvariant uc sp.sp_variant;
@@ -778,7 +791,9 @@ let create_assert lenv f =
 
 let create_pre lenv fs = t_and_simp_l (List.map (create_assert lenv) fs)
 
-let create_post lenv log_denv log_vars f =
+let create_post lenv res dty x f =
+  let log_vars = Mstr.add x res lenv.log_vars in
+  let log_denv = Typing.add_var x dty lenv.log_denv in
   let f = Typing.type_fmla lenv.th_old log_denv log_vars f in
   let f = t_label_add Split_goal.stop_split f in
   let f = remove_old f in
@@ -786,18 +801,19 @@ let create_post lenv log_denv log_vars f =
   check_at f;
   f
 
-let create_post lenv x ty fs =
+let create_post lenv ty fs =
+  let dty = dty_of_ty ty in
+  let x = match fs with (x,_)::_ -> x | [] -> "result" in
   let res = create_vsymbol (id_fresh x) ty in
-  let log_vars = Mstr.add x res lenv.log_vars in
-  let log_denv = Typing.add_var x (dty_of_ty ty) lenv.log_denv in
-  let f = t_and_simp_l (List.map (create_post lenv log_denv log_vars) fs) in
+  let post (x,f) = create_post lenv res dty x f in
+  let f = t_and_simp_l (List.map post fs) in
   Mlw_ty.create_post res f
 
-let create_xpost lenv x xs fs = create_post lenv x (ty_of_ity xs.xs_ity) fs
+let create_xpost lenv xs fs = create_post lenv (ty_of_ity xs.xs_ity) fs
 
-let create_post lenv x vty fs = create_post lenv x (ty_of_vty vty) fs
+let create_post lenv vty fs = create_post lenv (ty_of_vty vty) fs
 
-let create_xpost lenv x xq = Mexn.mapi (create_xpost lenv x) xq
+let create_xpost lenv xq = Mexn.mapi (create_xpost lenv) xq
 
 let add_local x lv lenv = match lv with
   | LetA _ ->
@@ -926,8 +942,8 @@ let check_user_effect lenv e dsp =
 
 let spec_of_dspec lenv eff vty dsp = {
   c_pre     = create_pre lenv dsp.ds_pre;
-  c_post    = create_post lenv "result" vty dsp.ds_post;
-  c_xpost   = create_xpost lenv "result" dsp.ds_xpost;
+  c_post    = create_post lenv vty dsp.ds_post;
+  c_xpost   = create_xpost lenv dsp.ds_xpost;
   c_effect  = eff;
   c_variant = List.map (create_variant lenv) dsp.ds_variant;
   c_letrec  = 0;