whyml: accept multiple pre/post/xpost/invariants

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;
   }
@@ -419,7 +419,7 @@ type_args:
 
 typedefn:
 | /* epsilon */
-    { false, Public, TDabstract, None }
+    { false, Public, TDabstract, [] }
 | equal_model visibility typecases invariant
     { $1, $2, TDalgebraic $3, $4 }
 | equal_model visibility BAR typecases invariant
@@ -429,7 +429,7 @@ typedefn:
 /* abstract/private is not allowed for alias type */
 | equal_model visibility primitive_type
     { if $2 <> Public then Loc.error ~loc:(floc_i 2) Parsing.Parse_error;
-      $1, Public, TDalias $3, None }
+      $1, Public, TDalias $3, [] }
 ;
 
 visibility:
@@ -1242,8 +1242,8 @@ loop_annotation:
 ;
 
 invariant:
-| INVARIANT annotation { Some $2 }
-| /* epsilon */        { None    }
+| INVARIANT annotation { [$2] }
+| /* epsilon */        { [] }
 ;
 
 list1_type_v_binder:

src/parser/ptree.ml

@@ -126,7 +126,7 @@ type type_def =
 
 type visibility = Public | Private | Abstract
 
-type invariant = lexpr option
+type invariant = lexpr list
 
 type type_decl = {
   td_loc    : loc;
@@ -196,9 +196,9 @@ type effect = {
   pe_raises : qualid list;
 }
 
-type pre = lexpr
-type post = lexpr
-type xpost = (qualid * post) list
+type pre = lexpr list
+type post = lexpr list
+type xpost = (qualid * lexpr) list list
 
 type spec = {
   sp_pre     : pre;

src/parser/typing.ml

@@ -922,7 +922,7 @@ let prepare_typedef td =
     errorm ~loc:td.td_loc "model types are not allowed in the logic";
   if td.td_vis <> Public then
     errorm ~loc:td.td_loc "logic types cannot be abstract or private";
-  if td.td_inv <> None then
+  if td.td_inv <> [] then
     errorm ~loc:td.td_loc "logic types cannot have invariants";
   match td.td_def with
   | TDabstract | TDalgebraic _ | TDalias _ ->

src/programs/pgm_ttree.ml

@@ -42,7 +42,7 @@ type for_direction = Ptree.for_direction
 
 (* user type_v *)
 
-type dpre = Ptree.pre
+type dpre = Ptree.lexpr
 type dpost_fmla = Ptree.lexpr
 type dexn_post_fmla = Ptree.lexpr
 type dpost = dpost_fmla * (Term.lsymbol * dexn_post_fmla) list

src/programs/pgm_typing.ml

@@ -305,6 +305,17 @@ let rec dtype ~user env = function
       let ts = ts_tuple (List.length tyl) in
       tyapp ts (List.map (dtype ~user env) tyl)
 
+let rec lexpr_conj = function
+  | [] -> { pp_desc = PPtrue; pp_loc = Loc.dummy_position }
+  | [l] -> l
+  | l :: ll -> { l with pp_desc = PPbinop (l, PPand, lexpr_conj ll) }
+
+let get_xpost = function
+  | [] -> []
+  | [l] -> l
+  | _ :: _ -> Loc.errorm "Multiple exceptional postconditions \
+      are not supported in this version of WhyML"
+
 let rec dutype_v env = function
   | Ptree.Tpure pt ->
       DUTpure (dtype ~user:true env pt)
@@ -316,8 +327,9 @@ let rec dutype_v env = function
 and dutype_c env (ty,sp) =
   { duc_result_type = dutype_v env ty;
     duc_effect      = dueffect env sp.Ptree.sp_effect;
-    duc_pre         = sp.Ptree.sp_pre;
-    duc_post        = dpost env.uc (sp.Ptree.sp_post, sp.Ptree.sp_xpost);
+    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);
   }
 
 and dubinder env ({id=x; id_loc=loc} as id, gh, v) =
@@ -353,8 +365,12 @@ let dvariants env = function
   | [v] -> Some (dvariant env v)
   | _ -> errorm "multiple variants are not supported"
 
+let lexpr_conj_opt = function
+  | [] -> None
+  | ll -> Some (lexpr_conj ll)
+
 let dloop_annotation env a =
-  { dloop_invariant = a.Ptree.loop_invariant;
+  { dloop_invariant = lexpr_conj_opt a.Ptree.loop_invariant;
     dloop_variant   = dvariants env a.Ptree.loop_variant; }
 
 (***
@@ -713,7 +729,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
       let env = add_local env x.id dty_int in
       let e3 = dexpr ~ghost ~userloc env e3 in
       expected_type e3 dty_unit;
-      DEfor (x, e1, d, e2, inv, e3), dty_unit
+      DEfor (x, e1, d, e2, lexpr_conj_opt inv, e3), dty_unit
   | Ptree.Eassert (k, le) ->
       DEassert (k, le), dty_unit
   | Ptree.Emark ({id=s}, e1) ->
@@ -732,7 +748,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 (q.sp_post, q.sp_xpost) in
+      let q = dpost env.uc (lexpr_conj q.sp_post, get_xpost q.sp_xpost) in
       DEabstract(e1, q), e1.dexpr_type
   | Ptree.Eghost _ ->
       no_ghost true;
@@ -766,8 +782,8 @@ 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 (sp.sp_post, sp.sp_xpost) in
-  v, (sp.sp_pre, e, q)
+  let q = dpost env.uc (lexpr_conj sp.sp_post, get_xpost sp.sp_xpost) in
+  v, (lexpr_conj sp.sp_pre, e, q)
 
 (*** regions tables ********************************************************)
 
@@ -2056,7 +2072,7 @@ let check_type_vars ~loc vars ty =
 let make_immutable_type td =
   if td.td_vis = Private then errorm ~loc:td.td_loc
     "private types are not supported in this version of WhyML";
-  if td.td_inv <> None then errorm ~loc:td.td_loc
+  if td.td_inv <> [] then errorm ~loc:td.td_loc
     "type invariants are not supported in this version of WhyML";
   let td = { td with td_model = false; td_vis = Public } in
   let make_immutable_field f = { f with f_mutable = false; f_ghost = false } in

src/whyml/mlw_dtree.ml

@@ -29,10 +29,10 @@ type ident = Ptree.ident
 type ghost = bool
 
 type dpre = Ptree.pre
-type dpost = Ptree.pre
+type dpost = Ptree.post
 type dxpost = dpost Mexn.t
 type dvariant = Ptree.lexpr * Term.lsymbol option
-type dinvariant = Ptree.lexpr option
+type dinvariant = Ptree.lexpr list
 
 type deffect = {
   deff_reads  : Ptree.lexpr list;

src/whyml/mlw_typing.ml

@@ -375,8 +375,11 @@ exception DuplicateException of xsymbol
 let dxpost uc ql =
   let add_exn m (q,f) =
     let xs = find_xsymbol uc q in
-    Mexn.add_new (DuplicateException xs) xs f m in
-  List.fold_left add_exn Mexn.empty ql
+    Mexn.add_new (DuplicateException xs) xs [f] m in
+  let exn_map ql = List.fold_left add_exn Mexn.empty ql 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
 
 let dvariant uc var =
   List.map (fun (le,q) -> le, Util.option_map (find_variant_ls uc) q) var
@@ -758,32 +761,39 @@ let rec dty_of_ty ty = match ty.ty_node with
   | Ty.Tyapp (ts, tyl) -> Denv.tyapp ts (List.map dty_of_ty tyl)
   | Ty.Tyvar v -> Denv.tyuvar v
 
-let create_post lenv x ty f =
-  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 = Typing.type_fmla lenv.th_old log_denv log_vars f in
-  let f = remove_old f in
+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 create_assert 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;
-  create_post res f
+  f
 
-let create_xpost lenv x xs f = create_post lenv x (ty_of_ity xs.xs_ity) f
-let create_post lenv x vty f = create_post lenv x (ty_of_vty vty) f
+let create_pre lenv fs = t_and_simp_l (List.map (create_assert lenv) fs)
 
-let create_xpost lenv x xq = Mexn.mapi (create_xpost lenv x) xq
-
-let create_pre lenv f =
-  let f = Typing.type_fmla lenv.th_at lenv.log_denv lenv.log_vars f in
+let create_post lenv log_denv log_vars 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;
   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 create_post lenv x ty fs =
+  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
+  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_post lenv x vty fs = create_post lenv x (ty_of_vty vty) fs
+
+let create_xpost lenv x xq = Mexn.mapi (create_xpost lenv x) xq
 
 let add_local x lv lenv = match lv with
   | LetA _ ->
@@ -1110,7 +1120,7 @@ and expr_desc lenv loc de = match de.de_desc with
         | Ptree.Aassert -> Aassert
         | Ptree.Aassume -> Aassume
         | Ptree.Acheck  -> Acheck in
-      e_assert ak (create_pre lenv f)
+      e_assert ak (create_assert lenv f)
   | DEabsurd ->
       e_absurd (ity_of_dity (snd de.de_type))
   | DEraise (xs, de1) ->
@@ -1138,9 +1148,7 @@ and expr_desc lenv loc de = match de.de_desc with
   | DEghost de1 ->
       e_ghostify true (expr lenv de1)
   | DEloop (var,inv,de1) ->
-      let inv = match inv with
-        | Some inv -> create_pre lenv inv
-        | None -> t_true in
+      let inv = create_pre lenv inv in
       let var = List.map (create_variant lenv) var in
       e_loop inv var (expr lenv de1)
   | DEfor (x,defrom,dir,deto,inv,de1) ->
@@ -1148,13 +1156,11 @@ and expr_desc lenv loc de = match de.de_desc with
       let eto = expr lenv deto in
       let pv = create_pvsymbol (Denv.create_user_id x) (vty_value ity_int) in
       let lenv = add_local x.id (LetV pv) lenv in
+      let inv = create_pre lenv inv in
+      let e1 = expr lenv de1 in
       let dir = match dir with
         | Ptree.To -> To
         | Ptree.Downto -> DownTo in
-      let inv = match inv with
-        | Some inv -> create_pre lenv inv
-        | None -> t_true in
-      let e1 = expr lenv de1 in
       e_for pv efrom dir eto inv e1
 
 and expr_rec lenv dfdl =
@@ -1260,7 +1266,7 @@ let add_types ~wp uc tdl =
       Hashtbl.replace mutables x false;
       let mut =
         let td = Mstr.find x def in
-        td.td_inv <> None ||
+        td.td_inv <> [] ||
         match td.td_def with
         | TDabstract -> false
         | TDalias ty -> check ty
@@ -1284,7 +1290,7 @@ let add_types ~wp uc tdl =
       | Some ts -> ts
       | None ->
           let td = Mstr.find x def in let loc = td.td_loc in
-          if td.td_inv <> None
+          if td.td_inv <> []
           then errorm ~loc "Recursive types cannot have invariants"
           else errorm ~loc "Recursive types cannot have mutable components"
     with Not_found ->
@@ -1352,7 +1358,7 @@ let add_types ~wp uc tdl =
               let s,pjl = Util.map_fold_left mk_proj s pjl in
               s, (Denv.create_user_id cid, pjl)
             in
-            let init = (Sreg.empty, d.td_inv <> None) in
+            let init = (Sreg.empty, d.td_inv <> []) in
             let (regs,inv),def = Util.map_fold_left mk_constr init csl in
             Hashtbl.replace predefs x def;
             create_itysymbol id ~abst ~priv ~inv vl (Sreg.elements regs) None
@@ -1371,7 +1377,7 @@ let add_types ~wp uc tdl =
               let vtv = vty_value ?mut ~ghost ity in
               (regs, inv), (create_pvsymbol fid vtv, true)
             in
-            let init = (Sreg.empty, d.td_inv <> None) in
+            let init = (Sreg.empty, d.td_inv <> []) in
             let (regs,inv),pjl = Util.map_fold_left mk_field init fl in
             let cid = { d.td_ident with id = "mk " ^ d.td_ident.id } in
             Hashtbl.replace predefs x [Denv.create_user_id cid, pjl];
@@ -1493,31 +1499,30 @@ let add_types ~wp uc tdl =
     else
       add_decl_with_tuples uc (Decl.create_ty_decl ts.its_pure)
   in
-  let add_invariant uc d = match d.td_inv with
-    | None -> uc
-    | Some f ->
-        let ts = Util.of_option (Hashtbl.find tysymbols d.td_ident.id) in
-        let ty = ty_app ts.its_pure (List.map ty_var ts.its_pure.ts_args) in
-        let x = "result" in
-        let f = match d.td_def with
-          | TDrecord fl ->
-              let loc = f.pp_loc in
-              let field { f_loc = loc; f_ident = id } =
-                Qident id, { pat_loc = loc; pat_desc = PPpvar id } in
-              let pat = PPprec (List.map field fl) in
-              let pat = { pat_loc = loc; pat_desc = pat } in
-              let id = { id = x; id_lab = []; id_loc = loc } in
-              let id = { pp_loc = loc; pp_desc = Ptree.PPvar (Qident id) } in
-              { pp_loc = loc; pp_desc = Ptree.PPmatch (id, [pat, f]) }
-          | TDabstract | TDalias _ | TDalgebraic _ -> f
-        in
-        let res = create_vsymbol (id_fresh x) ty in
-        let log_vars = Mstr.singleton x res in
-        let log_denv = Typing.add_var x (dty_of_ty ty) Typing.denv_empty in
-        let f = Typing.type_fmla (get_theory uc) log_denv log_vars f in
-        let uc = (count_term_tuples f; flush_tuples uc) in
-        Mlw_module.add_invariant uc ts (Mlw_ty.create_post res f)
+  let add_invariant d uc f =
+    let ts = Util.of_option (Hashtbl.find tysymbols d.td_ident.id) in
+    let ty = ty_app ts.its_pure (List.map ty_var ts.its_pure.ts_args) in
+    let x = "result" in
+    let f = match d.td_def with
+      | TDrecord fl ->
+          let loc = f.pp_loc in
+          let field { f_loc = loc; f_ident = id } =
+            Qident id, { pat_loc = loc; pat_desc = PPpvar id } in
+          let pat = PPprec (List.map field fl) in
+          let pat = { pat_loc = loc; pat_desc = pat } in
+          let id = { id = x; id_lab = []; id_loc = loc } in
+          let id = { pp_loc = loc; pp_desc = Ptree.PPvar (Qident id) } in
+          { pp_loc = loc; pp_desc = Ptree.PPmatch (id, [pat, f]) }
+      | TDabstract | TDalias _ | TDalgebraic _ -> f
+    in
+    let res = create_vsymbol (id_fresh x) ty in
+    let log_vars = Mstr.singleton x res in
+    let log_denv = Typing.add_var x (dty_of_ty ty) Typing.denv_empty in
+    let f = Typing.type_fmla (get_theory uc) log_denv log_vars f in
+    let uc = (count_term_tuples f; flush_tuples uc) in
+    Mlw_module.add_invariant uc ts (Mlw_ty.create_post res f)
   in
+  let add_invariant uc d = List.fold_left (add_invariant d) uc d.td_inv in
   try
     let uc = List.fold_left add_type_decl uc abstr in
     let uc = if algeb = [] then uc else