tactic: match: out of TCB

src/ecCoreGoal.ml

@@ -886,6 +886,10 @@ let (!!) = FApi.tc1_penv
 let (!$) = FApi.tc_penv
 let (!@) = FApi.tcenv_of_tcenv1
 
+(* -------------------------------------------------------------------- *)
+let (let+) (type a) (x : tcenv) (f : tcenv1 -> a) : a =
+  f (FApi.as_tcenv1 x)
+
 (* -------------------------------------------------------------------- *)
 module RApi = struct
   type rproofenv = proofenv ref

src/ecCoreGoal.mli

@@ -379,6 +379,8 @@ val (!!) : tcenv1 -> proofenv
 val (!$) : tcenv  -> proofenv
 val (!@) : tcenv1 -> tcenv
 
+val (let+) : tcenv -> (tcenv1 -> 'a) -> 'a
+
 (* -------------------------------------------------------------------- *)
 (* Imperative API                                                       *)
 (* -------------------------------------------------------------------- *)

src/ecLowGoal.ml

@@ -550,6 +550,10 @@ let t_intros_n ?(clear = false) (n : int) (tc : tcenv1) =
   let tc, xs = t_intros_x (EcUtils.List.make n (notag None)) tc in
   if clear then FApi.t_first (t_clears xs) tc else tc
 
+(* -------------------------------------------------------------------- *)
+let t_intros_n_x (n : int) (tc : tcenv1) =
+  t_intros_x (EcUtils.List.make n (notag None)) tc
+
 (* -------------------------------------------------------------------- *)
 let t_intro_i_x (id : EcIdent.t option) (tc : tcenv1) =
   snd_map EcUtils.as_seq1 (t_intros_x [notag id] tc)

src/ecLowGoal.mli

@@ -254,6 +254,7 @@ val t_intros_sx_seq : inames -> (ident list -> FApi.backward) -> FApi.backward
 val t_intros_s_seq  : inames -> FApi.backward -> FApi.backward
 
 val t_intros_n : ?clear:bool -> int -> FApi.backward
+val t_intros_n_x : int -> tcenv1 -> tcenv * ident list
 
 (* -------------------------------------------------------------------- *)
 type genclear = [`Clear | `TryClear | `NoClear]

src/ecLowPhlGoal.ml

@@ -192,13 +192,13 @@ let is_program_logic (f : form) (ks : hlkind list) =
 let tc1_get_stmt side tc =
   let concl = FApi.tc1_goal tc in
   match side, concl.f_node with
-  | None, FhoareS hs -> hs.hs_s
-  | None, FeHoareS hs -> hs.ehs_s
-  | None, FbdHoareS hs -> hs.bhs_s
+  | None, FhoareS hs -> hs.hs_m, hs.hs_s
+  | None, FeHoareS hs -> hs.ehs_m, hs.ehs_s
+  | None, FbdHoareS hs -> hs.bhs_m, hs.bhs_s
   | Some _ , (FhoareS _ | FbdHoareS _) ->
       tc_error_noXhl ~kinds:[`Hoare `Stmt; `PHoare `Stmt] !!tc
-  | Some `Left, FequivS es   -> es.es_sl
-  | Some `Right, FequivS es  -> es.es_sr
+  | Some `Left, FequivS es   -> es.es_ml, es.es_sl
+  | Some `Right, FequivS es  -> es.es_mr, es.es_sr
   | None, FequivS _ ->
       tc_error_noXhl ~kinds:[`Equiv `Stmt] !!tc
   | _            ->

src/phl/ecPhlCodeTx.ml

@@ -317,7 +317,7 @@ let process_case ((side, pos) : side option * codepos) (tc : tcenv1) =
   if not (EcLowPhlGoal.is_program_logic concl kinds) then
     assert false;
 
-  let s = EcLowPhlGoal.tc1_get_stmt side tc in
+  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
 

src/phl/ecPhlCond.ml

@@ -1,7 +1,6 @@
 (* -------------------------------------------------------------------- *)
 open EcUtils
 open EcTypes
-open EcModules
 open EcFol
 open EcEnv
 
@@ -114,86 +113,95 @@ let rec t_equiv_cond side tc =
           tc
 
 (* -------------------------------------------------------------------- *)
-let t_hoare_match tc =
-  let hyps = FApi.tc1_hyps tc in
-  let env  = LDecl.toenv hyps in
-  let hs   = tc1_as_hoareS tc in
-
-  let me, st = hs.hs_m, hs.hs_s in
-
-  let sets st = { hs with hs_s = st } in
-
-  let (e, bs), tl = tc1_first_match tc st in
-  let indp, indt, tyinst = oget (EcEnv.Ty.get_top_decl e.e_ty env) in
-  let indt = oget (EcDecl.tydecl_as_datatype indt) in
-  let f = form_of_expr (EcMemory.memory me) e in
-
-  let do1 ((ids, b), (cname, _)) =
-    let subst, lvars =
-      add_elocals Fsubst.f_subst_id ids in
+module LowMatchInternal : sig
+  val t_gen_match : side option -> FApi.backward
+end = struct
+  let t_gen_match (side : side option) (tc : tcenv1) : tcenv =
+    let hyps   = FApi.tc1_hyps tc in
+    let env    = LDecl.toenv hyps in
+    let me, st = EcLowPhlGoal.tc1_get_stmt side tc in
+
+    let (e, _), _ = tc1_first_match tc st in
+    let _, indt, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in
+    let indt = oget (EcDecl.tydecl_as_datatype indt) in
+    let f = form_of_expr (EcMemory.memory me) e in
+
+    let onsub (i : int) (tc : tcenv1) =
+      let cname, cargs = List.nth indt.tydt_ctors i in
+      let cargs = List.length cargs in
+
+      let tc, names = t_intros_n_x cargs tc in
+      let tc = FApi.as_tcenv1 tc in
+
+      let discharge (tc : tcenv1) =
+        let+ tc =
+          if   Option.is_some side
+          then EcLowGoal.t_intros_n 1 tc
+          else t_id tc
+        in
+
+        let+ tc = EcPhlSkip.t_skip tc in
+        let+ tc = EcLowGoal.t_intro_s `Fresh tc in
+        let+ tc = EcLowGoal.t_elim_and tc in
+
+        let e = EcEnv.LDecl.fresh_id (FApi.tc1_hyps tc) "e" in
+
+        let+ tc = EcLowGoal.t_intros_i [e] tc in
+        let+ tc = EcLowGoal.t_intros_n ~clear:true 1 tc in
+
+        let+ tc =
+          let hyps = FApi.tc1_hyps tc in
+          let args =
+            List.map
+              (fun x ->
+                 let ty = EcEnv.LDecl.var_by_id x hyps in
+                 PAFormula (f_local x ty))
+              names in
+          EcLowGoal.t_exists_intro_s args tc in
+
+        let+ tc = EcLowGoal.t_symmetry tc in
+        let+ tc = EcLowGoal.t_apply_hyp e ~args:[] ~sk:0 tc in
+
+        t_id tc
+      in
 
-    let cop = EcPath.pqoname (EcPath.prefix indp) cname in
-    let cop = f_op cop tyinst (toarrow (List.snd ids) f.f_ty) in
-    let cop =
-      let args = List.map (curry f_local) lvars in
-      f_app cop args f.f_ty in
-    let cop = f_eq f cop in
+      let clean (tc : tcenv1) =
+        let pre = oget (EcLowPhlGoal.get_pre (FApi.tc1_goal tc)) in
+        let post = oget (EcLowPhlGoal.get_post (FApi.tc1_goal tc)) in
+        let eq, _, pre = destr_and3 pre in
+        let tc = EcPhlConseq.t_conseq (f_and eq pre) post tc in
 
-    f_forall
-      (List.map (snd_map gtty) lvars)
-      (f_hoareS_r
-         { (sets (stmt ((s_subst subst b).s_node @ tl.s_node)))
-             with hs_pr = f_and_simpl cop hs.hs_pr })
+        FApi.t_onall
+          (EcLowGoal.t_clears names)
+          (FApi.t_firsts (EcLowGoal.t_trivial ~keep:false) 2 tc)
+      in
 
-  in
+      tc
+        |> EcPhlRCond.t_rcond_match side cname (Zpr.cpos 1)
+        @+ [discharge; clean]
+    in
 
-  let concl = List.map do1 (List.combine bs indt.EcDecl.tydt_ctors) in
+    let tc = FApi.as_tcenv1 (EcPhlExists.t_hr_exists_intro [f] tc) in
+    let tc = FApi.as_tcenv1 (EcPhlExists.t_hr_exists_elim_r ~bound:1 tc) in
+    let tc = EcLowGoal.t_elimT_ind `Case tc in
 
-  FApi.xmutate1 tc `Match concl
+    FApi.t_onalli onsub tc
+end
 
 (* -------------------------------------------------------------------- *)
-let t_equiv_match s tc =
-  let hyps = FApi.tc1_hyps tc in
-  let env  = LDecl.toenv hyps in
-  let es   = tc1_as_equivS tc in
-
-  let me, st =
-    match s with
-    | `Left  -> es.es_ml, es.es_sl
-    | `Right -> es.es_mr, es.es_sr in
-
-  let sets st =
-    match s with
-    | `Left  -> { es with es_sl = st; }
-    | `Right -> { es with es_sr = st; } in
-
-  let (e, bs), tl = tc1_first_match tc st in
-  let indp, indt, tyinst = oget (EcEnv.Ty.get_top_decl e.e_ty env) in
-  let indt = oget (EcDecl.tydecl_as_datatype indt) in
-  let f = form_of_expr (EcMemory.memory me) e in
+let t_hoare_match (tc : tcenv1) : tcenv =
+  let _ : sHoareS = tc1_as_hoareS tc in
+  LowMatchInternal.t_gen_match None tc
 
-  let do1 ((ids, b), (cname, _)) =
-    let subst, lvars =
-      add_elocals Fsubst.f_subst_id ids in
-
-    let cop = EcPath.pqoname (EcPath.prefix indp) cname in
-    let cop = f_op cop tyinst (toarrow (List.snd ids) f.f_ty) in
-    let cop =
-      let args = List.map (curry f_local) lvars in
-      f_app cop args f.f_ty in
-    let cop = f_eq f cop in
-
-    f_forall
-      (List.map (snd_map gtty) lvars)
-      (f_equivS_r
-         { (sets (stmt ((s_subst subst b).s_node @ tl.s_node)))
-             with es_pr = f_and_simpl cop es.es_pr })
-
-  in
-
-  let concl = List.map do1 (List.combine bs indt.EcDecl.tydt_ctors) in
+(* -------------------------------------------------------------------- *)
+let t_bdhoare_match (tc : tcenv1) : tcenv =
+  let _ : bdHoareS = tc1_as_bdhoareS tc in
+  LowMatchInternal.t_gen_match None tc
 
-  FApi.xmutate1 tc (`Match s) concl
+(* -------------------------------------------------------------------- *)
+let t_equiv_match (s : side) (tc : tcenv1) : tcenv =
+  let _ : equivS = tc1_as_equivS tc in
+  LowMatchInternal.t_gen_match (Some s) tc
 
 (* -------------------------------------------------------------------- *)
 let t_equiv_match_same_constr tc =

src/phl/ecPhlCond.mli

@@ -9,5 +9,6 @@ val t_bdhoare_cond : backward
 val t_equiv_cond   : oside -> backward
 
 (* -------------------------------------------------------------------- *)
-val t_hoare_match : backward
-val t_equiv_match : matchmode -> backward
+val t_hoare_match   : backward
+val t_bdhoare_match : backward
+val t_equiv_match   : matchmode -> backward

src/phl/ecPhlExists.mli

@@ -4,8 +4,9 @@ open EcFol
 open EcCoreGoal.FApi
 
 (* -------------------------------------------------------------------- *)
-val t_hr_exists_elim  : backward
-val t_hr_exists_intro : form list -> backward
+val t_hr_exists_elim_r : ?bound:int -> backward
+val t_hr_exists_elim   : backward
+val t_hr_exists_intro  : form list -> backward
 
 (* -------------------------------------------------------------------- *)
 val process_exists_intro : elim:bool -> pformula list -> backward

src/phl/ecPhlHiCond.ml

@@ -37,4 +37,7 @@ let process_cond info tc =
 
 (* -------------------------------------------------------------------- *)
 let process_match infos tc =
-  t_hS_or_bhS_or_eS ~th:(t_hoare_match) ~te:(t_equiv_match infos) tc
+  t_hS_or_bhS_or_eS
+    ~th:t_hoare_match
+    ~tbh:t_bdhoare_match
+    ~te:(t_equiv_match infos) tc

src/phl/ecPhlLoopTx.ml

@@ -223,7 +223,7 @@ let process_unroll_for side cpos tc =
 
   let env  = FApi.tc1_env tc in
   let hyps = FApi.tc1_hyps tc in
-  let c    = EcLowPhlGoal.tc1_get_stmt side tc in
+  let _, c = EcLowPhlGoal.tc1_get_stmt side tc in
   let z    = Zpr.zipper_of_cpos cpos c in
   let pos  = 1 + List.length z.Zpr.z_head in
 

src/phl/ecPhlRewrite.ml

@@ -22,7 +22,7 @@ let t_change
 =
   let hyps, concl = FApi.tc1_flat tc in
 
-  let change (i : instr) =
+  let change (m : memenv) (i : instr) =
     let e, mk =
       EcUtils.ofdfl
         (fun () ->
@@ -32,7 +32,6 @@ let t_change
         (get_expression_of_instruction i)
     in
 
-    let m, _ = EcFol.destr_programS side concl in
     let data, e' = expr e (hyps, m) in
     let mid = EcMemory.memory m in
 
@@ -49,8 +48,8 @@ let t_change
       "conclusion should be a program logic \
       (hoare | ehoare | phoare | equiv)";
 
-  let s = EcLowPhlGoal.tc1_get_stmt side tc in
-  let (data, goals), s = EcMatching.Zipper.map pos change s in
+  let m, s = EcLowPhlGoal.tc1_get_stmt side tc in
+  let (data, goals), s = EcMatching.Zipper.map pos (change m) s in
   let concl = EcLowPhlGoal.hl_set_stmt side concl s in
 
   data, FApi.xmutate1 tc `ProcChange (goals @ [concl])