Merge PR #11785: [proof] consolidation of mutual definition declaration path

Reviewed-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: ppedrot

9 files changed, 149 insertions, 126 deletions

diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 7fd1634dcf..623e6b8a42 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -8,14 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(***********************************************************************)
-(*                                                                     *)
-(*      This module defines proof facilities relevant to the           *)
-(*      toplevel. In particular it defines the global proof            *)
-(*      environment.                                                   *)
-(*                                                                     *)
-(***********************************************************************)
-
 open Util
 open Names
 open Context
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index f1281d1291..e1c75c0649 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -8,9 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** This module defines proof facilities relevant to the
-     toplevel. In particular it defines the global proof
-     environment. *)
+(** State for interactive proofs. *)
 
 type t
 
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 0a70954dd2..6580495295 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -236,16 +236,22 @@ let interp_fixpoint ~cofix l =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
-  let fix_kind, cofix, indexes = match indexes with
-    | Some indexes -> Decls.Fixpoint, false, indexes
-    | None -> Decls.CoFixpoint, true, []
+let build_recthms ~indexes fixnames fixtypes fiximps =
+  let fix_kind, cofix = match indexes with
+    | Some indexes -> Decls.Fixpoint, false
+    | None -> Decls.CoFixpoint, true
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        { Lemmas.Recthm.name; typ
+        { DeclareDef.Recthm.name; typ
         ; args = List.map Context.Rel.Declaration.get_name ctx; impargs})
-      fixnames fixtypes fiximps in
+      fixnames fixtypes fiximps
+  in
+  fix_kind, cofix, thms
+
+let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
+  let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in
+  let indexes = Option.default [] indexes in
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
   let lemma =
@@ -255,40 +261,17 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
 
-let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  let indexes, cofix, fix_kind =
-    match indexes with
-    | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint)
-    | None -> [], true, Decls.(IsDefinition CoFixpoint)
-  in
+let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
   (* We shortcut the proof process *)
+  let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
-  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let vars, fixdecls, gidx =
-    if not cofix then
-      let env = Global.env() in
-      let indexes = Pretyping.search_guard env indexes fixdecls in
-      let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),fixdecls)) in
-      let fixdecls = List.map_i (fun i _ -> Constr.mkFix ((indexes,i),fixdecls)) 0 fixnames in
-      vars, fixdecls, Some indexes
-    else (* cofix *)
-      let fixdecls = List.map_i (fun i _ -> Constr.mkCoFix (i,fixdecls)) 0 fixnames in
-      let vars = Vars.universes_of_constr (List.hd fixdecls) in
-      vars, fixdecls, None
-  in
-  let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-  let evd = Evd.from_ctx ctx in
-  let evd = Evd.restrict_universe_context evd vars in
-  let ctx = Evd.check_univ_decl ~poly evd pl in
-  let ubind = Evd.universe_binders evd in
+  let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
+  let fix_kind = Decls.IsDefinition fix_kind in
   let _ : GlobRef.t list =
-    List.map4 (fun name body types impargs ->
-        let ce = Declare.definition_entry ~opaque:false ~types ~univs:ctx body in
-        DeclareDef.declare_definition ~name ~scope ~kind:fix_kind ~ubind ~impargs ce)
-      fixnames fixdecls fixtypes fiximps
+    DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
+      ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
+      fixitems
   in
-  Declare.recursive_message (not cofix) gidx fixnames;
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   ()
 
 let extract_decreasing_argument ~structonly { CAst.v = v; _ } =
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 09582f4ef2..fc53abdcea 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,6 +69,59 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
+let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
+  match possible_indexes with
+  | Some possible_indexes ->
+    let env = Global.env() in
+    let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
+    let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in
+    vars, fixdecls, Some indexes
+  | None ->
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in
+    let vars = Vars.universes_of_constr (List.hd fixdecls) in
+    vars, fixdecls, None
+
+module Recthm = struct
+  type t =
+    { name : Names.Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Names.Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
+let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
+  let vars, fixdecls, indexes =
+    mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
+  let ubind, univs =
+    (* XXX: Obligations don't do this, this seems like a bug? *)
+    if restrict_ucontext
+    then
+      let evd = Evd.from_ctx uctx in
+      let evd = Evd.restrict_universe_context evd vars in
+      let univs = Evd.check_univ_decl ~poly evd udecl in
+      Evd.universe_binders evd, univs
+    else
+      let univs = UState.univ_entry ~poly uctx in
+      UnivNames.empty_binders, univs
+  in
+  let csts = CList.map2
+      (fun Recthm.{ name; typ; impargs } body ->
+         let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in
+         declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+      fixitems fixdecls
+  in
+  let isfix = Option.is_empty possible_indexes in
+  let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
+  Declare.recursive_message isfix indexes fixnames;
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+  csts
+
 let warn_let_as_axiom =
   CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index fb1fc9242c..1d7fd3a3bf 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -59,6 +59,35 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
+module Recthm : sig
+  type t =
+    { name : Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
+val declare_mutually_recursive
+  : opaque:bool
+  -> scope:locality
+  -> kind:Decls.logical_kind
+  -> poly:bool
+  -> uctx:UState.t
+  -> udecl:UState.universe_decl
+  -> ntns:Vernacexpr.decl_notation list
+  -> rec_declaration:Constr.rec_declaration
+  -> possible_indexes:int list list option
+  -> ?restrict_ucontext:bool
+  (** XXX: restrict_ucontext should be always true, this seems like a
+     bug in obligations, so this parameter should go away *)
+  -> Recthm.t list
+  -> Names.GlobRef.t list
+
 val prepare_definition
   :  allow_evars:bool
   -> ?opaque:bool
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index c13e884736..98a9e4b9c9 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -436,48 +436,35 @@ let declare_mutual_definition l =
         (xdef :: defs, xobls @ obls)) l ([], [])
   in
   (*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixdefs, fixrs,fixtypes, fiximps = List.split4 defs in
+  let fixdefs, fixrs, fixtypes, fixitems =
+    List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) ->
+        d :: a1, r :: a2, typ :: a3,
+        DeclareDef.Recthm.{ name; typ; impargs; args = [] } :: a4
+      ) defs first.prg_deps ([],[],[],[])
+  in
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
   let rvec = Array.of_list fixrs in
   let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
-  let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
-  let fixnames = first.prg_deps in
-  let opaque = first.prg_opaque in
-  let indexes, fixdecls =
+  let rec_declaration = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
+  let possible_indexes =
     match fixkind with
     | IsFixpoint wfl ->
-      let possible_indexes =
-        List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes
-      in
-      let indexes =
-        Pretyping.search_guard (Global.env ()) possible_indexes fixdecls
-      in
-      ( Some indexes
-      , List.map_i (fun i _ -> mkFix ((indexes, i), fixdecls)) 0 l
-      )
-    | IsCoFixpoint ->
-      (None, List.map_i (fun i _ -> mkCoFix (i, fixdecls)) 0 l)
+      Some (List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes)
+    | IsCoFixpoint -> None
   in
+  (* In the future we will pack all this in a proper record *)
+  let poly, scope, ntns, opaque = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque in
+  let kind = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint) else Decls.(IsDefinition CoFixpoint) in
   (* Declare the recursive definitions *)
-  let poly = first.prg_poly in
-  let scope = first.prg_scope in
-  let univs = UState.univ_entry ~poly first.prg_ctx in
-  let fix_exn = Hook.get get_fix_exn () in
-  let kind = Decls.IsDefinition (if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint) in
-  let ubind = UnivNames.empty_binders in
+  let udecl = UState.default_univ_decl in
   let kns =
-    List.map4
-      (fun name body types impargs ->
-         let ce = Declare.definition_entry ~opaque ~types ~univs body in
-         DeclareDef.declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
-      fixnames fixdecls fixtypes fiximps
+    DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind
+      ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
+      ~restrict_ucontext:false fixitems
   in
-  (* Declare notations *)
-  List.iter
-    (Metasyntax.add_notation_interpretation (Global.env ()))
-    first.prg_notations;
-  Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
+  (* Only for the first constant *)
+  let fix_exn = Hook.get get_fix_exn () in
   let dref = List.hd kns in
   DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref });
   List.iter progmap_remove l;
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7782ff8ac9..e08d2ce117 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -39,15 +39,6 @@ module Proof_ending = struct
 
 end
 
-module Recthm = struct
-  type t =
-    { name : Id.t
-    ; typ : Constr.t
-    ; args : Name.t list
-    ; impargs : Impargs.manual_implicits
-    }
-end
-
 module Info = struct
 
   type t =
@@ -56,7 +47,7 @@ module Info = struct
     ; impargs : Impargs.manual_implicits
     ; proof_ending : Proof_ending.t CEphemeron.key
     (* This could be improved and the CEphemeron removed *)
-    ; other_thms : Recthm.t list
+    ; other_thms : DeclareDef.Recthm.t list
     ; scope : DeclareDef.locality
     ; kind : Decls.logical_kind
     }
@@ -129,7 +120,7 @@ let start_dependent_lemma ~name ~poly
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun { Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
+    match List.map (fun { DeclareDef.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -137,12 +128,12 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun { Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
+    in match List.map2 (fun { DeclareDef.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
 let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
-  let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
+  let intro_tac { DeclareDef.Recthm.args; _ } = Tactics.auto_intros_tac args in
   let init_tac, compute_guard = match recguard with
   | Some (finite,guard,init_terms) ->
     let rec_tac = rec_tac_initializer finite guard thms snl in
@@ -162,7 +153,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
     intro_tac (List.hd thms), [] in
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
-  | { Recthm.name; typ; impargs; _}::other_thms ->
+  | { DeclareDef.Recthm.name; typ; impargs; _}::other_thms ->
     let info =
       Info.{ hook
            ; impargs
@@ -185,25 +176,25 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
 (* XXX: Most of this does belong to Declare, due to proof_entry manip *)
 module MutualEntry : sig
 
-  (* We keep this type abstract and to avoid uncontrolled hacks *)
-  type t
-
-  val variable : info:Info.t -> Entries.parameter_entry -> t
-
-  val adjust_guardness_conditions
+  val declare_variable
     : info:Info.t
-    -> Evd.side_effects Declare.proof_entry
-    -> t
+    -> uctx:UState.t
+    (* Only for the first constant, introduced by compat *)
+    -> ubind:UnivNames.universe_binders
+    -> name:Id.t
+    -> Entries.parameter_entry
+    -> Names.GlobRef.t list
 
   val declare_mutdef
     (* Common to all recthms *)
-    : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+    : info:Info.t
+    -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
     -> uctx:UState.t
     -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list
     (* Only for the first constant, introduced by compat *)
     -> ubind:UnivNames.universe_binders
     -> name:Id.t
-    -> t
+    -> Evd.side_effects Declare.proof_entry
     -> Names.GlobRef.t list
 
 end = struct
@@ -219,8 +210,6 @@ end = struct
     ; info : Info.t
     }
 
-  let variable ~info t = { entry = NoBody t; info }
-
   (* XXX: Refactor this with the code in
      [ComFixpoint.declare_fixpoint_generic] *)
   let guess_decreasing env possible_indexes ((body, ctx), eff) =
@@ -290,9 +279,17 @@ end = struct
     let ubind = UnivNames.empty_binders in
     let rs =
       List.map_i (
-        fun i { Recthm.name; typ; impargs } ->
+        fun i { DeclareDef.Recthm.name; typ; impargs } ->
           declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms
     in r :: rs
+
+  let declare_variable ~info ~uctx ~ubind ~name pe =
+    declare_mutdef ~uctx ~ubind ~name { entry = NoBody pe; info }
+
+  let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind ~name const =
+    let mutpe = adjust_guardness_conditions ~info const in
+    declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name mutpe
+
 end
 
 (************************************************************************)
@@ -320,10 +317,8 @@ let compute_proof_using_for_admitted proof typ pproofs =
     | _ -> None
 
 let finish_admitted ~name ~info ~uctx pe =
-  let mutpe = MutualEntry.variable ~info pe in
   let ubind = UnivNames.empty_binders in
-  let _r : Names.GlobRef.t list =
-    MutualEntry.declare_mutdef ~uctx ~ubind ~name mutpe in
+  let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx ~ubind ~name pe in
   ()
 
 let save_lemma_admitted ~(lemma : t) : unit =
@@ -361,11 +356,10 @@ let finish_proved idopt po info =
       | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
     let fix_exn = Declare.Internal.get_fix_exn const in
     let () = try
-      let mutpe = MutualEntry.adjust_guardness_conditions ~info const in
       let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
       let ubind = UState.universe_binders uctx in
       let _r : Names.GlobRef.t list =
-        MutualEntry.declare_mutdef ~fix_exn ~uctx ?hook_data ~ubind ~name mutpe
+        MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind ~name const
       in ()
     with e when CErrors.noncritical e ->
       let e = Exninfo.capture e in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 471c955311..6a1f8c09f3 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -44,19 +44,6 @@ module Proof_ending : sig
 
 end
 
-module Recthm : sig
-  type t =
-    { name : Id.t
-    (** Name of theorem *)
-    ; typ : Constr.t
-    (** Type of theorem  *)
-    ; args : Name.t list
-    (** Names to pre-introduce  *)
-    ; impargs : Impargs.manual_implicits
-    (** Explicitily declared implicit arguments  *)
-    }
-end
-
 module Info : sig
 
   type t
@@ -104,7 +91,7 @@ val start_lemma_with_initialization
   -> udecl:UState.universe_decl
   -> Evd.evar_map
   -> (bool * lemma_possible_guards * Constr.t option list option) option
-  -> Recthm.t list
+  -> DeclareDef.Recthm.t list
   -> int list option
   -> t
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d273573270..8641c67d9f 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -501,7 +501,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let recguard,thms,snl = 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))) ->
-      { Lemmas.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
+      { DeclareDef.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