Forward call with framed pre

Author: strub

src/ecAst.mli

@@ -478,6 +478,7 @@ val pv_hash  : prog_var hash
 val pv_fv    : prog_var fv
 
 val pv_kind : prog_var -> pvar_kind
+
 (* -------------------------------------------------------------------- *)
 val idty_equal : (EcIdent.t * ty) equality
 val idty_hash  : (EcIdent.t * ty) hash

src/ecCoreFol.ml

@@ -562,6 +562,11 @@ let f_iter g f =
   | FeagerF   eg  -> g (eg_pr eg).inv; g (eg_po eg).inv
   | Fpr       pr  -> g pr.pr_args; g pr.pr_event.inv
 
+(* -------------------------------------------------------------------- *)
+let f_fold (tx : 'a -> form -> 'a) (state : 'a) (f : form) =
+  let state = ref state in
+  f_iter (fun f -> state := tx !state f) f;
+  !state
 
 (* -------------------------------------------------------------------- *)
 let form_exists g f =

src/ecCoreFol.mli

@@ -76,6 +76,7 @@ val f_node  : form -> f_node
 (* not recursive *)
 val f_map  : (EcTypes.ty -> EcTypes.ty) -> (form -> form) -> form -> form
 val f_iter : (form -> unit) -> form -> unit
+val f_fold : ('a -> form -> 'a) -> 'a -> form -> 'a
 val form_exists: (form -> bool) -> form -> bool
 val form_forall: (form -> bool) -> form -> bool
 

src/ecEnv.ml

@@ -3569,30 +3569,40 @@ module LDecl = struct
   let fresh_id  hyps s = fresh_id  (tohyps hyps) s
   let fresh_ids hyps s = snd (fresh_ids (tohyps hyps) s)
 
+  (* ------------------------------------------------------------------ *)
+  let mapenv (f : env -> env) (lenv : hyps) =
+    { lenv with le_env = f lenv.le_env }
+
   (* ------------------------------------------------------------------ *)
   let push_active_ss m lenv =
-    { lenv with le_env = Memory.push_active_ss m lenv.le_env }
+    mapenv (Memory.push_active_ss m) lenv
 
   let push_active_ts ml mr lenv =
-    { lenv with le_env = Memory.push_active_ts ml mr lenv.le_env }
+    mapenv (Memory.push_active_ts ml mr) lenv
 
   let push_all l lenv =
-    { lenv with le_env = Memory.push_all l lenv.le_env }
+    mapenv (Memory.push_all l) lenv
+
+  let push_active_all l lenv =
+    let lenv = mapenv (Memory.push_all l) lenv in
+
+    match l with
+    | [(m, _)] -> mapenv (Memory.set_active_ss m) lenv
+    | _ -> lenv
 
   let hoareF mem xp lenv =
      let env1, env2 = Fun.hoareF mem xp lenv.le_env in
-    { lenv with le_env = env1}, {lenv with le_env = env2 }
+    { lenv with le_env = env1 }, { lenv with le_env = env2 }
 
   let equivF ml mr xp1 xp2 lenv =
     let env1, env2 = Fun.equivF ml mr xp1 xp2 lenv.le_env in
-    { lenv with le_env = env1}, {lenv with le_env = env2 }
+    { lenv with le_env = env1 }, { lenv with le_env = env2 }
 
   let inv_memenv ml mr lenv =
-    { lenv with le_env = Fun.inv_memenv ml mr lenv.le_env }
+    mapenv (Fun.inv_memenv ml mr) lenv
 
   let inv_memenv1 m lenv =
-    { lenv with le_env = Fun.inv_memenv1 m lenv.le_env }
+    mapenv (Fun.inv_memenv1 m) lenv
 end
 
-
 let pp_debug_form = ref (fun _env _f -> assert false)

src/ecEnv.mli

@@ -515,9 +515,10 @@ module LDecl : sig
 
   val clear : ?leniant:bool -> EcIdent.Sid.t -> hyps -> hyps
 
-  val push_all       : memenv list -> hyps -> hyps
-  val push_active_ss : memenv -> hyps -> hyps
-  val push_active_ts : memenv -> memenv -> hyps -> hyps
+  val push_all        : memenv list -> hyps -> hyps
+  val push_active_all : memenv list -> hyps -> hyps
+  val push_active_ss  : memenv -> hyps -> hyps
+  val push_active_ts  : memenv -> memenv -> hyps -> hyps
 
   val hoareF : memory -> xpath -> hyps -> hyps * hyps
   val equivF : memory -> memory -> xpath -> xpath -> hyps -> hyps * hyps

src/ecFol.ml

@@ -1104,6 +1104,25 @@ let rec one_sided_vs mem fp =
   | Fapp (f, args) -> one_sided_vs mem f @ List.concat_map (one_sided_vs mem) args
   | _ -> []
 
+(* -------------------------------------------------------------------- *)
+let filter_topand_form (test : form -> bool) =
+  let rec doit (f : form) =
+    match sform_of_form f with
+    | SFand (mode, (f1, f2)) -> begin
+      match doit f1, doit f2 with
+      | None, None -> None
+      | Some f, None | None, Some f -> Some f
+      | Some f1, Some f2 -> begin
+        match mode with
+        | `Sym -> Some (f_and f1 f2)
+        | `Asym -> Some (f_anda f1 f2)
+      end
+    end
+    | _ ->
+      if test f then Some f else None
+  in fun f -> doit f
+
+(* -------------------------------------------------------------------- *)
 let rec dump_f f =
   let dump_quant q =
     match q with

src/ecFol.mli

@@ -260,5 +260,8 @@ module DestrReal : sig
   val abs : form -> form
 end
 
+(* -------------------------------------------------------------------- *)
+val filter_topand_form : (form -> bool) -> form -> form option
+
 (* -------------------------------------------------------------------- *)
 val dump_f : form -> string

src/ecHiTacticals.ml

@@ -206,7 +206,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pconcave info             -> EcPhlConseq.process_concave info
     | Phrex_elim                -> EcPhlExists.t_hr_exists_elim
     | Phrex_intro (fs, b)       -> EcPhlExists.process_exists_intro ~elim:b fs
-    | Phecall (oside, x)        -> EcPhlExists.process_ecall oside x
+    | Phecall (d, s, data)      -> EcPhlExists.process_ecall d s data
     | Pexfalso                  -> EcPhlAuto.t_exfalso
     | Pbydeno (mode, info)      -> EcPhlDeno.process_deno mode info
     | Pbyupto                   -> EcPhlUpto.process_uptobad

src/ecMatching.ml

@@ -372,6 +372,10 @@ module EV = struct
     | Some (`Set _) -> true
     | _ -> false
 
+  let map (f : 'a -> 'a) (m : 'a evmap) =
+    { ev_map   = Mid.map (omap f) m.ev_map
+    ; ev_unset = m.ev_unset }
+
   let doget (x : ident) (m : 'a evmap) =
     match get x m with
     | Some (`Set a) -> a

src/ecMatching.mli

@@ -150,6 +150,7 @@ module EV : sig
   val isset  : ident -> 'a evmap -> bool
   val set    : ident -> 'a -> 'a evmap -> 'a evmap
   val get    : ident -> 'a evmap -> [`Unset | `Set of 'a] option
+  val map    : ('a -> 'a) -> 'a evmap -> 'a evmap
   val doget  : ident -> 'a evmap -> 'a
   val fold   : (ident -> 'a -> 'b -> 'b) -> 'a evmap -> 'b -> 'b
   val filled : 'a evmap -> bool