[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.

1 files changed, 30 insertions, 44 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 =