New tactic: "case <-"

This tactic "inlines" tuple assignments, i.e. it transforms

```
(lv1,...,lvn) <- (e1,...,en);
```

in

```
lv1 <- e1;
...
lvn <- en;
```

Author: strub

src/ecHiTacticals.ml

@@ -193,6 +193,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pinterleave info          -> EcPhlSwap.process_interleave info
     | Pcfold info               -> EcPhlCodeTx.process_cfold info
     | Pkill info                -> EcPhlCodeTx.process_kill info
+    | Pasgncase info            -> EcPhlCodeTx.process_case info
     | Palias info               -> EcPhlCodeTx.process_alias info
     | Pset info                 -> EcPhlCodeTx.process_set info
     | Pweakmem info             -> EcPhlCodeTx.process_weakmem info

src/ecPV.ml

@@ -622,6 +622,9 @@ and i_read_r env r i =
 (* -------------------------------------------------------------------- *)
 type 'a pvaccess0 = env -> 'a -> PV.t
 
+let lp_write env lp =
+  lp_write_r env PV.empty lp
+
 let i_write  ?(except=Sx.empty) env i  = i_write_r  ~except env PV.empty i
 let is_write ?(except=Sx.empty) env is = is_write_r ~except env PV.empty is
 let s_write  ?(except=Sx.empty) env s  = s_write_r  ~except env PV.empty s

src/ecPV.mli

@@ -131,6 +131,7 @@ val f_read_r   : xpath      pvaccess
 (* -------------------------------------------------------------------- *)
 type 'a pvaccess0 = env -> 'a -> PV.t
 
+val lp_write :                 lvalue     pvaccess0
 val i_write  : ?except:Sx.t -> instr      pvaccess0
 val is_write : ?except:Sx.t -> instr list pvaccess0
 val s_write  : ?except:Sx.t -> stmt       pvaccess0

src/ecParser.mly

@@ -3233,6 +3233,9 @@ phltactic:
 | KILL s=side? o=codepos NOT STAR
     { Pkill (s, o, None) }
 
+| CASE LARROW s=side? o=codepos
+    { Pasgncase (s, o) }
+
 | ALIAS s=side? o=codepos
     { Palias (s, o, None) }
 

src/ecParsetree.ml

@@ -755,6 +755,7 @@ type phltactic =
   | Poutline       of outline_info
   | Pinterleave    of interleave_info located
   | Pkill          of (oside * codepos * int option)
+  | Pasgncase      of (oside * codepos)
   | Prnd           of oside * semrndpos option * rnd_tac_info_f
   | Prndsem        of bool * oside * codepos1
   | Palias         of (oside * codepos * osymbol_r)

src/phl/ecPhlCodeTx.ml

@@ -1,5 +1,6 @@
 (* -------------------------------------------------------------------- *)
 open EcUtils
+open EcParsetree
 open EcAst
 open EcTypes
 open EcModules
@@ -293,3 +294,42 @@ let process_weakmem (side, id, params) tc =
   in
   let concl = f_imp h (FApi.tc1_goal tc) in
   FApi.xmutate1 tc `WeakenMem [concl]
+
+(* -------------------------------------------------------------------- *)
+let process_case ((side, pos) : side option * codepos) (tc : tcenv1) =
+  let (env, _, concl) = FApi.tc1_eflat tc in
+
+  let change (i : instr) =
+    if not (is_asgn i) then
+      tc_error !!tc "the code position should target an assignment";
+
+    let lv, e = destr_asgn i in
+
+    let pvl = EcPV.lp_write env lv in
+    let pve = EcPV.e_read env e in
+    let lv  = lv_to_list lv in
+
+    if not (EcPV.PV.indep env pvl pve) then
+      assert false;
+
+    let e =
+      match lv, e.e_node with
+      | [_], _         -> [e]
+      | _  , Etuple es -> es
+      | _  ,_          -> assert false in
+
+    let s = List.map2 (fun pv e -> i_asgn (LvVar (pv, e.e_ty), e)) lv e in
+
+    ([], s)
+  in
+
+  let kinds = [`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] in
+
+  if not (EcLowPhlGoal.is_program_logic concl kinds) then
+    assert false;
+
+  let s = EcLowPhlGoal.tc1_get_stmt side tc in
+  let goals, s = EcMatching.Zipper.map pos change s in
+  let concl = EcLowPhlGoal.hl_set_stmt side concl s in
+
+  FApi.xmutate1 tc `ProcCase (goals @ [concl])

src/phl/ecPhlCodeTx.mli

@@ -14,6 +14,7 @@ val process_kill  : oside * codepos * int option -> backward
 val process_alias : oside * codepos * psymbol option -> backward
 val process_set   : oside * codepos * bool * psymbol * pexpr -> backward
 val process_cfold : oside * codepos * int option -> backward
+val process_case  : oside * codepos -> backward
 
 (* -------------------------------------------------------------------- *)
 val process_weakmem : (oside * psymbol * fun_params) -> backward

tests/asgncase.ec

@@ -0,0 +1,23 @@
+(* -------------------------------------------------------------------- *)
+require import AllCore.
+
+(* -------------------------------------------------------------------- *)
+module M = {
+  proc f(x : int, y : int) = {
+    var x', y' : int;
+
+    (x', y') <- (x, y);
+
+    return (x', y');
+  }
+}.
+
+(* -------------------------------------------------------------------- *)
+lemma L : hoare[M.f : arg = (0, 1) ==> res = (0, 1)].
+proof.
+proc.
+case <- 1.
+seq 1 : (x' = 0 /\ y = 1).
+- by auto.
+- by auto.
+qed.