From d68f695b5a953c50bcf5e80182ef317682de1a05 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Jul 2019 14:01:38 +0200
Subject: [vernacexpr] Refactor fixpoint AST.

We turn the tuples used for (co)-fixpoints into records, cleaning up
their users.

More cleanup is be possible, in particular a few functions can now
shared among co and fixpoints, also `structured_fixpoint_expr` could
like be folded into the new record.

Feedback on the naming of the records fields is welcome.

This is a step towards cleaning up code in `funind`, as it is the main
consumer of this data structure, as it does quite a bit of fixpoint
manipulation.

cc: #6019
---
 vernac/comProgramFixpoint.ml | 36 ++++++++++++++++--------------------
 1 file changed, 16 insertions(+), 20 deletions(-)

(limited to 'vernac/comProgramFixpoint.ml')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 0fd65ad9b4..0104c99e41 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -244,10 +244,10 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive ~scope ~poly fixkind fixl ntns =
+let do_program_recursive ~scope ~poly fixkind fixl =
   let cofix = fixkind = DeclareObl.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info =
-    interp_recursive ~cofix ~program_mode:true fixl ntns
+    interp_recursive ~cofix ~program_mode:true fixl
   in
     (* Program-specific code *)
     (* Get the interesting evars, those that were not instantiated *)
@@ -289,16 +289,19 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns =
   | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
   | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
   in
+  let ntns = List.map_append (fun { fix_notations } -> fix_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 ((_,wf,_,_,_),_) -> wf) l in
+  let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
-    | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+    | [Some { CAst.v = CWfRec (n,r) }],
+      [ Vernacexpr.{id_decl=({CAst.v=id},pl);binders;rtype;body_def;notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn
+        build_wellfounded (id, pl, binders, rtype, out_def body_def) poly r recarg notations
 
-    | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+    | [Some { CAst.v = CMeasureRec (n, m, r) }],
+      [Vernacexpr.{id_decl=({CAst.v=id},pl); 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 ->
@@ -308,25 +311,18 @@ 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, bl, typ, out_def def) poly
-          (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn
+        build_wellfounded (id, pl, 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,ntns = 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 ntns
+      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
 
     | _, _ ->
         user_err ~hdr:"do_program_fixpoint"
           (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let extract_cofixpoint_components l =
-  let fixl, ntnl = List.split l in
-  List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
-            {fix_name = id; fix_annot = None; fix_univs = pl;
-             fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
-  List.flatten ntnl
-
 let check_safe () =
   let open Declarations in
   let flags = Environ.typing_flags (Global.env ()) in
@@ -337,6 +333,6 @@ let do_fixpoint ~scope ~poly l =
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
 let do_cofixpoint ~scope ~poly l =
-  let fixl,ntns = extract_cofixpoint_components l in
-  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns;
+  let fixl = extract_cofixpoint_components l in
+  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
-- 
cgit v1.2.3