reduce when needed in proc and call rules (#849)

* reduce in t_hF_or_bhF_or_eF
* add reduction in call tactic

Author: bgregoir

src/ecLowGoal.ml

@@ -406,7 +406,8 @@ let t_hred_with_info ?target (ri : reduction_info) (tc : tcenv1) =
   FApi.tcenv_of_tcenv1 (t_change_r ~fail:true ?target action tc)
 
 (* -------------------------------------------------------------------- *)
-let rec t_lazy_match ?(reduce = `Full) (tx : form -> FApi.backward)
+let rec t_lazy_match ?(reduce = `Full) ?(texn = fun _ -> raise InvalidGoalShape)
+                    (tx : form -> FApi.backward)
   (tc : tcenv1) =
   let concl = FApi.tc1_goal tc in
   try tx concl tc
@@ -416,7 +417,7 @@ let rec t_lazy_match ?(reduce = `Full) (tx : form -> FApi.backward)
       | `None    -> raise InvalidGoalShape
       | `Full    -> EcReduction.full_red
       | `NoDelta -> EcReduction.nodelta in
-    FApi.t_seq (t_hred_with_info strategy) (t_lazy_match ~reduce tx) tc
+    FApi.t_seq (FApi.t_or (t_hred_with_info strategy) texn) (t_lazy_match ~reduce tx) tc
 
 (* -------------------------------------------------------------------- *)
 type smode = [ `Cbv | `Cbn ]
@@ -2598,8 +2599,8 @@ let t_solve ?(canfail = true) ?(bases = [EcEnv.Auto.dname]) ?(mode = fmdelta) ?(
     let pt = PT.pt_of_uglobal !!tc (FApi.tc1_hyps tc) p in
     try
       Apply.t_apply_bwd_r ~ri ~mode ~canview:false pt tc
-    with Apply.NoInstance _ -> 
-      t_fail tc 
+    with Apply.NoInstance _ ->
+      t_fail tc
   in
 
   let rec t_apply ctn ip tc =

src/ecLowGoal.mli

@@ -69,7 +69,7 @@ val t_change  : ?ri:EcReduction.reduction_info -> ?target:ident -> form -> FApi.
 
 (* -------------------------------------------------------------------- *)
 val t_lazy_match:
-  ?reduce:lazyred -> (form -> FApi.backward)-> FApi.backward
+  ?reduce:lazyred -> ?texn:EcCoreGoal.FApi.backward -> (form -> FApi.backward)-> FApi.backward
 
 (* -------------------------------------------------------------------- *)
 val t_reflex       : ?mode:[`Alpha | `Conv] -> ?reduce:lazyred -> FApi.backward
@@ -362,4 +362,4 @@ val pp_tc :tcenv -> unit
   [@@ocaml.alert debug "Debug function, remove uses before merging"]
 
 val pp_tc1 :tcenv1 -> unit
-  [@@ocaml.alert debug "Debug function, remove uses before merging"]
+  [@@ocaml.alert debug "Debug function, remove uses before merging"]

src/ecLowPhlGoal.ml

@@ -206,6 +206,27 @@ let tc1_get_stmt side tc =
   | _            ->
       tc_error_noXhl ~kinds:(hlkinds_Xhl_r `Stmt) !!tc
 
+(* ------------------------------------------------------------------ *)
+let tc1_process_codepos_range tc (side, cpr) =
+  let me, _ = tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active_ss me env in
+  EcTyping.trans_codepos_range env cpr
+
+(* ------------------------------------------------------------------ *)
+let tc1_process_codepos tc (side, cpos) =
+  let me, _ = tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active_ss me env in
+  EcTyping.trans_codepos env cpos
+
+(* ------------------------------------------------------------------ *)
+let tc1_process_codepos1 tc (side, cpos) =
+  let me, _ = tc1_get_stmt side tc in
+  let env = FApi.tc1_env tc in
+  let env = EcEnv.Memory.push_active_ss me env in
+  EcTyping.trans_codepos1 env cpos
+
 (* -------------------------------------------------------------------- *)
 let hl_set_stmt (side : side option) (f : form) (s : stmt) =
   match side, f.f_node with
@@ -256,28 +277,28 @@ let tc1_get_post tc =
 (* -------------------------------------------------------------------- *)
 let set_pre ~pre f =
   match f.f_node, pre with
- | FhoareF hf, Inv_ss pre   -> 
+ | FhoareF hf, Inv_ss pre   ->
     let pre = ss_inv_rebind pre hf.hf_m in
     f_hoareF pre hf.hf_f (hf_po hf)
- | FhoareS hs, Inv_ss pre   -> 
+ | FhoareS hs, Inv_ss pre   ->
     let pre = ss_inv_rebind pre (fst hs.hs_m) in
     f_hoareS (snd hs.hs_m) pre hs.hs_s (hs_po hs)
- | FeHoareF hf, Inv_ss pre  -> 
+ | FeHoareF hf, Inv_ss pre  ->
     let pre = ss_inv_rebind pre hf.ehf_m in
     f_eHoareF pre hf.ehf_f (ehf_po hf)
- | FeHoareS hs, Inv_ss pre  -> 
+ | FeHoareS hs, Inv_ss pre  ->
     let pre = ss_inv_rebind pre (fst hs.ehs_m) in
     f_eHoareS (snd hs.ehs_m) pre hs.ehs_s (ehs_po hs)
  | FbdHoareF hf, Inv_ss pre ->
     let pre = ss_inv_rebind pre hf.bhf_m in
     f_bdHoareF pre hf.bhf_f (bhf_po hf) hf.bhf_cmp (bhf_bd hf)
- | FbdHoareS hs, Inv_ss pre -> 
+ | FbdHoareS hs, Inv_ss pre ->
     let pre = ss_inv_rebind pre (fst hs.bhs_m) in
     f_bdHoareS (snd hs.bhs_m) pre hs.bhs_s (bhs_po hs) hs.bhs_cmp (bhs_bd hs)
- | FequivF ef, Inv_ts pre   -> 
+ | FequivF ef, Inv_ts pre   ->
     let pre = ts_inv_rebind pre ef.ef_ml ef.ef_mr in
     f_equivF pre ef.ef_fl ef.ef_fr (ef_po ef)
- | FequivS es, Inv_ts pre   -> 
+ | FequivS es, Inv_ts pre   ->
     let pre = ts_inv_rebind pre (fst es.es_ml) (fst es.es_mr) in
     f_equivS (snd es.es_ml) (snd es.es_mr) pre es.es_sl es.es_sr (es_po es)
  | _            -> assert false
@@ -307,33 +328,33 @@ let t_hS_or_bhS_or_eS ?th ?teh ?tbh ?te tc =
   | FeHoareS  _ when EcUtils.is_some teh -> (oget teh) tc
   | FbdHoareS _ when EcUtils.is_some tbh -> (oget tbh) tc
   | FequivS   _ when EcUtils.is_some te  -> (oget te ) tc
-
   | _ ->
     let kinds = List.flatten [
-         if EcUtils.is_some th  then [`Hoare  `Stmt] else [];
-         if EcUtils.is_some teh then [`EHoare `Stmt] else [];
-         if EcUtils.is_some tbh then [`PHoare `Stmt] else [];
-         if EcUtils.is_some te  then [`Equiv  `Stmt] else []]
-
+       if EcUtils.is_some th  then [`Hoare  `Stmt] else [];
+       if EcUtils.is_some teh then [`EHoare `Stmt] else [];
+       if EcUtils.is_some tbh then [`PHoare `Stmt] else [];
+       if EcUtils.is_some te  then [`Equiv  `Stmt] else []]
     in tc_error_noXhl ~kinds !!tc
 
 let t_hF_or_bhF_or_eF ?th ?teh ?tbh ?te ?teg tc =
-  match (FApi.tc1_goal tc).f_node with
-  | FhoareF  _ when EcUtils.is_some th  -> (oget th ) tc
-  | FeHoareF  _ when EcUtils.is_some teh -> (oget teh) tc
-  | FbdHoareF _ when EcUtils.is_some tbh -> (oget tbh) tc
-  | FequivF   _ when EcUtils.is_some te  -> (oget te ) tc
-  | FeagerF   _ when EcUtils.is_some teg -> (oget teg) tc
-
-  | _ ->
+  let texn tc =
     let kinds = List.flatten [
          if EcUtils.is_some th  then [`Hoare  `Pred] else [];
          if EcUtils.is_some teh then [`EHoare `Pred] else [];
          if EcUtils.is_some tbh then [`PHoare `Pred] else [];
          if EcUtils.is_some te  then [`Equiv  `Pred] else [];
          if EcUtils.is_some teg then [`Eager       ] else []]
+    in tc_error_noXhl ~kinds !!tc in
+  let tx f tc =
+    match f.f_node with
+    | FhoareF  _ when EcUtils.is_some th  -> (oget th ) tc
+    | FeHoareF  _ when EcUtils.is_some teh -> (oget teh) tc
+    | FbdHoareF _ when EcUtils.is_some tbh -> (oget tbh) tc
+    | FequivF   _ when EcUtils.is_some te  -> (oget te ) tc
+    | FeagerF   _ when EcUtils.is_some teg -> (oget teg) tc
+    | _ -> raise EcProofTyping.NoMatch in
+  EcLowGoal.t_lazy_match ~texn tx tc
 
-    in tc_error_noXhl ~kinds !!tc
 
 (* -------------------------------------------------------------------- *)
 let tag_sym_with_side ?mc name m =
@@ -672,7 +693,7 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
           let pr, po = bhs_pr bhs, bhs_po bhs in
           let (me, stmt, cs) =
             tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in
-          let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs) 
+          let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs)
                       bhs.bhs_cmp (bhs_bd bhs) in
           FApi.xmutate1 tc (tr None) (cs @ [concl])
 

src/ecProofTyping.ml

@@ -132,7 +132,7 @@ let tc1_process_stmt ?map hyps tc c =
 
 let tc1_process_prhl_stmt ?map tc side c =
   let concl = FApi.tc1_goal tc in
-  let ml, mr = match concl.f_node with 
+  let ml, mr = match concl.f_node with
     | FequivS {es_ml=ml; es_mr=mr} -> (ml, mr)
     | FeagerF {eg_ml=ml; eg_mr=mr} ->
         EcMemory.abstract ml, EcMemory.abstract mr
@@ -188,27 +188,6 @@ let tc1_process_Xhl_formula ?side tc pf =
 let tc1_process_Xhl_formula_xreal tc pf =
   tc1_process_Xhl_form tc txreal pf
 
-(* ------------------------------------------------------------------ *)
-let tc1_process_codepos_range tc (side, cpr) =
-  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
-  let env = FApi.tc1_env tc in
-  let env = EcEnv.Memory.push_active_ss me env in
-  EcTyping.trans_codepos_range env cpr
-
-(* ------------------------------------------------------------------ *)
-let tc1_process_codepos tc (side, cpos) =
-  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
-  let env = FApi.tc1_env tc in
-  let env = EcEnv.Memory.push_active_ss me env in
-  EcTyping.trans_codepos env cpos
-
-(* ------------------------------------------------------------------ *)
-let tc1_process_codepos1 tc (side, cpos) =
-  let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
-  let env = FApi.tc1_env tc in
-  let env = EcEnv.Memory.push_active_ss me env in
-  EcTyping.trans_codepos1 env cpos
-
 (* ------------------------------------------------------------------ *)
 (* FIXME: factor out to typing module                                 *)
 (* FIXME: TC HOOK - check parameter constraints                       *)

src/ecProofTyping.mli

@@ -4,7 +4,6 @@ open EcIdent
 open EcDecl
 open EcEnv
 open EcCoreGoal
-open EcMatching.Position
 open EcAst
 
 (* -------------------------------------------------------------------- *)
@@ -59,10 +58,6 @@ val tc1_process_prhl_stmt :
 val tc1_process_Xhl_stmt :
      ?map:EcTyping.ismap -> tcenv1 -> pstmt -> stmt
 
-val tc1_process_codepos_range : tcenv1 -> oside * pcodepos_range -> codepos_range
-val tc1_process_codepos : tcenv1 -> oside * pcodepos -> codepos
-val tc1_process_codepos1 : tcenv1 -> oside * pcodepos1 -> codepos1
-
 (* -------------------------------------------------------------------- *)
 exception NoMatch
 

src/ecReduction.ml

@@ -1258,23 +1258,23 @@ let rec simplify ri env f =
   match f.f_node with
   | FhoareF hf when ri.ri.modpath ->
       let hf_f = EcEnv.NormMp.norm_xfun env hf.hf_f in
-      f_map (fun ty -> ty) (simplify ri env) 
+      f_map (fun ty -> ty) (simplify ri env)
       (f_hoareF (hf_pr hf) hf_f (hf_po hf))
 
   | FeHoareF hf when ri.ri.modpath ->
       let ehf_f = EcEnv.NormMp.norm_xfun env hf.ehf_f in
-      f_map (fun ty -> ty) (simplify ri env) 
+      f_map (fun ty -> ty) (simplify ri env)
       (f_eHoareF (ehf_pr hf) ehf_f (ehf_po hf))
 
   | FbdHoareF hf when ri.ri.modpath ->
       let bhf_f = EcEnv.NormMp.norm_xfun env hf.bhf_f in
-      f_map (fun ty -> ty) (simplify ri env) 
+      f_map (fun ty -> ty) (simplify ri env)
       (f_bdHoareF (bhf_pr hf) bhf_f (bhf_po hf) hf.bhf_cmp (bhf_bd hf))
 
   | FequivF ef when ri.ri.modpath ->
       let ef_fl = EcEnv.NormMp.norm_xfun env ef.ef_fl in
       let ef_fr = EcEnv.NormMp.norm_xfun env ef.ef_fr in
-      f_map (fun ty -> ty) (simplify ri env) 
+      f_map (fun ty -> ty) (simplify ri env)
       (f_equivF (ef_pr ef) ef_fl ef_fr (ef_po ef))
 
   | FeagerF eg when ri.ri.modpath ->
@@ -1666,6 +1666,12 @@ let h_red_opt ri hyps f =
   try Some (h_red ri hyps f)
   with NotReducible -> None
 
+let rec h_red_until ?(until = fun _ -> false) ri hyps f =
+  if until f then f
+  else match h_red ri hyps f with
+  | f -> h_red_until ~until ri hyps f
+  | exception NotReducible -> f
+
 (* -------------------------------------------------------------------- *)
 type xconv = [`Eq | `AlphaEq | `Conv]
 

src/ecReduction.mli

@@ -88,6 +88,14 @@ val reduce_logic : reduction_info -> env -> LDecl.hyps -> form -> form
 val h_red_opt : reduction_info -> LDecl.hyps -> form -> form option
 val h_red     : reduction_info -> LDecl.hyps -> form -> form
 
+(* [hred_until ~until ri hyps f] performs head reduction on [f]
+   until [test f] is true or that no more head reduction is possible.
+   If no [until] argument is provided then head reduction is performed
+   until it is possible.
+*)
+val h_red_until :
+  ?until:(form -> bool) -> reduction_info -> LDecl.hyps -> form -> form
+
 val reduce_user_gen :
   (EcFol.form -> EcFol.form) ->
   reduction_info ->
@@ -109,4 +117,4 @@ type xconv = [`Eq | `AlphaEq | `Conv]
 val xconv : xconv -> LDecl.hyps -> form -> form -> bool
 
 val ss_inv_alpha_eq : LDecl.hyps -> ss_inv -> ss_inv -> bool
-val ts_inv_alpha_eq : LDecl.hyps -> ts_inv -> ts_inv -> bool
+val ts_inv_alpha_eq : LDecl.hyps -> ts_inv -> ts_inv -> bool

src/phl/ecPhlApp.ml

@@ -67,7 +67,7 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
   let (ir1, ir2) = EcIdent.create "r", EcIdent.create "r" in
   let (r1 , r2 ) = f_local ir1 treal, f_local ir2 treal in
   let condnm =
-    let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2) 
+    let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2)
                                 (map_ss_inv1 ((EcUtils.flip f_eq) r2) g2) in
     f_forall
       [(ir1, GTty treal); (ir2, GTty treal)]
@@ -124,11 +124,11 @@ let t_equiv_app_onesided side i pre post tc =
   let (ml, mr) = fst es.es_ml, fst es.es_mr in
   let s, s', p', q' =
     match side with
-    | `Left  -> 
+    | `Left  ->
       let p' = ss_inv_generalize_right (EcSubst.ss_inv_rebind pre ml) mr in
       let q' = ss_inv_generalize_right (EcSubst.ss_inv_rebind post ml) mr in
       es.es_sl, es.es_sr, p', q'
-    | `Right -> 
+    | `Right ->
       let p' = ss_inv_generalize_left (EcSubst.ss_inv_rebind pre mr) ml in
       let q' = ss_inv_generalize_left (EcSubst.ss_inv_rebind post mr) ml in
       es.es_sr, es.es_sl, p', q'
@@ -227,13 +227,13 @@ let process_app (side, dir, k, phi, bd_info) tc =
   | Single i, PAppNone when is_hoareS concl ->
     check_side side;
     let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
-    let i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
+    let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in
     t_hoare_app i phi tc
 
   | Single i, PAppNone when is_eHoareS concl ->
     check_side side;
     let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in
-    let i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
+    let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in
     t_ehoare_app i phi tc
 
   | Single i, PAppNone when is_equivS concl ->
@@ -248,21 +248,21 @@ let process_app (side, dir, k, phi, bd_info) tc =
       match side with
       | None -> tc_error !!tc "seq onsided: side information expected"
       | Some side -> side in
-    let i = EcProofTyping.tc1_process_codepos1 tc (Some side, i) in
+    let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some side, i) in
     t_equiv_app_onesided side i pre post tc
 
   | Single i, _ when is_bdHoareS concl ->
       check_side side;
       let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in
       let (ra, f1, f2, f3, f4) = process_phl_bd_info dir bd_info tc in
-      let i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
+      let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in
       t_bdhoare_app i (ra, pia, f1, f2, f3, f4) tc
 
   | Double (i, j), PAppNone when is_equivS concl ->
       check_side side;
       let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in
-      let i = EcProofTyping.tc1_process_codepos1 tc (Some `Left, i) in
-      let j = EcProofTyping.tc1_process_codepos1 tc (Some `Left, j) in
+      let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, i) in
+      let j = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, j) in
       t_equiv_app (i, j) phi tc
 
   | Single _, PAppNone