[seq]: remove bck/fwd option + cleanup

strub · strub · commit 84bbdd2abc7f · 2026-02-02T09:40:22.000+01:00
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
@@ -173,7 +173,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pfun (`Upto info)         -> EcPhlFun.process_fun_upto info
     | Pfun `Code                -> EcPhlFun.process_fun_to_code
     | Pskip                     -> EcPhlSkip.t_skip
-    | Papp info                 -> EcPhlApp.process_app info
+    | Pseq info                 -> EcPhlSeq.process_seq info
     | Pwp wp                    -> EcPhlWp.process_wp wp
     | Psp sp                    -> EcPhlSp.process_sp sp
     | Prcond (side, b, i)       -> EcPhlRCond.process_rcond side b i
diff --git a/src/ecLexer.mll b/src/ecLexer.mll
@@ -262,8 +262,6 @@
     ("+"   , (PLUS             , false));
     ("-"   , (MINUS            , false));
     ("*"   , (STAR             , false));
-    ("<<"  , (BACKS            , false));
-    (">>"  , (FWDS             , false));
     ("<:"  , (LTCOLON          , false));
     ("==>" , (LONGARROW        , false));
     ("="   , (EQ               , false));
diff --git a/src/ecParser.mly b/src/ecParser.mly
@@ -391,7 +391,6 @@
 %token AUTO
 %token AXIOM
 %token AXIOMATIZED
-%token BACKS
 %token BACKSLASH
 %token BETA
 %token BY
@@ -458,7 +457,6 @@
 %token FROM
 %token FUN
 %token FUSION
-%token FWDS
 %token GEN
 %token GLOB
 %token GLOBAL
@@ -2522,11 +2520,6 @@ call_info:
 | bad=form COMMA p=form              { CI_upto (bad,p,None) }
 | bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) }
 
-tac_dir:
-| BACKS { Backs }
-| FWDS  { Fwds }
-| empty { Backs }
-
 icodepos_r:
 | IF       { (`If     :> pcp_match) }
 | WHILE    { (`While  :> pcp_match) }
@@ -2697,13 +2690,13 @@ dbhint:
 
 app_bd_info:
 | empty
-    { PAppNone }
+    { PSeqNone }
 
 | f=sform
-    { PAppSingle f }
+    { PSeqSingle f }
 
 | f=prod_form g=prod_form s=sform?
-    { PAppMult (s, fst f, snd f, fst g, snd g) }
+    { PSeqMult (s, fst f, snd f, fst g, snd g) }
 
 revert:
 | cl=ioption(brace(loc(ipcore_name)+)) gp=genpattern*
@@ -2940,8 +2933,8 @@ interleave_info:
 | PROC STAR
    { Pfun `Code }
 
-| SEQ s=side? d=tac_dir pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info
-   { Papp (s, d, pos, p, f) }
+| SEQ s=side? pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info
+   { Pseq (s, pos, p, f) }
 
 | WP n=s_codepos1?
    { Pwp n }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
@@ -542,10 +542,10 @@ type call_info =
   | CI_inv of pformula
   | CI_upto of (pformula * pformula * pformula option)
 
-type p_app_xt_info =
-  | PAppNone
-  | PAppSingle of pformula
-  | PAppMult   of (pformula option) tuple5
+type p_seq_xt_info =
+  | PSeqNone
+  | PSeqSingle of pformula
+  | PSeqMult   of (pformula option) tuple5
 
 type ('a, 'b, 'c) rnd_tac_info =
   | PNoRndParams
@@ -558,8 +558,6 @@ type rnd_tac_info_f =
 
 type psemrndpos = (bool * pcodepos1) doption
 
-type tac_dir = Backs | Fwds
-
 type pfel_spec_preds = (pgamepath * pformula) list
 
 (* -------------------------------------------------------------------- *)
@@ -617,8 +615,8 @@ type fun_info = [
 ]
 
 (* -------------------------------------------------------------------- *)
-type app_info =
-  oside * tac_dir * pcodepos1 doption * pformula doption * p_app_xt_info
+type seq_info =
+  oside * pcodepos1 doption * pformula doption * p_seq_xt_info
 
 (* -------------------------------------------------------------------- *)
 type pcond_info = [
@@ -725,7 +723,7 @@ type phltactic =
   | Pskip
   | Prepl_stmt     of trans_info
   | Pfun           of fun_info
-  | Papp           of app_info
+  | Pseq           of seq_info
   | Pwp            of pdocodepos1
   | Psp            of pdocodepos1
   | Pwhile         of (oside * while_info)
diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml
@@ -145,14 +145,14 @@ let t_ehoare_call_core fpre fpost tc =
 let t_ehoare_call fpre fpost tc =
   let _, _, _, s, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in
   let tcenv =
-    EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in
+    EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in
   let tcenv = FApi.t_swap_goals 0 1 tcenv in
   FApi.t_sub [t_ehoare_call_core fpre fpost; t_id] tcenv
 
 let t_ehoare_call_concave f fpre fpost tc =
   let _, _, _, s, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in
   let tcenv =
-    EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node))
+    EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node))
      (map_ss_inv2 (fun wppre f -> f_app_simpl f [wppre] txreal) wppre f) tc in
   let tcenv = FApi.t_swap_goals 0 1 tcenv in
   let t_call =
diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml
@@ -476,7 +476,7 @@ let process_eqobs_inS info tc =
       let _, eqi =
         try s_eqobs_in_full (stmt sl2) (stmt sr2) sim Mpv2.empty_local eqo
         with EqObsInError -> tc_error !!tc "cannot apply sim" in
-      (EcPhlApp.t_equiv_app (p1, p2) (Mpv2.to_form_ts_inv eqi inv) @+ [
+      (EcPhlSeq.t_equiv_seq (p1, p2) (Mpv2.to_form_ts_inv eqi inv) @+ [
         t_id;
         fun tc ->
           FApi.t_last
diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml
@@ -153,16 +153,16 @@ let process_ecall oside (l, tvi, fs) tc =
   let t_local_seq p1 tc =
     match kind, oside, p1 with
     | `Hoare n, _, Inv_ss p1 ->
-        EcPhlApp.t_hoare_app
+        EcPhlSeq.t_hoare_seq
           (Zpr.cpos (n-1)) p1 tc
     | `Equiv (n1, n2), None, Inv_ts p1 ->
-        EcPhlApp.t_equiv_app
+        EcPhlSeq.t_equiv_seq
           (Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc
     | `Equiv (n1, n2), Some `Left, Inv_ts p1 ->
-        EcPhlApp.t_equiv_app
+        EcPhlSeq.t_equiv_seq
           (Zpr.cpos (n1-1), Zpr.cpos n2) p1 tc
     | `Equiv(n1, n2), Some `Right, Inv_ts p1 ->
-        EcPhlApp.t_equiv_app
+        EcPhlSeq.t_equiv_seq
           (Zpr.cpos n1, Zpr.cpos (n2-1)) p1 tc
     | _ -> tc_error !!tc "mismatched sidedness or kind of conclusion"
   in
diff --git a/src/phl/ecPhlHiAuto.ml b/src/phl/ecPhlHiAuto.ml
@@ -68,7 +68,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
 
   | LL_JUMP ->
       let m = EcIdent.create "&hr" in
-        ( EcPhlApp.t_bdhoare_app
+        ( EcPhlSeq.t_bdhoare_seq
            (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, 
             {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1})
 
@@ -86,7 +86,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
         @+ [apply_ll_strategy lls1; apply_ll_strategy lls2]
       in
 
-        ( EcPhlApp.t_bdhoare_app
+        ( EcPhlSeq.t_bdhoare_seq
            (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1})
 
         @~ FApi.t_onalli (function
@@ -142,8 +142,8 @@ let t_lossless tc =
 
   | FequivS hs ->
     let ml, mr = fst hs.es_ml, fst hs.es_mr in
-      ((EcPhlApp.t_equiv_app_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+
-         [ (EcPhlApp.t_equiv_app_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+
+      ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+
+         [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+
              [ EcPhlSkip.t_skip @! t_trivial ;
                t_single
              ];
diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml
@@ -26,7 +26,7 @@ let process_cond (info : EcParsetree.pcond_info) tc =
     let i2 = Option.map (fun i2 -> EcLowPhlGoal.tc1_process_codepos1 tc (side, i2)) i2 in
     let n1 = default_if i1 es.es_sl in
     let n2 = default_if i2 es.es_sr in
-    FApi.t_seqsub (EcPhlApp.t_equiv_app (n1, n2) f)
+    FApi.t_seqsub (EcPhlSeq.t_equiv_seq (n1, n2) f)
       [ t_id; t_equiv_cond side ] tc
 
   | `SeqOne (s, i, f1, f2) ->
@@ -36,7 +36,7 @@ let process_cond (info : EcParsetree.pcond_info) tc =
     let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in
     let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in
     FApi.t_seqsub
-      (EcPhlApp.t_equiv_app_onesided s n f1 f2)
+      (EcPhlSeq.t_equiv_seq_onesided s n f1 f2)
       [ t_id; t_bdhoare_cond] tc
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml
@@ -320,7 +320,7 @@ let process_unroll_for side cpos tc =
       let (h', pos', z') = oget hds.(i-1) in
       FApi.t_seqs [
         EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos-2))));
-        EcPhlApp.t_hoare_app (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
+        EcPhlSeq.t_hoare_seq (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
         [t_apply_hd h'; t_conseq_nm] ] tc
   in
 
diff --git a/src/phl/ecPhlSeq.ml b/src/phl/ecPhlSeq.ml
diff --git a/src/phl/ecPhlSeq.mli b/src/phl/ecPhlSeq.mli
diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml
