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.

6 files changed, 41 insertions, 26 deletions

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 2aadbd224f..1912646ffd 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -329,16 +329,27 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   pstate
 
-let extract_decreasing_argument limit = function
-  | (na,CStructRec) -> na
-  | (na,_) when not limit -> na
+let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
+  | CStructRec na -> na
+  | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na
+  | CMeasureRec (None,_,_) when not structonly ->
+    user_err Pp.(str "Decreasing argument must be specificed in measure clause.")
   | _ -> user_err Pp.(str
-      "Only structural decreasing is supported for a non-Program Fixpoint")
+           "Well-founded induction requires Program Fixpoint or Function.")
 
-let extract_fixpoint_components limit l =
+let extract_fixpoint_components ~structonly l =
   let fixl, ntnl = List.split l in
   let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) ->
-    let ann = extract_decreasing_argument limit ann in
+      (* This is a special case: if there's only one binder, we pick it as the
+      recursive argument if none is provided. *)
+      let ann = Option.map (fun ann -> match bl, ann with
+        | [CLocalAssum([{ CAst.v = Name x }],_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+          CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+        | [CLocalDef({ CAst.v = Name x },_,_)], { CAst.v = CMeasureRec(None, mes, rel); CAst.loc } ->
+          CAst.make ?loc @@ CMeasureRec(Some (CAst.make x), mes, rel)
+        | _, x -> x) ann
+      in
+      let ann = Option.map (extract_decreasing_argument ~structonly) ann in
       {fix_name = id; fix_annot = ann; fix_univs = pl;
        fix_binders = bl; fix_body = def; fix_type = typ}) fixl in
   fixl, List.flatten ntnl
@@ -356,7 +367,7 @@ let check_safe () =
   flags.check_universes && flags.check_guarded
 
 let do_fixpoint ~ontop local poly l =
-  let fixl, ntns = extract_fixpoint_components true l in
+  let fixl, ntns = extract_fixpoint_components ~structonly:true l in
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
   let possible_indexes =
     List.map compute_possible_guardness_evidences info in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 15ff5f4498..5937842f17 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -62,7 +62,7 @@ val interp_recursive :
 (** Extracting the semantical components out of the raw syntax of
    (co)fixpoints declarations *)
 
-val extract_fixpoint_components : bool ->
+val extract_fixpoint_components : structonly:bool ->
   (fixpoint_expr * decl_notation list) list ->
     structured_fixpoint_expr list * decl_notation list
 
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 350b2d2945..20a2db7ca2 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -85,7 +85,7 @@ let rec telescope sigma l =
 let nf_evar_context sigma ctx =
   List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
 
-let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
+let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   let open EConstr in
   let open Vars in
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -304,22 +304,26 @@ let do_program_recursive local poly fixkind fixl ntns =
 let do_program_fixpoint local poly l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
-    | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
-        let recarg =
-          match n with
-          | Some n -> mkIdentC n.CAst.v
-          | None ->
-              user_err ~hdr:"do_program_fixpoint"
-                (str "Recursive argument required for well-founded fixpoints")
-        in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
+    | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+        let recarg = mkIdentC n.CAst.v in
+        build_wellfounded (id, pl, bl, typ, out_def def) poly r recarg ntn
 
-    | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
-        build_wellfounded (id, pl, n, bl, typ, out_def def) poly
+    | [Some { CAst.v = CMeasureRec (n, m, r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
+      (* 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 ->
+          let loc = id.CAst.loc in
+          Some (CAst.make ?loc @@ CRef(qualid_of_ident ?loc id.CAst.v,None))
+        | Some _, Some _ ->
+          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
 
-    | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
-        let fixl,ntns = extract_fixpoint_components true l in
-        let fixkind = Obligations.IsFixpoint g in
+    | _, _ 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 = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
           do_program_recursive local poly fixkind fixl ntns
 
     | _, _ ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 07194578c1..1b1c618dc7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -295,7 +295,7 @@ type obligation =
 type obligations = (obligation array * int)
 
 type fixpoint_kind =
-  | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
+  | IsFixpoint of lident option list
   | IsCoFixpoint
 
 type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
@@ -486,7 +486,7 @@ let rec lam_index n t acc =
 	lam_index n b (succ acc)
     | _ -> raise Not_found
 
-let compute_possible_guardness_evidences (n,_) fixbody fixtype =
+let compute_possible_guardness_evidences n fixbody fixtype =
   match n with
   | Some { CAst.loc; v = n } -> [lam_index n fixbody 0]
   | None ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index b1b7b1ec90..d25daeed9c 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -70,7 +70,7 @@ type notations =
     (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
 type fixpoint_kind =
-  | IsFixpoint of (lident option * Constrexpr.recursion_order_expr) list
+  | IsFixpoint of lident option list
   | IsCoFixpoint
 
 val add_mutual_definitions :
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index ebfc473522..8eacaed2eb 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -129,7 +129,7 @@ type definition_expr =
       * constr_expr option
 
 type fixpoint_expr =
-    ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
+    ident_decl * recursion_order_expr CAst.t option * local_binder_expr list * constr_expr * constr_expr option
 
 type cofixpoint_expr =
     ident_decl * local_binder_expr list * constr_expr * constr_expr option