Skip to content

Commit 96b17a3

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 c3a0bf3 commit 96b17a3

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
@@ -261,8 +261,6 @@
261261
("+" , (PLUS , false));
262262
("-" , (MINUS , false));
263263
("*" , (STAR , false));
264-
("<<" , (BACKS , false));
265-
(">>" , (FWDS , false));
266264
("<:" , (LTCOLON , false));
267265
("==>" , (LONGARROW , false));
268266
("=" , (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
@@ -457,7 +456,6 @@
457456
%token FROM
458457
%token FUN
459458
%token FUSION
460-
%token FWDS
461459
%token GEN
462460
%token GLOB
463461
%token GLOBAL
@@ -2497,11 +2495,6 @@ call_info:
24972495
| bad=form COMMA p=form { CI_upto (bad,p,None) }
24982496
| bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) }
24992497

2500-
tac_dir:
2501-
| BACKS { Backs }
2502-
| FWDS { Fwds }
2503-
| empty { Backs }
2504-
25052498
icodepos_r:
25062499
| IF { (`If :> pcp_match) }
25072500
| WHILE { (`While :> pcp_match) }
@@ -2672,13 +2665,13 @@ dbhint:
26722665

26732666
app_bd_info:
26742667
| empty
2675-
{ PAppNone }
2668+
{ PSeqNone }
26762669

26772670
| f=sform
2678-
{ PAppSingle f }
2671+
{ PSeqSingle f }
26792672

26802673
| f=prod_form g=prod_form s=sform?
2681-
{ PAppMult (s, fst f, snd f, fst g, snd g) }
2674+
{ PSeqMult (s, fst f, snd f, fst g, snd g) }
26822675

26832676
revert:
26842677
| cl=ioption(brace(loc(ipcore_name)+)) gp=genpattern*
@@ -2915,8 +2908,8 @@ interleave_info:
29152908
| PROC STAR
29162909
{ Pfun `Code }
29172910

2918-
| SEQ s=side? d=tac_dir pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info
2919-
{ Papp (s, d, pos, p, f) }
2911+
| SEQ s=side? pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info
2912+
{ Pseq (s, pos, p, f) }
29202913

29212914
| WP n=s_codepos1?
29222915
{ Pwp n }

‎src/ecParsetree.ml‎

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

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

551551
type ('a, 'b, 'c) rnd_tac_info =
552552
| PNoRndParams
@@ -559,8 +559,6 @@ type rnd_tac_info_f =
559559

560560
type psemrndpos = (bool * pcodepos1) doption
561561

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

566564
(* -------------------------------------------------------------------- *)
@@ -618,8 +616,8 @@ type fun_info = [
618616
]
619617

620618
(* -------------------------------------------------------------------- *)
621-
type app_info =
622-
oside * tac_dir * pcodepos1 doption * pformula doption * p_app_xt_info
619+
type seq_info =
620+
oside * pcodepos1 doption * pformula doption * p_seq_xt_info
623621

624622
(* -------------------------------------------------------------------- *)
625623
type pcond_info = [
@@ -726,7 +724,7 @@ type phltactic =
726724
| Pskip
727725
| Prepl_stmt of trans_info
728726
| Pfun of fun_info
729-
| Papp of app_info
727+
| Pseq of seq_info
730728
| Pwp of pdocodepos1
731729
| Psp of pdocodepos1
732730
| 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)