fix conseq for exception with argument

Author: bgregoir

examples/exception.ec

@@ -107,12 +107,14 @@ proof.
   auto. smt(a5 a3 a4).
 qed.
 
+op o : exn = e2.
+
 module M1 ={
   var i:int
 
   proc f1 (x:int) : int = {
     i <- 0;
-    raise e2;
+    raise o;
     return x;
   }
 
@@ -128,7 +130,7 @@ lemma test (_x: int):
 proof.
   proc.
   call (: true ==> true | e2 => M1.i = 0).
-  + by proc; auto.
+  + proc. wp. auto.
   by auto.
 qed.
 
@@ -167,3 +169,30 @@ proof.
   ecall(test3 x).
   auto.
 qed.
+
+exception arg1 of int.
+
+module M3 = {
+  proc f () = {
+    raise (arg1 3);
+  }
+
+}.
+
+lemma test5 : 
+  hoare [M3.f : true ==> false | arg1 x => x = 3].
+proof.
+  proc. wp. skip => //.
+qed.
+
+lemma test6 : 
+  hoare [M3.f : true ==> false | arg1 x => x = 3].
+proof.
+  conseq (: _ ==> _ | arg1 x => 3 = x).
+  + done.
+  proc. wp. skip => //.
+qed.
+
+
+
+

src/ecAst.ml

@@ -652,26 +652,6 @@ let iter2_poe f (p1,m1,d1) (p2,m2,d2) =
   | Some d1, Some d2 -> f d1 d2
   | _, _ -> failwith "missing default exception"
 
-let merge2_poe_list f (poe1,d1) (poe2,d2) =
-  let get_default d =
-    match d with
-    | Some d -> d
-    | None ->  failwith "no default exception"
-  in
-  let aux _ a b =
-    match a,b with
-    | Some a, Some b -> Some (f b a)
-    | Some a, None -> Some (f (get_default d2) a)
-    | None, Some b -> Some (f b (get_default d1))
-    | None, None -> assert false
-  in
-  let epost = Mp.merge aux poe1 poe2 in
-  let poe = List.map snd (Mp.bindings epost) in
-  match d2, d1 with
-  | None, _ -> poe
-  | Some d2, Some d1 -> f d2 d1 :: poe
-  | _, _ -> failwith "no default exception"
-
 (* ----------------------------------------------------------------- *)
 (* Accessors for program logic                                       *)
 (* ----------------------------------------------------------------- *)

src/ecAst.mli

@@ -386,12 +386,6 @@ val forall2_poe : (form -> form -> bool) -> post -> post -> bool
 val poe_to_list : 'a * 'a Mp.t * 'a option -> 'a list
 val iter_poe : (form -> unit) -> post -> unit
 val iter2_poe : (form -> form -> unit) -> post -> post -> unit
-val merge2_poe_list :
-  (form -> form -> form) ->
-  form Mp.t * form option ->
-  form Mp.t * form option ->
-  form list
-
 
 (* -------------------------------------------------------------------- *)
 

src/ecProofTyping.ml

@@ -263,22 +263,30 @@ let destruct_exists ?(reduce = true) hyps fp : dexists option =
     lazy_destruct ~reduce hyps doit fp
 
 (* -------------------------------------------------------------------- *)
-let merge2_poe_list f (poe1,d1) (poe2,d2) =
+let merge2_poe_list (poe1,d1) (poe2,d2) =
   let get_default d =
     match d with
     | Some d -> d
     | None ->  failwith "no default exception"
   in
   let aux _ a b =
     match a,b with
-    | Some a, Some b -> Some (f b a)
-    | Some a, None -> Some (f (get_default d2) a)
-    | None, Some b -> Some (f b (get_default d1))
+    | Some a, Some b ->
+      let bd, body = decompose_lambda a in
+      let args = List.map (fun (x, gty) -> f_local x (gty_as_ty gty)) bd in
+      Some (f_forall bd (f_imp (f_app_simpl b args tbool) body))
+
+    | Some a, None ->
+      let bd, body = decompose_lambda a in
+      Some (f_forall bd (f_imp (get_default d2) body))
+    | None, Some b ->
+      let bd, body = decompose_lambda b in
+      Some (f_forall bd (f_imp body (get_default d1)))
     | None, None -> assert false
   in
   let epost = Mp.merge aux poe1 poe2 in
   let poe = List.map snd (Mp.bindings epost) in
   match d2, d1 with
   | None, _ -> poe
-  | Some d2, Some d1 -> f d2 d1 :: poe
+  | Some d2, Some d1 -> f_imp d2 d1 :: poe
   | _, _ -> failwith "no default exception"

src/ecProofTyping.mli

@@ -86,7 +86,6 @@ val destruct_exists : ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dexists  optio
 (* -------------------------------------------------------------------- *)
 
 val merge2_poe_list :
-  (form -> form -> form) ->
   form Mp.t * form option ->
   form Mp.t * form option ->
   form list

src/phl/ecPhlCall.ml

@@ -88,7 +88,7 @@ let t_hoare_call fpre fpost tc =
   let spre = subst_args_call env m (e_tuple args) PVM.empty in
   let post = map_ss_inv2 f_anda_simpl (map_ss_inv1 (PVM.subst env spre) fpre) post in
 
-  let poe = merge2_poe_list f_imp_simpl (epost,d) (fepost,fd) in
+  let poe = TTC.merge2_poe_list (epost,d) (fepost,fd) in
   let poe = List.map (fun inv -> {m;inv}) poe in
   let penv_e = EcEnv.Fun.inv_memenv1 m env in
   let poe = List.map (generalize_mod_ss_inv penv_e modi) poe in

src/phl/ecPhlConseq.ml

@@ -71,14 +71,15 @@ let t_hoareF_conseq pre post tc =
   let cond1, cond2 =
     conseq_cond_ss (hf_pr hf) {m;inv=fpost} pre {m;inv=post}
   in
-  let cond2e = merge2_poe_list f_imp (fepost,fd) (epost,d) in
+  let cond2e = TTC.merge2_poe_list (fepost,fd) (epost,d) in
   let cond2 = List.fold f_and cond2.inv cond2e in
   let concl1 = f_forall_mems_ss_inv mpr cond1 in
   let concl2 = f_forall_mems_ss_inv mpo {m;inv=cond2} in
   let concl3 = f_hoareF pre hf.hf_f {hsi_m=m;hsi_inv=(post, epost,d)} in
   FApi.xmutate1 tc `Conseq [concl1; concl2; concl3]
 
 (* -------------------------------------------------------------------- *)
+
 let t_hoareS_conseq pre post tc =
   let hs = tc1_as_hoareS tc in
   let pre = ss_inv_rebind pre (fst hs.hs_m) in
@@ -89,7 +90,7 @@ let t_hoareS_conseq pre post tc =
   let cond1, cond2 =
     conseq_cond_ss (hs_pr hs) {m;inv=fpost} pre {m;inv=post}
   in
-  let cond2e = merge2_poe_list f_imp (fepost,fd) (epost,d) in
+  let cond2e = TTC.merge2_poe_list (fepost,fd) (epost,d) in
   let cond2 = List.fold f_and cond2.inv cond2e in
   let concl1 = f_forall_mems_ss_inv hs.hs_m cond1 in
   let concl2 = f_forall_mems_ss_inv hs.hs_m {m=fst hs.hs_m;inv=cond2} in
@@ -351,7 +352,7 @@ let t_hoareF_notmod post tc =
   let (post, epost, d) = p.hsi_inv in
   let (fpost, fepost,fd) = (hf_po hf).hsi_inv in
   let cond = f_imp post fpost in
-  let econd1 = merge2_poe_list f_imp (fepost,fd) (epost,d) in
+  let econd1 = TTC.merge2_poe_list (fepost,fd) (epost,d) in
   let cond1 = List.fold f_and cond econd1 in
   let cond1, _, _ = cond_hoareF_notmod tc {m=hf.hf_m;inv=cond1} in
   let cond2 = f_hoareF (hf_pr hf) hf.hf_f p in
@@ -379,7 +380,7 @@ let t_hoareS_notmod post tc =
   let (post, epost, d) = p.hsi_inv in
   let (fpost, fepost,fd) = (hs_po hs).hsi_inv in
   let cond = f_imp post fpost in
-  let econd1 = merge2_poe_list f_imp (fepost,fd) (epost,d) in
+  let econd1 = TTC.merge2_poe_list (fepost,fd) (epost,d) in
   let cond1 = List.fold f_and cond econd1 in
   let cond1, _, _ = cond_hoareS_notmod tc {m=fst hs.hs_m;inv=cond1} in
   let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s p in

src/phl/ecPhlWp.ml

@@ -18,7 +18,7 @@ module LowInternal = struct
     let f = EcReduction.h_red_until EcReduction.full_red hyps f in
     let (ex, _tys), args = destr_op_app f in
     match Mp.find ex epost with
-    | f -> f_app f args EcTypes.tbool
+    | f -> f_app_simpl f args EcTypes.tbool
     | exception Not_found ->
       match d with
       | Some d -> d

theories/prelude/Pervasive.ec

@@ -34,3 +34,7 @@ op mu: 'a distr -> ('a -> bool) -> real.
 
 (* -------------------------------------------------------------------- *)
 op witness : 'a.                (* All types are inhabited in EC *)
+
+(* -------------------------------------------------------------------- *)
+
+type exn.