Arguments: cleanup + detect discrepancy rename/implicit (#3753)

It seems warnings are not taken into account in output/
tests.

1 files changed, 63 insertions, 27 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 25d16f91f..1d6278066 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -979,12 +979,17 @@ let warn_arguments_assert =
             strbrk "to clear implicit arguments add ': clear implicits'. " ++
             strbrk "If you want to clear notation scopes add ': clear scopes'")
          
+let warn_renaming_nonimplicit =
+  CWarnings.create ~name:"arguments-assert" ~category:"vernacular"
+         (fun (oldn, newn) ->
+          strbrk "Ignoring rename of "++pr_id oldn++str" into "++pr_id newn++
+          strbrk ". Only implicit arguments can be renamed.")
 
 let vernac_declare_arguments locality r l nargs flags =
   let extra_scope_flag = List.mem `ExtraScopes flags in
-  let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
+  let names = List.map (List.map (fun { name } -> name)) l in
   let names, rest = List.hd names, List.tl names in
-  let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in
+  let scopes = List.map (List.map (fun { notation_scope = s } -> s)) l in
   if List.exists (fun na -> not (List.equal Name.equal na names)) rest then
     error "All arguments lists must declare the same names.";
   if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names))
@@ -1023,13 +1028,15 @@ let vernac_declare_arguments locality r l nargs flags =
   | [[]] -> l
   | _ ->
     let name_anons = function
-      | (Anonymous, a,b,c,d), Name id -> Name id, a,b,c,d
+      | { name = Anonymous } as x, Name id -> { x with name = Name id }
       | x, _ -> x in
     List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in
-  let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
+  let names_decl = List.map (List.map (fun { name } -> name)) l in
   let renamed_arg = ref None in
   let set_renamed a b =
-    if Option.is_empty !renamed_arg && not (Id.equal a b) then renamed_arg := Some(b,a) in
+    if Option.is_empty !renamed_arg && not (Id.equal a b) then
+      renamed_arg := Some(b,a)
+  in
   let some_renaming_specified =
     try
       let names = Arguments_renaming.arguments_names sr in
@@ -1039,22 +1046,50 @@ let vernac_declare_arguments locality r l nargs flags =
     match l with
     | [[]] -> false, [[]]
     | _ ->
-    List.fold_map (fun sr il ->
-      let sr', impl = List.fold_map (fun b -> function
-        | (Anonymous, _,_, true, max), Name id -> assert false
-        | (Name x, _,_, true, _), Anonymous ->
-            errorlabstrm "vernac_declare_arguments"
-              (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.")
-        | (Name iid, _,_, true, max), Name id ->
-           set_renamed iid id;
-           b || not (Id.equal iid id), Some (ExplByName id, max, false)
-        | (Name iid, _,_, _, _), Name id ->
-           set_renamed iid id;
-           b || not (Id.equal iid id), None
-        | _ -> b, None)
-        sr (List.combine il inf_names) in
-      sr || sr', List.map_filter (fun x -> x) impl)
-      some_renaming_specified l in
+       let some_renaming = ref some_renaming_specified in
+       let rec aux il =
+         match il with
+         | [] -> []
+         | il :: ils -> aux_single il inf_names :: aux ils
+       and aux_single impl inf_names =
+         match impl, inf_names with
+         | [], _ -> []
+         | { name = Anonymous;
+             implicit_status = (`Implicit|`MaximallyImplicit)} :: _,
+           Name id :: _ ->
+             assert false
+         | { name = Name x;
+             implicit_status = (`Implicit|`MaximallyImplicit)} :: _,
+           Anonymous :: _ ->
+             errorlabstrm "vernac_declare_arguments"
+               (str"Argument "++ pr_id x ++str " cannot be declared implicit.")
+         | { name = Name iid;
+             implicit_status = (`Implicit|`MaximallyImplicit as i)} :: impl,
+           Name id :: inf_names ->
+            let max = i = `MaximallyImplicit in
+            set_renamed iid id;
+            some_renaming := !some_renaming || not (Id.equal iid id);
+            (ExplByName id,max,false) :: aux_single impl inf_names
+         | { name = Name iid } :: impl,
+           Name id :: inf_names when not (Id.equal iid id) ->
+            warn_renaming_nonimplicit (id, iid);
+            aux_single impl inf_names
+         | { name = Name iid } :: impl, Name id :: inf_names
+           when not (Id.equal iid id) ->
+            aux_single impl inf_names
+         | { name = Name iid } :: impl, Name id :: inf_names ->
+            set_renamed iid id;
+            some_renaming := !some_renaming || not (Id.equal iid id);
+            aux_single impl inf_names
+         | _ :: impl, _ :: inf_names ->
+            (* no rename, no implicit status *) aux_single impl inf_names
+         | _ :: _, [] -> assert false (* checked before in check() *)
+       in
+       !some_renaming, aux l in
+  (* We check if renamed arguments do match previously declared imp args,
+   * since the system has this invariant *)
+  let some_implicits_specified =
+    match implicits with [[]] -> false | _ -> true in
   if some_renaming_specified then
     if not (List.mem `Rename flags) then
       errorlabstrm "vernac_declare_arguments"
@@ -1062,14 +1097,13 @@ let vernac_declare_arguments locality r l nargs flags =
            match !renamed_arg with
            | None -> mt ()
            | Some (o,n) ->
-              str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".")
+              str "\nArgument " ++ pr_id o ++
+              str " renamed to " ++ pr_id n ++ str ".")
     else
       Arguments_renaming.rename_arguments
-        (make_section_locality locality) sr names_decl;
+         (make_section_locality locality) sr names_decl;
   (* All other infos are in the first item of l *)
   let l = List.hd l in
-  let some_implicits_specified = match implicits with
-  | [[]] -> false | _ -> true in
   let scopes = List.map (function
     | None -> None
     | Some (o, k) ->
@@ -1080,7 +1114,7 @@ let vernac_declare_arguments locality r l nargs flags =
   let some_scopes_specified = List.exists ((!=) None) scopes in
   let rargs =
     Util.List.map_filter (function (n, true) -> Some n | _ -> None)
-      (Util.List.map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in
+      (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 l) in
   if some_scopes_specified || List.mem `ClearScopes flags then
     vernac_arguments_scope locality r scopes;
   if not some_implicits_specified && List.mem `DefaultImplicits flags then
@@ -1101,7 +1135,9 @@ let vernac_declare_arguments locality r l nargs flags =
     | ConstRef _ as c ->
        Reductionops.ReductionBehaviour.set
          (make_section_locality locality) c (rargs, nargs, flags)
-    | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
+    | _ -> errorlabstrm ""
+             (strbrk "Modifiers of the behavior of the simpl tactic "++
+              strbrk "are relevant for constants only.")
   end;
   if not (some_renaming_specified ||
           some_implicits_specified ||