From db72bf79423fc17a3eecdfd559736bb887936cc6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 23 Apr 2019 18:39:13 +0200
Subject: Code factorization in conversion tactics.

---
 tactics/tactics.ml  | 121 ++++++++++++++++++----------------------------------
 tactics/tactics.mli |   4 +-
 2 files changed, 43 insertions(+), 82 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 60027b06e8..af7db6f79b 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -614,18 +614,22 @@ let cofix id = mutual_cofix id [] 0
 type tactic_reduction = Reductionops.reduction_function
 type e_tactic_reduction = Reductionops.e_reduction_function
 
-let pf_reduce_decl redfun where decl gl =
+let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
   let open Context.Named.Declaration in
-  let redfun' c = Tacmach.New.pf_apply redfun gl c in
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
         user_err  (Id.print id.binder_name ++ str " has no value.");
-      LocalAssum (id,redfun' ty)
+    let (sigma, ty') = redfun false env sigma ty in
+    (sigma, LocalAssum (id, ty'))
   | LocalDef (id,b,ty) ->
-      let b' = if where != InHypTypeOnly then redfun' b else b in
-      let ty' =	if where != InHypValueOnly then redfun' ty else ty in
-      LocalDef (id,b',ty')
+      let (sigma, b') =
+        if where != InHypTypeOnly then redfun true env sigma b else (sigma, b)
+      in
+      let (sigma, ty') =
+        if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty)
+      in
+      (sigma, LocalDef (id,b',ty'))
 
 (* Possibly equip a reduction with the occurrences mentioned in an
    occurrence clause *)
@@ -695,41 +699,9 @@ let bind_red_expr_occurrences occs nbcl redexp =
    reduction function either to the conclusion or to a
    certain hypothesis *)
 
-let reduct_in_concl (redfun,sty) =
-  Proofview.Goal.enter begin fun gl ->
-    convert_concl ~check:false (Tacmach.New.pf_apply redfun gl (Tacmach.New.pf_concl gl)) sty
-  end
-
-let reduct_in_hyp ?(check=false) redfun (id,where) =
-  Proofview.Goal.enter begin fun gl ->
-  convert_hyp ~check (pf_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl)
-  end
-
-let revert_cast (redfun,kind as r) =
-  if kind == DEFAULTcast then (redfun,REVERTcast) else r
-
-let reduct_option ?(check=false) redfun = function
-  | Some id -> reduct_in_hyp ~check (fst redfun) id
-  | None    -> reduct_in_concl (revert_cast redfun)
-
 (** Tactic reduction modulo evars (for universes essentially) *)
 
-let pf_e_reduce_decl redfun where decl gl =
-  let open Context.Named.Declaration in
-  let sigma = Proofview.Goal.sigma gl in
-  let redfun sigma c = redfun (Tacmach.New.pf_env gl) sigma c in
-  match decl with
-  | LocalAssum (id,ty) ->
-      if where == InHypValueOnly then
-        user_err  (Id.print id.binder_name ++ str " has no value.");
-    let (sigma, ty') = redfun sigma ty in
-    (sigma, LocalAssum (id, ty'))
-  | LocalDef (id,b,ty) ->
-      let (sigma, b') = if where != InHypTypeOnly then redfun sigma b else (sigma, b) in
-      let (sigma, ty') = if where != InHypValueOnly then redfun sigma ty else (sigma, ty) in
-      (sigma, LocalDef (id, b', ty'))
-
-let e_reduct_in_concl ~check (redfun, sty) =
+let e_change_in_concl ?(check = false) (redfun, sty) =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let (sigma, c') = redfun (Tacmach.New.pf_env gl) sigma (Tacmach.New.pf_concl gl) in
@@ -737,53 +709,39 @@ let e_reduct_in_concl ~check (redfun, sty) =
     (convert_concl ~check c' sty)
   end
 
-let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+let e_change_in_hyp ?(check = false) redfun (id,where) =
   Proofview.Goal.enter begin fun gl ->
-    let (sigma, decl') = pf_e_reduce_decl redfun where (Tacmach.New.pf_get_hyp id gl) gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let hyp = Tacmach.New.pf_get_hyp id gl in
+    let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_hyp ~check decl')
+    (convert_hyp ~check c)
   end
 
-let e_reduct_option ?(check=false) redfun = function
-  | Some id -> e_reduct_in_hyp ~check (fst redfun) id
-  | None    -> e_reduct_in_concl ~check (revert_cast redfun)
+let e_reduct_in_concl = e_change_in_concl
 
-(** Versions with evars to maintain the unification of universes resulting
-    from conversions. *)
+let reduct_in_concl ?(check = false) (redfun, sty) =
+  let redfun env sigma c = (sigma, redfun env sigma c) in
+  e_change_in_concl ~check (redfun, sty)
 
-let e_change_in_concl (redfun,sty) =
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let (sigma, c) = redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_concl ~check:false c sty)
-  end
+let e_reduct_in_hyp ?(check=false) redfun (id, where) =
+  let redfun _ env sigma c = redfun env sigma c in
+  e_change_in_hyp ~check redfun (id, where)
 
-let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigma =
-  let open Context.Named.Declaration in
-  match decl with
-  | LocalAssum (id,ty) ->
-      if where == InHypValueOnly then
-        user_err  (Id.print id.binder_name ++ str " has no value.");
-    let (sigma, ty') = redfun false env sigma ty in
-    (sigma, LocalAssum (id, ty'))
-  | LocalDef (id,b,ty) ->
-      let (sigma, b') =
-	if where != InHypTypeOnly then redfun true env sigma b else (sigma, b)
-      in
-      let (sigma, ty') =
-	if where != InHypValueOnly then redfun false env sigma ty else (sigma, ty)
-      in
-      (sigma, LocalDef (id,b',ty'))
+let reduct_in_hyp ?(check = false) redfun (id, where) =
+  let redfun _ env sigma c = (sigma, redfun env sigma c) in
+  e_change_in_hyp ~check redfun (id, where)
 
-let e_change_in_hyp redfun (id,where) =
-  Proofview.Goal.enter begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let hyp = Tacmach.New.pf_get_hyp id gl in
-    let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (convert_hyp c)
-  end
+let revert_cast (redfun,kind as r) =
+  if kind == DEFAULTcast then (redfun,REVERTcast) else r
+
+let e_reduct_option ?(check=false) redfun = function
+  | Some id -> e_reduct_in_hyp ~check (fst redfun) id
+  | None    -> e_change_in_concl ~check (revert_cast redfun)
+
+let reduct_option ?(check = false) (redfun, sty) where =
+  let redfun env sigma c = (sigma, redfun env sigma c) in
+  e_reduct_option ~check (redfun, sty) where
 
 type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr
 
@@ -837,10 +795,13 @@ let change_on_subterm cv_pb deep t where env sigma c =
   (sigma, c)
 
 let change_in_concl occl t =
-  e_change_in_concl ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
+  e_change_in_concl ~check:false ((change_on_subterm Reduction.CUMUL false t occl),DEFAULTcast)
 
 let change_in_hyp occl t id  =
-  e_change_in_hyp (fun x -> change_on_subterm Reduction.CONV x t occl) id
+  (* FIXME: we set the [check] flag only to reorder hypotheses in case of
+    introduction of dependencies in new variables. We should separate this
+    check from the conversion function. *)
+  e_change_in_hyp ~check:true (fun x -> change_on_subterm Reduction.CONV x t occl) id
 
 let change_option occl t = function
   | Some id -> change_in_hyp occl t id
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index e545ec9b5f..e7b95a820e 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -154,8 +154,8 @@ type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
 val make_change_arg   : constr -> change_arg
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
 val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> unit Proofview.tactic
-val reduct_in_concl   : tactic_reduction * cast_kind -> unit Proofview.tactic
-val e_reduct_in_concl   : check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
+val reduct_in_concl   : ?check:bool -> tactic_reduction * cast_kind -> unit Proofview.tactic
+val e_reduct_in_concl   : ?check:bool -> e_tactic_reduction * cast_kind -> unit Proofview.tactic
 val change_in_concl   : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic
 val change_concl      : constr -> unit Proofview.tactic
 val change_in_hyp     : (occurrences * constr_pattern) option -> change_arg ->
-- 
cgit v1.2.3