feat: variant for up-to-bad call/proc tactics

src/ecHiTacticals.ml

@@ -188,7 +188,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pfusion info              -> EcPhlLoopTx.process_fusion info
     | Punroll info              -> EcPhlLoopTx.process_unroll info
     | Psplitwhile info          -> EcPhlLoopTx.process_splitwhile info
-    | Pcall (side, info)        -> EcPhlCall.process_call side info
+    | Pcall info                -> EcPhlCall.process_call info
     | Pcallconcave info         -> EcPhlCall.process_call_concave info
     | Pswap sw                  -> EcPhlSwap.process_swap sw
     | Pinline info              -> EcPhlInline.process_inline info

src/ecParser.mly

@@ -21,6 +21,15 @@
     pty_locality = locality;
   }
 
+  let map_gppterm f a =
+    let fp_head = match a.fp_head with
+      | FPNamed _ as x -> x
+      | FPCut x -> FPCut (f x)
+    in
+    { a with fp_head }
+
+  let apply_gppterm x = map_gppterm (fun f -> f x)
+
   let opdef_of_opbody ty b =
     match b with
     | None            -> PO_abstr ty
@@ -2315,6 +2324,13 @@ intro_pattern:
 | cm=crushmode
    { IPCrush cm }
 
+gpterm_head0(F):
+| p=qident tvi=tvars_app?
+   { (false, FPNamed (p, tvi)) }
+
+| LPAREN exp=iboption(AT) UNDERSCORE? COLON f=F RPAREN
+   { (exp, FPCut f) }
+
 gpterm_head(F):
 | exp=iboption(AT) p=qident tvi=tvars_app?
    { (exp, FPNamed (p, tvi)) }
@@ -2353,7 +2369,7 @@ gpterm_arg:
     { EA_tactic `DoneSmt }
 
 gpterm(F):
-| hd=gpterm_head(F)
+| hd=gpterm_head0(F)
    { mk_pterm (fst hd) (snd hd) [] }
 
 | LPAREN hd=gpterm_head(F) args=loc(gpterm_arg)* RPAREN
@@ -2534,13 +2550,13 @@ conseq_xt:
 
 call_info:
 | f1=form LONGARROW f2=form poe=hoare_epost(none)
-    { CI_spec (f1, { pnormal = f2; pexcept = poe}) }
+    { fun _ -> CI_spec (f1, { pnormal = f2; pexcept = poe}) }
 | f=form
-    { CI_inv  (f) }
+    { fun _ -> CI_inv  (f) }
 | bad=form COMMA p=form
-    { CI_upto (bad,p,None) }
+    { fun b -> CI_upto (b,bad,p,None) }
 | bad=form COMMA p=form COMMA q=form
-    { CI_upto (bad,p,Some q) }
+    { fun b -> CI_upto (b,bad,p,Some q) }
 
 icodepos_r:
 | IF       { (`If     :> pcp_match) }
@@ -2646,11 +2662,11 @@ s_codegap1_before_(I):
 | LBRACKET cps=codepos1 DOTDOT cpe=codepos1 RBRACKET
     { (GapBefore cps, GapAfter cpe) }
 
-| LBRACKET cps=codepos1 PLUSGT cpo=loc(mparen(sword)) RBRACKET { 
+| LBRACKET cps=codepos1 PLUSGT cpo=loc(mparen(sword)) RBRACKET {
     if unloc cpo > 0 then begin
         let (offset, base) = cps in
         (GapBefore cps, GapAfter (offset + unloc cpo, base))
-    end else 
+    end else
         parse_error (loc cpo) (Some "cannot give negative offset for codepos range end")
   }
 
@@ -2955,7 +2971,7 @@ eager_tac:
     { Peager_fun_abs f }
 
 | CALL info=gpterm(call_info)
-    { Peager_call info }
+    { Peager_call (apply_gppterm None info) }
 
 form_or_double_form:
 | f=sform
@@ -3033,8 +3049,8 @@ direction:
 | PROC f=sform
    { Pfun (`Abs f) }
 
-| PROC bad=sform p=sform q=sform?
-   { Pfun (`Upto (bad, p, q)) }
+| PROC c=calloptions bad=sform p=sform q=sform?
+   { Pfun (`Upto (c, bad, p, q)) }
 
 | PROC STAR
    { Pfun `Code }
@@ -3057,11 +3073,11 @@ direction:
 | ASYNC WHILE info=async_while_tac_info
     { Pasyncwhile info }
 
-| CALL s=side? info=gpterm(call_info)
-    { Pcall (s, info) }
+| CALL c=calloptions s=side? info=gpterm(call_info)
+    { Pcall (s, apply_gppterm c info) }
 
 | CALL SLASH fc=sform info=gpterm(call_info)
-    { Pcallconcave (fc,info) }
+    { Pcallconcave (fc, apply_gppterm None info) }
 
 | RCONDT s=side? i=codepos1
     { Prcond (s, true, i) }
@@ -3436,6 +3452,20 @@ caseoption:
 %inline caseoptions:
 | AT xs=bracket(caseoption+) { xs }
 
+
+calloption:
+| b=boption(MINUS) x=lident {
+    match unloc x with
+    | "ll" -> (not b)
+    | _ ->
+       parse_error x.pl_loc
+         (Some ("invalid option: " ^ (unloc x) ^ ", [-]ll expected"))
+  }
+
+%inline calloptions:
+| AT b=bracket(calloption) { Some b }
+| { None }
+
 %inline do_repeat:
 | n=word? NOT      { (`All, n) }
 | n=word? QUESTION { (`Maybe, n) }

src/ecParsetree.ml

@@ -594,10 +594,12 @@ type pipattern =
 
 and pspattern = unit
 
+type fun_upto_info = bool option * pformula * pformula * pformula option
+
 type call_info =
   | CI_spec of (pformula * phoare_post)
   | CI_inv of pformula
-  | CI_upto of (pformula * pformula * pformula option)
+  | CI_upto of fun_upto_info
 
 type p_seq_xt_info =
   | PSeqNone
@@ -668,7 +670,7 @@ type fun_info = [
   | `Def
   | `Code
   | `Abs  of pformula
-  | `Upto of pformula * pformula * pformula option
+  | `Upto of fun_upto_info
 ]
 
 (* -------------------------------------------------------------------- *)
@@ -798,7 +800,7 @@ type phltactic =
   | Pfusion        of (oside * pcodepos * (int * (int * int)))
   | Punroll        of (oside * pcodepos * [`While | `For of bool])
   | Psplitwhile    of (pexpr * oside * pcodepos)
-  | Pcall          of oside * call_info gppterm
+  | Pcall          of (oside * call_info gppterm)
   | Pcallconcave   of (pformula * call_info gppterm)
   | Prcond         of (oside * bool * pcodepos1)
   | Prmatch        of (oside * symbol * pcodepos1)

src/phl/ecPhlCall.ml

@@ -531,7 +531,7 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr =
 let ensure_none_poe tc poe =
   if not (is_none poe) then tc_error !!tc "exception are not supported"
 
-let process_call side info tc =
+let process_call (side, info) tc =
   let process_spec_2 tc side pre post =
     let (hyps, concl) = FApi.tc1_flat tc in
       match concl.f_node, side with
@@ -649,7 +649,7 @@ let process_call side info tc =
         let ml, mr = fst es.es_ml, fst es.es_mr in
         let (_,fl,_) = fst (tc1_last_call tc es.es_sl) in
         let (_,fr,_) = fst (tc1_last_call tc es.es_sr) in
-        let bad,invP,invQ = EcPhlFun.process_fun_upto_info info tc in
+        let weakened_pre,bad,invP,invQ = EcPhlFun.process_fun_upto_info info tc in
         let bad2 = ss_inv_generalize_as_right bad ml mr in
         let invP = ts_inv_rebind invP ml mr in
         let invQ = ts_inv_rebind invQ ml mr in
@@ -664,7 +664,7 @@ let process_call side info tc =
         let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in
         let pre    = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands (eq_params::lpre)) in
         let post   = map_ts_inv3 f_if_simpl bad2 invQ (map_ts_inv f_ands [eq_res;eqglob;invP]) in
-        (bad,invP,invQ, f_equivF pre fl fr post)
+        (weakened_pre,bad,invP,invQ, f_equivF pre fl fr post)
 
     | _ -> tc_error !!tc "the conclusion is not an equiv" in
 
@@ -691,10 +691,10 @@ let process_call side info tc =
       end
 
     | CI_upto info ->
-      let bad, p, q, form = process_upto tc side info in
+      let weakened_pre, bad, p, q, form = process_upto tc side info in
       let t_tr = FApi.t_or (t_assumption `Conv) t_trivial in
       subtactic := (fun tc ->
-        FApi.t_firsts t_tr 3 (EcPhlFun.t_equivF_abs_upto bad p q tc));
+        FApi.t_firsts t_tr 3 (EcPhlFun.t_equivF_abs_upto weakened_pre bad p q tc));
       form
 
   in

src/phl/ecPhlCall.mli

@@ -41,6 +41,6 @@ val t_equiv_call1  : side -> ss_inv -> ss_inv -> backward
 val t_call         : oside -> form -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_call : oside -> call_info gppterm -> backward
+val process_call : oside * call_info gppterm -> backward
 
 val process_call_concave : pformula * call_info gppterm -> backward

src/phl/ecPhlFun.ml

@@ -1,6 +1,5 @@
 (* -------------------------------------------------------------------- *)
 open EcUtils
-open EcParsetree
 open EcPath
 open EcAst
 open EcTypes
@@ -309,7 +308,9 @@ let t_equivF_abs   = FApi.t_low1 "equiv-fun-abs"   t_equivF_abs_r
 (* -------------------------------------------------------------------- *)
 module UpToLow = struct
   (* ------------------------------------------------------------------ *)
-  let equivF_abs_upto pf env fl fr (bad: ss_inv) (invP: ts_inv) (invQ: ts_inv) =
+  let equivF_abs_upto pf env weakened_pre fl fr (bad: ss_inv) (invP: ts_inv) (invQ: ts_inv) =
+    let weakened_pre = Option.value ~default:false weakened_pre in
+
     let (topl, _fl, oil, sigl), (topr, _fr, oir, sigr) =
       EcLowPhlGoal.abstract_info2 env fl fr
     in
@@ -345,23 +346,38 @@ module UpToLow = struct
       let pre   = map_ts_inv EcFol.f_ands [map_ts_inv1 EcFol.f_not bad2; eq_params; invP] in
       let post  = map_ts_inv3 EcFol.f_if_simpl bad2 invQ (map_ts_inv2 f_and eq_res invP) in
       let cond1 = f_equivF pre o_l o_r post in
-      let cond2 =
-        let f_r1 = {m=invQ.ml; inv=f_r1} in
-        let concl = ts_inv_lower_left1 (fun bq -> (f_bdHoareF bq o_l bq FHeq f_r1)) invQ in
-        f_forall_mems_ss_inv (mr, abstract_mt)
-          (map_ss_inv2 f_imp bad concl) in
-      let cond3 =
-        let f_r1 = {m=invQ.mr; inv=f_r1} in
-        let bq = map_ts_inv2 f_and bad2 invQ in
-          f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_bdHoareF bq o_r bq FHeq f_r1) bq) in
-
-      [cond1; cond2; cond3]
+      if not weakened_pre then
+        let cond2 =
+          let f_r1 = {m=invQ.ml; inv=f_r1} in
+          let concl = ts_inv_lower_left1 (fun bq -> (f_bdHoareF bq o_l bq FHeq f_r1)) invQ in
+          f_forall_mems_ss_inv (mr, abstract_mt)
+            (map_ss_inv2 f_imp bad concl) in
+        let cond3 =
+          let f_r1 = {m=invQ.mr; inv=f_r1} in
+          let bq = map_ts_inv2 f_and bad2 invQ in
+            f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_bdHoareF bq o_r bq FHeq f_r1) bq) in
+
+        [cond1; cond2; cond3]
+      else
+        let cond2 =
+          let concl = ts_inv_lower_left1 (fun bq -> (f_hoareF bq o_l (POE.lift bq))) invQ in
+          f_forall_mems_ss_inv (mr, abstract_mt)
+            (map_ss_inv2 f_imp bad concl) in
+        let cond3 =
+          let bq = map_ts_inv2 f_and bad2 invQ in
+            f_forall_mems_ss_inv (ml, abstract_mt) (ts_inv_lower_right1 (fun bq -> f_hoareF bq o_r (POE.lift bq)) bq) in
+
+        [cond1; cond2; cond3]
     in
 
     let sg = List.map2 ospec (OI.allowed oil) (OI.allowed oir) in
     let sg = List.flatten sg in
-    let lossless_a = lossless_hyps env topl fl.x_sub in
-    let sg = lossless_a :: sg in
+    let lossless_a = if not weakened_pre then
+       [ lossless_hyps env topl fl.x_sub ]
+    else
+      [ f_losslessF fl; f_losslessF fr ]
+    in
+    let sg = lossless_a @ sg in
 
     let eq_params =
       ts_inv_eqparams
@@ -378,17 +394,17 @@ module UpToLow = struct
 end
 
 (* -------------------------------------------------------------------- *)
-let t_equivF_abs_upto_r bad invP invQ tc =
+let t_equivF_abs_upto_r weakened_pre bad invP invQ tc =
   let env = FApi.tc1_env tc in
   let ef = tc1_as_equivF tc in
   let pre, post, sg =
-    UpToLow.equivF_abs_upto !!tc env ef.ef_fl ef.ef_fr bad invP invQ
+    UpToLow.equivF_abs_upto !!tc env weakened_pre ef.ef_fl ef.ef_fr bad invP invQ
   in
 
   let tactic tc = FApi.xmutate1 tc `FunUpto sg in
   FApi.t_last tactic (EcPhlConseq.t_equivF_conseq pre post tc)
 
-let t_equivF_abs_upto = FApi.t_low3 "equiv-fun-abs-upto" t_equivF_abs_upto_r
+let t_equivF_abs_upto = t_equivF_abs_upto_r
 
 (* -------------------------------------------------------------------- *)
 module ToCodeLow = struct
@@ -594,9 +610,6 @@ let t_fun_r (inv: inv) tc =
 
 let t_fun = FApi.t_low1 "fun" t_fun_r
 
-(* -------------------------------------------------------------------- *)
-type p_upto_info = pformula * pformula * (pformula option)
-
 (* -------------------------------------------------------------------- *)
 let process_fun_def tc =
   let t_cont tcenv =
@@ -610,7 +623,7 @@ let process_fun_to_code tc =
   t_fun_to_code_r tc
 
 (* -------------------------------------------------------------------- *)
-let process_fun_upto_info (bad, p, q) tc =
+let process_fun_upto_info (weakened_pre, bad, p, q) tc =
   let hyps = FApi.tc1_hyps tc in
   let ml, mr = EcIdent.create "&1", EcIdent.create "&2" in
   let env' = LDecl.inv_memenv ml mr hyps in
@@ -621,12 +634,12 @@ let process_fun_upto_info (bad, p, q) tc =
     let env' = LDecl.push_active_ss (EcMemory.abstract m) hyps in
     TTC.pf_process_form !!tc env' tbool bad
   in
-    ({inv=bad;m}, {inv=p;ml;mr}, {inv=q;ml;mr})
+    (weakened_pre, {inv=bad;m}, {inv=p;ml;mr}, {inv=q;ml;mr})
 
 (* -------------------------------------------------------------------- *)
 let process_fun_upto info g =
-  let (bad, p, q) = process_fun_upto_info info g in
-    t_equivF_abs_upto bad p q g
+  let (weakened_pre, bad, p, q) = process_fun_upto_info info g in
+    t_equivF_abs_upto weakened_pre bad p q g
 
 (* -------------------------------------------------------------------- *)
 let process_fun_abs inv tc =

src/phl/ecPhlFun.mli

@@ -15,12 +15,10 @@ val subst_pre :
   -> EcPV.PVM.subst
 
 (* -------------------------------------------------------------------- *)
-type p_upto_info = pformula * pformula * (pformula option)
-
 val process_fun_def       : FApi.backward
 val process_fun_abs       : pformula -> FApi.backward
-val process_fun_upto_info : p_upto_info -> tcenv1 -> ss_inv * ts_inv * ts_inv
-val process_fun_upto      : p_upto_info -> FApi.backward
+val process_fun_upto_info : fun_upto_info -> tcenv1 -> bool option * ss_inv * ts_inv * ts_inv
+val process_fun_upto      : fun_upto_info -> FApi.backward
 val process_fun_to_code   : FApi.backward
 
 (* -------------------------------------------------------------------- *)
@@ -49,7 +47,7 @@ val t_bdhoareF_fun_def : FApi.backward
 val t_equivF_fun_def   : FApi.backward
 
 (* -------------------------------------------------------------------- *)
-val t_equivF_abs_upto : ss_inv -> ts_inv -> ts_inv -> FApi.backward
+val t_equivF_abs_upto : bool option -> ss_inv -> ts_inv -> ts_inv -> FApi.backward
 
 (* -------------------------------------------------------------------- *)
 val t_fun : inv -> FApi.backward