[vernacexpr] Remove duplicate fixpoint record.

We continue over the previous commit and remove redundant
`structured_fixpoint_expr` record in favor of the one used in the AST.

This removes some term-shuffling, tho we still have discrepancies
related to adjustments on the recursive annotation.

8 files changed, 71 insertions, 85 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index b7da4f964d..74c9bc2886 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -107,27 +107,20 @@ let check_mutuality env evd isfix fixl =
        warn_non_full_mutual (x,xge,y,yge,isfix,rest)
     | _ -> ()
 
-type structured_fixpoint_expr =
-  { fix_name : Id.t
-  ; fix_univs : Constrexpr.universe_decl_expr option
-  ; fix_annot : lident option
-  ; fix_binders : local_binder_expr list
-  ; fix_body : constr_expr option
-  ; fix_type : constr_expr
-  ; fix_notations : Vernacexpr.decl_notation list
-  }
-
 let interp_fix_context ~program_mode ~cofix env sigma fix =
-  let before, after = if not cofix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in
+  let before, after =
+    if not cofix
+    then split_at_annot fix.Vernacexpr.binders fix.Vernacexpr.rec_order
+    else [], fix.Vernacexpr.binders in
   let sigma, (impl_env, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma before in
   let sigma, (impl_env', ((env'', ctx'), imps')) =
     interp_context_evars ~program_mode ~impl_env ~shift:(Context.Rel.nhyps ctx) env' sigma after
   in
-  let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in
+  let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.Vernacexpr.rec_order in
   sigma, ((env'', ctx' @ ctx), (impl_env',imps @ imps'), annot)
 
 let interp_fix_ccl ~program_mode sigma impls (env,_) fix =
-  let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.fix_type in
+  let sigma, (c, impl) = interp_type_evars_impls ~program_mode ~impls env sigma fix.Vernacexpr.rtype in
   let r = Retyping.relevance_of_type env sigma c in
   sigma, (c, r, impl)
 
@@ -136,7 +129,7 @@ let interp_fix_body ~program_mode env_rec sigma impls (_,ctx) fix ccl =
   Option.cata (fun body ->
     let env = push_rel_context ctx env_rec in
     let sigma, body = interp_casted_constr_evars ~program_mode env sigma ~impls body ccl in
-    sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.fix_body
+    sigma, Some (it_mkLambda_or_LetIn body ctx)) (sigma, None) fix.Vernacexpr.body_def
 
 let build_fix_type (_,ctx) ccl = EConstr.it_mkProd_or_LetIn ccl ctx
 
@@ -168,16 +161,16 @@ type recursive_preentry =
 let fix_proto sigma =
   Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto")
 
-let interp_recursive ~program_mode ~cofix fixl =
+let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) =
   let open Context.Named.Declaration in
   let open EConstr in
   let env = Global.env() in
-  let fixnames = List.map (fun fix -> fix.fix_name) fixl in
+  let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in
 
   (* Interp arities allowing for unresolved types *)
   let all_universes =
     List.fold_right (fun sfe acc ->
-        match sfe.fix_univs , acc with
+        match sfe.Vernacexpr.univs , acc with
         | None , acc -> acc
         | x , None -> x
         | Some ls , Some us ->
@@ -223,7 +216,7 @@ let interp_recursive ~program_mode ~cofix fixl =
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let sigma, fixdefs =
     Metasyntax.with_syntax_protection (fun () ->
-      let notations = List.map_append (fun { fix_notations } -> fix_notations) fixl in
+      let notations = List.map_append (fun { Vernacexpr.notations } -> notations) fixl in
       List.iter (Metasyntax.set_notation_for_interpretation env_rec impls) notations;
       List.fold_left4_map
         (fun sigma fixctximpenv -> interp_fix_body ~program_mode env_rec sigma (Id.Map.fold Id.Map.add fixctximpenv impls))
@@ -318,35 +311,28 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v
   | _ -> user_err Pp.(str
            "Well-founded induction requires Program Fixpoint or Function.")
 
-let extract_fixpoint_components ~structonly l =
-  let open Vernacexpr in
-  List.map (fun { id_decl=({CAst.v=id},pl); rec_order; binders; rtype; body_def; notations } ->
-      (* This is a special case: if there's only one binder, we pick it as the
-         recursive argument if none is provided. *)
-      let rec_order = Option.map (fun rec_order -> match binders, rec_order with
-          | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
-            CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
-          | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
-            CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
-          | _, x -> x) rec_order
-      in
-      let rec_order = Option.map (extract_decreasing_argument ~structonly) rec_order in
-      { fix_name = id; fix_annot = rec_order; fix_univs = pl;
-        fix_binders = binders; fix_body = body_def; fix_type = rtype; fix_notations = notations }) l
-
-let extract_cofixpoint_components l =
-  List.map (fun { Vernacexpr.id_decl=({CAst.v=id},pl); binders; rtype; body_def; notations} ->
-      {fix_name = id; fix_annot = None; fix_univs = pl;
-       fix_binders = binders; fix_body = body_def; fix_type = rtype; fix_notations = notations}) l
+(* This is a special case: if there's only one binder, we pick it as
+   the recursive argument if none is provided. *)
+let adjust_rec_order ~structonly binders rec_order =
+  let rec_order = Option.map (fun rec_order -> match binders, rec_order with
+      | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+        CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+      | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+        CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+      | _, x -> x) rec_order
+  in
+  Option.map (extract_decreasing_argument ~structonly) rec_order
 
 let check_safe () =
   let open Declarations in
   let flags = Environ.typing_flags (Global.env ()) in
   flags.check_universes && flags.check_guarded
 
-let do_fixpoint_common l =
-  let fixl = extract_fixpoint_components ~structonly:true l in
-  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in
+let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
+  let fixl = List.map (fun fix ->
+      Vernacexpr.{ fix
+                   with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in
+  let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in
   fixl, ntns, fix, List.map compute_possible_guardness_evidences info
 
@@ -361,9 +347,9 @@ let do_fixpoint ~scope ~poly l =
   declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
-let do_cofixpoint_common l =
-  let fixl = extract_cofixpoint_components l in
-  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in
+let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
+  let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
+  let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
   interp_fixpoint ~cofix:true fixl, ntns
 
 let do_cofixpoint_interactive ~scope ~poly l =
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 1018c463c6..4f8e9018de 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Constrexpr
 open Vernacexpr
 
 (** {6 Fixpoints and cofixpoints} *)
@@ -33,24 +32,20 @@ val do_cofixpoint :
 (** Internal API  *)
 (************************************************************************)
 
-type structured_fixpoint_expr =
-  { fix_name : Id.t
-  ; fix_univs : Constrexpr.universe_decl_expr option
-  ; fix_annot : lident option
-  ; fix_binders : local_binder_expr list
-  ; fix_body : constr_expr option
-  ; fix_type : constr_expr
-  ; fix_notations : decl_notation list
-  }
-
 (** Typing global fixpoints and cofixpoint_expr *)
 
+val adjust_rec_order
+  :  structonly:bool
+  -> Constrexpr.local_binder_expr list
+  -> Constrexpr.recursion_order_expr option
+  -> lident option
+
 (** Exported for Program *)
 val interp_recursive :
   (* Misc arguments *)
   program_mode:bool -> cofix:bool ->
   (* Notations of the fixpoint / should that be folded in the previous argument? *)
-  structured_fixpoint_expr list ->
+  lident option fix_expr_gen list ->
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
@@ -60,20 +55,11 @@ val interp_recursive :
 
 (** Exported for Funind *)
 
-(** Extracting the semantical components out of the raw syntax of
-   (co)fixpoints declarations *)
-
-val extract_fixpoint_components
-  : structonly:bool -> fixpoint_expr list -> structured_fixpoint_expr list
-
-val extract_cofixpoint_components
-  : cofixpoint_expr list -> structured_fixpoint_expr list
-
 type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list
 
 val interp_fixpoint
   :  cofix:bool
-  -> structured_fixpoint_expr list
+  -> lident option fix_expr_gen list
   -> recursive_preentry * UState.universe_decl * UState.t *
      (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0104c99e41..c6e68effd7 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -289,19 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
   | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
   in
-  let ntns = List.map_append (fun { fix_notations } -> fix_notations ) fixl in
+  let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
   Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind
 
 let do_program_fixpoint ~scope ~poly l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }],
-      [ Vernacexpr.{id_decl=({CAst.v=id},pl);binders;rtype;body_def;notations} ] ->
+      [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded (id, pl, binders, rtype, out_def body_def) poly r recarg notations
+        build_wellfounded (id, univs, binders, rtype, out_def body_def) poly r recarg notations
 
     | [Some { CAst.v = CMeasureRec (n, m, r) }],
-      [Vernacexpr.{id_decl=({CAst.v=id},pl); binders; rtype; body_def; notations }] ->
+      [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
       (* We resolve here a clash between the syntax of Program Fixpoint and the one of funind *)
       let r = match n, r with
         | Some id, None ->
@@ -311,13 +311,15 @@ let do_program_fixpoint ~scope ~poly l =
           user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
         | _, _ -> r
       in
-        build_wellfounded (id, pl, binders, rtype, out_def body_def) poly
+        build_wellfounded (id, univs, binders, rtype, out_def body_def) poly
           (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
 
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
-      let fixl = extract_fixpoint_components ~structonly:true l in
-      let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
-      do_program_recursive ~scope ~poly fixkind fixl
+      let annots = List.map (fun fix ->
+          Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
+      let fixkind = DeclareObl.IsFixpoint annots in
+      let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
+      do_program_recursive ~scope ~poly fixkind l
 
     | _, _ ->
         user_err ~hdr:"do_program_fixpoint"
@@ -332,7 +334,7 @@ let do_fixpoint ~scope ~poly l =
   do_program_fixpoint ~scope ~poly l;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
-let do_cofixpoint ~scope ~poly l =
-  let fixl = extract_cofixpoint_components l in
+let do_cofixpoint ~scope ~poly fixl =
+  let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
   do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index fa3d2b7020..a851e4dff5 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
 open Vernacexpr
 
 (** Special Fixpoint handling when command is activated. *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 678d4436d2..15f9e0328c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -407,13 +407,14 @@ GRAMMAR EXTEND Gram
         rtype = type_cstr;
         body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation ->
           { let binders, rec_order = bl in
-            {id_decl; rec_order; binders; rtype; body_def; notations}
+            {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations}
           } ] ]
   ;
   corec_definition:
     [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr;
         body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation ->
-          { {id_decl; rec_order=(); binders; rtype; body_def; notations} } ] ]
+        { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations}
+        } ]]
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> { c }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 835f5e0b75..e25118e0a8 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -419,12 +419,12 @@ let string_of_theorem_kind = let open Decls in function
     | l -> spc() ++
       hov 1 (str"(" ++ prlist_with_sep sep_v2 pr_syntax_modifier l ++ str")")
 
-  let pr_rec_definition { id_decl; rec_order; binders; rtype; body_def; notations } =
+  let pr_rec_definition { fname; univs; rec_order; binders; rtype; body_def; notations } =
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
     let annot = pr_guard_annot (pr_lconstr_expr env sigma) binders rec_order in
-    pr_ident_decl id_decl ++ pr_binders_arg binders ++ annot
+    pr_ident_decl (fname,univs) ++ pr_binders_arg binders ++ annot
     ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr env sigma c) rtype
     ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_pure_lconstr env sigma def) body_def
     ++ prlist (pr_decl_notation @@ pr_constr env sigma) notations
@@ -858,8 +858,8 @@ let string_of_definition_object_kind = let open Decls in function
           | DoDischarge -> keyword "Let" ++ spc ()
           | NoDischarge -> str ""
         in
-        let pr_onecorec {id_decl; binders; rtype; body_def; notations } =
-          pr_ident_decl id_decl ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++
+        let pr_onecorec {fname; univs; binders; rtype; body_def; notations } =
+          pr_ident_decl (fname,univs) ++ spc() ++ pr_binders env sigma binders ++ spc() ++ str":" ++
             spc() ++ pr_lconstr_expr env sigma rtype ++
             pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr env sigma def) body_def ++
             prlist (pr_decl_notation @@ pr_constr env sigma) notations
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0205a653c5..6c048c7d83 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -772,7 +772,7 @@ let vernac_inductive ~atts cum lo finite indl =
 
 let vernac_fixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
-    List.iter (fun { id_decl = (lid,_) } -> Dumpglob.dump_definition lid false "def") l;
+    List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l;
   enforce_locality_exp atts.DefAttributes.locality discharge
 
 let vernac_fixpoint_interactive ~atts discharge l =
@@ -793,7 +793,7 @@ let vernac_fixpoint ~atts discharge l =
 
 let vernac_cofixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
-    List.iter (fun { id_decl = (lid,_) } -> Dumpglob.dump_definition lid false "def") l;
+    List.iter (fun { fname } -> Dumpglob.dump_definition fname false "def") l;
   enforce_locality_exp atts.DefAttributes.locality discharge
 
 let vernac_cofixpoint_interactive ~atts discharge l =
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8b8123bd30..6f09d9a39b 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -131,7 +131,8 @@ type definition_expr =
 type decl_notation = lstring * constr_expr * scope_name option
 
 type 'a fix_expr_gen =
-  { id_decl : ident_decl
+  { fname : lident
+  ; univs : universe_decl_expr option
   ; rec_order : 'a
   ; binders : local_binder_expr list
   ; rtype : constr_expr