Internal: minor additions to EcLowPhlGoal & EcMatching modules

 - EcMatching.Zipper.map
 - EcLowPhlGoal.{is_program_logic,hl_set_stmt}

Author: strub

src/ecLowPhlGoal.ml

@@ -176,6 +176,26 @@ let tc1_as_equivF   tc = pf_as_equivF   !!tc (FApi.tc1_goal tc)
 let tc1_as_equivS   tc = pf_as_equivS   !!tc (FApi.tc1_goal tc)
 let tc1_as_eagerF   tc = pf_as_eagerF   !!tc (FApi.tc1_goal tc)
 
+(* -------------------------------------------------------------------- *)
+let is_program_logic (f : form) (ks : hlkind list) =
+  let do1 (k : hlkind) =
+    match f.f_node, k with
+    | FhoareF   _, `Hoare  (`Any | `Pred) -> true
+    | FeHoareF  _, `EHoare (`Any | `Pred) -> true
+    | FcHoareF  _, `CHoare (`Any | `Pred) -> true
+    | FbdHoareF _, `PHoare (`Any | `Pred) -> true
+    | FequivF   _, `Equiv  (`Any | `Pred) -> true
+    | FhoareS   _, `Hoare  (`Any | `Stmt) -> true
+    | FeHoareS  _, `EHoare (`Any | `Stmt) -> true
+    | FcHoareS  _, `CHoare (`Any | `Stmt) -> true
+    | FbdHoareS _, `PHoare (`Any | `Stmt) -> true
+    | FequivS   _, `Equiv  (`Any | `Stmt) -> true
+    | FeagerF   _, `Eager                 -> true
+    | _          , _                      -> false
+  in
+
+  List.exists do1 ks
+
 (* -------------------------------------------------------------------- *)
 let tc1_get_stmt side tc =
   let concl = FApi.tc1_goal tc in
@@ -193,6 +213,17 @@ let tc1_get_stmt side tc =
   | _            ->
       tc_error_noXhl ~kinds:(hlkinds_Xhl_r `Stmt) !!tc
 
+(* -------------------------------------------------------------------- *)
+let hl_set_stmt (side : side option) (f : form) (s : stmt) =
+  match side, f.f_node with
+  | None       , FhoareS   hs -> f_hoareS_r   { hs with hs_s  = s }
+  | None       , FeHoareS  hs -> f_eHoareS_r  { hs with ehs_s = s }
+  | None       , FcHoareS  hs -> f_cHoareS_r  { hs with chs_s = s }
+  | None       , FbdHoareS hs -> f_bdHoareS_r { hs with bhs_s = s }
+  | Some `Left , FequivS   es -> f_equivS_r   { es with es_sl = s }
+  | Some `Right, FequivS   es -> f_equivS_r   { es with es_sr = s }
+  | _          , _            -> assert false
+
 (* -------------------------------------------------------------------- *)
 let get_pre f =
   match f.f_node with

src/ecMatching.ml

@@ -188,6 +188,11 @@ module Zipper = struct
           | (state', [i']) when i == i' && state == state' -> (state, s)
           | (state', si  ) -> (state', zip { zpr with z_tail = si @ tl })
       end
+
+  let map cpos f s =
+    fst_map
+      Option.get
+      (fold () cpos (fun () _ i -> fst_map some (f i)) None s)
 end
 
 (* -------------------------------------------------------------------- *)

src/ecMatching.mli

@@ -58,14 +58,20 @@ module Zipper : sig
 
   type ('a, 'state) folder = 'a -> 'state -> instr -> 'state * instr list
 
-  (* [fold cl cpos f state s] create the zipper for [s] at [cpos], and apply
+  (* [fold v cpos f state s] create the zipper for [s] at [cpos], and apply
    * [f] to it, along with [v] and the state [state]. [f] must return the
    * new [state] and a new [zipper]. These last are directly returned.
    *
    * Raise [InvalidCPos] if [cpos] is not valid for [s], or any exception
    * raised by [f].
    *)
   val fold : 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
+
+  (* [map cpos f s] is a special case of [fold] where the state and the
+   * out-of-band data are absent
+   *)
+  val map : codepos -> (instr -> 'a * instr list) -> stmt -> 'a * stmt
+
 end
 
 (* -------------------------------------------------------------------- *)