remove unused argument extend t_code_transform to ehoare

Author: bgregoir

src/ecLowPhlGoal.ml

@@ -789,7 +789,7 @@ let t_zip f (cenv : code_txenv) (cpos : codepos) (prpo : form * form) (state, s)
       ((me, Zpr.zip zpr, gs) : memenv * _ * form list)
   with InvalidCPos -> tc_error (fst cenv) "invalid code position"
 
-let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
+let t_code_transform (side : oside) cpos tr tx tc =
   let pf = FApi.tc1_penv tc in
 
   match side with
@@ -799,27 +799,32 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
       match concl.f_node with
       | FhoareS hs ->
           let pr, po = hs_pr hs, hs_po hs in
+          (* FIXME: This is very suspicious why only main is provided ? *)
           let po = po.hsi_inv.main in
           let (me, stmt, cs) =
             tx (pf, hyps) cpos (pr.inv, po) (hs.hs_m, hs.hs_s) in
           let concl =
-            f_hoareS (snd me) (hs_pr hs) stmt (hs_po hs)
+            f_hoareS (snd me) pr stmt (hs_po hs)
           in
           FApi.xmutate1 tc (tr None) (cs @ [concl])
 
-      | FbdHoareS bhs when bdhoare ->
+      | FbdHoareS bhs ->
           let pr, po = bhs_pr bhs, bhs_po bhs in
           let (me, stmt, cs) =
             tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in
-          let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs)
-                      bhs.bhs_cmp (bhs_bd bhs) in
+          let concl = f_bdHoareS (snd me) pr stmt po bhs.bhs_cmp (bhs_bd bhs) in
+          FApi.xmutate1 tc (tr None) (cs @ [concl])
+
+      | FeHoareS ehs ->
+          let pr, po = ehs_pr ehs, ehs_po ehs in
+          let (me, stmt, cs) =
+            tx (pf, hyps) cpos (pr.inv, po.inv) (ehs.ehs_m, ehs.ehs_s) in
+          let concl = f_eHoareS (snd me) pr stmt po in
           FApi.xmutate1 tc (tr None) (cs @ [concl])
 
       | _ ->
         let kinds =
-            (if bdhoare then [`PHoare `Stmt] else [])
-          @ [`Hoare `Stmt] in
-
+            [`PHoare `Stmt; `Hoare `Stmt; `EHoare `Stmt ] in
         tc_error_noXhl ~kinds:kinds pf
   end
 

src/phl/ecPhlCodeTx.ml

@@ -78,7 +78,7 @@ let t_kill_r side cpos olen tc =
   in
 
   let tr = fun side -> `Kill (side, cpos, olen) in
-  t_code_transform side ~bdhoare:true cpos tr (t_zip kill_stmt) tc
+  t_code_transform side cpos tr (t_zip kill_stmt) tc
 
 (* -------------------------------------------------------------------- *)
 let alias_stmt env id (pf, _) me i =
@@ -109,7 +109,7 @@ let alias_stmt env id (pf, _) me i =
 let t_alias_r side cpos id g =
   let env = FApi.tc1_env g in
   let tr = fun side -> `Alias (side, cpos) in
-  t_code_transform side ~bdhoare:true cpos tr (t_fold (alias_stmt env id)) g
+  t_code_transform side cpos tr (t_fold (alias_stmt env id)) g
 
 (* -------------------------------------------------------------------- *)
 let set_stmt (fresh, id) e =
@@ -136,7 +136,7 @@ let set_stmt (fresh, id) e =
 
 let t_set_r side cpos (fresh, id) e tc =
   let tr = fun side -> `Set (side, cpos) in
-  t_code_transform side ~bdhoare:true cpos tr (t_zip (set_stmt (fresh, id) e)) tc
+  t_code_transform side cpos tr (t_zip (set_stmt (fresh, id) e)) tc
 
 (* -------------------------------------------------------------------- *)
 let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) =
@@ -181,7 +181,7 @@ let set_match_stmt (id : symbol) ((ue, mev, ptn) : _ * _ * form) =
 
 let t_set_match_r (side : oside) (cpos : Position.codepos) (id : symbol) pattern tc =
   let tr = fun side -> `SetMatch (side, cpos) in
-  t_code_transform side ~bdhoare:true cpos tr
+  t_code_transform side cpos tr
     (t_zip (set_match_stmt id pattern)) tc
 
 (* -------------------------------------------------------------------- *)
@@ -424,7 +424,7 @@ let t_cfold
 =
     let tr = fun side -> `Fold (side, cpos, olen) in
     let cb = fun cenv _ me zpr -> cfold_stmt ~eager cenv me olen zpr in
-    t_code_transform side ~bdhoare:true cpos tr (t_zip cb) tc
+    t_code_transform side cpos tr (t_zip cb) tc
 
 (* -------------------------------------------------------------------- *)
 let t_kill      = FApi.t_low3 "code-tx-kill"      t_kill_r
@@ -619,7 +619,7 @@ let transform_if_stmt env (pf, _) me i =
 let t_transform_if_r side cpos g =
   let env = FApi.tc1_env g in
   let tr = fun side -> `TransformIf (side, cpos) in
-  t_code_transform side ~bdhoare:true cpos tr (t_fold (transform_if_stmt env)) g
+  t_code_transform side cpos tr (t_fold (transform_if_stmt env)) g
 
 let t_transform_if = FApi.t_low2 "code-tx-transform_if" t_transform_if_r
 

src/phl/ecPhlLoopTx.ml

@@ -115,7 +115,7 @@ let fission_stmt (il, (d1, d2)) (pf, hyps) me zpr =
 let t_fission_r side cpos infos g =
   let tr = fun side -> `LoopFission (side, cpos, infos) in
   let cb = fun cenv _ me zpr -> fission_stmt infos cenv me zpr in
-  t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g
+  t_code_transform side cpos tr (t_zip cb) g
 
 let t_fission = FApi.t_low3 "loop-fission" t_fission_r
 
@@ -170,7 +170,7 @@ let fusion_stmt (il, (d1, d2)) (pf, hyps) me zpr =
 let t_fusion_r side cpos infos g =
   let tr = fun side -> `LoopFusion (side, cpos, infos) in
   let cb = fun cenv _ me zpr -> fusion_stmt infos cenv me zpr in
-  t_code_transform side ~bdhoare:true cpos tr (t_zip cb) g
+  t_code_transform side cpos tr (t_zip cb) g
 
 let t_fusion = FApi.t_low3 "loop-fusion" t_fusion_r
 
@@ -182,7 +182,7 @@ let unroll_stmt (pf, _) me i =
 
 let t_unroll_r side cpos g =
   let tr = fun side -> `LoopUnraoll (side, cpos) in
-  t_code_transform side ~bdhoare:true cpos tr (t_fold unroll_stmt) g
+  t_code_transform side cpos tr (t_fold unroll_stmt) g
 
 let t_unroll = FApi.t_low2 "loop-unroll" t_unroll_r
 
@@ -199,7 +199,7 @@ let splitwhile_stmt b (pf, _) me i =
 
 let t_splitwhile_r b side cpos g =
   let tr = fun side -> `SplitWhile (b, side, cpos) in
-  t_code_transform side ~bdhoare:true cpos tr (t_fold (splitwhile_stmt b)) g
+  t_code_transform side cpos tr (t_fold (splitwhile_stmt b)) g
 
 let t_splitwhile = FApi.t_low3 "split-while" t_splitwhile_r