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/comFixpoint.mli | 51 ++++++++++++++++++++++++--------------------------
 1 file changed, 24 insertions(+), 27 deletions(-)

(limited to 'vernac/comFixpoint.mli')

diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 982d316605..1018c463c6 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -18,29 +18,30 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
+  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
 
 val do_fixpoint :
-  scope:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
+  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
 
 val do_cofixpoint :
-  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit
 
 (************************************************************************)
 (** 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
-}
+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 *)
 
@@ -49,8 +50,7 @@ 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 -> decl_notation list ->
-
+  structured_fixpoint_expr list ->
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
@@ -63,22 +63,19 @@ val interp_recursive :
 (** Extracting the semantical components out of the raw syntax of
    (co)fixpoints declarations *)
 
-val extract_fixpoint_components : structonly:bool ->
-  (fixpoint_expr * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation list
+val extract_fixpoint_components
+  : structonly:bool -> fixpoint_expr list -> structured_fixpoint_expr list
 
-val extract_cofixpoint_components :
-  (cofixpoint_expr * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation 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
+type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list
 
-val interp_fixpoint :
-  cofix:bool ->
-  structured_fixpoint_expr list -> decl_notation list ->
-  recursive_preentry * UState.universe_decl * UState.t *
-  (EConstr.rel_context * Impargs.manual_implicits * int option) list
+val interp_fixpoint
+  :  cofix:bool
+  -> structured_fixpoint_expr list
+  -> recursive_preentry * UState.universe_decl * UState.t *
+     (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Very private function, do not use *)
 val compute_possible_guardness_evidences :
-- 
cgit v1.2.3


From d407d1f3f2f877fca8673eaf0470b3390e55dbaa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Jul 2019 18:55:05 +0200
Subject: [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.
---
 vernac/comFixpoint.mli | 30 ++++++++----------------------
 1 file changed, 8 insertions(+), 22 deletions(-)

(limited to 'vernac/comFixpoint.mli')

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
 
-- 
cgit v1.2.3