Arguments supports extra notation scopes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 46 insertions, 10 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index d056149897..a2e053ab8c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -656,6 +656,7 @@ GEXTEND Gram
       | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
       | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
       | IDENT "rename" -> [`Rename]
+      | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes]
       | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
           [`ClearImplicits; `ClearScopes]
       | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index cff1a53080..5a8f2db79a 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -810,6 +810,7 @@ let rec pr_vernac = function
         | `SimplNeverUnfold -> str "simpl never"
         | `DefaultImplicits -> str "default implicits"
         | `Rename -> str "rename"
+        | `ExtraScopes -> str "extra scopes"
         | `ClearImplicits -> str "clear implicits"
         | `ClearScopes -> str "clear scopes")
         mods)
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 139f9e9922..7c9b1e27cf 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -91,3 +91,11 @@ The simpl tactic unfolds f
   when the 5th, 6th and 7th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.f
+forall w : r, w 3 true = tt
+     : Prop
+The command has indeed failed with message:
+=> Error: Unknown interpretation for notation "$".
+w 3 true = tt
+     : Prop
+The command has indeed failed with message:
+=> Error: Extra argument _.
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 3a94f19a71..573cfdab22 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -38,3 +38,15 @@ End S1.
 About f.
 Arguments f : clear implicits and scopes.
 About f.
+Record r := { pi :> nat -> bool -> unit }.
+Notation "$" := 3 (only parsing) : foo_scope.
+Notation "$" := true (only parsing) : bar_scope.
+Delimit Scope bar_scope with B.
+Arguments pi _ _%F _%B. 
+Check (forall w : r, pi w $ $ = tt).
+Fail Check (forall w : r, w $ $ = tt).
+Axiom w : r.
+Arguments w  _%F _%B : extra scopes.
+Check (w $ $ = tt).
+Fail Arguments w  _%F _%B.
+
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b99cc02a39..f7466d0371 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -772,8 +772,10 @@ let vernac_declare_implicits local r = function
 	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
 let vernac_declare_arguments local 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, rest = List.hd names, List.tl names in
+  let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in
   if List.exists ((<>) names) rest then
     error "All arguments lists must declare the same names.";
   if not (Util.list_distinct (List.filter ((<>) Anonymous) names)) then
@@ -782,14 +784,26 @@ let vernac_declare_arguments local r l nargs flags =
   let inf_names =
     Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in
   let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in
-  let rec check li ld = match li, ld with
-    | [], [] -> ()
-    | [], x::_ -> error ("Extra argument " ^ string_of_name x ^ ".")
-    | l, [] -> error ("The following arguments are not declared: " ^
+  let rec check li ld ls = match li, ld, ls with
+    | [], [], [] -> ()
+    | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls
+    | [], _::_, (Some _)::ls when extra_scope_flag ->
+       error "Extra notation scopes can be set on anonymous arguments only"
+    | [], x::_, _ -> error ("Extra argument " ^ string_of_name x ^ ".")
+    | l, [], _ -> error ("The following arguments are not declared: " ^
        (String.concat ", " (List.map string_of_name l)) ^ ".")
-    | _::li, _::ld -> check li ld in
+    | _::li, _::ld, _::ls -> check li ld ls 
+    | _ -> assert false in
   if l <> [[]] then
-    List.iter (fun l -> check inf_names l) (names :: rest);
+    List.iter2 (fun l -> check inf_names l) (names :: rest) scopes;
+  (* we take extra scopes apart, and we check they are consistent *)
+  let l, scopes = 
+    let scopes, rest = List.hd scopes, List.tl scopes in
+    if List.exists (List.exists ((<>) None)) rest then
+      error "Notation scopes can be given only once";
+    if not extra_scope_flag then l, scopes else
+    let l, _ = List.split (List.map (list_chop (List.length inf_names)) l) in
+    l, scopes in
   (* we interpret _ as the inferred names *)
   let l = if l = [[]] then l else
     let name_anons = function
@@ -822,10 +836,10 @@ let vernac_declare_arguments local r l nargs flags =
   let l = List.hd l in
   let some_implicits_specified = implicits <> [[]] in
   let scopes = List.map (function
-    | (_,_, None,_,_) -> None
-    | (_,_, Some (o, k), _,_) -> 
+    | None -> None
+    | Some (o, k) -> 
         try Some(ignore(Notation.find_scope k); k)
-        with _ -> Some (Notation.find_delimiters_scope o k)) l in
+        with _ -> Some (Notation.find_delimiters_scope o k)) scopes in
   let some_scopes_specified = List.exists ((<>) None) scopes in
   let rargs =
     Util.list_map_filter (function (n, true) -> Some n | _ -> None)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 6566fe59cd..78207f6a24 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -317,7 +317,7 @@ type vernac_expr =
       (explicitation * bool * bool) list list
   | VernacArguments of locality_flag * reference or_by_notation * 
       ((name * bool * (loc * string) option * bool * bool) list) list *
-      int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename
+      int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes
             | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
   | VernacArgumentsScope of locality_flag * reference or_by_notation *
       scope_name option list