[proof] [mutual] Factorize mutual body construction.

4 files changed, 37 insertions, 38 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index ced9656218..6e6be4fe3a 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -256,26 +256,15 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   lemma
 
 let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  let indexes, cofix, fix_kind =
+  let possible_indexes, cofix, fix_kind =
     match indexes with
-    | Some indexes -> indexes, false, Decls.(IsDefinition Fixpoint)
-    | None -> [], true, Decls.(IsDefinition CoFixpoint)
+    | Some indexes -> Some indexes, false, Decls.(IsDefinition Fixpoint)
+    | None -> None, true, Decls.(IsDefinition CoFixpoint)
   in
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
-  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let vars, fixdecls, indexes =
-    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 rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
+  let vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes 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
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index b3bcf58b4a..ba84734360 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -69,6 +69,19 @@ let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
   end;
   dref
 
+let mutual_make_bodies ~fixnames ~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 fixnames in
+    vars, fixdecls, Some indexes
+  | None ->
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixnames in
+    let vars = Vars.universes_of_constr (List.hd fixdecls) in
+    vars, fixdecls, None
+
 let declare_mutually_recursive ~cofix ~indexes ~opaque ~univs ~scope ~kind ~ubind ~ntns fixnames fixdecls fixtypes fiximps =
   let csts = CList.map4
       (fun name body types impargs ->
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 971f924c6c..6400fa8ee7 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -59,6 +59,14 @@ val declare_assumption
   -> Entries.parameter_entry
   -> GlobRef.t
 
+(* Returns [uvars, bodies, indexes], [possible_indexes] determines if
+   we are in a fix / cofix case *)
+val mutual_make_bodies
+  : fixnames:'a list
+  -> rec_declaration:Constr.rec_declaration
+  -> possible_indexes:int list list option
+  -> Univ.LSet.t * Constr.constr list * int array option
+
 val declare_mutually_recursive
   : cofix:bool
   -> indexes:int array option
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index e530a6e494..73566f47f4 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -441,38 +441,27 @@ let declare_mutual_definition l =
   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
-  (* Declare the recursive definitions *)
-  let poly = first.prg_poly in
-  let scope = first.prg_scope in
+  (* In the future we will pack all this in a proper record *)
+  let poly, scope, ntns, opaque, fixnames = first.prg_poly, first.prg_scope, first.prg_notations, first.prg_opaque, first.prg_deps in
+  let kind, cofix = if fixkind != IsCoFixpoint then Decls.(IsDefinition Fixpoint, false) else Decls.(IsDefinition CoFixpoint, true) 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 cofix = fixkind = IsCoFixpoint in
-  let ntns = first.prg_notations in
+  (* XXX: Note that obligations doesn't call restrict_universe_context *)
+  let _vars, fixdecls, indexes = DeclareDef.mutual_make_bodies ~fixnames ~rec_declaration ~possible_indexes in
+  (* Declare the recursive definitions *)
   let kns =
     DeclareDef.declare_mutually_recursive ~cofix ~indexes ~scope ~opaque ~univs ~kind ~ubind ~ntns
       fixnames fixdecls fixtypes fiximps
   in
   (* 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;