[declare] Refactor analysis and construction of mutual lemmas

When declaring a lemma, the code path is quite different depending on
whether the lemma is inferred to be a mutually-defined lemma or not.

We refactor the code path in declare to reflect that; this will allow
to better organize constant information and to reuse the `Recthm.t`
type in particular.

6 files changed, 85 insertions, 34 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 99db8df803..304df6fe93 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -271,8 +271,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
-    Declare.Proof.start_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
-      evd (Some(cofix,indexes,init_terms)) thms None in
+    Declare.Proof.start_mutual_with_initialization ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl
+      evd ~mutual_info:(cofix,indexes,init_terms) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 011e00eb2d..e9735eeb7d 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -92,6 +92,7 @@ module Info = struct
     ; udecl: UState.universe_decl
     (** Initial universe declarations *)
     ; thms : Recthm.t list
+    (** thms contains each individual constant info in a mutual decl *)
     ; compute_guard : lemma_possible_guards
     (** thms and compute guard are specific only to
        start_lemma_with_initialization + regular terminator *)
@@ -216,10 +217,24 @@ let rec_tac_initializer finite guard thms snl =
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
+let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma thm =
   let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
-  let init_tac, compute_guard = match recguard with
-  | Some (finite,guard,init_terms) ->
+  let init_tac = intro_tac thm in
+  let { Recthm.name; typ; impargs; _} = thm in
+  let info = Info.make ?hook ~scope ~kind ~udecl () in
+  let info = { info with Info.thms = [] } in
+  (* start_lemma has the responsibility to add (name, impargs, typ)
+       to thms, once Info.t is more refined this won't be necessary *)
+  let lemma = start_proof ~name ~impargs ~poly ~info sigma (EConstr.of_constr typ) in
+  map_proof (fun p ->
+      pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) lemma
+
+type mutual_info = (bool * lemma_possible_guards * Constr.t option list option)
+
+let start_mutual_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma ~mutual_info thms snl =
+  let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
+  let init_tac, compute_guard =
+    let (finite,guard,init_terms) = mutual_info in
     let rec_tac = rec_tac_initializer finite guard thms snl in
     let term_tac =
       match init_terms with
@@ -232,9 +247,7 @@ let start_proof_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
         List.map2 (fun tac thm -> Tacticals.New.tclTHEN tac (intro_tac thm)) tacl thms
     in
     Tacticals.New.tclTHENS rec_tac term_tac, guard
-  | None ->
-    let () = match thms with [_] -> () | _ -> assert false in
-    intro_tac (List.hd thms), [] in
+  in
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
   | { Recthm.name; typ; impargs; _} :: thms ->
@@ -2079,6 +2092,8 @@ module Proof = struct
   let start = start_proof
   let start_dependent = start_dependent_proof
   let start_with_initialization = start_proof_with_initialization
+  type nonrec mutual_info = mutual_info
+  let start_mutual_with_initialization = start_mutual_with_initialization
   let save = save_lemma_proved
   let save_admitted = save_lemma_admitted
   let by = by
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 91950a264a..386635cb3f 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -213,7 +213,7 @@ module Proof : sig
     -> Proofview.telescope
     -> t
 
-  (** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
+  (** Pretty much internal, used by the Lemmavernaculars *)
   val start_with_initialization
     :  ?hook:Hook.t
     -> poly:bool
@@ -221,7 +221,20 @@ module Proof : sig
     -> kind:Decls.logical_kind
     -> udecl:UState.universe_decl
     -> Evd.evar_map
-    -> (bool * lemma_possible_guards * Constr.t option list option) option
+    -> Recthm.t
+    -> t
+
+  type mutual_info = (bool * lemma_possible_guards * Constr.t option list option)
+
+  (** Pretty much internal, used by mutual Lemma / Fixpoint vernaculars *)
+  val start_mutual_with_initialization
+    :  ?hook:Hook.t
+    -> poly:bool
+    -> scope:Locality.locality
+    -> kind:Decls.logical_kind
+    -> udecl:UState.universe_decl
+    -> Evd.evar_map
+    -> mutual_info:mutual_info
     -> Recthm.t list
     -> int list option
     -> t
diff --git a/vernac/recLemmas.ml b/vernac/recLemmas.ml
index eb0e1fb795..797eaa7202 100644
--- a/vernac/recLemmas.ml
+++ b/vernac/recLemmas.ml
@@ -16,9 +16,9 @@ module RelDecl = Context.Rel.Declaration
 
 let find_mutually_recursive_statements sigma thms =
     let n = List.length thms in
-    let inds = List.map (fun (id,(t,impls)) ->
+    let inds = List.map (fun (id,t,args,impls) ->
       let (hyps,ccl) = EConstr.decompose_prod_assum sigma t in
-      let x = (id,(t,impls)) in
+      let x = (id,t,args,impls) in
       let whnf_hyp_hds = EConstr.map_rel_context_in_env
         (fun env c -> fst (Reductionops.whd_all_stack env sigma c))
         (Global.env()) hyps in
@@ -89,14 +89,23 @@ let find_mutually_recursive_statements sigma thms =
     in
     (finite,guard,None), ordered_inds
 
-let look_for_possibly_mutual_statements sigma = function
-  | [id,(t,impls)] ->
+type mutual_info =
+  | NonMutual of Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits
+  | Mutual of
+      { mutual_info : bool * int list list * Constr.t option list option
+      ; thms : (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list
+      ; possible_guards : int list
+      }
+
+let look_for_possibly_mutual_statements sigma thms : mutual_info =
+  match thms with
+  | [id,t,args,impls] ->
       (* One non recursively proved theorem *)
-      None,[id,(t,impls)],None
+    NonMutual (id,t,args,impls)
   | _::_ as thms ->
     (* More than one statement and/or an explicit decreasing mark: *)
     (* we look for a common inductive hyp or a common coinductive conclusion *)
     let recguard,ordered_inds = find_mutually_recursive_statements sigma thms in
     let thms = List.map pi2 ordered_inds in
-    Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
+    Mutual { mutual_info = recguard; thms; possible_guards = List.map (fun (_,_,i) -> succ i) ordered_inds }
   | [] -> CErrors.anomaly (Pp.str "Empty list of theorems.")
diff --git a/vernac/recLemmas.mli b/vernac/recLemmas.mli
index 1a697c1e88..0d297ca9b9 100644
--- a/vernac/recLemmas.mli
+++ b/vernac/recLemmas.mli
@@ -8,8 +8,15 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+type mutual_info =
+  | NonMutual of Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits
+  | Mutual of
+      { mutual_info : bool * int list list * Constr.t option list option
+      ; thms : (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list
+      ; possible_guards : int list
+      }
+
 val look_for_possibly_mutual_statements
   :  Evd.evar_map
-  -> ('a * (EConstr.t * 'b)) list
-  -> (bool * int list list * 'c option) option *
-     ('a * (EConstr.t * 'b)) list * int list option
+  -> (Names.Id.t * EConstr.t * Names.Name.t list * Impargs.manual_implicits) list
+  -> mutual_info
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 89294fee8c..650fc00e88 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -490,6 +490,16 @@ let program_inference_hook env sigma ev =
     user_err Pp.(str "The statement obligations could not be resolved \
                       automatically, write a statement definition first.")
 
+(* Checks for start_lemma_com *)
+let post_check_evd ~udecl ~poly evd =
+  let () =
+    let open UState in
+    if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
+      ignore (Evd.check_univ_decl ~poly evd udecl) in
+  if poly then evd
+  else (* We fix the variables to ensure they won't be lowered to Set *)
+    Evd.fix_undefined_variables evd
+
 let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let env0 = Global.env () in
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
@@ -505,23 +515,20 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
     let evd = Pretyping.solve_remaining_evars ?hook:inference_hook flags env evd in
     let ids = List.map Context.Rel.Declaration.get_name ctx in
     check_name_freshness scope id;
-    evd, (id.CAst.v, (EConstr.it_mkProd_or_LetIn t' ctx, (ids, imps @ imps'))))
+    evd, (id.CAst.v, EConstr.it_mkProd_or_LetIn t' ctx, ids, imps @ imps'))
       evd thms in
-  let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in
+  let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
-  let thms = List.map (fun (name, (typ, (args, impargs))) ->
-      { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
-  let () =
-    let open UState in
-    if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
-       ignore (Evd.check_univ_decl ~poly evd udecl)
-  in
-  let evd =
-    if poly then evd
-    else (* We fix the variables to ensure they won't be lowered to Set *)
-      Evd.fix_undefined_variables evd
-  in
-  Declare.Proof.start_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
+  match mut_analysis with
+  | RecLemmas.NonMutual (name, typ, args, impargs) ->
+    let thm = { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs } in
+    let evd = post_check_evd ~udecl ~poly evd in
+    Declare.Proof.start_with_initialization ?hook ~poly ~scope ~kind evd ~udecl thm
+  | RecLemmas.Mutual { mutual_info; thms ; possible_guards } ->
+    let thms = List.map (fun (name, typ, args, impargs) ->
+        { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
+    let evd = post_check_evd ~udecl ~poly evd in
+    Declare.Proof.start_mutual_with_initialization ?hook ~poly ~scope ~kind evd ~udecl ~mutual_info thms (Some possible_guards)
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->