Fix Conseq rule

Author: lyonel2017

examples/exception.ec

@@ -5,16 +5,86 @@ exception tata.
 
 module M ={
   proc truc (x:int) : int = {
-    if (x = 3)  {raise toto;} else{ x <- 5; }
+    if (x = 3)  {
+       raise toto;
+    } else { x <- 5; }
   return x;
   }
 }.
 
-lemma truc :
-hoare [M.truc : true ==> (4 < res) | toto:(res = 3) |tata:(res=2) ].
+lemma truc (_x: int):
+hoare [M.truc : _x = x ==> (4 < res) | toto:(_x = 3) | tata:(false) ].
     proof.
       proc.
-      conseq (: _ ==> x = 5).
-      + smt.
+       conseq (: _ ==> x = 5).
       + auto.
+      + auto.
+    qed.
+
+exception assume.
+exception assert.
+
+module M' ={
+  proc truc (x:int) : int = {
+    if (x = 3)  {
+       raise assume;
+    }
+    if (x=3) {
+        raise assert;
+      }
+  return x;
+  }
+}.
+
+(* lemma assume_assert : *)
+(* hoare [M'.truc : true ==> true | assume:true |assert: false ]. *)
+(*     proof. *)
+(*       proc. *)
+(*       wp. *)
+(*     auto. *)
+(*     qed. *)
+
+(* lemma assert_assume : *)
+(* hoare [M'.truc : x <> 3 ==> true | assume:false |assert: true ]. *)
+(*     proof. *)
+(*       proc. *)
+(*       wp. *)
+(*     auto. *)
+(*     qed. *)
+
+op p1: bool.
+op p2: bool.
+op p3: bool.
+op p4: bool.
+op p5: bool.
+op p6: bool.
+op p7: bool.
+op p8: bool.
+op p9: bool.
+
+lemma assume_assert :
+hoare [M'.truc : p7 ==> p3 | assume:p1 |assert: p2 ].
+    proof.
+admitted.
+
+op q1: bool.
+op q2: bool.
+op q3: bool.
+
+
+  lemma assert_assume :
+hoare [M'.truc : p8 ==> q3 | assume:q1 |assert: q2 ].
+    proof.
+admitted.
+
+
+(*Conseq is brocken, should take into account the post of exception*)
+  lemma assert_assume' :
+hoare [M'.truc : p9 ==> p4 | assume:p6 |assert: p5 ].
+    proof.
+      conseq (assume_assert) (assert_assume).
+      + admit.
+      + admit.
+      + admit.
+      + admit.
     qed.

src/ecAst.ml

@@ -230,7 +230,7 @@ and equivS = {
   es_sr  : stmt;
   es_po  : form; }
 
-and post = (memory * form) list
+and post = ((* EcPath.path *) memory * form) list
 
 and sHoareF = {
   hf_pr : form;

src/ecLowPhlGoal.ml

@@ -251,6 +251,18 @@ let tc1_get_post tc =
   | None   -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc
   | Some f -> f
 
+(* -------------------------------------------------------------------- *)
+let get_poste f =
+  match f.f_node with
+  | FhoareF hf   -> Some (hf.hf_poe )
+  | FhoareS hs   -> Some (hs.hs_poe )
+  | _            -> None
+
+let tc1_get_poste tc =
+  match get_poste (FApi.tc1_goal tc) with
+  | None   -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc
+  | Some f -> f
+
 (* -------------------------------------------------------------------- *)
 let set_pre ~pre f =
   match f.f_node with

src/ecTyping.ml

@@ -3501,7 +3501,7 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
         let epost' =
           List.map (fun (e,f) ->
               let symb,_ = except_genpath env e in
-              EcIdent.create symb,transf qenv f
+              EcIdent.create symb,transf penv f
             ) eposts
         in
 

src/phl/ecPhlApp.ml

@@ -86,7 +86,7 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
 let t_bdhoare_app_r i info tc =
   let tactic tc =
     let hs  = tc1_as_hoareS tc in
-    let tt1 = EcPhlConseq.t_hoareS_conseq_nm hs.hs_pr f_true in
+    let tt1 = EcPhlConseq.t_hoareS_conseq_nm hs.hs_pr f_true hs.hs_poe in
     let tt2 = EcPhlAuto.t_pl_trivial in
     FApi.t_seqs [tt1; tt2; t_fail] tc
   in