Merge PR #12943: Move Elim-specific code

Ack-by: SkySkimmer
Reviewed-by: herbelin

6 files changed, 134 insertions, 187 deletions

diff --git a/tactics/elim.ml b/tactics/elim.ml
index 274ebc9f60..852ad626e1 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -10,33 +10,145 @@
 
 open Util
 open Names
+open Constr
 open Termops
 open EConstr
 open Inductiveops
 open Hipattern
 open Tacmach.New
 open Tacticals.New
+open Clenv
 open Tactics
 open Proofview.Notations
 
+type branch_args = {
+  ity        : pinductive;   (* the type we were eliminating on *)
+  branchnum  : int;         (* the branch number *)
+  nassums    : int;         (* number of assumptions/letin to be introduced *)
+  branchsign : bool list;   (* the signature of the branch.
+                               true=assumption, false=let-in *)
+  branchnames : Tactypes.intro_patterns}
+
 module NamedDecl = Context.Named.Declaration
 
+(* Find the right elimination suffix corresponding to the sort of the goal *)
+(* c should be of type A1->.. An->B with B an inductive definition *)
+let general_elim_then_using mk_elim
+    rec_flag allnames tac predicate ind (c, t) =
+  let open Pp in
+  Proofview.Goal.enter begin fun gl ->
+  let sigma, elim = mk_elim ind gl in
+  let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
+  Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+  (Proofview.Goal.enter begin fun gl ->
+  let indclause = mk_clenv_from gl (c, t) in
+  (* applying elimination_scheme just a little modified *)
+  let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim)  in
+  let indmv =
+    match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
+    | Meta mv -> mv
+    | _         -> CErrors.anomaly (str"elimination.")
+  in
+  let pmv =
+    let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
+    match EConstr.kind elimclause.evd p with
+    | Meta p -> p
+    | _ ->
+        let name_elim =
+          match EConstr.kind sigma elim with
+          | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
+          | _ -> mt ()
+        in
+        CErrors.user_err ~hdr:"Tacticals.general_elim_then_using"
+          (str "The elimination combinator " ++ name_elim ++ str " is unknown.")
+  in
+  let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
+  let branchsigns = Tacticals.compute_constructor_signatures ~rec_flag ind in
+  let brnames = Tacticals.compute_induction_names false branchsigns allnames in
+  let flags = Unification.elim_flags () in
+  let elimclause' =
+    match predicate with
+    | None   -> elimclause'
+    | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
+  in
+  let after_tac i =
+    let ba = { branchsign = branchsigns.(i);
+                branchnames = brnames.(i);
+                nassums = List.length branchsigns.(i);
+                branchnum = i+1;
+                ity = ind; }
+    in
+    tac ba
+  in
+  let branchtacs = List.init (Array.length branchsigns) after_tac in
+  Proofview.tclTHEN
+    (Clenv.res_pf ~flags elimclause')
+    (Proofview.tclEXTEND [] tclIDTAC branchtacs)
+  end) end
+
+(* computing the case/elim combinators *)
+
+let gl_make_elim ind = begin fun gl ->
+  let env = Proofview.Goal.env gl in
+  let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in
+  let (sigma, c) = pf_apply Evd.fresh_global gl gr in
+  (sigma, c)
+end
+
+let gl_make_case dep (ind, u) = begin fun gl ->
+  let sigma = project gl in
+  let u = EInstance.kind (project gl) u in
+  let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) dep
+    (elimination_sort_of_goal gl)
+  in
+  (sigma, EConstr.of_constr r)
+end
+
+let make_elim_branch_assumptions ba hyps =
+  let assums =
+    try List.rev (List.firstn ba.nassums hyps)
+    with Failure _ -> CErrors.anomaly (Pp.str "make_elim_branch_assumptions.") in
+  assums
+
+let elim_on_ba tac ba =
+  Proofview.Goal.enter begin fun gl ->
+  let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
+  tac branches
+  end
+
+let elimination_then tac c =
+  let open Declarations in
+  Proofview.Goal.enter begin fun gl ->
+  let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in
+  let isrec,mkelim =
+    match (Global.lookup_mind (fst (fst ind))).mind_record with
+    | NotRecord -> true,gl_make_elim
+    | FakeRecord | PrimRecord _ -> false,gl_make_case true
+  in
+  general_elim_then_using mkelim isrec None tac None ind (c, t)
+  end
+
 (* Supposed to be called without as clause *)
 let introElimAssumsThen tac ba =
-  assert (ba.Tacticals.branchnames == []);
-  let introElimAssums = tclDO ba.Tacticals.nassums intro in
+  assert (ba.branchnames == []);
+  let introElimAssums = tclDO ba.nassums intro in
   (tclTHEN introElimAssums (elim_on_ba tac ba))
 
 (* Supposed to be called with a non-recursive scheme *)
 let introCaseAssumsThen with_evars tac ba =
-  let n1 = List.length ba.Tacticals.branchsign in
-  let n2 = List.length ba.Tacticals.branchnames in
+  let n1 = List.length ba.branchsign in
+  let n2 = List.length ba.branchnames in
   let (l1,l2),l3 =
-    if n1 < n2 then List.chop n1 ba.Tacticals.branchnames, []
-    else (ba.Tacticals.branchnames, []), List.make (n1-n2) false in
+    if n1 < n2 then List.chop n1 ba.branchnames, []
+    else (ba.branchnames, []), List.make (n1-n2) false in
   let introCaseAssums =
     tclTHEN (intro_patterns with_evars l1) (intros_clearing l3) in
-  (tclTHEN introCaseAssums (case_on_ba (tac l2) ba))
+  (tclTHEN introCaseAssums (elim_on_ba (tac l2) ba))
+
+let case_tac dep names tac elim ind c =
+  let mkcase = gl_make_case dep in
+  let tac = introCaseAssumsThen false (* ApplyOn not supported by inversion *) tac in
+  general_elim_then_using mkcase false names tac (Some elim) ind c
 
 (* The following tactic Decompose repeatedly applies the
    elimination(s) rule(s) of the types satisfying the predicate
@@ -68,7 +180,7 @@ and general_decompose_aux recognizer id =
        (fun bas ->
           tclTHEN (clear [id])
             (tclMAP (general_decompose_on_hyp recognizer)
-               (ids_of_named_context bas.Tacticals.assums))))
+               (ids_of_named_context bas))))
     id
 
 (* We should add a COMPLETE to be sure that the created hypothesis
@@ -136,7 +248,7 @@ let induction_trailer abs_i abs_j bargs =
           let idty = pf_get_type_of gl (mkVar id) in
           let fvty = global_vars (pf_env gl) (project gl) idty in
           let possible_bring_hyps =
-            (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
+            (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs
           in
           let (hyps,_) =
             List.fold_left
diff --git a/tactics/elim.mli b/tactics/elim.mli
index e89855a050..4c5cdc8a31 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -10,14 +10,13 @@
 
 open Names
 open EConstr
-open Tacticals
 open Tactypes
 
 (** Eliminations tactics. *)
 
-val introCaseAssumsThen : Tactics.evars_flag ->
-  (intro_patterns -> branch_assumptions -> unit Proofview.tactic) ->
-    branch_args -> unit Proofview.tactic
+val case_tac : bool -> or_and_intro_pattern option ->
+  (intro_patterns -> named_context -> unit Proofview.tactic) ->
+  constr -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
 
 val h_decompose       : inductive list -> constr -> unit Proofview.tactic
 val h_decompose_or    : constr -> unit Proofview.tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 4b94dd0e72..f77b52b931 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -409,7 +409,7 @@ let nLastDecls i tac =
 
 let rewrite_equations as_mode othin neqns names ba =
   Proofview.Goal.enter begin fun gl ->
-  let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
+  let (depids,nodepids) = split_dep_and_nodep ba gl in
   let first_eq = ref Logic.MoveLast in
   let avoid = if as_mode then Id.Set.of_list (List.map NamedDecl.get_id nodepids) else Id.Set.empty in
   match othin with
@@ -474,13 +474,12 @@ let raw_inversion inv_kind id status names =
     let (elim_predicate, args) =
       make_inv_predicate env evdref indf realargs id status concl in
     let sigma = !evdref in
-    let (cut_concl,case_tac) =
-      if status != NoDep && (local_occur_var sigma id concl) then
-        Reductionops.beta_applist sigma (elim_predicate, realargs@[c]),
-        case_then_using
+    let dep = status != NoDep && (local_occur_var sigma id concl) in
+    let cut_concl =
+      if dep then
+        Reductionops.beta_applist sigma (elim_predicate, realargs@[c])
       else
-        Reductionops.beta_applist sigma (elim_predicate, realargs),
-        case_nodep_then_using
+        Reductionops.beta_applist sigma (elim_predicate, realargs)
     in
     let refined id =
       let prf = mkApp (mkVar id, args) in
@@ -491,10 +490,7 @@ let raw_inversion inv_kind id status names =
     tclTHEN (Proofview.Unsafe.tclEVARS sigma)
       (tclTHENS
         (assert_before Anonymous cut_concl)
-        [case_tac names
-            (introCaseAssumsThen false (* ApplyOn not supported by inversion *)
-               (rewrite_equations_tac as_mode inv_kind id neqns))
-            (Some elim_predicate) ind (c,t);
+        [case_tac dep names (rewrite_equations_tac as_mode inv_kind id neqns) elim_predicate ind (c,t);
         onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
   end
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ec770e2473..fc099f643d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -14,10 +14,8 @@ open Util
 open Names
 open Constr
 open EConstr
-open Termops
 open Declarations
 open Tacmach
-open Clenv
 open Tactypes
 
 module RelDecl = Context.Rel.Declaration
@@ -335,18 +333,6 @@ let ifOnHyp pred tac1 tac2 id gl =
   used to keep track of some information about the ``branches'' of
   the elimination. *)
 
-type branch_args = {
-  ity        : pinductive;   (* the type we were eliminating on *)
-  branchnum  : int;         (* the branch number *)
-  nassums    : int;         (* number of assumptions/letin to be introduced *)
-  branchsign : bool list;   (* the signature of the branch.
-                               true=assumption, false=let-in *)
-  branchnames : intro_patterns}
-
-type branch_assumptions = {
-  ba        : branch_args;       (* the branch args *)
-  assums    : named_context}   (* the list of assumptions introduced *)
-
 let fix_empty_or_and_pattern nv l =
   (* 1- The syntax does not distinguish between "[ ]" for one clause with no
      names and "[ ]" for no clause at all *)
@@ -401,15 +387,13 @@ let get_and_check_or_and_pattern_gen ?loc check_and names branchsigns =
 
 let get_and_check_or_and_pattern ?loc = get_and_check_or_and_pattern_gen ?loc true
 
-let compute_induction_names_gen check_and branchletsigns = function
+let compute_induction_names check_and branchletsigns = function
   | None ->
       Array.make (Array.length branchletsigns) []
   | Some {CAst.loc;v=names} ->
       let names = fix_empty_or_and_pattern (Array.length branchletsigns) names in
       get_and_check_or_and_pattern_gen check_and ?loc names branchletsigns
 
-let compute_induction_names = compute_induction_names_gen true
-
 (* Compute the let-in signature of case analysis or standard induction scheme *)
 let compute_constructor_signatures ~rec_flag ((_,k as ity),u) =
   let rec analrec c recargs =
@@ -844,60 +828,6 @@ module New = struct
     tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
     end
 
-  (* Find the right elimination suffix corresponding to the sort of the goal *)
-  (* c should be of type A1->.. An->B with B an inductive definition *)
-  let general_elim_then_using mk_elim
-      rec_flag allnames tac predicate ind (c, t) =
-    Proofview.Goal.enter begin fun gl ->
-    let sigma, elim = mk_elim ind gl in
-    let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
-    Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (Proofview.Goal.enter begin fun gl ->
-    let indclause = mk_clenv_from gl (c, t) in
-    (* applying elimination_scheme just a little modified *)
-    let elimclause = mk_clenv_from gl (elim,Tacmach.New.pf_get_type_of gl elim)  in
-    let indmv =
-      match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with
-      | Meta mv -> mv
-      | _         -> anomaly (str"elimination.")
-    in
-    let pmv =
-      let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in
-      match EConstr.kind elimclause.evd p with
-      | Meta p -> p
-      | _ ->
-          let name_elim =
-            match EConstr.kind sigma elim with
-            | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim
-            | _ -> mt ()
-          in
-          user_err ~hdr:"Tacticals.general_elim_then_using"
-            (str "The elimination combinator " ++ name_elim ++ str " is unknown.")
-    in
-    let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
-    let branchsigns = compute_constructor_signatures ~rec_flag ind in
-    let brnames = compute_induction_names_gen false branchsigns allnames in
-    let flags = Unification.elim_flags () in
-    let elimclause' =
-      match predicate with
-      | None   -> elimclause'
-      | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
-    in
-    let after_tac i =
-      let ba = { branchsign = branchsigns.(i);
-                 branchnames = brnames.(i);
-                 nassums = List.length branchsigns.(i);
-                 branchnum = i+1;
-                 ity = ind; }
-      in
-      tac ba
-    in
-    let branchtacs = List.init (Array.length branchsigns) after_tac in
-    Proofview.tclTHEN
-      (Clenv.res_pf ~flags elimclause')
-      (Proofview.tclEXTEND [] tclIDTAC branchtacs)
-    end) end
-
   let elimination_sort_of_goal gl =
     (* Retyping will expand evars anyway. *)
     let c = Proofview.Goal.concl gl in
@@ -912,68 +842,6 @@ module New = struct
   | None -> elimination_sort_of_goal gl
   | Some id -> elimination_sort_of_hyp id gl
 
-  (* computing the case/elim combinators *)
-
-  let gl_make_elim ind = begin fun gl ->
-    let env = Proofview.Goal.env gl in
-    let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in
-    let (sigma, c) = pf_apply Evd.fresh_global gl gr in
-    (sigma, c)
-  end
-
-  let gl_make_case_dep (ind, u) = begin fun gl ->
-    let sigma = project gl in
-    let u = EInstance.kind (project gl) u in
-    let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) true
-      (elimination_sort_of_goal gl)
-    in
-    (sigma, EConstr.of_constr r)
-  end
-
-  let gl_make_case_nodep (ind, u) = begin fun gl ->
-    let sigma = project gl in
-    let u = EInstance.kind sigma u in
-    let (sigma, r) = Indrec.build_case_analysis_scheme (pf_env gl) sigma (ind, u) false
-      (elimination_sort_of_goal gl)
-    in
-    (sigma, EConstr.of_constr r)
-  end
-
-  let make_elim_branch_assumptions ba hyps =
-    let assums =
-      try List.rev (List.firstn ba.nassums hyps)
-      with Failure _ -> anomaly (Pp.str "make_elim_branch_assumptions.") in
-    { ba = ba; assums = assums }
-
-  let elim_on_ba tac ba =
-    Proofview.Goal.enter begin fun gl ->
-    let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
-    tac branches
-    end
-
-  let case_on_ba tac ba =
-    Proofview.Goal.enter begin fun gl ->
-    let branches = make_elim_branch_assumptions ba (Proofview.Goal.hyps gl) in
-    tac branches
-    end
-
-  let elimination_then tac c =
-    Proofview.Goal.enter begin fun gl ->
-    let (ind,t) = pf_reduce_to_quantified_ind gl (pf_get_type_of gl c) in
-    let isrec,mkelim =
-      match (Global.lookup_mind (fst (fst ind))).mind_record with
-      | NotRecord -> true,gl_make_elim
-      | FakeRecord | PrimRecord _ -> false,gl_make_case_dep
-    in
-    general_elim_then_using mkelim isrec None tac None ind (c, t)
-    end
-
-  let case_then_using =
-    general_elim_then_using gl_make_case_dep false
-
-  let case_nodep_then_using =
-    general_elim_then_using gl_make_case_nodep false
-
   let pf_constr_of_global ref =
     Proofview.tclEVARMAP >>= fun sigma ->
     Proofview.tclENV >>= fun env ->
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 48a06e6e1d..bfead34b3b 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Constr
 open EConstr
 open Evd
 open Locus
@@ -94,18 +93,6 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic
 
 (** {6 Elimination tacticals. } *)
 
-type branch_args = private {
-  ity        : pinductive;  (** the type we were eliminating on *)
-  branchnum  : int;         (** the branch number *)
-  nassums    : int;         (** number of assumptions/letin to be introduced *)
-  branchsign : bool list;   (** the signature of the branch.
-                                true=assumption, false=let-in *)
-  branchnames : intro_patterns}
-
-type branch_assumptions = private {
-  ba        : branch_args;       (** the branch args *)
-  assums    : named_context}   (** the list of assumptions introduced *)
-
 (** [get_and_check_or_and_pattern loc pats branchsign] returns an appropriate
    error message if |pats| <> |branchsign|; extends them if no pattern is given
    for let-ins in the case of a conjunctive pattern *)
@@ -122,7 +109,7 @@ val compute_constructor_signatures : rec_flag:bool -> inductive * 'a -> bool lis
 
 (** Useful for [as intro_pattern] modifier *)
 val compute_induction_names :
-  bool list array -> or_and_intro_pattern option -> intro_patterns array
+  bool -> bool list array -> or_and_intro_pattern option -> intro_patterns array
 
 val elimination_sort_of_goal : Goal.goal sigma -> Sorts.family
 val elimination_sort_of_hyp  : Id.t -> Goal.goal sigma -> Sorts.family
@@ -249,20 +236,5 @@ module New : sig
   val elimination_sort_of_hyp  : Id.t -> Proofview.Goal.t -> Sorts.family
   val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family
 
-  val elimination_then :
-    (branch_args -> unit Proofview.tactic) ->
-    constr -> unit Proofview.tactic
-
-  val case_then_using :
-    or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
-
-  val case_nodep_then_using :
-    or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-    constr option -> inductive * EInstance.t -> constr * types -> unit Proofview.tactic
-
-  val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
-  val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args  -> unit Proofview.tactic
-
   val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index eb7b7e363f..e2d60dfabd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4397,7 +4397,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
     let branchletsigns =
       let f (_,is_not_let,_,_) = is_not_let in
       Array.map (fun (_,l) -> List.map f l) indsign in
-    let names = compute_induction_names branchletsigns names in
+    let names = compute_induction_names true branchletsigns names in
     Array.iter (check_name_unicity env toclear []) names;
     let tac =
     (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)