Clean the representation of recursive annotation in Constrexpr

We make clearer which arguments are optional and which are mandatory.
Some of these representations are tricky because of small differences
between Program and Function, which share the same infrastructure.

As a side-effect of this cleanup, Program Fixpoint can now be used with
e.g. {measure (m + n) R}. Previously, parentheses were required around
R.

5 files changed, 26 insertions, 39 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index eaa5736336..062e3ca8b2 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -653,7 +653,7 @@ let detype_fix detype flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
   let v = Array.map3
     (fun c t i -> share_names detype flags (i+1) [] def_avoid def_env sigma c (lift n t))
     bodies tys vn in
-  GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+  GRec(GFix (Array.map (fun i -> Some i) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 6da168711c..85b9faac77 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -106,19 +106,9 @@ let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) =
   Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
   Option.equal f c1 c2 && f t1 t2
 
-let fix_recursion_order_eq f o1 o2 = match o1, o2 with
-  | GStructRec, GStructRec -> true
-  | GWfRec c1, GWfRec c2 -> f c1 c2
-  | GMeasureRec (c1, o1), GMeasureRec (c2, o2) ->
-    f c1 c2 && Option.equal f o1 o2
-  | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false
-
-let fix_kind_eq f k1 k2 = match k1, k2 with
+let fix_kind_eq k1 k2 = match k1, k2 with
   | GFix (a1, i1), GFix (a2, i2) ->
-    let eq (i1, o1) (i2, o2) =
-      Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2
-    in
-    Int.equal i1 i2 && Array.equal eq a1 a2
+    Int.equal i1 i2 && Array.equal (Option.equal Int.equal) a1 a2
   | GCoFix i1, GCoFix i2 -> Int.equal i1 i2
   | (GFix _ | GCoFix _), _ -> false
 
@@ -150,7 +140,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
     f m1 m2 && Name.equal pat1 pat2 &&
     Option.equal f p1 p2 && f c1 c2 && f t1 t2
   | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) ->
-    fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
+    fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 &&
     Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
     Array.equal f c1 c2 && Array.equal f t1 t2
   | GSort s1, GSort s2 -> glob_sort_eq s1 s2
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index c57cf88cc6..02cb294f6d 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -41,6 +41,12 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level
 type sort_info = (Libnames.qualid * int) option list
 type glob_sort = sort_info glob_sort_gen
 
+type glob_recarg = int option
+
+and glob_fix_kind =
+  | GFix of (glob_recarg array * int)
+  | GCoFix of int
+
 (** Casts *)
 
 type 'a cast_type =
@@ -78,7 +84,7 @@ type 'a glob_constr_r =
       (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *)
   | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
   | GIf   of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g
-  | GRec  of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array *
+  | GRec  of glob_fix_kind * Id.t array * 'a glob_decl_g list array *
              'a glob_constr_g array * 'a glob_constr_g array
   | GSort of glob_sort
   | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option
@@ -88,15 +94,6 @@ and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t
 
 and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g
 
-and 'a fix_recursion_order_g =
-  | GStructRec
-  | GWfRec of 'a glob_constr_g
-  | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option
-
-and 'a fix_kind_g =
-  | GFix of ((int option * 'a fix_recursion_order_g) array * int)
-  | GCoFix of int
-
 and 'a predicate_pattern_g =
     Name.t * (inductive * Name.t list) CAst.t option
       (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
@@ -117,9 +114,7 @@ type tomatch_tuples = [ `any ] tomatch_tuples_g
 type cases_clause = [ `any ] cases_clause_g
 type cases_clauses = [ `any ] cases_clauses_g
 type glob_decl = [ `any ] glob_decl_g
-type fix_kind = [ `any ] fix_kind_g
 type predicate_pattern = [ `any ] predicate_pattern_g
-type fix_recursion_order = [ `any ] fix_recursion_order_g
 
 type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index b29afd1fd2..c788efda48 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -470,17 +470,19 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
       PCase (info, pred, pat_of_raw metas vars c, brs)
 
   | GRec (GFix (ln,n), ids, decls, tl, cl) ->
-    if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
-      err ?loc (Pp.str "\"struct\" annotation is expected.")
-    else
-      let ln = Array.map (fst %> Option.get) ln in
-      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
-      let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
-      let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
-      let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
-      let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
-      let names = Array.map (fun id -> Name id) ids in
-      PFix ((ln,n), (names, tl, cl))
+    let get_struct_arg = function
+      | Some n -> n
+      | None -> err ?loc (Pp.str "\"struct\" annotation is expected.")
+        (* TODO why can't the annotation be omitted? *)
+    in
+    let ln = Array.map get_struct_arg ln in
+    let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+    let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+    let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+    let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+    let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+    let names = Array.map (fun id -> Name id) ids in
+    PFix ((ln,n), (names, tl, cl))
 
   | GRec (GCoFix n, ids, decls, tl, cl) ->
       let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0f7676cd19..48d981082c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -607,10 +607,10 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
 		 fixpoints ?) *)
 	  let possible_indexes =
 	    Array.to_list (Array.mapi
-			     (fun i (n,_) -> match n with
+                             (fun i annot -> match annot with
 			     | Some n -> [n]
 			     | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i))
-			     vn)
+           vn)
 	  in
           let fixdecls = (names,ftys,fdefs) in
           let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in