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

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

1 files changed, 53 insertions, 0 deletions

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 ++