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

@@ -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.

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
 

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) }
 

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 *)
 ]
 
 (* -------------------------------------------------------------------- *)