Skip to content

Commit dbe838e

Browse files
authored
Improvements to module tweaks
- Allow for code position ranges to specify blocks of changes. + `[cp .. cp]` specify a block using two code positions. + `[cp - cp1]` specify a block using an initial position and another position relative to it. - Minor change to syntax for adding above a statement ( `+ ^`).
1 parent 0c26f58 commit dbe838e

File tree

4 files changed

+61
-31
lines changed

4 files changed

+61
-31
lines changed

src/ecParser.mly

+18-6
Original file line numberDiff line numberDiff line change
@@ -1444,6 +1444,9 @@ mod_item:
14441444
| IMPORT VAR ms=loc(mod_qident)+
14451445
{ Pst_import ms }
14461446

1447+
mod_remove_var:
1448+
| MINUS VAR xs=plist1(lident, COMMA) { xs }
1449+
14471450
mod_update_var:
14481451
| v=var_decl { v }
14491452

@@ -1453,19 +1456,20 @@ mod_update_fun:
14531456

14541457
update_stmt:
14551458
| PLUS s=brace(stmt){ [Pups_add (s, true)] }
1456-
| MINUS s=brace(stmt){ [Pups_add (s, false)] }
1459+
| PLUS HAT s=brace(stmt){ [Pups_add (s, false)] }
14571460
| TILD s=brace(stmt) { [Pups_del; Pups_add (s, true)] }
14581461
| MINUS { [Pups_del] }
14591462

14601463
update_cond:
1461-
| PLUS e=sexpr { Pupc_add e }
1464+
| PLUS e=sexpr { Pupc_add (e, true) }
1465+
| PLUS HAT e=sexpr { Pupc_add (e, false) }
14621466
| TILD e=sexpr { Pupc_mod e }
14631467
| MINUS bs=branch_select { Pupc_del bs }
14641468

14651469
fun_update:
1466-
| cp=loc(codepos) sup=update_stmt
1470+
| cp=loc(codepos_or_range) sup=update_stmt
14671471
{ List.map (fun v -> (cp, Pup_stmt v)) sup }
1468-
| cp=loc(codepos) cup=update_cond
1472+
| cp=loc(codepos_or_range) cup=update_cond
14691473
{ [(cp, Pup_cond cup)] }
14701474

14711475
(* -------------------------------------------------------------------- *)
@@ -1478,8 +1482,8 @@ mod_body:
14781482
| LBRACE stt=loc(mod_item)* RBRACE
14791483
{ Pm_struct stt }
14801484

1481-
| m=mod_qident WITH LBRACE vs=mod_update_var* fs=mod_update_fun* RBRACE
1482-
{ Pm_update (m, vs, fs) }
1485+
| m=mod_qident WITH LBRACE dvs=mod_remove_var? vs=mod_update_var* fs=mod_update_fun* RBRACE
1486+
{ Pm_update (m, odfl [] dvs, vs, fs) }
14831487

14841488
mod_def_or_decl:
14851489
| locality=locality MODULE header=mod_header c=mod_cast? EQ ptm_body=loc(mod_body)
@@ -2537,6 +2541,14 @@ codepos:
25372541
| nm=rlist0(nm1_codepos, empty) i=codepos1
25382542
{ (nm, i) }
25392543

2544+
codepos_range:
2545+
| LBRACKET cps=codepos DOTDOT cpe=codepos RBRACKET { (cps, `Base cpe) }
2546+
| LBRACKET cps=codepos MINUS cpe=codepos1 RBRACKET { (cps, `Offset cpe) }
2547+
2548+
codepos_or_range:
2549+
| cp=codepos { (cp, `Offset (0, `ByPos 0)) }
2550+
| cpr=codepos_range { cpr }
2551+
25402552
codeoffset1:
25412553
| i=sword { (`ByOffset i :> pcodeoffset1) }
25422554
| AT p=codepos1 { (`ByPosition p :> pcodeoffset1) }

src/ecParsetree.ml

+4-3
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@ type pcp_base = [ `ByPos of int | `ByMatch of int option * pcp_match ]
5353
type pbranch_select = [`Cond of bool | `Match of psymbol]
5454
type pcodepos1 = int * pcp_base
5555
type pcodepos = (pcodepos1 * pbranch_select) list * pcodepos1
56+
type pcodepos_range = pcodepos * [`Base of pcodepos | `Offset of pcodepos1]
5657
type pdocodepos1 = pcodepos1 doption option
5758

5859
type pcodeoffset1 = [
@@ -330,7 +331,7 @@ and pmodule_params = (psymbol * pmodule_type) list
330331
and pmodule_expr_r =
331332
| Pm_ident of pmsymbol
332333
| Pm_struct of pstructure
333-
| Pm_update of pmsymbol * pupdate_var list * pupdate_fun list
334+
| Pm_update of pmsymbol * psymbol list * pupdate_var list * pupdate_fun list
334335

335336
and pmodule_expr = pmodule_expr_r located
336337

@@ -345,7 +346,7 @@ and pstructure_item =
345346
| Pst_import of (pmsymbol located) list
346347

347348
and pupdate_var = psymbol list * pty
348-
and pupdate_fun = psymbol * (psymbol list * pty) list * ((pcodepos located * pupdate_item) list * pexpr option)
349+
and pupdate_fun = psymbol * (psymbol list * pty) list * ((pcodepos_range located * pupdate_item) list * pexpr option)
349350

350351
and pupdate_item =
351352
| Pup_stmt of pupdate_stmt
@@ -356,7 +357,7 @@ and pupdate_stmt =
356357
| Pups_del
357358

358359
and pupdate_cond =
359-
| Pupc_add of pexpr
360+
| Pupc_add of (pexpr * bool)
360361
| Pupc_mod of pexpr
361362
| Pupc_del of pbranch_select
362363

src/ecTyping.ml

+37-19
Original file line numberDiff line numberDiff line change
@@ -2025,7 +2025,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
20252025
me
20262026
| Pm_struct ps ->
20272027
transstruct ~attop env x.pl_desc stparams (mk_loc me.pl_loc ps)
2028-
| Pm_update (m, vars, funs) ->
2028+
| Pm_update (m, delete_vars, vars, funs) ->
20292029
let loc = me.pl_loc in
20302030
let (mp, sig_) = trans_msymbol env {pl_desc = m; pl_loc = loc} in
20312031

@@ -2046,6 +2046,8 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
20462046
vars
20472047
in
20482048

2049+
let delete_vars = List.map (fun v -> v.pl_desc) delete_vars in
2050+
20492051
let me, _ = EcEnv.Mod.by_mpath mp env in
20502052
let p = match mp.m_top with | `Concrete (p, _) -> p | _ -> assert false in
20512053
let subst = EcSubst.add_moddef EcSubst.empty ~src:p ~dst:(EcEnv.mroot env) in
@@ -2084,32 +2086,39 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
20842086
let memenv = ref memenv in
20852087

20862088
(* Semantics for stmt updating, `i` is the target of the update. *)
2087-
let eval_supdate env sup i =
2089+
let eval_supdate env sup si =
20882090
match sup with
20892091
| Pups_add (s, after) ->
20902092
let ue = UE.create (Some []) in
20912093
let s = transstmt env ue s in
20922094
let ts = Tuni.subst (UE.close ue) in
20932095
if after then
2094-
i :: (s_subst ts s).s_node
2096+
si @ (s_subst ts s).s_node
20952097
else
2096-
(s_subst ts s).s_node @ [i]
2098+
(s_subst ts s).s_node @ si
20972099
| Pups_del -> []
20982100
in
20992101

21002102
(* Semantics for condition updating *)
2101-
(* `i` is the target of the update, and `tl` is the instr suffix. *)
2102-
let eval_cupdate cp_loc env cup i tl =
2103+
let eval_cupdate cp_loc env cup si =
2104+
(* NOTE: There will always be a head element *)
2105+
(* `i` is the target of the update, and `tl` is the instr suffix. *)
2106+
let i, tl = List.takedrop 1 si in
2107+
let i = List.hd i in
2108+
21032109
match cup with
21042110
(* Insert an if with condition `e` with body `tl` *)
2105-
| Pupc_add e ->
2111+
| Pupc_add (e, after) ->
21062112
let loc = e.pl_loc in
21072113
let ue = UE.create (Some []) in
21082114
let e, ty = transexp env `InProc ue e in
21092115
let ts = Tuni.subst (UE.close ue) in
21102116
let ty = ty_subst ts ty in
21112117
unify_or_fail env ue loc ~expct:tbool ty;
2112-
i :: [i_if (e_subst ts e, stmt tl, s_empty)]
2118+
if after then
2119+
i :: [i_if (e_subst ts e, stmt tl, s_empty)]
2120+
else
2121+
[i_if (e_subst ts e, stmt (i :: tl), s_empty)]
21132122

21142123
(* Change the condition expression to `e` for a conditional instr `i` *)
21152124
| Pupc_mod e -> begin
@@ -2191,23 +2200,19 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
21912200
(* Apply each of updates in reverse *)
21922201
(* NOTE: This is with the expectation that the user entered them in chronological order. *)
21932202
let body =
2194-
List.fold_right (fun (cp, up) bd ->
2195-
let {pl_desc = cp; pl_loc = loc} = cp in
2196-
let cp = trans_codepos env cp in
2203+
List.fold_right (fun (cpr, up) bd ->
2204+
let {pl_desc = cpr; pl_loc = loc} = cpr in
2205+
let cp = trans_codepos_range env cpr in
21972206
let change env si =
2198-
(* NOTE: There will always be a head element *)
2199-
let i, tl = List.takedrop 1 si in
2200-
let i = List.hd i in
2201-
22022207
match up with
22032208
| Pup_stmt sup ->
2204-
eval_supdate env sup i @ tl
2209+
eval_supdate env sup si
22052210
| Pup_cond cup ->
2206-
eval_cupdate loc env cup i tl
2211+
eval_cupdate loc env cup si
22072212
in
22082213
let env = EcEnv.Memory.push_active !memenv env in
22092214
try
2210-
EcMatching.Zipper.map_range env (cp, `Offset (EcMatching.Zipper.cpos (-1))) change bd
2215+
EcMatching.Zipper.map_range env cp change bd
22112216
with
22122217
| EcMatching.Zipper.InvalidCPos ->
22132218
tyerror loc env (InvalidModUpdate MUE_InvalidCodePos);
@@ -2250,7 +2255,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
22502255
| ME_Structure mb ->
22512256
let doit (env, items) mi =
22522257
match mi with
2253-
| MI_Variable v ->
2258+
| MI_Variable v when not (List.mem (v_name v) delete_vars) ->
22542259
let env = EcEnv.Var.bind_pvglob v.v_name v.v_type env in
22552260
env, items @ [mi]
22562261
| MI_Function f -> begin
@@ -2266,6 +2271,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
22662271
| MI_Module me ->
22672272
let env = EcEnv.bind1 (me.me_name, `Module me) env in
22682273
env, items @ [mi]
2274+
| _ -> env, items
22692275
in
22702276
List.fold_left doit (env, []) (items @ mb.ms_body)
22712277

@@ -3635,6 +3641,18 @@ and trans_codepos ?(memory : memory option) (env : EcEnv.env) ((nm, p) : pcodepo
36353641
let p = trans_codepos1 ?memory env p in
36363642
(nm, p)
36373643

3644+
(* -------------------------------------------------------------------- *)
3645+
and trans_codepos_range ?(memory : memory option) (env : EcEnv.env) ((cps, cpe) : pcodepos_range) : codepos_range =
3646+
let cps = trans_codepos ?memory env cps in
3647+
let cpe =
3648+
match cpe with
3649+
| `Base cp ->
3650+
`Base (trans_codepos ?memory env cp)
3651+
| `Offset cp ->
3652+
`Offset (trans_codepos1 ?memory env cp)
3653+
in
3654+
(cps, cpe)
3655+
36383656
(* -------------------------------------------------------------------- *)
36393657
and trans_dcodepos1 ?(memory : memory option) (env : EcEnv.env) (p : pcodepos1 doption) : codepos1 doption =
36403658
DOption.map (trans_codepos1 ?memory env) p

tests/fine-grained-module-defs.ec

+2-3
Original file line numberDiff line numberDiff line change
@@ -31,11 +31,10 @@ end;
3131

3232
module A_count (B : T) = A(B) with {
3333
var c : int
34-
proc f [1 - { c <- c + 1;}]
35-
proc g [1 ~ { c <- c - 1;} 2 -] res ~ (x + 1)
34+
proc f [1 + ^ { c <- c + 1;}]
35+
proc g [[^x<- .. ^ <@] ~ { c <- c - 1;}] res ~ (x + 1)
3636
proc h [^match - #Some.]
3737
}.
38-
print A_count.
3938

4039
equiv A_A_count (B <: T{-A_count, -A}) : A(B).f ~ A_count(B).f: ={arg, glob B} /\ ={x}(A, A_count) ==> ={res, glob B} /\ ={x}(A, A_count).
4140
proof.

0 commit comments

Comments
 (0)