Skip to content

[seq]: remove bck/fwd option + cleanup #878

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
strub wants to merge 1 commit into
base: main
Choose a base branch
from
Open

[seq]: remove bck/fwd option + cleanup #878

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/ecHiTacticals.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 0 additions & 2 deletions src/ecLexer.mll
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -261,8 +261,6 @@
("+" , (PLUS , false));
("-" , (MINUS , false));
("*" , (STAR , false));
("<<" , (BACKS , false));
(">>" , (FWDS , false));
("<:" , (LTCOLON , false));
("==>" , (LONGARROW , false));
("=" , (EQ , false));
Expand Down
17 changes: 5 additions & 12 deletions src/ecParser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,7 +391,6 @@
%token AUTO
%token AXIOM
%token AXIOMATIZED
%token BACKS
%token BACKSLASH
%token BETA
%token BY
Expand Down Expand Up @@ -457,7 +456,6 @@
%token FROM
%token FUN
%token FUSION
%token FWDS
%token GEN
%token GLOB
%token GLOBAL
Expand Down Expand Up @@ -2497,11 +2495,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) }
Expand Down Expand Up @@ -2672,13 +2665,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*
Expand Down Expand Up @@ -2915,8 +2908,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 }
Expand Down
16 changes: 7 additions & 9 deletions src/ecParsetree.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -543,10 +543,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
Expand All @@ -559,8 +559,6 @@ type rnd_tac_info_f =

type psemrndpos = (bool * pcodepos1) doption

type tac_dir = Backs | Fwds

type pfel_spec_preds = (pgamepath * pformula) list

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -618,8 +616,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 = [
Expand Down Expand Up @@ -726,7 +724,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)
Expand Down
4 changes: 2 additions & 2 deletions src/phl/ecPhlCall.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
2 changes: 1 addition & 1 deletion src/phl/ecPhlEqobs.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/phl/ecPhlExists.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions src/phl/ecPhlHiAuto.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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})

Expand All @@ -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
Expand Down Expand Up @@ -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
];
Expand Down
4 changes: 2 additions & 2 deletions src/phl/ecPhlHiCond.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand All @@ -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

(* -------------------------------------------------------------------- *)
Expand Down
2 changes: 1 addition & 1 deletion src/phl/ecPhlLoopTx.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading