Add forward ecall with framed preconditions

src/ecAst.mli

@@ -480,6 +480,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/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/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

src/ecPV.ml

@@ -155,6 +155,9 @@ module PVM = struct
     try Mid.change (fun o -> Some (Mpv.add env pv f (odfl Mpv.empty o))) m s
     with AliasClash (env,c) -> uerror env c
 
+  let of_list env pvs =
+    List.fold_left (fun s ((pv, m), f) -> add env pv m f s) empty pvs
+
   let find env pv m s =
     try Mpv.find env pv (Mid.find m s)
     with AliasClash (env,c) -> uerror env c
@@ -580,6 +583,11 @@ let rec e_read_r env r e =
   | Evar pv -> PV.add env pv e.e_ty r
   | _ -> e_fold (e_read_r env) r e
 
+let rec form_read_r env r f =
+  match f.f_node with
+  | Fpvar (pv, _) -> PV.add env pv f.f_ty r
+  | _ -> f_fold (form_read_r env) r f
+
 let rec is_read_r env w s =
   List.fold_left (i_read_r env) w s
 
@@ -624,11 +632,12 @@ let is_write ?(except=Sx.empty) env is = is_write_r ~except env PV.empty is
 let s_write  ?(except=Sx.empty) env s  = s_write_r  ~except env PV.empty s
 let f_write  ?(except=Sx.empty) env f  = f_write_r  ~except env PV.empty f
 
-let e_read  env e  = e_read_r  env PV.empty e
-let i_read  env i  = i_read_r  env PV.empty i
-let is_read env is = is_read_r env PV.empty is
-let s_read  env s  = s_read_r  env PV.empty s
-let f_read  env f  = f_read_r  env PV.empty f
+let e_read     env e  = e_read_r  env PV.empty e
+let form_read  env e  = form_read_r  env PV.empty e
+let i_read     env i  = i_read_r  env PV.empty i
+let is_read    env is = is_read_r env PV.empty is
+let s_read     env s  = s_read_r  env PV.empty s
+let f_read     env f  = f_read_r  env PV.empty f
 
 (* -------------------------------------------------------------------- *)
 type pmvs = PV.t Mid.t

src/ecPV.mli

@@ -71,6 +71,8 @@ module PVM : sig
 
   val add : env -> prog_var -> EcIdent.t -> form -> subst -> subst
 
+  val of_list : env -> ((prog_var * EcIdent.t) * form) list -> subst
+
   val add_glob : env -> mpath -> EcIdent.t -> form -> subst -> subst
 
   val of_mpv : (form,form) Mpv.t -> EcIdent.t -> subst
@@ -127,11 +129,12 @@ val is_write_r : ?except:Sx.t -> instr list pvaccess
 val s_write_r  : ?except:Sx.t -> stmt       pvaccess
 val f_write_r  : ?except:Sx.t -> xpath      pvaccess
 
-val e_read_r   : expr       pvaccess
-val i_read_r   : instr      pvaccess
-val is_read_r  : instr list pvaccess
-val s_read_r   : stmt       pvaccess
-val f_read_r   : xpath      pvaccess
+val e_read_r      : expr       pvaccess
+val form_read_r   : form       pvaccess
+val i_read_r      : instr      pvaccess
+val is_read_r     : instr list pvaccess
+val s_read_r      : stmt       pvaccess
+val f_read_r      : xpath      pvaccess
 
 (* -------------------------------------------------------------------- *)
 type 'a pvaccess0 = env -> 'a -> PV.t
@@ -142,11 +145,12 @@ val is_write : ?except:Sx.t -> instr list pvaccess0
 val s_write  : ?except:Sx.t -> stmt       pvaccess0
 val f_write  : ?except:Sx.t -> xpath      pvaccess0
 
-val e_read  : expr       pvaccess0
-val i_read  : instr      pvaccess0
-val is_read : instr list pvaccess0
-val s_read  : stmt       pvaccess0
-val f_read  : xpath      pvaccess0
+val e_read     : expr       pvaccess0
+val form_read  : form       pvaccess0
+val i_read     : instr      pvaccess0
+val is_read    : instr list pvaccess0
+val s_read     : stmt       pvaccess0
+val f_read     : xpath      pvaccess0
 
 (* -------------------------------------------------------------------- *)
 type pmvs = PV.t EcIdent.Mid.t

src/ecParser.mly

@@ -2930,6 +2930,10 @@ interleave_info:
 | TILD f=loc(fident) { OKproc(f, true) }
 | f=loc(fident) { OKproc(f, false) }
 
+direction:
+| RRARROW { (`Forward  :> pdirection) }
+| LLARROW { (`Backward :> pdirection) }
+
 %public phltactic:
 | PROC
    { Pfun `Def }
@@ -3115,8 +3119,8 @@ interleave_info:
 
     { Phrex_intro (l, b) }
 
-| ECALL s=side? x=paren(p=qident tvi=tvars_app? fs=sform* { (p, tvi, fs) })
-    { Phecall (s, x) }
+| ECALL d=direction? s=side? x=paren(p=qident tvi=tvars_app? fs=loc(gpterm_arg)* { (p, tvi, fs) })
+    { Phecall (odfl `Backward d, s, x) }
 
 | EXFALSO
     { Pexfalso }

src/ecParsetree.ml

@@ -736,6 +736,12 @@ type matchmode = [
 (* -------------------------------------------------------------------- *)
 type prrewrite = [`Rw of ppterm | `Simpl]
 
+(* -------------------------------------------------------------------- *)
+type pecall = pqsymbol * ptyannot option * ppt_arg located list
+
+(* -------------------------------------------------------------------- *)
+type pdirection = [`Forward | `Backward]
+
 (* -------------------------------------------------------------------- *)
 type phltactic =
   | Pskip
@@ -774,7 +780,7 @@ type phltactic =
   | Pconcave       of (pformula option tuple2 gppterm * pformula)
   | Phrex_elim
   | Phrex_intro    of (pformula list * bool)
-  | Phecall        of (oside * (pqsymbol * ptyannot option * pformula list))
+  | Phecall        of (pdirection * oside * pecall)
   | Pexfalso
   | Pbydeno        of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option))
   | PPr            of (pformula * pformula) option

src/ecProofTerm.ml

@@ -789,6 +789,12 @@ and apply_pterm_to_hole ?loc pt =
 and apply_pterm_to_holes ?loc n pt =
   EcUtils.iterop (apply_pterm_to_hole ?loc) n pt
 
+(* -------------------------------------------------------------------- *)
+and apply_pterm_to_max_holes (hyps : LDecl.hyps) (pt : pt_ev) =
+  if is_some (PT.destruct_product ~reduce:true hyps pt.ptev_ax) then
+    apply_pterm_to_max_holes hyps (apply_pterm_to_hole pt)
+  else pt
+
 (* -------------------------------------------------------------------- *)
 and apply_pterm_to_local ?loc pt id =
   match LDecl.by_id id pt.ptev_env.pte_hy with
@@ -964,3 +970,90 @@ module Prept = struct
   let ahyp h    = asub (hyp h)
   let ahdl h    = asub (hdl h)
 end
+
+(* -------------------------------------------------------------------- *)
+let pvcompare (pv1 : prog_var) (pv2 : prog_var) =
+  match pv1, pv2 with
+  | PVglob x1, PVglob x2 ->
+    EcPath.x_compare x1 x2
+  | PVloc s1, PVloc s2 ->
+    EcSymbols.sym_compare s1 s2
+
+  | PVglob _, PVloc  _ ->  1
+  | PVloc  _, PVglob _ -> -1
+
+module Mpv = Map.Make(struct
+  type t = prog_var
+  let compare = pvcompare
+end)
+
+type mpvars = (ty Mpv.t) Mid.t
+
+(* -------------------------------------------------------------------- *)
+let rec collect_pvars_from_pt (pvs : mpvars) (pt : proofterm) =
+  match pt with
+  | PTApply { pt_args = args } -> begin
+    List.fold_left collect_pvars_from_ptarg pvs args
+  end
+  | PTQuant (_, pt) ->
+    collect_pvars_from_pt pvs pt
+
+and collect_pvars_from_ptarg (pvs : mpvars) (ptarg : pt_arg) =
+  match ptarg with
+  | PAFormula f -> collect_pvars_from_form pvs f
+  | PAMemory _ -> pvs
+  | PAModule _ -> pvs
+  | PASub None -> pvs
+  | PASub (Some pt) -> collect_pvars_from_pt pvs pt
+
+and collect_pvars_from_form (pvs : mpvars) (f : form) =
+  let rec doit (pvs : mpvars) (f : form) =
+    match f.f_node with
+    | Fpvar (pv, m) ->
+      Mid.change (fun pvmap ->
+        Some (Mpv.add pv f.f_ty (odfl Mpv.empty pvmap))
+      ) m pvs
+    | _ -> EcFol.f_fold doit pvs f
+  in doit pvs f
+
+(* -------------------------------------------------------------------- *)
+let collect_pvars_from_pt (pt : proofterm) =
+  Mid.map Mpv.bindings (collect_pvars_from_pt Mid.empty pt)
+
+(* -------------------------------------------------------------------- *)
+module PV = struct
+  open EcPV.PVM
+
+  let rec subst_pt (env : env) (subst : subst) (pt : proofterm) =
+    match pt with
+    | PTApply { pt_head; pt_args } ->
+      PTApply
+        { pt_head = subst_pt_head env subst pt_head
+        ; pt_args = List.map (subst_pt_arg env subst) pt_args }
+    | PTQuant (bds, pt) ->
+      PTQuant (bds, subst_pt env subst pt)
+
+  and subst_pt_head (env : env) (subst : subst) (pth : pt_head) =
+    match pth with
+    | PTHandle _
+    | PTLocal _
+    | PTGlobal _ -> pth
+    | PTCut (f, cs) -> PTCut (subst_form env subst f, cs)
+    | PTTerm pt -> PTTerm (subst_pt env subst pt)
+
+  and subst_pt_arg (env : env) (subst : subst) (pta : pt_arg) =
+    match pta with
+    | PAFormula f -> PAFormula (subst_form env subst f)
+    | PAMemory _  -> pta
+    | PAModule _  -> pta
+    | PASub    pt -> PASub (omap (subst_pt env subst) pt)
+
+  and subst_form (env : env) (subst : subst) (f : form) =
+    EcPV.PVM.subst env subst f
+end
+
+let subst_pv_pt (env : env) (subst : EcPV.PVM.subst) (pt : proofterm) =
+  PV.subst_pt env subst pt
+
+let subst_pv_pt_arg (env : env) (subst : EcPV.PVM.subst) (pt_arg : pt_arg) =
+  PV.subst_pt_arg env subst pt_arg

src/ecProofTerm.mli

@@ -64,6 +64,8 @@ val process_pterm_cut
   : prcut:('a -> form) -> pt_env -> 'a ppt_head -> pt_ev
 val process_pterm
   : pt_env -> (pformula option) ppt_head -> pt_ev
+val process_pterm_arg
+  :  ?implicits:bool -> pt_ev  -> ppt_arg located -> pt_ev_arg
 val process_pterm_args_app
   :  ?implicits:bool -> ?ip:(bool list) -> pt_ev  -> ppt_arg located list
   -> pt_ev * bool list
@@ -99,11 +101,12 @@ val check_pterm_arg :
   -> pt_ev_arg_r
  -> form * pt_arg
 
-val apply_pterm_to_arg   : ?loc:EcLocation.t -> pt_ev -> pt_ev_arg -> pt_ev
-val apply_pterm_to_arg_r : ?loc:EcLocation.t -> pt_ev -> pt_ev_arg_r -> pt_ev
-val apply_pterm_to_local : ?loc:EcLocation.t -> pt_ev -> EcIdent.t -> pt_ev
-val apply_pterm_to_hole  : ?loc:EcLocation.t -> pt_ev -> pt_ev
-val apply_pterm_to_holes : ?loc:EcLocation.t -> int -> pt_ev -> pt_ev
+val apply_pterm_to_arg       : ?loc:EcLocation.t -> pt_ev -> pt_ev_arg -> pt_ev
+val apply_pterm_to_arg_r     : ?loc:EcLocation.t -> pt_ev -> pt_ev_arg_r -> pt_ev
+val apply_pterm_to_local     : ?loc:EcLocation.t -> pt_ev -> EcIdent.t -> pt_ev
+val apply_pterm_to_hole      : ?loc:EcLocation.t -> pt_ev -> pt_ev
+val apply_pterm_to_holes     : ?loc:EcLocation.t -> int -> pt_ev -> pt_ev
+val apply_pterm_to_max_holes : LDecl.hyps -> pt_ev -> pt_ev
 
 (* pattern matching - raise [MatchFailure] on failure. *)
 val pf_form_match : pt_env -> ?mode:fmoptions -> ptn:form -> form -> unit
@@ -198,3 +201,9 @@ module Prept : sig
   val ahyp  : EcIdent.t -> prept_arg
   val ahdl  : handle -> prept_arg
 end
+
+(* -------------------------------------------------------------------- *)
+val collect_pvars_from_pt : proofterm -> ((prog_var * ty) list) EcIdent.Mid.t
+
+val subst_pv_pt :  EcEnv.env -> EcPV.PVM.subst -> proofterm -> proofterm
+val subst_pv_pt_arg :  EcEnv.env -> EcPV.PVM.subst -> pt_arg -> pt_arg