Skip to content

Commit d79a237

Browse files
strubstrub
committed
[seq]: remove bck/fwd option + cleanup
The bck/fwd variants of `seq` are unused and are a leftover from CertiCrypt. No other tactic provides such variants. We may want to reintroduce them in the future, but for now this code is largely dead since it is not used by any project. Internally, the `seq` tactic was called `app`. This commit updates that.
1 parent a0bf172 commit d79a237

13 files changed

Lines changed: 64 additions & 83 deletions

‎src/ecHiTacticals.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -173,7 +173,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
173173
| Pfun (`Upto info) -> EcPhlFun.process_fun_upto info
174174
| Pfun `Code -> EcPhlFun.process_fun_to_code
175175
| Pskip -> EcPhlSkip.t_skip
176-
| Papp info -> EcPhlApp.process_app info
176+
| Pseq info -> EcPhlSeq.process_seq info
177177
| Pwp wp -> EcPhlWp.process_wp wp
178178
| Psp sp -> EcPhlSp.process_sp sp
179179
| Prcond (side, b, i) -> EcPhlRCond.process_rcond side b i

‎src/ecLexer.mll‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -262,8 +262,6 @@
262262
("+" , (PLUS , false));
263263
("-" , (MINUS , false));
264264
("*" , (STAR , false));
265-
("<<" , (BACKS , false));
266-
(">>" , (FWDS , false));
267265
("<:" , (LTCOLON , false));
268266
("==>" , (LONGARROW , false));
269267
("=" , (EQ , false));

‎src/ecParser.mly‎

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -391,7 +391,6 @@
391391
%token AUTO
392392
%token AXIOM
393393
%token AXIOMATIZED
394-
%token BACKS
395394
%token BACKSLASH
396395
%token BETA
397396
%token BY
@@ -458,7 +457,6 @@
458457
%token FROM
459458
%token FUN
460459
%token FUSION
461-
%token FWDS
462460
%token GEN
463461
%token GLOB
464462
%token GLOBAL
@@ -2522,11 +2520,6 @@ call_info:
25222520
| bad=form COMMA p=form { CI_upto (bad,p,None) }
25232521
| bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) }
25242522

2525-
tac_dir:
2526-
| BACKS { Backs }
2527-
| FWDS { Fwds }
2528-
| empty { Backs }
2529-
25302523
icodepos_r:
25312524
| IF { (`If :> pcp_match) }
25322525
| WHILE { (`While :> pcp_match) }
@@ -2697,13 +2690,13 @@ dbhint:
26972690

26982691
app_bd_info:
26992692
| empty
2700-
{ PAppNone }
2693+
{ PSeqNone }
27012694

27022695
| f=sform
2703-
{ PAppSingle f }
2696+
{ PSeqSingle f }
27042697

27052698
| f=prod_form g=prod_form s=sform?
2706-
{ PAppMult (s, fst f, snd f, fst g, snd g) }
2699+
{ PSeqMult (s, fst f, snd f, fst g, snd g) }
27072700

27082701
revert:
27092702
| cl=ioption(brace(loc(ipcore_name)+)) gp=genpattern*
@@ -2940,8 +2933,8 @@ interleave_info:
29402933
| PROC STAR
29412934
{ Pfun `Code }
29422935

2943-
| SEQ s=side? d=tac_dir pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info
2944-
{ Papp (s, d, pos, p, f) }
2936+
| SEQ s=side? pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info
2937+
{ Pseq (s, pos, p, f) }
29452938

29462939
| WP n=s_codepos1?
29472940
{ Pwp n }

‎src/ecParsetree.ml‎

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -542,10 +542,10 @@ type call_info =
542542
| CI_inv of pformula
543543
| CI_upto of (pformula * pformula * pformula option)
544544

545-
type p_app_xt_info =
546-
| PAppNone
547-
| PAppSingle of pformula
548-
| PAppMult of (pformula option) tuple5
545+
type p_seq_xt_info =
546+
| PSeqNone
547+
| PSeqSingle of pformula
548+
| PSeqMult of (pformula option) tuple5
549549

550550
type ('a, 'b, 'c) rnd_tac_info =
551551
| PNoRndParams
@@ -558,8 +558,6 @@ type rnd_tac_info_f =
558558

559559
type psemrndpos = (bool * pcodepos1) doption
560560

561-
type tac_dir = Backs | Fwds
562-
563561
type pfel_spec_preds = (pgamepath * pformula) list
564562

565563
(* -------------------------------------------------------------------- *)
@@ -617,8 +615,8 @@ type fun_info = [
617615
]
618616

619617
(* -------------------------------------------------------------------- *)
620-
type app_info =
621-
oside * tac_dir * pcodepos1 doption * pformula doption * p_app_xt_info
618+
type seq_info =
619+
oside * pcodepos1 doption * pformula doption * p_seq_xt_info
622620

623621
(* -------------------------------------------------------------------- *)
624622
type pcond_info = [
@@ -725,7 +723,7 @@ type phltactic =
725723
| Pskip
726724
| Prepl_stmt of trans_info
727725
| Pfun of fun_info
728-
| Papp of app_info
726+
| Pseq of seq_info
729727
| Pwp of pdocodepos1
730728
| Psp of pdocodepos1
731729
| Pwhile of (oside * while_info)

‎src/phl/ecPhlCall.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -145,14 +145,14 @@ let t_ehoare_call_core fpre fpost tc =
145145
let t_ehoare_call fpre fpost tc =
146146
let _, _, _, s, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in
147147
let tcenv =
148-
EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in
148+
EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in
149149
let tcenv = FApi.t_swap_goals 0 1 tcenv in
150150
FApi.t_sub [t_ehoare_call_core fpre fpost; t_id] tcenv
151151

152152
let t_ehoare_call_concave f fpre fpost tc =
153153
let _, _, _, s, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in
154154
let tcenv =
155-
EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node))
155+
EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node))
156156
(map_ss_inv2 (fun wppre f -> f_app_simpl f [wppre] txreal) wppre f) tc in
157157
let tcenv = FApi.t_swap_goals 0 1 tcenv in
158158
let t_call =

‎src/phl/ecPhlEqobs.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -476,7 +476,7 @@ let process_eqobs_inS info tc =
476476
let _, eqi =
477477
try s_eqobs_in_full (stmt sl2) (stmt sr2) sim Mpv2.empty_local eqo
478478
with EqObsInError -> tc_error !!tc "cannot apply sim" in
479-
(EcPhlApp.t_equiv_app (p1, p2) (Mpv2.to_form_ts_inv eqi inv) @+ [
479+
(EcPhlSeq.t_equiv_seq (p1, p2) (Mpv2.to_form_ts_inv eqi inv) @+ [
480480
t_id;
481481
fun tc ->
482482
FApi.t_last

‎src/phl/ecPhlExists.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -153,16 +153,16 @@ let process_ecall oside (l, tvi, fs) tc =
153153
let t_local_seq p1 tc =
154154
match kind, oside, p1 with
155155
| `Hoare n, _, Inv_ss p1 ->
156-
EcPhlApp.t_hoare_app
156+
EcPhlSeq.t_hoare_seq
157157
(Zpr.cpos (n-1)) p1 tc
158158
| `Equiv (n1, n2), None, Inv_ts p1 ->
159-
EcPhlApp.t_equiv_app
159+
EcPhlSeq.t_equiv_seq
160160
(Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc
161161
| `Equiv (n1, n2), Some `Left, Inv_ts p1 ->
162-
EcPhlApp.t_equiv_app
162+
EcPhlSeq.t_equiv_seq
163163
(Zpr.cpos (n1-1), Zpr.cpos n2) p1 tc
164164
| `Equiv(n1, n2), Some `Right, Inv_ts p1 ->
165-
EcPhlApp.t_equiv_app
165+
EcPhlSeq.t_equiv_seq
166166
(Zpr.cpos n1, Zpr.cpos (n2-1)) p1 tc
167167
| _ -> tc_error !!tc "mismatched sidedness or kind of conclusion"
168168
in

‎src/phl/ecPhlHiAuto.ml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
6868

6969
| LL_JUMP ->
7070
let m = EcIdent.create "&hr" in
71-
( EcPhlApp.t_bdhoare_app
71+
( EcPhlSeq.t_bdhoare_seq
7272
(Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true},
7373
{m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1})
7474

@@ -86,7 +86,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc =
8686
@+ [apply_ll_strategy lls1; apply_ll_strategy lls2]
8787
in
8888

89-
( EcPhlApp.t_bdhoare_app
89+
( EcPhlSeq.t_bdhoare_seq
9090
(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})
9191

9292
@~ FApi.t_onalli (function
@@ -142,8 +142,8 @@ let t_lossless tc =
142142

143143
| FequivS hs ->
144144
let ml, mr = fst hs.es_ml, fst hs.es_mr in
145-
((EcPhlApp.t_equiv_app_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+
146-
[ (EcPhlApp.t_equiv_app_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+
145+
((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+
146+
[ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+
147147
[ EcPhlSkip.t_skip @! t_trivial ;
148148
t_single
149149
];

‎src/phl/ecPhlHiCond.ml‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@ let process_cond (info : EcParsetree.pcond_info) tc =
2626
let i2 = Option.map (fun i2 -> EcLowPhlGoal.tc1_process_codepos1 tc (side, i2)) i2 in
2727
let n1 = default_if i1 es.es_sl in
2828
let n2 = default_if i2 es.es_sr in
29-
FApi.t_seqsub (EcPhlApp.t_equiv_app (n1, n2) f)
29+
FApi.t_seqsub (EcPhlSeq.t_equiv_seq (n1, n2) f)
3030
[ t_id; t_equiv_cond side ] tc
3131

3232
| `SeqOne (s, i, f1, f2) ->
@@ -36,7 +36,7 @@ let process_cond (info : EcParsetree.pcond_info) tc =
3636
let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in
3737
let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in
3838
FApi.t_seqsub
39-
(EcPhlApp.t_equiv_app_onesided s n f1 f2)
39+
(EcPhlSeq.t_equiv_seq_onesided s n f1 f2)
4040
[ t_id; t_bdhoare_cond] tc
4141

4242
(* -------------------------------------------------------------------- *)

‎src/phl/ecPhlLoopTx.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -320,7 +320,7 @@ let process_unroll_for side cpos tc =
320320
let (h', pos', z') = oget hds.(i-1) in
321321
FApi.t_seqs [
322322
EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos-2))));
323-
EcPhlApp.t_hoare_app (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
323+
EcPhlSeq.t_hoare_seq (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+
324324
[t_apply_hd h'; t_conseq_nm] ] tc
325325
in
326326

0 commit comments

Comments
 (0)