Merge PR #10537: [vernacexpr] Refactor fixpoint AST.

Reviewed-by: SkySkimmer
Reviewed-by: gares

1 files changed, 17 insertions, 34 deletions

diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 982d316605..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} *)
@@ -18,39 +17,35 @@ 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
-}
-
 (** 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 -> decl_notation 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,25 +55,13 @@ 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 * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation list
+type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list
 
-val extract_cofixpoint_components :
-  (cofixpoint_expr * decl_notation list) list ->
-    structured_fixpoint_expr list * decl_notation 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
+  -> lident option fix_expr_gen 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 :