Merge PR #13776: Fix #13739 - disable some warnings when calling Function.

Reviewed-by: gares
Ack-by: Zimmi48
Ack-by: SkySkimmer

7 files changed, 79 insertions, 6 deletions

diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index cc1fa647f9..ee7dab92bc 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -173,3 +173,9 @@ let create ~name ~category ?(default=Enabled) pp =
     | Disabled -> ()
     | AsError -> CErrors.user_err ?loc (pp x)
     | Enabled -> Feedback.msg_warning ?loc (pp x)
+
+(* Remark: [warn] does not need to start with a comma, but if present
+   it won't hurt (",," is normalized into ","). *)
+let with_warn warn (f:'b -> 'a) x =
+  let s = get_flags () in
+  Util.try_finally (fun x -> set_flags (s^","^warn);f x) x set_flags s
diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli
index ded1f9be3b..b63eed09d0 100644
--- a/lib/cWarnings.mli
+++ b/lib/cWarnings.mli
@@ -19,3 +19,10 @@ val set_flags : string -> unit
 (** Cleans up a user provided warnings status string, e.g. removing unknown
     warnings (in which case a warning is emitted) or subsumed warnings . *)
 val normalize_flags_string : string -> string
+
+(** [with_warn "-xxx,+yyy..." f x] calls [f x] after setting the
+   warnings as specified in the string (keeping other previously set
+   warnings), and restores current warnings after [f()] returns or
+   raises an exception. If both f and restoring the warnings raise
+   exceptions, the latter is raised. *)
+val with_warn: string -> ('b -> 'a) -> 'b -> 'a
diff --git a/lib/util.ml b/lib/util.ml
index 87cc30e557..e8aa0f3e48 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -135,6 +135,13 @@ type 'a delayed = unit -> 'a
 
 let delayed_force f = f ()
 
+(* finalize - Credit X.Leroy, D.Remy. *)
+let try_finally f x finally y =
+  let res = try f x with exn -> finally y; raise exn in
+  finally y;
+  res
+
+
 (* Misc *)
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
diff --git a/lib/util.mli b/lib/util.mli
index fe34525671..aefb015c38 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -112,6 +112,15 @@ type 'a delayed = unit -> 'a
 
 val delayed_force : 'a delayed -> 'a
 
+(** [try_finally f x g y] applies the main code [f] to [x] and
+   returns the result after having applied the finalization
+   code [g] to [y]. If the main code raises the exception
+   [exn], the finalization code is executed and [exn] is raised.
+   If the finalization code itself fails, the exception
+   returned is always the one from the finalization code.
+   Credit X.Leroy, D.Remy. *)
+val try_finally: ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b
+
 (** {6 Enriched exceptions} *)
 
 type iexn = Exninfo.iexn
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ca6ae150a7..15cf88f827 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -195,16 +195,29 @@ let is_interactive recsl =
 
 }
 
+(* For usability we temporarily switch off some flags during the call
+   to Function. However this is not satisfactory:
+
+ 1- Function should not warn "non-recursive" and call the Definition
+    mechanism instead of Fixpoint when needed
+
+ 2- Only for automatically generated names should
+    unused-pattern-matching-variable be ignored. *)
+
 VERNAC COMMAND EXTEND Function STATE CUSTOM
 | ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
     => { classify_funind recsl }
     -> {
-         if is_interactive recsl then
-           Vernacextend.VtOpenProof (fun () ->
-             Gen_principle.do_generate_principle_interactive (List.map snd recsl))
-         else
-           Vernacextend.VtDefault (fun () ->
-             Gen_principle.do_generate_principle (List.map snd recsl)) }
+    let warn = "-unused-pattern-matching-variable,-matching-variable,-non-recursive" in
+    if is_interactive recsl then
+      Vernacextend.VtOpenProof (fun () ->
+          CWarnings.with_warn warn
+            Gen_principle.do_generate_principle_interactive (List.map snd recsl))
+    else
+      Vernacextend.VtDefault (fun () ->
+          CWarnings.with_warn warn
+            Gen_principle.do_generate_principle (List.map snd recsl))
+  }
 END
 
 {
diff --git a/test-suite/output/Function.out b/test-suite/output/Function.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/Function.out
diff --git a/test-suite/output/Function.v b/test-suite/output/Function.v
new file mode 100644
index 0000000000..b3e2a93895
--- /dev/null
+++ b/test-suite/output/Function.v
@@ -0,0 +1,31 @@
+Require Import FunInd List.
+
+(* Explanations: This kind of pattern matching displays a legitimate
+   unused variable warning in v8.13.
+
+Fixpoint f (l:list nat) : nat :=
+  match l with
+  | nil => O
+  | S n :: nil  => 1
+  | x :: l'  => f l'
+  end.
+*)
+
+(* In v8.13 the same code with "Function" generates a lot more
+   warnings about variables created automatically by Function. These
+   are not legitimate. PR #13776 (post v8.13) removes all warnings
+   about pattern matching variables (and non truly recursive fixpoint)
+   for "Function". So this should not generate any warning. Note that
+   this PR removes also the legitimate warnings. It would be better if
+   this test generate the same warning as the Fixpoint above. This
+   test would then need to be updated. *)
+
+(* Ensuring the warning is a warning. *)
+Set Warnings "matching-variable".
+(* But no warning generated here. *)
+Function f (l:list nat) : nat :=
+  match l with
+  | nil => O
+  | S n :: nil  => 1
+  | n :: l'  => f l'
+  end.