[fixpoint] Remove code duplication in (co) fixpoint declaration.

2 files changed, 40 insertions, 81 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index d5fb2a140c..62f16961a3 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,84 +255,59 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint_notations ntns =
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
-
-let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
-  (* Some bodies to define by proof *)
+let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+  let fix_kind, cofix, indexes = match indexes with
+    | Some indexes -> Fixpoint, false, indexes
+    | None -> CoFixpoint, true, []
+  in
   let thms =
     List.map3 (fun name t (ctx,impargs,_) ->
         { Lemmas.Recthm.name; typ = EConstr.of_constr t
         ; args = List.map RelDecl.get_name ctx; impargs})
       fixnames fixtypes fiximps in
   let init_tac =
-    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
-      fixdefs) in
+    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in
   let evd = Evd.from_ctx ctx in
-  let lemma = Lemmas.start_lemma_with_initialization (local,poly,DefinitionBody Fixpoint)
-    evd pl (Some(false,indexes,init_tac)) thms None in
-  declare_fixpoint_notations ntns;
+  let lemma =
+    Lemmas.start_lemma_with_initialization (local,poly,DefinitionBody fix_kind)
+      evd pl (Some(cofix,indexes,init_tac)) thms None in
+  (* Declare notations *)
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
 
-let declare_fixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint_generic ?indexes local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+  let indexes, cofix, fix_kind =
+    match indexes with
+    | Some indexes -> indexes, false, Fixpoint
+    | None -> [], true, 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 env = Global.env() in
-  let indexes = search_guard env indexes fixdecls in
+  let vars, fixdecls, gidx =
+    if not cofix then
+      let env = Global.env() in
+      let indexes = search_guard env indexes fixdecls in
+      let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+      let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+      vars, fixdecls, Some indexes
+    else (* cofix *)
+      let fixdecls = List.map_i (fun i _ -> 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 vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
-  let fixdecls =
-    List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames 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 pl = Evd.universe_binders evd in
   let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
   let fixdecls = List.map mk_pure fixdecls in
-  ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
-            fixnames fixdecls fixtypes fiximps);
-  (* Declare the recursive definitions *)
-  fixpoint_message (Some indexes) fixnames;
-  declare_fixpoint_notations ntns
-
-let declare_cofixpoint_notations = declare_fixpoint_notations
-
-let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  (* Some bodies to define by proof *)
-  let thms =
-    List.map3 (fun name t (ctx,impargs,_) ->
-        { Lemmas.Recthm.name; typ = EConstr.of_constr t
-        ; args = List.map RelDecl.get_name ctx; impargs})
-      fixnames fixtypes fiximps in
-  let init_tac =
-    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
-      fixdefs) in
-  let evd = Evd.from_ctx ctx in
-  let lemma = Lemmas.start_lemma_with_initialization
-    (Global ImportDefaultBehavior,poly, DefinitionBody CoFixpoint)
-    evd pl (Some(true,[],init_tac)) thms None in
-  declare_cofixpoint_notations ntns;
-  lemma
-
-let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  (* We shortcut the proof process *)
-  let fixdefs = List.map Option.get fixdefs in
-  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-  let vars = Vars.universes_of_constr (List.hd fixdecls) in
-  let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
-  let fixdecls = List.map mk_pure fixdecls in
-  let fiximps = List.map (fun (len,imps,idx) -> imps) 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 pl = Evd.universe_binders evd in
-  ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
+  ignore (List.map4 (DeclareDef.declare_fix (local, poly, fix_kind) pl ctx)
             fixnames fixdecls fixtypes fiximps);
-  (* Declare the recursive definitions *)
-  cofixpoint_message fixnames;
-  declare_cofixpoint_notations ntns
+  recursive_message (not cofix) gidx fixnames;
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+  ()
 
 let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
   | CStructRec na -> na
@@ -376,15 +351,15 @@ let do_fixpoint_common l =
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
   fixl, ntns, fix, List.map compute_possible_guardness_evidences info
 
-let do_fixpoint_interactive local poly l =
+let do_fixpoint_interactive local poly l : Lemmas.t =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  let pstate = declare_fixpoint_interactive local poly fix possible_indexes ntns in
+  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes local poly fix ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
-  pstate
+  lemma
 
 let do_fixpoint local poly l =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  declare_fixpoint local poly fix possible_indexes ntns;
+  declare_fixpoint_generic ~indexes:possible_indexes local poly fix ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
 let do_cofixpoint_common l =
@@ -393,11 +368,11 @@ let do_cofixpoint_common l =
 
 let do_cofixpoint_interactive local poly l =
   let ntns, cofix = do_cofixpoint_common l in
-  let pstate = declare_cofixpoint_interactive local poly cofix ntns in
+  let lemma = declare_fixpoint_interactive_generic local poly cofix ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
-  pstate
+  lemma
 
 let do_cofixpoint local poly l =
   let ntns, cofix = do_cofixpoint_common l in
-  declare_cofixpoint local poly cofix ntns;
+  declare_fixpoint_generic local poly cofix ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index b42e877d41..8d76a30cee 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -81,22 +81,6 @@ val interp_fixpoint :
   recursive_preentry * UState.universe_decl * UState.t *
   (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
-(** Registering fixpoints and cofixpoints in the environment *)
-
-(** [Not used so far] *)
-val declare_fixpoint :
-  locality -> polymorphic ->
-  recursive_preentry * UState.universe_decl * UState.t *
-  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  Lemmas.lemma_possible_guards -> decl_notation list ->
-  unit
-
-val declare_cofixpoint :
-  locality -> polymorphic ->
-  recursive_preentry * UState.universe_decl * UState.t *
-  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  decl_notation list -> unit
-
 (** Very private function, do not use *)
 val compute_possible_guardness_evidences :
   ('a, 'b) Context.Rel.pt * 'c * int option -> int list