Adopting the same rules for interpreting @, abbreviations and

notations in patterns than in terms, wrt implicit arguments and
scopes.

See file Notations2.v for the conventions in use in terms.

Somehow this could be put in 8.5 since it puts in agreement the
interpretation of abbreviations and notations in "symmetric patterns"
to what is done in terms (even though the interpretation rules for
terms are a bit ad hoc).

There is one exception: in terms, "(foo args) args'" deactivates the
implicit arguments and scopes in args'. This is a bit complicated to
implement in patterns so the syntax is not supported (and anyway, this
convention is a bit questionable).

4 files changed, 80 insertions, 68 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b62df8dfff..fa38695705 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -918,7 +918,7 @@ let chop_params_pattern loc ind args with_letin =
   args
 
 let find_constructor loc add_params ref =
-  let cstr = match ref with
+  let (ind,_ as cstr) = match ref with
   | ConstructRef cstr -> cstr
   | IndRef _ ->
     let error = str "There is an inductive name deep in a \"in\" clause." in
@@ -927,15 +927,15 @@ let find_constructor loc add_params ref =
     let error = str "This reference is not a constructor." in
     user_err_loc (loc, "find_constructor", error)
   in
-  cstr, (function (ind,_ as c) -> match add_params with
-    |Some nb_args ->
+  cstr, match add_params with
+    | Some nb_args ->
       let nb =
-        if Int.equal nb_args (Inductiveops.constructor_nrealdecls c)
+        if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr)
           then Inductiveops.inductive_nparamdecls ind
           else Inductiveops.inductive_nparams ind
       in
       List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))])
-    |None -> []) cstr
+    | None -> []
 
 let find_pattern_variable = function
   | Ident (loc,id) -> id
@@ -1099,16 +1099,17 @@ let drop_notations_pattern looked_for =
 	let (vars,a) = Syntax_def.search_syntactic_definition sp in
 	(match a with
 	| NRef g ->
+          (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	  test_kind top g;
 	  let () = assert (List.is_empty vars) in
 	  let (_,argscs) = find_remaining_scopes [] pats g in
 	  Some (g, [], List.map2 (in_pat_sc env) argscs pats)
-	| NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *)
+	| NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
 	      test_kind top g;
               let () = assert (List.is_empty vars) in
-	      let (argscs,_) = find_remaining_scopes pats [] g in
-	      Some (g, List.map2 (in_pat_sc env) argscs pats, [])
+	      Some (g, List.map (in_pat false env) pats, [])
 	| NApp (NRef g,args) ->
+              (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
 	      test_kind top g;
 	      let nvars = List.length vars in
 	      if List.length pats < nvars then error_not_enough_arguments loc;
@@ -1146,12 +1147,18 @@ let drop_notations_pattern looked_for =
 	  | Some (a,b,c) -> RCPatCstr(loc, a, b, c)
 	  | None -> raise (InternalizationError (loc,NotAConstructor head))
       end
-    | CPatCstr (loc, r, Some expl_pl, pl) ->
+     | CPatCstr (loc, r, Some expl_pl, pl) ->
       let g = try locate (snd (qualid_of_reference r))
 	      with Not_found ->
  	      raise (InternalizationError (loc,NotAConstructor r)) in
-      let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in
-      RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl)
+      if expl_pl == [] then
+        (* Convention: (@r) deactivates all further implicit arguments and scopes *)
+        RCPatCstr (loc, g, List.map (in_pat false env) pl, [])
+      else
+        (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
+        (* but not scopes in expl_pl *)
+        let (argscs1,_) = find_remaining_scopes expl_pl pl g in
+        RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl @ List.map (in_pat false env) pl, [])
     | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[])
 	when Bigint.is_strictly_pos p ->
       fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p))
@@ -1203,8 +1210,8 @@ let drop_notations_pattern looked_for =
       ensure_kind top loc g;
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
       RCPatCstr (loc, g,
-		 List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl,
-		 List.map2 (in_pat_sc env) argscs2 args)
+		 List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl @
+		 List.map (in_pat false env) args, [])
     | NList (x,_,iter,terminator,lassoc) ->
       if not (List.is_empty args) then user_err_loc
         (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns.");
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index f5855a971e..efd5129b66 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -40,7 +40,7 @@ type raw_cases_pattern_expr =
   | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
   | RCPatCstr of Loc.t * Globnames.global_reference
     * raw_cases_pattern_expr list * raw_cases_pattern_expr list
-  (** [CPatCstr (_, c, l1, l2)] represents (@c l1) l2 *)
+  (** [CPatCstr (_, c, l1, l2)] represents ((@c l1) l2) *)
   | RCPatAtom of Loc.t * Id.t option
   | RCPatOr of Loc.t * raw_cases_pattern_expr list
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index b11204cbc5..7e470e8445 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -380,6 +380,9 @@ GEXTEND Gram
       [ p = pattern; lp = LIST1 NEXT ->
         (match p with
 	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
+	  | CPatCstr (_, r, None, l2) -> Errors.user_err_loc
+              (cases_pattern_expr_loc p, "compound_pattern",
+               Pp.str "Nested applications not supported.")
 	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
 	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
           | _ -> Errors.user_err_loc
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index ac41819f56..9505a56e3f 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -1,40 +1,33 @@
 (* This file is giving some examples about how implicit arguments and
-   scopes are (inconsistently) treated when using abbreviations or
-   notations, in terms or patterns, or when using @ and parentheses in
-   terms and patterns *)
-
-(* One compromise would be that:
-   - Neither abbreviations nor notations break implicit arguments and
-     scopes unless the head constant is with @ and surrounded with parentheses.
-     + This would change 3. terms and patterns to behave like 4. terms,
-       with former behavior possible by using instead (@pair' _ x%nat)
-       or (pair' x%nat).
-     + This would change 4. patterns to behave like 4. terms, introducing the
-       possibibility to have the deactivation in patterns, as it is in terms,
-       by using (@pair').
-     + This would change 5. terms to behave like 5. patterns, introducing the
-       possibibility to have the activation behavior in terms, as it with
-       abbreviations, using either (@(pair') _ x%nat) or (pair' _ x).
-     + This would change 6. patterns to behave like 6. terms, introducing the
-       possibibility to have the deactivation behavior in patterns, as it with
-       abbreviations in terms, using either (@(pair') _ x%nat) or (pair' _ x).
-   - "(foo args)" directly in terms would still deactivation implicit
-     arguments and scopes for further arguments, as of today.
-   - "(@foo args)" directly in terms would deactivate implicit arguments and scopes
-     in args as of today, but not for further arguments, on the contrary of today
-   - "((@foo) args)" directly in terms would deactivate implicit
-     arguments and scopes in args and for further arguments, as it is today
-
-   Then, in both terms and patterns:
-   - "(@foo args)" in an abbreviation or notation would behave the same as
-     "(@foo args)" when expanded, i.e. with deactivation of implicit arguments
-     and scopes only for args, but not for further arguments.
-   - "((@foo) args)" in an abbreviation or notation would behave the same as
-     "((@foo) args)" when expanded, i.e. with deactivation of implicit arguments and scopes.
-   - "(foo args)" in an abbreviation or notation would behave the same as
-     "foo args" when expanded, i.e. with no change on implicit arguments and scopes.
+   scopes are treated when using abbreviations or notations, in terms
+   or patterns, or when using @ and parentheses in terms and patterns.
+
+The convention is:
+
+Constant foo with implicit arguments and scopes used in a term or a pattern:
+
+       foo      do not deactivate further arguments and scopes
+       @foo     deactivates further arguments and scopes
+       (foo x)  deactivates further arguments and scopes
+       (@foo x) deactivates further arguments and scopes
+
+Notations binding to foo:
+
+#   := foo      do not deactivate further arguments and scopes
+#   := @foo     deactivates further arguments and scopes
+# x := foo x    deactivates further arguments and scopes
+# x := @foo x   deactivates further arguments and scopes
+
+Abbreviations binding to foo:
+
+f   := foo      do not deactivate further arguments and scopes
+f   := @foo     deactivates further arguments and scopes
+f x := foo x    do not deactivate further arguments and scopes
+f x := @foo x   do not deactivate further arguments and scopes
 *)
 
+(* One checks that abbreviations and notations in patterns now behave like in terms *)
+
 Inductive prod' A : Type -> Type :=
 | pair' (a:A) B (b:B) (c:bool) : prod' A B.
 Arguments pair' [A] a%bool_scope [B] b%bool_scope c%bool_scope.
@@ -46,14 +39,13 @@ Check pair' 0 0 0 : prod' bool bool.
 Check (pair' 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *)
 Check c1 0 0 0 : prod' bool bool.
 Check fun x : prod' bool bool => match x with c1 0 y 0 => 2 | _ => 1 end.
-Check fun x : prod' bool bool => match x with (pair' 0) y 0 => 2 | _ => 1 end. (* Inconsistent with terms *)
 
 (* 2. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
 Notation c2 x := (@pair' _ x).
 Check (@pair' _ 0) _ 0%bool 0%bool : prod' bool bool. (* parentheses are blocking implicit and scopes *)
 Check c2 0 0 0 : prod' bool bool.
 Check fun A (x : prod' bool A) => match x with c2 0 y 0 => 2 | _ => 1 end.
-Check fun A (x : prod' bool A) => match x with (@pair' _ 0) y 0 => 2 | _ => 1 end. (* Inconsistent with terms *)
+Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _ => 1 end.
 
 (* 3. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
 Notation c3 x := ((@pair') _ x).
@@ -61,30 +53,40 @@ Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking impl
 Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *)
 Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *)
 Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end.
-(* Check fun A (x :prod' nat A) => match x with ((@pair') _ 0) y 0 => 2 | _ => 1 end.*)
 
 (* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
-(* unless an atomic @ is given, in terms but not in patterns *)
+(* unless an atomic @ is given *)
 Notation c4 := (@pair').
 Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
-Check c4 _ 0 _ 0 0%bool : prod' nat nat. (* all 0 are in nat_scope: would there be incompatibilities to change that? *)
-Check fun A (x :prod' bool A) => match x with c4 _ 0 _ y 0 => 2 | _ => 1 end. (* Inconsistent with terms: both 0 are in bool_scope *)
-Check fun A (x :prod' nat A) => match x with (@pair') _ 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: the implicit arguments and scopes are not deactivated *)
+Check c4 _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with c4 _ 0%bool _ y 0%bool => 2 | _ => 1 end.
+Check fun A (x :prod' bool A) => match x with (@pair') _ 0%bool _ y 0%bool => 2 | _ => 1 end.
 
 (* 5. Notations stop further implicit arguments to be inserted and scopes to be used *)
-(* in terms but not in patterns *)
-Notation "% x" := (pair' x) (at level 0, x at level 0).
+Notation "# x" := (pair' x) (at level 0, x at level 1).
 Check pair' 0 0 0 : prod' bool bool.
-Check % 0 _ 0 0%bool : prod' bool nat. (* last two 0 are in nat_scope *)
-Check fun A (x :prod' bool A) => match x with % 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: both 0 are in bool_scope *)
-Check fun A (x :prod' bool A) => match x with pair' 0 y 0 => 2 | _ => 1 end.
+Check # 0 _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with # 0 _ y 0%bool => 2 | _ => 1 end.
 
 (* 6. Notations stop further implicit arguments to be inserted and scopes to be used *)
-(* in terms but not in patterns *)
-Notation "% x" := ((@pair') _ x%nat) (at level 0, x at level 0).
-Check (@pair') _ 0 _ 0%bool 0%bool : prod' nat bool.
-Check ((@pair') _ 0) _ 0%bool 0%bool : prod' nat bool.
-Check % 0 _ 0 0%bool : prod' nat nat. (* last two 0 are in nat_scope *)
-Check fun A (x :prod' nat A) => match x with % 0 y 0 => 2 | _ => 1 end. (* Inconsistent with terms: last 0 is in bool_scope, and implicit is not given *)
-Check fun A (x :prod' bool A) => match x with (@pair') 0 y 0 => 2 | _ => 1 end. (* inconsistent with terms: the implicit arguments and scopes are not deactivated *)
-Check fun A (x :prod' nat A) => match x with ((@pair') _) 0 y 0 => 2 | _ => 1 end.
+Notation "## x" := ((@pair') _ x) (at level 0, x at level 1).
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool.
+Check ## 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ## 0%bool _ y 0%bool => 2 | _ => 1 end.
+
+(* 7. Notations stop further implicit arguments to be inserted and scopes to be used *)
+Notation "###" := (@pair') (at level 0).
+Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check ### _ 0%bool _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ### _ 0%bool _ y 0%bool => 2 | _ => 1 end.
+
+(* 8. Notations w/o @ preserves implicit arguments and scopes *)
+Notation "####" := pair' (at level 0).
+Check #### 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
+
+(* 9. Notations w/o @ but arguments do not preserve further implicit arguments and scopes *)
+Notation "##### x" := (pair' x) (at level 0, x at level 1).
+Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.