Generalized the possibility to refer to a global name by a notation

string in most commands expecting a global name (e.g. 'Print "+"' for
an infix notation or 'Print "{ _ } + { _ }"' for a misfix notation,
possibly surrounded by a scope delimiter). Support for such smart
globals in VERNAC EXTEND to do.

Added a file smartlocate.ml for high-level globalization functions.

Mini-nettoyage metasyntax.ml.



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

10 files changed, 116 insertions, 50 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index d38ef592fc..6879dc9659 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -15,7 +15,7 @@ open Term
 open Libnames
 open Pattern
 open Nametab
-open Syntax_def
+open Smartlocate
 
 (************************************************************************)
 (* Generic functions to find Coq objects *)
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 8724b0bfd6..c6dc12164e 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -47,7 +47,11 @@ type argument_type =
 type 'a and_short_name = 'a * identifier located option
 type 'a or_by_notation =
   | AN of 'a
-  | ByNotation of loc * string * Notation.delimiters option
+  | ByNotation of (loc * string * Notation.delimiters option)
+
+let loc_of_or_by_notation f = function
+  | AN c -> f c
+  | ByNotation (loc,s,_) -> loc
 
 type rawconstr_and_expr = rawconstr * constr_expr option
 type open_constr_expr = unit * constr_expr
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 9072456c3e..e6747db171 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -21,7 +21,9 @@ type 'a and_short_name = 'a * identifier located option
 
 type 'a or_by_notation =
   | AN of 'a
-  | ByNotation of loc * string * Notation.delimiters option
+  | ByNotation of (loc * string * Notation.delimiters option)
+
+val loc_of_or_by_notation : ('a -> loc) -> 'a or_by_notation -> loc
 
 (* In globalize tactics, we need to keep the initial [constr_expr] to recompute*)
 (* in the environment by the effective calls to Intro, Inversion, etc *)
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 234487bc9d..991cfac57b 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -4,7 +4,8 @@ Ppextend
 Notation
 Dumpglob
 Genarg 
-Syntax_def 
+Syntax_def
+Smartlocate
 Reserve
 Impargs 
 Implicit_quantifiers
diff --git a/interp/notation.ml b/interp/notation.ml
index 08936759dd..58c28149dd 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -536,7 +536,7 @@ let decompose_notation_key s =
     let tok =
       match String.sub s n (pos-n) with
       | "_" -> NonTerminal (id_of_string "_")
-      | s -> Terminal s in
+      | s -> Terminal (drop_simple_quotes s) in
     decomp_ntn (tok::dirs) (pos+1)	  
   in
     decomp_ntn [] 0
@@ -650,15 +650,16 @@ let interp_notation_as_global_reference loc test ntn sc =
       | [] -> error_notation_not_reference loc ntn
       | _ -> error_ambiguous_notation loc ntn
 
-let locate_notation prraw ntn =
+let locate_notation prraw ntn scope =
   let ntns = factorize_entries (browse_notation false ntn !scope_map) in
+  let scopes = Option.fold_right push_scope scope !scope_stack in
   if ntns = [] then
     str "Unknown notation"
   else
     t (str "Notation            " ++
     tab () ++ str "Scope     " ++ tab () ++ fnl () ++ 
     prlist (fun (ntn,l) ->
-      let scope = find_default ntn !scope_stack in
+      let scope = find_default ntn scopes in
       prlist 
 	(fun (sc,r,(_,df)) ->
 	  hov 0 (
diff --git a/interp/notation.mli b/interp/notation.mli
index 21d3ae1a08..57e0deb10a 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -167,7 +167,8 @@ val decompose_notation_key : notation -> symbol list
 (* Prints scopes (expect a pure aconstr printer *)
 val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
 val pr_scopes : (rawconstr -> std_ppcmds) -> std_ppcmds
-val locate_notation : (rawconstr -> std_ppcmds) -> notation -> std_ppcmds
+val locate_notation : (rawconstr -> std_ppcmds) -> notation -> 
+      scope_name option -> std_ppcmds
 
 val pr_visibility: (rawconstr -> std_ppcmds) -> scope_name option -> std_ppcmds
 
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
new file mode 100644
index 0000000000..07ae87fa08
--- /dev/null
+++ b/interp/smartlocate.ml
@@ -0,0 +1,62 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Created by Hugo Herbelin from code formerly dispatched in
+   syntax_def.ml or tacinterp.ml, Sep 2009 *)
+
+(* This file provides high-level name globalization functions *)
+
+(* $Id:$ *)
+
+(* *)
+open Pp
+open Util
+open Names
+open Libnames
+open Genarg
+open Syntax_def
+open Topconstr
+
+let global_of_extended_global = function
+  | TrueGlobal ref -> ref
+  | SynDef kn -> 
+  match search_syntactic_definition dummy_loc kn with
+  | [],ARef ref -> ref
+  | _ -> raise Not_found
+
+let locate_global_with_alias (loc,qid) =
+  let ref = Nametab.locate_extended qid in
+  try global_of_extended_global ref
+  with Not_found ->
+    user_err_loc (loc,"",pr_qualid qid ++ 
+      str " is bound to a notation that does not denote a reference")
+
+let global_inductive_with_alias r =
+  match locate_global_with_alias (qualid_of_reference r) with
+  | IndRef ind -> ind
+  | ref ->
+      user_err_loc (loc_of_reference r,"global_inductive",
+        pr_reference r ++ spc () ++ str "is not an inductive type")
+
+let global_with_alias r =
+  let (loc,qid as lqid) = qualid_of_reference r in
+  try locate_global_with_alias lqid
+  with Not_found -> Nametab.error_global_not_found_loc loc qid
+
+let smart_global = function
+  | AN r ->
+      global_with_alias r
+  | ByNotation (loc,ntn,sc) ->
+      Notation.interp_notation_as_global_reference loc (fun _ -> true) ntn sc
+
+let smart_global_inductive = function
+  | AN r ->
+      global_inductive_with_alias r
+  | ByNotation (loc,ntn,sc) ->
+      destIndRef
+        (Notation.interp_notation_as_global_reference loc isIndRef ntn sc)
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
new file mode 100644
index 0000000000..682484f57f
--- /dev/null
+++ b/interp/smartlocate.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+open Util
+open Names
+open Libnames
+open Genarg
+
+(* [locate_global_with_alias] locates global reference possibly following
+   a notation if this notation has a role of aliasing; raise Not_found
+   if not bound in the global env; raise an error if bound to a
+   syntactic def that does not denote a reference *)
+
+val locate_global_with_alias : qualid located -> global_reference
+
+(* Extract a global_reference from a reference that can be an "alias" *)
+val global_of_extended_global : extended_global_reference -> global_reference
+
+(* Locate a reference taking into account possible "alias" notations *)
+val global_with_alias : reference -> global_reference
+
+(* The same for inductive types *)
+val global_inductive_with_alias : reference -> inductive
+
+(* Locate a reference taking into account notations and "aliases" *)
+val smart_global : reference or_by_notation -> global_reference
+
+(* The same for inductive types *)
+val smart_global_inductive : reference or_by_notation -> inductive
+
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 1619bad278..e58bb000a0 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -81,29 +81,3 @@ let declare_syntactic_definition local id onlyparse pat =
 
 let search_syntactic_definition loc kn =
   out_pat (KNmap.find kn !syntax_table)
-
-let global_of_extended_global = function
-  | TrueGlobal ref -> ref
-  | SynDef kn -> 
-  match search_syntactic_definition dummy_loc kn with
-  | [],ARef ref -> ref
-  | _ -> raise Not_found
-
-let locate_global_with_alias (loc,qid) =
-  let ref = Nametab.locate_extended qid in
-  try global_of_extended_global ref
-  with Not_found ->
-    user_err_loc (loc,"",pr_qualid qid ++ 
-      str " is bound to a notation that does not denote a reference")
-
-let global_inductive_with_alias r =
-  match locate_global_with_alias (qualid_of_reference r) with
-  | IndRef ind -> ind
-  | ref ->
-      user_err_loc (loc_of_reference r,"global_inductive",
-        pr_reference r ++ spc () ++ str "is not an inductive type")
-
-let global_with_alias r =
-  let (loc,qid as lqid) = qualid_of_reference r in
-  try locate_global_with_alias lqid
-  with Not_found -> Nametab.error_global_not_found_loc loc qid
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index fb0c3c9f28..3ba78e91d9 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -25,19 +25,3 @@ val declare_syntactic_definition : bool -> identifier -> bool ->
   syndef_interpretation -> unit
 
 val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation
-
-(* [locate_global_with_alias] locates global reference possibly following
-   a notation if this notation has a role of aliasing; raise Not_found
-   if not bound in the global env; raise an error if bound to a
-   syntactic def that does not denote a reference *)
-
-val locate_global_with_alias : qualid located -> global_reference
-
-(* Extract a global_reference from a reference that can be an "alias" *)
-val global_of_extended_global : extended_global_reference -> global_reference
-
-(* Locate a reference taking into account possible "alias" notations *)
-val global_with_alias : reference -> global_reference
-
-(* The same for inductive types *)
-val global_inductive_with_alias : reference -> inductive