Added tactic: outline.

examples/tactics/outline.ec

@@ -0,0 +1,125 @@
+require import AllCore.
+
+op dint : int distr.
+
+module M = {
+  var x : int
+
+  proc f1() : unit = {
+    M.x <- 0;
+  }
+
+  proc f2(a: int) : unit = {
+    M.x <- a;
+  }
+
+  proc f3(a: int, b: int) : int = {
+    return a + b;
+  }
+
+  proc f4(a: int, b: int) : int = {
+    var t;
+    if (a <= b) {
+      t <- b;
+    } else {
+      t <- a;
+    }
+    return t;
+  }
+
+  proc f5(d: int distr) : int = {
+    var v;
+    v <$ d;
+    return v;
+  }
+}.
+
+module N = {
+  proc g1() : unit = {
+    M.f1();
+  }
+
+  proc g2(a) : unit = {
+    M.f2(a);
+  }
+
+  proc g3(a, b) : unit = {
+    var r;
+    r <@ M.f3(a, b);
+  }
+
+  proc g4(a: int, b: int) : unit = {
+    var m;
+    if (a <= b) {
+      m <- b;
+    } else {
+      m <- a;
+    }
+    M.x <- m;
+  }
+
+  proc g5() : unit = {
+    var x;
+    x <$ dint;
+  }
+
+  proc g6() : unit = {
+    var a, b, m;
+    a <$ dint;
+    b <$ dint;
+    if (a <= b) {
+      m <- b;
+    } else {
+      m <- a;
+    }
+    M.x <- m;
+  }
+}.
+
+equiv outline_no_args_no_ret: N.g1 ~ N.g1: true ==> true.
+proc.
+inline {1} 1.
+outline {1} [1] M.f1.
+admitted.
+
+equiv outline_no_ret: N.g2 ~ N.g2: true ==> true.
+proc.
+inline {1} 1.
+outline {1} [2] M.f2.
+admitted.
+
+equiv outline_no_body: N.g3 ~ N.g3: true ==> true.
+proc.
+inline {1} 1.
+outline {1} [3] M.f3.
+admitted.
+
+equiv outline_slice: N.g4 ~ N.g4: true ==> true.
+proc.
+outline {1} [1-2] M.f4.
+admitted.
+
+equiv outline_explicit_ret: N.g5 ~ N.g5: true ==> true.
+proc.
+outline {1} [1] M.f5 @ x.
+admitted.
+
+equiv outline_multi: N.g6 ~ N.g6: true ==> true.
+proof.
+proc.
+outline {1} [3-4] N.g4.
+outline {1} [2] M.f5 @ b.
+outline {1} [1] M.f5 @ a.
+by inline*; auto.
+qed.
+
+equiv outline_stmt: N.g6 ~ N.g6: true ==> true.
+proof.
+proc.
+outline {1} [1-4] {
+  a <@ M.f5(dint);
+  b <@ M.f5(dint);
+  N.g4(a,b);
+}.
+by inline*; auto.
+qed.

src/ecCoreModules.ml

@@ -43,6 +43,14 @@ let name_of_lv lv =
   | LvTuple pvs ->
      String.concat "_" (List.map (EcTypes.name_of_pvar |- fst) pvs)
 
+let lv_of_expr e =
+  match e.e_node with
+  | Evar pv ->
+     LvVar (pv, e_ty e)
+  | Etuple pvs ->
+     LvTuple (List.map (fun e -> EcTypes.destr_var e, e_ty e) pvs)
+  | _ -> failwith "failed to construct lv from expr"
+
 (* -------------------------------------------------------------------- *)
 type instr = EcAst.instr
 

src/ecCoreModules.mli

@@ -12,6 +12,7 @@ val ty_of_lv     : lvalue -> EcTypes.ty
 val lv_of_list   : (prog_var * ty) list -> lvalue option
 val lv_to_list   : lvalue -> prog_var list
 val name_of_lv   : lvalue -> string
+val lv_of_expr   : expr -> lvalue
 
 (* --------------------------------------------------------------------- *)
 type instr = EcAst.instr

src/ecHiTacticals.ml

@@ -189,6 +189,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pcallconcave info         -> EcPhlCall.process_call_concave info
     | Pswap sw                  -> EcPhlSwap.process_swap sw
     | Pinline info              -> EcPhlInline.process_inline info
+    | Poutline info             -> EcPhlOutline.process_outline info
     | Pinterleave info          -> EcPhlSwap.process_interleave info
     | Pcfold info               -> EcPhlCodeTx.process_cfold info
     | Pkill info                -> EcPhlCodeTx.process_kill info

src/ecLexer.mll

@@ -154,6 +154,7 @@
     "conseq"      , CONSEQ     ;        (* KW: tactic *)
     "exfalso"     , EXFALSO    ;        (* KW: tactic *)
     "inline"      , INLINE     ;        (* KW: tactic *)
+    "outline"     , OUTLINE    ;        (* KW: tactic *)
     "interleave"  , INTERLEAVE ;        (* KW: tactic *)
     "alias"       , ALIAS      ;        (* KW: tactic *)
     "fission"     , FISSION    ;        (* KW: tactic *)

src/ecParser.mly

@@ -511,6 +511,7 @@
 %token NOTATION
 %token OF
 %token OP
+%token OUTLINE
 %token PCENT
 %token PHOARE
 %token PIPE
@@ -3127,6 +3128,10 @@ interleave_info:
 | s=side? c1=interleavepos c2=interleavepos c3=interleavepos* k=word
    { (s, c1, c2 :: c3, k) }
 
+%inline outline_kind:
+| s=brace(stmt) { OKstmt(s) }
+| f=loc(fident) r=option(AT e=sexpr { e }) { OKproc(f, r) }
+
 phltactic:
 | PROC
    { Pfun `Def }
@@ -3217,6 +3222,14 @@ phltactic:
 | INLINE s=side? u=inlineopt? p=codepos
     { Pinline (`CodePos (s, u, p)) }
 
+| OUTLINE s=side LBRACKET st=codepos1 e=option(MINUS e=codepos1 {e}) RBRACKET k=outline_kind
+    { Poutline {
+	  outline_side  = s; 
+	  outline_start = st; 
+	  outline_end   = odfl st e; 
+	  outline_kind  = k }
+    }
+
 | KILL s=side? o=codepos
     { Pkill (s, o, Some 1) }
 

src/ecParsetree.ml

@@ -670,6 +670,18 @@ type inline_info = [
  (* | `All       of oside * inlineopt *)
 ]
 
+(* -------------------------------------------------------------------- *)
+type outline_kind =
+  | OKstmt of pstmt
+  | OKproc of pgamepath * pexpr option
+
+type outline_info = {
+    outline_side: side;
+    outline_start: codepos1;
+    outline_end: codepos1;
+    outline_kind: outline_kind;
+}
+
 (* -------------------------------------------------------------------- *)
 type fel_info = {
   pfel_cntr  : pformula;
@@ -731,6 +743,7 @@ type phltactic =
   | Pswap          of ((oside * swap_kind) located list)
   | Pcfold         of (oside * codepos * int option)
   | Pinline        of inline_info
+  | Poutline       of outline_info
   | Pinterleave    of interleave_info located
   | Pkill          of (oside * codepos * int option)
   | Prnd           of oside * semrndpos option * rnd_tac_info_f

src/ecUtils.ml

@@ -457,6 +457,11 @@ module List = struct
   include Parallel
 
   (* ------------------------------------------------------------------ *)
+  let rec zip xs ys =
+    match xs, ys with
+    | (x :: xs), (y :: ys) -> (x, y) :: zip xs ys
+    | _, _ -> []
+
   let nth_opt (s : 'a list) (i : int) =
     try  Some (List.nth s i)
     with Failure _ | Invalid_argument _ -> None

src/ecUtils.mli

@@ -274,6 +274,7 @@ module List : sig
   val min : ?cmp:('a -> 'a -> int) -> 'a list -> 'a
   val max : ?cmp:('a -> 'a -> int) -> 'a list -> 'a
 
+  val zip        : 'a list -> 'b list -> ('a * 'b) list
   val nth_opt    : 'a list -> int -> 'a option
   val mbfilter   : ('a -> bool) -> 'a list -> 'a list
   val fusion     : ('a -> 'a -> 'a) -> 'a list -> 'a list -> 'a list