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.

interp/constrexpr.ml

@@ -134,16 +134,16 @@ and branch_expr =
   (cases_pattern_expr list list * constr_expr) CAst.t
 
 and fix_expr =
-    lident * (lident option * recursion_order_expr) *
+    lident * (recursion_order_expr CAst.t) option *
       local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
     lident * local_binder_expr list * constr_expr * constr_expr
 
 and recursion_order_expr =
-  | CStructRec
-  | CWfRec of constr_expr
-  | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
+  | CStructRec of lident
+  | CWfRec of lident * constr_expr
+  | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *)
 
 (* Anonymous defs allowed ?? *)
 and local_binder_expr =

interp/constrexpr_ops.ml

@@ -196,10 +196,9 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
   List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
   constr_expr_eq e1 e2
 
-and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
+and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
   (eq_ast Id.equal id1 id2) &&
-  Option.equal (eq_ast Id.equal) j1 j2 &&
-  recursion_order_expr_eq r1 r2 &&
+  Option.equal (eq_ast recursion_order_expr_eq) r1 r2 &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
@@ -211,9 +210,11 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
   constr_expr_eq b1 b2
 
 and recursion_order_expr_eq r1 r2 = match r1, r2 with
-  | CStructRec, CStructRec -> true
-  | CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2
-  | CMeasureRec (e1, o1), CMeasureRec (e2, o2) ->
+  | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2
+  | CWfRec (i1,e1), CWfRec (i2,e2) ->
+    constr_expr_eq e1 e2
+  | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) ->
+    Option.equal (eq_ast Id.equal) i1 i2 &&
     constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2
   | _ -> false
 
@@ -349,7 +350,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
         (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
     | CFix (_,l) ->
       let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
-      List.fold_right (fun (_,(_,o),lb,t,c) acc ->
+      List.fold_right (fun (_,ro,lb,t,c) acc ->
           fold_local_binders g f n'
             (fold_local_binders g f n acc t lb) c lb) l acc
     | CCoFix (_,_) ->

interp/constrextern.ml

@@ -938,13 +938,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
                  let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
                  let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
-		 let n =
-		   match fst nv.(i) with
-		     | None -> None
-                     | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x))
-		 in
-		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
-                 ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty,
+                 let n =
+                   match nv.(i) with
+                   | None -> None
+                   | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
+                             in
+                 ((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
                   extern false scopes vars1 def)) idv
 	     in
              CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
@@ -1159,13 +1158,6 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
         let lonely_seen = add_lonely keyrule lonely_seen in
         extern_notation allscopes lonely_seen vars t rules
 
-and extern_recursion_order scopes vars = function
-    GStructRec -> CStructRec
-  | GWfRec c -> CWfRec (extern true scopes vars c)
-  | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
-				     Option.map (extern true scopes vars) r)
-
-
 let extern_glob_constr vars c =
   extern false (InConstrEntrySomeLevel,(None,[])) vars c
 
@@ -1294,7 +1286,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
      let v = Array.map3
                (fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
     bl tl ln in
-     GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+     GRec(GFix (Array.map (fun i -> Some i) ln,i),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)

interp/constrintern.ml

@@ -1845,51 +1845,44 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	in
 	  apply_impargs c env imp subscopes l loc
 
-    | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
+      | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
         let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
         let dl = Array.of_list dl in
-	let n =
-	  try List.index0 Id.equal iddef lf
+        let n =
+          try List.index0 Id.equal iddef lf
           with Not_found ->
-	    raise (InternalizationError (locid,UnboundFixName (false,iddef)))
-	in
-	let idl_temp = Array.map
-          (fun (id,(n,order),bl,ty,_) ->
-	     let intern_ro_arg f =
-	       let before, after = split_at_annot bl n in
-	       let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
-	       let ro = f (intern env') in
-	       let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
-                                                                  | GLocalAssum _ -> true
-                                                                  | _ -> false (* remove let-ins *))
-                        rbefore) n in
-		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
-	     in
-	     let n, ro, (env',rbl) =
-	       match order with
-	       | CStructRec ->
-		   intern_ro_arg (fun _ -> GStructRec)
-	       | CWfRec c ->
-		   intern_ro_arg (fun f -> GWfRec (f c))
-	       | CMeasureRec (m,r) ->
-		   intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
-	     in
-	     let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
-             ((n, ro), bl, intern_type env' ty, env')) dl in
+            raise (InternalizationError (locid,UnboundFixName (false,iddef)))
+        in
+        let idl_temp = Array.map
+            (fun (id,recarg,bl,ty,_) ->
+               let recarg = Option.map (function { CAst.v = v } -> match v with
+                 | CStructRec i -> i
+                 | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg
+               in
+               let before, after = split_at_annot bl recarg in
+               let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
+               let n = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
+                   | GLocalAssum _ -> true
+                   | _ -> false (* remove let-ins *))
+                   rbefore) recarg in
+               let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in
+               let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
+               (n, bl, intern_type env' ty, env')) dl in
         let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
-	     let env'' = List.fold_left_i (fun i en name -> 
-					     let (_,bli,tyi,_) = idl_temp.(i) in
-					     let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
-					       push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
-                                            en (CAst.make @@ Name name)) 0 env' lf in
-             (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
-	DAst.make ?loc @@
-          GRec (GFix
-	      (Array.map (fun (ro,_,_,_) -> ro) idl,n),
+            let env'' = List.fold_left_i (fun i en name ->
+                let (_,bli,tyi,_) = idl_temp.(i) in
+                let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
+                push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
+                  en (CAst.make @@ Name name)) 0 env' lf in
+            (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
+        DAst.make ?loc @@
+        GRec (GFix
+                (Array.map (fun (ro,_,_,_) -> ro) idl,n),
               Array.of_list lf,
               Array.map (fun (_,bl,_,_) -> bl) idl,
               Array.map (fun (_,_,ty,_) -> ty) idl,
               Array.map (fun (_,_,_,bd) -> bd) idl)
+
     | CCoFix ({ CAst.loc = locid; v = iddef }, dl) ->
         let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in
         let dl = Array.of_list dl in

interp/notation_ops.ml

@@ -957,7 +957,7 @@ let match_fix_kind fk1 fk2 =
   match (fk1,fk2) with
   | GCoFix n1, GCoFix n2 -> Int.equal n1 n2
   | GFix (nl1,n1), GFix (nl2,n2) ->
-      let test (n1, _) (n2, _) = match n1, n2 with
+      let test n1 n2 = match n1, n2 with
       | _, None -> true
       | Some id1, Some id2 -> Int.equal id1 id2
       | _ -> false

interp/notation_term.ml

@@ -38,7 +38,7 @@ type notation_constr =
       notation_constr * notation_constr
   | NIf of notation_constr * (Name.t * notation_constr option) *
       notation_constr * notation_constr
-  | NRec of fix_kind * Id.t array *
+  | NRec of glob_fix_kind * Id.t array *
       (Name.t * notation_constr option * notation_constr) list array *
       notation_constr array * notation_constr array
   | NSort of glob_sort

parsing/g_constr.mlg

@@ -56,10 +56,10 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr =
   (id,ann,bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr =
-  let _ = Option.map (fun { CAst.loc = aloc } ->
+  Option.iter (fun { CAst.loc = aloc } ->
     CErrors.user_err ?loc:aloc
       ~hdr:"Constr:mk_cofixb"
-      (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
+      (Pp.str"Annotation forbidden in cofix expression.")) ann;
   let ty = match tyc with
       Some ty -> ty
     | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in
@@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   fixannot:
-    [ [ "{"; IDENT "struct"; id=identref; "}" -> { (Some id, CStructRec) }
-    | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> { (id, CWfRec rel) }
+    [ [ "{"; IDENT "struct"; id=identref; "}" -> { CStructRec id }
+    | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CWfRec(id,rel) }
     | "{"; IDENT "measure"; m=constr; id=OPT identref;
-	rel=OPT constr; "}" -> { (id, CMeasureRec (m,rel)) }
+        rel=OPT constr; "}" -> { CMeasureRec (id,m,rel) }
     ] ]
   ;
   impl_name_head:
@@ -452,9 +452,9 @@ GRAMMAR EXTEND Gram
   binders_fixannot:
     [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot ->
           { (assum na :: fst bl), snd bl }
-      | f = fixannot -> { [], f }
+      | f = fixannot -> { [], Some (CAst.make ~loc f) }
       | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl }
-      | -> { [], (None, CStructRec) }
+      | -> { [], None }
     ] ]
   ;
   open_binders:

parsing/pcoq.mli

@@ -191,7 +191,7 @@ module Constr :
     val binder : local_binder_expr list Entry.t (* closed_binder or variable *)
     val binders : local_binder_expr list Entry.t (* list of binder *)
     val open_binders : local_binder_expr list Entry.t
-    val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Entry.t
+    val binders_fixannot : (local_binder_expr list * recursion_order_expr CAst.t option) Entry.t
     val typeclass_constraint : (lname * bool * constr_expr) Entry.t
     val record_declaration : constr_expr Entry.t
     val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t

plugins/funind/g_indfun.mlg

@@ -179,8 +179,10 @@ let () =
 VERNAC COMMAND EXTEND Function
 | ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
     => { let hard = List.exists (function
-           | _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true
-           | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
+           | _,((_,(Some { CAst.v = CMeasureRec _ }
+             | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
+           | _,((_,Some { CAst.v = CStructRec _ },_,_,_),_)
+           | _,((_,None,_,_,_),_) -> false) recsl in
          match
            Vernac_classifier.classify_vernac
              (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))