Implemented match branch collapsing, other small refactorings.

src/ecMatching.ml

@@ -86,7 +86,7 @@ module Zipper = struct
 
   let cpos (i : int) : codepos1 = (0, `ByPos i)
 
-  let zipper ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env}
+  let zipper ?env hd tl zpr = { z_head = hd; z_tail = tl; z_path = zpr; z_env = env; }
 
   let find_by_cp_match
     (env     : EcEnv.env)
@@ -291,7 +291,7 @@ module Zipper = struct
       end
 
   let fold env cenv cpos f state s =
-    let f e ce st i tl = 
+    let f e ce st i tl =
       let state', si = f e ce st i in
       state', si @ tl
     in

src/ecMatching.mli

@@ -105,7 +105,6 @@ module Zipper : sig
   type ('a, 'state) folder = env -> 'a -> 'state -> instr -> 'state * instr list
   type ('a, 'state) folder_tl = env -> 'a -> 'state -> instr -> instr list -> 'state * instr list
 
-  val fold_tl : env -> 'a -> codepos -> ('a, 'state) folder_tl -> 'state -> stmt -> 'state * stmt
   (* [fold env v cpos f state s] create the zipper for [s] at [cpos], and apply
    * [f] to it, along with [v] and the state [state]. [f] must return the
    * new [state] and a new [zipper]. These last are directly returned.
@@ -115,6 +114,9 @@ module Zipper : sig
    *)
   val fold : env -> 'a -> codepos -> ('a, 'state) folder -> 'state -> stmt -> 'state * stmt
 
+  (* Same as above but using [folder_tl]. *)
+  val fold_tl : env -> 'a -> codepos -> ('a, 'state) folder_tl -> 'state -> stmt -> 'state * stmt
+
   (* [map cpos env f s] is a special case of [fold] where the state and the
    * out-of-band data are absent
    *)

src/ecTyping.ml

@@ -2263,34 +2263,33 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
     let (mp, sig_) = trans_msymbol env {pl_desc = m; pl_loc = loc} in
 
     (* Prohibit functor updates *)
-    if 0 < List.length sig_.miss_params then
+    if not (List.is_empty sig_.miss_params) then
       tyerror loc env (InvalidModUpdate MUE_Functor);
 
     (* Construct the set of new module variables *)
     let items =
-      List.fold_right 
-        (fun (xs, ty) acc -> 
+      List.concat_map
+        (fun (xs, ty) ->
           let ty = transty_for_decl env ty in
           let items = List.map
             (fun { pl_desc = x } -> MI_Variable { v_name = x; v_type = ty; })
             xs
           in
-          items @ acc)
+          items)
         vars
-        []
     in
 
     let me, _ = EcEnv.Mod.by_mpath mp env in
     let p = match mp.m_top with | `Concrete (p, _) -> p | _ -> assert false in
     let subst = EcSubst.add_moddef EcSubst.empty ~src:p ~dst:(EcEnv.mroot env) in
     let me = EcSubst.subst_module subst me in
 
-    let update_fun env fn plocals pupdates pupdate_res = 
+    let update_fun env fn plocals pupdates pupdate_res =
       (* Extract the function body and load the memory *)
       let fun_ = EcEnv.Fun.by_xpath (xpath mp fn) env in
 
       (* Follow a function alias until we get to the concrete definition *)
-      let rec resolve_alias f = 
+      let rec resolve_alias f =
         match f.f_def with
         | FBabs _ ->
           tyerror loc env (InvalidModUpdate MUE_AbstractModule);
@@ -2304,7 +2303,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
       let fun_ = EcSubst.subst_function subst fun_ in
 
       (* Introduce the new local variables *)
-      let locals = List.concat_map (fun (vs, pty) -> 
+      let locals = List.concat_map (fun (vs, pty) ->
           let ty = transty_for_decl env pty in
           List.map (fun x -> { v_name = x.pl_desc; v_type = ty; }, x.pl_loc) vs
         )
@@ -2314,6 +2313,9 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
       let memenv = fundef_add_symbol env memenv locals in
       let env = EcEnv.Memory.push_active memenv env in
 
+      let locals = ref locals in
+      let memenv = ref memenv in
+
       (* Semantics for stmt updating, `i` is the target of the update. *)
       let eval_supdate env sup i =
         match sup with
@@ -2340,7 +2342,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
           let ts = Tuni.subst (UE.close ue) in
           let ty = ty_subst ts ty in
           unify_or_fail env ue loc ~expct:tbool ty;
-          [i] @ [i_if (e_subst ts e, stmt tl, s_empty)]
+          i :: [i_if (e_subst ts e, stmt tl, s_empty)]
 
         (* Change the condition expression to `e` for a conditional instr `i` *)
         | Pupc_mod e -> begin
@@ -2350,7 +2352,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
           let ts = Tuni.subst (UE.close ue) in
           let ty = ty_subst ts ty in
           match i.i_node with
-          | Sif (_, t, f) -> 
+          | Sif (_, t, f) ->
             unify_or_fail env ue loc ~expct:tbool ty;
             [i_if (e_subst ts e, t, f)] @ tl
           | Smatch (p, bs) ->
@@ -2370,27 +2372,58 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
           | Sif (_, t, _), `Cond true -> t.s_node
           | Sif (_, _, f), `Cond false -> f.s_node
           | Swhile (_, t), `Cond true -> t.s_node
-          | Smatch (_e, _bs), `Match _cn ->
-            (* FIXME: need to introduce binding for constructor pattern variables *)
+          | Smatch (e, bs), `Match cn -> begin
             (* match e with | C a b c => b | ...  ---> (a, b, c) <- oget (get_as_C e); b *)
-            (*
-            let _, indt, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in
-            let indt = oget (EcDecl.tydecl_as_datatype indt) in
+
+            let typ, tydc, tyinst = oget (EcEnv.Ty.get_top_decl e.e_ty env) in
+            let tyinst = List.combine tydc.tyd_params tyinst in
+            let indt = oget (EcDecl.tydecl_as_datatype tydc) in
             let cnames = List.fst indt.tydt_ctors in
-            let ix, _ = List.findi (fun _ n -> EcSymbols.sym_equal cn n) cnames in
-            let _, r = List.split_at ix bs in
-            let _p, b, _ = match r with (p, b) :: r -> p, b, r | _ -> assert false in
-            b.s_node @ tl
-            *)
-            tyerror cp_loc env (InvalidModUpdate MUE_InvalidTargetCond);
+            let r = List.assoc_opt cn (List.combine cnames bs) in
+            match r with
+            | None ->
+              tyerror cp_loc env (InvalidModUpdate MUE_InvalidTargetCond)
+            | Some (p, b) -> begin
+              (* TODO: Factorize. This is mostly just a copy/paste from EcPhlRCond.gen_rcond_full. *)
+              let cvars = List.map (fun (x, xty) -> { ov_name = Some (EcIdent.name x); ov_type = xty; }) p in
+              let me, cvars = EcMemory.bindall_fresh cvars !memenv in
+
+              let subst, pvs =
+                let s = Fsubst.f_subst_id in
+                let s, pvs = List.fold_left_map (fun s ((x, xty), name) ->
+                    let pv = pv_loc (oget name.ov_name) in
+                    let s  = bind_elocal s x (e_var pv xty) in
+                    (s, (pv, xty)))
+                  s (List.combine p cvars)
+                in
+                (s, pvs)
+              in
+
+              let asgn = EcModules.lv_of_list pvs |> omap (fun lv ->
+                  let rty  = ttuple (List.snd p) in
+                  let proj = EcInductive.datatype_proj_path typ cn in
+                  let proj = e_op proj (List.snd tyinst) (tfun e.e_ty (toption rty)) in
+                  let proj = e_app proj [e] (toption rty) in
+                  let proj = e_oget proj rty in
+                  i_asgn (lv, proj))
+              in
+
+              memenv := me;
+              locals := !locals @ (List.map (fun ov -> {v_name = oget ov.ov_name; v_type = ov.ov_type; }, cp_loc) cvars);
+
+              match asgn with
+              | None -> b.s_node @ tl
+              | Some a -> a :: (s_subst subst b).s_node @ tl
+            end
+          end
           | _ ->
             tyerror cp_loc env (InvalidModUpdate MUE_InvalidTargetCond);
           end
       in
 
       (* Apply each of updates in reverse *)
       (* NOTE: This is with the expectation that the user entered them in chronological order. *)
-      let body = 
+      let body =
         List.fold_right (fun (cp, up) bd ->
           let {pl_desc = cp; pl_loc = loc} = cp in
           let cp = trans_codepos env cp in
@@ -2401,15 +2434,16 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
             | Pup_cond cup ->
               eval_cupdate loc env cup i tl
           in
+          let env = EcEnv.Memory.push_active !memenv env in
           try
             let _, s = EcMatching.Zipper.fold_tl env () cp change () bd in
             s
           with
             | EcMatching.Zipper.InvalidCPos ->
               tyerror loc env (InvalidModUpdate MUE_InvalidCodePos);
         )
-          pupdates
-          fd.f_body
+        pupdates
+        fd.f_body
       in
 
       (* Apply the result update if given *)
@@ -2421,34 +2455,34 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
           unify_or_fail env ue loc ~expct:e.e_ty ty;
           let ts = Tuni.subst (UE.close ue) in
           Some (e_subst ts e')
-          | _ -> fd.f_ret
+        | _ -> fd.f_ret
       in
 
       (* Reconstruct the function def *)
       let uses = ret |> ofold ((^~) se_inuse) (s_inuse body) in
-      let fd = {f_locals = fd.f_locals @ (List.fst locals); f_body = body; f_ret = ret; f_uses = uses} in 
+      let fd = {f_locals = fd.f_locals @ (List.fst !locals); f_body = body; f_ret = ret; f_uses = uses; } in
       let fun_ = {fun_ with f_def = FBdef fd} in
       fun_
     in
 
     let allowed_funs = List.map (fun (Tys_function f) -> f.fs_name) me.me_sig_body in
     let funs = List.map (fun ({pl_loc = loc; pl_desc = fn}, lvs, v) ->
       if List.mem fn allowed_funs then
-      fn, (lvs, v)
+        fn, (lvs, v)
       else
         tyerror loc env (InvalidModUpdate MUE_InvalidFun)
     ) funs
     in
 
     (* Update all module items *)
-    let env, items = 
+    let env, items =
       match me.me_body with
       | ME_Structure mb ->
         let doit (env, items) mi =
           match mi with
           | MI_Variable v ->
             let env = EcEnv.Var.bind_pvglob v.v_name v.v_type env in
-            env, items @ [mi] 
+            env, items @ [mi]
           | MI_Function f  -> begin
             match List.assoc_opt f.f_name funs with
             | None ->
@@ -2459,9 +2493,9 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) =
               let env = EcEnv.bind1 (f.f_name, `Function f) env in
               env, items @ [MI_Function f]
             end
-          | MI_Module me -> 
+          | MI_Module me ->
             let env = EcEnv.bind1 (me.me_name, `Module me) env in
-            env, items @ [mi] 
+            env, items @ [mi]
         in
         List.fold_left doit (env, []) (items @ mb.ms_body)
 

tests/fine-grained-module-defs.ec

@@ -33,11 +33,18 @@ module A_count (B : T) = A(B) with {
   var c : int
   proc f [1 - { c <- c + 1;}]
   proc g [1 ~ { c <- c - 1;} 2 -] res ~ (x + 1)
-  proc h [^match#Some.^r<- ~ { r <- v + 1; }]
+  proc h [^match - #Some.]
 }.
+print A_count.
 
 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).
 proof.
 proc.
 by call (: true); auto.
 qed.
+
+lemma Check_Delete_Branch (B <: T): hoare[A_count(B).h: arg = Some 4 ==> res = 4].
+proof.
+proc.
+by auto.
+qed.