Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a coercion not being used

Reviewed-by: ejgallego

5 files changed, 115 insertions, 64 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cf88036f73..378adb566c 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -800,19 +800,21 @@ let extern_args extern env args =
 let match_coercion_app c = match DAst.get c with
   | GApp (r, args) ->
     begin match DAst.get r with
-    | GRef (r,_) -> Some (c.CAst.loc, r, 0, args)
+    | GRef (r,_) -> Some (c.CAst.loc, r, args)
     | _ -> None
     end
   | _ -> None
 
 let remove_one_coercion inctx c =
   try match match_coercion_app c with
-  | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
+  | Some (loc,r,args) when not (!Flags.raw_print || !print_coercions) ->
       let nargs = List.length args in
       (match Coercionops.hide_coercion r with
-          | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
+          | Some nparams when
+                 let inctx = inctx || (* coercion to funclass implying being in context *) nparams+1 < nargs in
+                 nparams < nargs && inctx ->
               (* We skip the coercion *)
-              let l = List.skipn (n - pars) args in
+              let l = List.skipn nparams args in
               let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
               (* Don't flatten App's in case of funclass so that
                  (atomic) notations on [a] work; should be compatible
@@ -824,7 +826,7 @@ let remove_one_coercion inctx c =
                  have been made explicit to match *)
               let a' = if List.is_empty l then a else DAst.make ?loc @@ GApp (a,l) in
               let inctx = inctx || not (List.is_empty l) in
-              Some (n-pars+1, inctx, a')
+              Some (nparams+1, inctx, a')
           | _ -> None)
   | _ -> None
   with Not_found ->
@@ -867,7 +869,7 @@ let filter_enough_applied nargs l =
   | Some nargs ->
   List.filter (fun (keyrule,pat,n as _rule) ->
       match n with
-      | AppBoundedNotation n -> n > nargs
+      | AppBoundedNotation n -> n >= nargs
       | AppUnboundedNotation | NotAppNotation -> false) l
 
 (* Helper function for safe and optimal printing of primitive tokens  *)
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index df64ae2af3..3477a293e3 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -31,12 +31,6 @@ end
      : Expr -> Expr
 [(1 + 1)]
      : Expr
-Let "x" e1 e2
-     : expr
-Let "x" e1 e2
-     : expr
-Let "x" e1 e2 : list string
-     : list string
 myAnd1 True True
      : Prop
 r 2 3
@@ -65,8 +59,6 @@ where
       |- Type] (pat, p0, p cannot be used)
 fun '{| |} => true
      : R -> bool
-b = a
-     : Prop
 The command has indeed failed with message:
 The format is not the same on the right- and left-hand sides of the special token "..".
 The command has indeed failed with message:
@@ -85,18 +77,18 @@ fun x : nat => [x]
      : nat -> nat
 ∀ x : nat, x = x
      : Prop
-File "stdin", line 226, characters 0-160:
+File "stdin", line 184, characters 0-160:
 Warning: Notation "∀ _ .. _ , _" was already defined with a different format
 in scope type_scope. [notation-incompatible-format,parsing]
 ∀x : nat,x = x
      : Prop
-File "stdin", line 239, characters 0-60:
+File "stdin", line 197, characters 0-60:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 243, characters 0-64:
+File "stdin", line 201, characters 0-64:
 Warning: Notation "_ %%% _" was already defined with a different format.
 [notation-incompatible-format,parsing]
-File "stdin", line 248, characters 0-62:
+File "stdin", line 206, characters 0-62:
 Warning: Lonely notation "_ %%%% _" was already defined with a different
 format. [notation-incompatible-format,parsing]
 3  %%  4
@@ -105,10 +97,10 @@ format. [notation-incompatible-format,parsing]
      : nat
 3   %%   4
      : nat
-File "stdin", line 276, characters 0-61:
+File "stdin", line 234, characters 0-61:
 Warning: The format modifier is irrelevant for only parsing rules.
 [irrelevant-format-only-parsing,parsing]
-File "stdin", line 280, characters 0-63:
+File "stdin", line 238, characters 0-63:
 Warning: The only parsing modifier has no effect in Reserved Notation.
 [irrelevant-reserved-notation-only-parsing,parsing]
 fun x : nat => U (S x)
@@ -119,7 +111,7 @@ fun x : nat => V x
      : forall x : nat, nat * (?T -> ?T)
 where
 ?T : [x : nat  x0 : ?T |- Type] (x0 cannot be used)
-File "stdin", line 297, characters 0-30:
+File "stdin", line 255, characters 0-30:
 Warning: Notation "_ :=: _" was already used. [notation-overridden,parsing]
 0 :=: 0
      : Prop
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ce488fe18d..ebad12af88 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -79,35 +79,7 @@ Check [1 + 1].
 
 End C.
 
-(* An example of interaction between coercion and notations from
-   Robbert Krebbers. *)
-
-Require Import String.
-
-Module D.
-
-Inductive expr :=
-  | Var : string -> expr
-  | Lam : string -> expr -> expr
-  | App : expr -> expr -> expr.
-
-Notation Let x e1 e2 := (App (Lam x e2) e1).
-
-Parameter e1 e2 : expr.
-
-Check (Let "x" e1 e2).
-
-Coercion App : expr >-> Funclass.
-
-Check (Let "x" e1 e2).
-
-Axiom free_vars :> expr -> list string.
-
-Check (Let "x" e1 e2) : list string.
-
-End D.
-
-(* Fixing bugs reported by G. Gonthier in #9207 *)
+(* Fixing overparenthesizing reported by G. Gonthier in #9207 (PR #9214, in 8.10)*)
 
 Module I.
 
@@ -152,20 +124,6 @@ Check fun '{|n:=x|} => true.
 
 End EmptyRecordSyntax.
 
-Module L.
-
-(* Testing regression #11053 *)
-
-Section Test.
-Variables (A B : Type) (a : A) (b : B).
-Variable c : A -> B.
-Coercion c : A >-> B.
-Notation COERCION := (c).
-Check b = a.
-End Test.
-
-End L.
-
 Module M.
 
 (* Accept boxes around the end variables of a recursive notation (if equal boxes) *)
diff --git a/test-suite/output/NotationsCoercions.out b/test-suite/output/NotationsCoercions.out
new file mode 100644
index 0000000000..56145e5fa5
--- /dev/null
+++ b/test-suite/output/NotationsCoercions.out
@@ -0,0 +1,22 @@
+Let "x" e1 e2
+     : expr
+Let "x" e1 e2
+     : expr
+Let "x" e1 e2 : list string
+     : list string
+b = a
+     : Prop
+foo
+     : (_ BitVec 32)
+#[ r ] 0
+     : nat
+##[ r ]
+     : nat
+##[ r ]
+     : nat
+#[ r ] 0
+     : nat
+##[ r ]
+     : nat
+##[ r ]
+     : nat
diff --git a/test-suite/output/NotationsCoercions.v b/test-suite/output/NotationsCoercions.v
new file mode 100644
index 0000000000..0524bed98c
--- /dev/null
+++ b/test-suite/output/NotationsCoercions.v
@@ -0,0 +1,77 @@
+(* Tests about skipping a coercion vs using a notation involving a coercion *)
+
+Require Import String.
+
+(* Skipping a coercion vs using a notation for the application of the
+    coercion (from Robbert Krebbers, see PR #8890) *)
+
+Module A.
+
+Inductive expr :=
+  | Var : string -> expr
+  | Lam : string -> expr -> expr
+  | App : expr -> expr -> expr.
+
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+Parameter e1 e2 : expr.
+Check (Let "x" e1 e2). (* always printed the same *)
+Coercion App : expr >-> Funclass.
+Check (Let "x" e1 e2). (* printed the same from #8890, in 8.10 *)
+Axiom free_vars :> expr -> list string.
+Check (Let "x" e1 e2) : list string. (* printed the same from #11172, in 8.12 *)
+
+End A.
+
+(* Skipping a coercion vs using a notation for the coercion itself
+   (regression #11053 in 8.10 after PR #8890, addressed by PR #11090) *)
+
+Module B.
+
+Section Test.
+Variables (A B : Type) (a : A) (b : B).
+Variable c : A -> B.
+Coercion c : A >-> B.
+Notation COERCION := (c).
+Check b = a. (* printed the same except in 8.10 *)
+End Test.
+
+End B.
+
+Module C.
+
+Record word := { rep: Type }.
+Coercion rep : word >-> Sortclass.
+Axiom myword: word.
+Axiom foo: myword.
+Notation "'(_' 'BitVec' '32)'" := (rep myword).
+Check foo. (* printed with Bitvec from #8890 in 8.10 and 8.11, regression due to #11172 in 8.12 *)
+
+End C.
+
+(* Examples involving coercions to funclass *)
+
+Module D.
+
+Record R := { f :> nat -> nat }.
+Axiom r : R.
+Notation "#[ x  ]" := (f x).
+Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *)
+Notation "##[ x  ]" := (f x 0).
+Check ##[ r ]. (* printed the same from 8.10 *)
+Check #[ r ] 0. (* printed ##[ r ] from 8.10 *)
+
+End D.
+
+(* Same examples with a parameter *)
+
+Module E.
+
+Record R A := { f :> A -> A }.
+Axiom r : R nat.
+Notation "#[ x  ]" := (f nat x).
+Check #[ r ] 0. (* printed the same from 8.10 (due to #8890), but not 8.11 and 8.12 (due to #11090) *)
+Notation "##[ x  ]" := (f nat x 0).
+Check ##[ r ]. (* printed the same from 8.10 *)
+Check #[ r ] 0. (* printed ##[ r ] from 8.10 *)
+
+End E.