From 991ec9225524555f8e1474480d1efda5f5eb9968 Mon Sep 17 00:00:00 2001 From: Benjamin Gregoire Date: Wed, 26 Oct 2022 20:18:55 +0200 Subject: [PATCH] New inline tactic We realized that sometimes we want to inline everything besides one procedure and found that it is cumbersome to have to list everything that has to be inlined instead of listing what should remain as is. So we decided to add this to the current inline. We should have kept the previous use cases identical as supported by the fact that nothing broke while not touching any old ec files. In doing so, we also added the possibility to provide the name of a module leading to inlining all the procedure in this module. Finally, one can now provide the name of a procedure and it will inline all the procedures with that name regardless of the module in which they belong. As already mentioned, one can find examples at the following link. https://github.com/EasyCrypt/easycrypt/blob/deploy-inline/examples/tactics/inline.ec start with parsing pattern matching on inline add some examples fix --- examples/tactics/inline.ec | 128 ++++++++++++++++++++++++++++++++++ src/ecHiGoal.ml | 2 +- src/ecParser.mly | 32 +++++++-- src/ecParsetree.ml | 13 +++- src/phl/ecPhlInline.ml | 138 ++++++++++++++++++++++++------------- 5 files changed, 258 insertions(+), 55 deletions(-) create mode 100644 examples/tactics/inline.ec diff --git a/examples/tactics/inline.ec b/examples/tactics/inline.ec new file mode 100644 index 0000000000..3f6c544a7a --- /dev/null +++ b/examples/tactics/inline.ec @@ -0,0 +1,128 @@ +module F = { + proc f () = { + var r; + + r <- 0; + } + + proc g () = { + var s; + + s <- 1; + } +}. + +module G = { + proc f () = { + var t; + + F.g(); + t <- 2; + } + + proc g () = { + var u; + + F.f(); + u <- 3; + } +}. + +module Game = { + proc main () = { + F.f(); + G.g(); + F.g(); + G.f(); + } +}. + +equiv inline_full_procedures : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline F.f G.g. +admitted. + +equiv inline_star : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline *. +admitted. + +equiv inline_blank : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline. +admitted. + +equiv inline_module : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline F. +admitted. + +equiv inline_procedure : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline f. +admitted. + +equiv inline_minus_full_procedure : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline * - F.f. +admitted. + +equiv inline_minus_procedure : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline * - f. +admitted. + +equiv inline_minus_module : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline * - F. +admitted. + +equiv inline_minuses : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline * - F - g. +admitted. + +equiv inline_add_back : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline * - F F. +admitted. + +equiv inline_remove_back : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline F - F. +admitted. + +equiv inline_side : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline{1} *. +admitted. + +equiv inline_occs : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline{1} (1 4). +admitted. + +equiv inline_occs_pat : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline{1} (1 2) * - G. +admitted. + +equiv inline_codepos : Game.main ~ Game.main : true ==> true. +proof. +proc. +inline {1} 3. +admitted. diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 5ef64cb1a5..47197a2a92 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -1034,7 +1034,7 @@ let process_rewrite1_r ttenv ?target ri tc = let tc = t_onselect p - (t_seq (EcPhlInline.process_inline (`All (None, None))) ((t_try (t_seq EcPhlAuto.t_auto process_done)))) + (t_seq (EcPhlInline.process_inline (`ByName (None, None, ([], None)))) ((t_try (t_seq EcPhlAuto.t_auto process_done)))) tc in diff --git a/src/ecParser.mly b/src/ecParser.mly index b241feef23..667ad47055 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -797,7 +797,7 @@ mod_ident1: { (mk_loc (EcLocation.make $startpos(_l) $endpos(_l)) EcCoreLib.i_self, None) :: x } -fident: +%inline fident: | nm=mod_qident DOT x=lident { (nm, x) } | x=lident { ([], x) } @@ -810,6 +810,26 @@ f_or_mod_ident: FM_FunOrVar fv} | m=loc(mod_qident) { FM_Mod m } + +inlinesubpat: +| m=rlist1(uident, DOT) { m, None } +| m=rlist1(uident, DOT) DOT f=lident { m, Some f} +| f=lident { [], Some f} + +inlinepat1: +| nm=loc(mod_qident) { `InlinePat(nm, ([], None)) } +| f=loc(fident) { + let f0 = unloc f in + if fst f0 = [] then `InlinePat(mk_loc (loc f) [], ([], Some (snd f0))) + else `InlineXpath f +} +| nm=loc(mod_qident) SLASH sub=inlinesubpat { `InlinePat(nm, sub) } +| u=loc(UNDERSCORE) SLASH sub=inlinesubpat { `InlinePat(mk_loc (loc u) [], sub) } +| STAR { `InlineAll } + +inlinepat: +| sign=iboption(MINUS) p=inlinepat1 { (if sign then `DIFF else `UNION), p } + (* -------------------------------------------------------------------- *) %inline ordering_op: | GT { ">" } @@ -3168,15 +3188,15 @@ phltactic: | RNDSEM s=side? c=codepos1 { Prndsem (s, c) } -| INLINE s=side? u=inlineopt? o=occurences? f=plist1(loc(fident), empty) - { Pinline (`ByName (s, u, (f, o))) } +| INLINE s=side? u=inlineopt? o=occurences? + { Pinline (`ByName(s, u, ([], o))) } + +| INLINE s=side? u=inlineopt? o=occurences? f1=inlinepat1 f=plist0(inlinepat, empty) + { Pinline (`ByName(s, u, ((`UNION, f1)::f, o))) } | INLINE s=side? u=inlineopt? p=codepos { Pinline (`CodePos (s, u, p)) } -| INLINE s=side? u=inlineopt? STAR - { Pinline (`All (s, u)) } - | KILL s=side? o=codepos { Pkill (s, o, Some 1) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 9bf58b3ef1..60d3bbbe4c 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -659,10 +659,19 @@ type async_while_info = { (* -------------------------------------------------------------------- *) type inlineopt = [`UseTuple of bool] option +type inline_pat1 = [ + | `InlineXpath of pgamepath + | `InlinePat of pmsymbol located * (psymbol list * psymbol option) + | `InlineAll +] + + +type inline_pat = ([ `DIFF | `UNION] * inline_pat1) list + type inline_info = [ - | `ByName of oside * inlineopt * (pgamepath list * int list option) + | `ByName of oside * inlineopt * (inline_pat * int list option) | `CodePos of (oside * inlineopt * codepos) - | `All of oside * inlineopt + (* | `All of oside * inlineopt *) ] (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlInline.ml b/src/phl/ecPhlInline.ml index e16f57296c..6806474a8f 100644 --- a/src/phl/ecPhlInline.ml +++ b/src/phl/ecPhlInline.ml @@ -2,6 +2,8 @@ open EcParsetree open EcUtils open EcMaps +open EcLocation +open EcPath open EcTypes open EcModules open EcFol @@ -216,19 +218,9 @@ let t_inline_equiv ~use_tuple = (* -------------------------------------------------------------------- *) module HiInternal = struct (* ------------------------------------------------------------------ *) - let pat_all env fs s = - let test f = - let is_defined = function FBdef _ -> true | _ -> false in - - match fs with - | Some fs -> EcPath.Sx.mem (EcEnv.NormMp.norm_xfun env f) fs - | None -> - let f = EcEnv.NormMp.norm_xfun env f in - let f = EcEnv.Fun.by_xpath f env in - is_defined f.f_def - in + let pat_all cond s = - let test = EcPath.Hx.memo 0 test in + let test = EcPath.Hx.memo 0 cond in let rec aux_i i = match i.i_node with @@ -334,62 +326,57 @@ module HiInternal = struct end (* -------------------------------------------------------------------- *) -let rec process_inline_all ~use_tuple side fs tc = - let env, _, concl = FApi.tc1_eflat tc in +let rec process_inline_all ~use_tuple side cond tc = + let concl = FApi.tc1_goal tc in match concl.f_node, side with | FequivS _, None -> FApi.t_seq - (process_inline_all ~use_tuple (Some `Left ) fs) - (process_inline_all ~use_tuple (Some `Right) fs) + (process_inline_all ~use_tuple (Some `Left ) cond) + (process_inline_all ~use_tuple (Some `Right) cond) tc | FequivS es, Some b -> begin let st = sideif b es.es_sl es.es_sr in - match HiInternal.pat_all env fs st with + match HiInternal.pat_all cond st with | [] -> t_id tc | sp -> FApi.t_seq (t_inline_equiv ~use_tuple b sp) - (process_inline_all ~use_tuple side fs) + (process_inline_all ~use_tuple side cond) tc end | FhoareS hs, None -> begin - match HiInternal.pat_all env fs hs.hs_s with + match HiInternal.pat_all cond hs.hs_s with | [] -> t_id tc | sp -> FApi.t_seq (t_inline_hoare ~use_tuple sp) - (process_inline_all ~use_tuple side fs) + (process_inline_all ~use_tuple side cond) tc end | FcHoareS chs, None -> begin - match HiInternal.pat_all env fs chs.chs_s with + match HiInternal.pat_all cond chs.chs_s with | [] -> t_id tc | sp -> FApi.t_seq (t_inline_choare ~use_tuple sp) - (process_inline_all ~use_tuple side fs) + (process_inline_all ~use_tuple side cond) tc end | FbdHoareS bhs, None -> begin - match HiInternal.pat_all env fs bhs.bhs_s with + match HiInternal.pat_all cond bhs.bhs_s with | [] -> t_id tc | sp -> FApi.t_seq (t_inline_bdhoare ~use_tuple sp) - (process_inline_all ~use_tuple side fs) + (process_inline_all ~use_tuple side cond) tc end | _, _ -> tc_error !!tc "invalid arguments" (* -------------------------------------------------------------------- *) -let process_inline_occs ~use_tuple side fs occs tc = - let env = FApi.tc1_env tc in - let cond = - if EcPath.Sx.is_empty fs - then fun _ -> true - else fun f -> EcPath.Sx.mem (EcEnv.NormMp.norm_xfun env f) fs in +let process_inline_occs ~use_tuple side cond occs tc = let occs = Sint.of_list occs in let concl = FApi.tc1_goal tc in @@ -441,27 +428,86 @@ let process_inline_codepos ~use_tuple side pos tc = with EcMatching.Zipper.InvalidCPos -> tc_error !!tc "invalid position" +(* -------------------------------------------------------------------- *) +let process_info tc infos = + let env = FApi.tc1_env tc in + let doit (dir, pat) = + let pat = + match pat with + | `InlineXpath f -> + let f = EcTyping.trans_gamepath env f in + `InlineXpath (EcEnv.NormMp.norm_xfun env f) + | `InlinePat (pm, (sub, f)) -> + let pm = + List.rev_map (fun (p, o) -> + if o <> None then tc_error !!tc ~loc:(loc p) "can not provide functor arguments"; + unloc p) (unloc pm) in + let sub = List.rev_map unloc sub in + let f = omap unloc f in + `InlinePat(pm, sub, f) + | `InlineAll -> `InlineAll in + (dir, pat) in + List.map doit infos + + +(* -------------------------------------------------------------------- *) +let test_match pm sub fx f = + + let rec test_path ids p = + match ids, p.p_node with + | [], _ -> true + | [id], EcPath.Psymbol id' -> EcSymbols.sym_equal id id' + | id::ids, EcPath.Pqname(p, id') -> EcSymbols.sym_equal id id' && test_path ids p + | _, _ -> false + in + + begin match fx with None -> true | Some sym -> EcSymbols.sym_equal sym f.x_sub end + && match f.x_top.m_top with + | `Local a -> + sub = [] && + begin match pm with + | [] -> true + | [id] -> EcSymbols.sym_equal id (EcIdent.name a) + | _ -> false + end + + | `Concrete (p, sp) -> ofold (fun sp b -> b && test_path sub sp) (test_path pm p) sp + + +let test_pat for_occ env infos f = + let fn = EcEnv.NormMp.norm_xfun env f in + + let test_pat1 all pat = + match pat with + | `InlineXpath fn' -> EcPath.x_equal fn fn' + | `InlinePat (pm, sub, fx) -> test_match pm sub fx f + | `InlineAll -> + all || + match (EcEnv.Fun.by_xpath fn env).f_def with + | FBdef _ -> true | _ -> false in + + let rec aux b infos = + match infos with + | [] -> b + | (`UNION, pat) :: infos -> aux (b || test_pat1 for_occ pat) infos + | (`DIFF, pat) :: infos -> aux (b && not(test_pat1 true pat)) infos in + + aux false infos + (* -------------------------------------------------------------------- *) let process_inline infos tc = let use_tuple use = odfl true (omap (function `UseTuple b -> b) use) in - match infos with - | `ByName (side, use, (fs, occs)) -> begin - let env = FApi.tc1_env tc in - let use_tuple = use_tuple use in - let fs = - List.fold_left (fun fs f -> - let f = EcTyping.trans_gamepath env f in - EcPath.Sx.add (EcEnv.NormMp.norm_xfun env f) fs) - EcPath.Sx.empty fs - in - match occs with - | None -> process_inline_all ~use_tuple side (Some fs) tc - | Some occs -> process_inline_occs ~use_tuple side fs occs tc + | `ByName (side, use, (infos, occs)) -> + let infos = process_info tc infos in + let infos = if infos = [] then [`UNION, `InlineAll] else infos in + let env = FApi.tc1_env tc in + let use_tuple = use_tuple use in + begin match occs with + | None -> process_inline_all ~use_tuple side (test_pat false env infos) tc + | Some occs -> process_inline_occs ~use_tuple side (test_pat true env infos) occs tc end | `CodePos (side, use, pos) -> - process_inline_codepos ~use_tuple:(use_tuple use) side pos tc - - | `All (side, use) -> process_inline_all ~use_tuple:(use_tuple use) side None tc + process_inline_codepos ~use_tuple:(use_tuple use) side pos tc