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

7 files changed, 72 insertions, 87 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 82fd9bc1aa..80de344586 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -46,6 +46,7 @@ open Goptions
 open Mod_subst
 open Evd
 open Decls
+open Smartlocate
 
 let rec abstract_constr_expr c = function
   | [] -> c
@@ -930,8 +931,8 @@ requested
        let l1,l2 = split_scheme q in
     ( match t with
       | InductionScheme (x,y,z) ->
-             let ind = mkInd (Nametab.global_inductive y) in
-             let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind)
+             let ind = smart_global_inductive y in
+             let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind)
 in
              let z' = family_of_sort (interp_sort z) in
              let suffix = (
@@ -955,8 +956,8 @@ in
                        | InSet  -> "_rec_nodep"
                        | InType -> "_rect_nodep")
                 ) in
-            let newid = (string_of_id (coerce_reference_to_id y))^suffix in
-            let newref = (dummy_loc,id_of_string newid) in
+            let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
+            let newref = (dummy_loc,newid) in
           ((newref,x,y,z)::l1),l2
       | EqualityScheme  x -> l1,(x::l2)
     )
@@ -969,7 +970,7 @@ let build_induction_scheme lnamedepindsort =
   let lrecspec =
     List.map
       (fun (_,dep,indid,sort) ->
-        let ind = Nametab.global_inductive indid in
+        let ind = smart_global_inductive indid in
         let (mib,mip) = Global.lookup_inductive ind in
          (ind,mib,mip,dep,interp_elimination_sort sort)) 
       lnamedepindsort
@@ -998,7 +999,7 @@ tried to declare different schemes at once *)
     else (
       if ischeme <> [] then build_induction_scheme ischeme;
       List.iter ( fun indname -> 
-        let ind = Nametab.global_inductive indname
+        let ind = smart_global_inductive indname
         in declare_eq_scheme (fst ind);
         try
            make_eq_decidability ind 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index adf3e93a4d..54cbc0ae3c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -240,8 +240,6 @@ let parse_format (loc,str) =
 
 type symbol_token = WhiteSpace of int | String of string
 
-(* Decompose the notation string into tokens *)
-
 let split_notation_string str =
   let push_token beg i l =
     if beg = i then l else
@@ -307,10 +305,6 @@ let rec interp_list_parser hd = function
 
 (* Find non-terminal tokens of notation *)
 
-let unquote_notation_token s =
-  let n = String.length s in
-  if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
-
 let is_normal_token str =
   try let _ = Lexer.check_ident str in true with Lexer.Error _ -> false
 
@@ -321,26 +315,18 @@ let quote_notation_token x =
   if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
   else x
 
-let rec raw_analyse_notation_tokens = function
-  | []    -> [], []
-  | String ".." :: sl ->
-      let (vars,l) = raw_analyse_notation_tokens sl in
-      (list_add_set ldots_var vars, NonTerminal ldots_var :: l)
+let rec raw_analyze_notation_tokens = function
+  | []    -> []
+  | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
   | String "_" :: _ -> error "_ must be quoted."
   | String x :: sl when is_normal_token x ->
       Lexer.check_ident x;
-      let id = Names.id_of_string x in
-      let (vars,l) = raw_analyse_notation_tokens sl in
-      if List.mem id vars then
-	error ("Variable "^x^" occurs more than once.");
-      (id::vars, NonTerminal id :: l)
+      NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
       Lexer.check_keyword s;
-      let (vars,l) = raw_analyse_notation_tokens sl in
-      (vars, Terminal (unquote_notation_token s) :: l)
+      Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl
   | WhiteSpace n :: sl ->
-      let (vars,l) = raw_analyse_notation_tokens sl in
-      (vars, Break n :: l)
+      Break n :: raw_analyze_notation_tokens sl
 
 let is_numeral symbs = 
   match List.filter (function Break _ -> false | _ -> true) symbs with
@@ -349,8 +335,23 @@ let is_numeral symbs =
   | _ ->
       false
 
-let analyse_notation_tokens l =
-  let vars,l = raw_analyse_notation_tokens l in
+let rec get_notation_vars = function
+  | [] -> []
+  | NonTerminal id :: sl ->
+      let vars = get_notation_vars sl in
+      if List.mem id vars then
+        if id <> ldots_var then
+	  error ("Variable "^string_of_id id^" occurs more than once.")
+        else
+          vars
+      else
+        id::vars
+  | (Terminal _ | Break _) :: sl -> get_notation_vars sl
+  | SProdList _ :: _ -> assert false
+
+let analyze_notation_tokens l =
+  let l = raw_analyze_notation_tokens l in
+  let vars = get_notation_vars l in
   let extrarecvars,recvars,l = interp_list_parser [] l in
   (if extrarecvars = [] then [], [], vars, l
    else extrarecvars, recvars, list_subtract vars recvars, l)
@@ -538,7 +539,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
       when s' = String.make (String.length s') ' ' ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | Terminal s :: symbs, (UnpTerminal s') :: fmt
-      when s = unquote_notation_token s' ->
+      when s = drop_simple_quotes s' ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
       let i = list_index s vars in
@@ -829,7 +830,7 @@ let compute_syntax_data (df,modifiers) =
   (* Notation defaults to NONA *)
   let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
   let toks = split_notation_string df in
-  let (extrarecvars,recvars,vars,symbols) = analyse_notation_tokens toks in
+  let (extrarecvars,recvars,vars,symbols) = analyze_notation_tokens toks in
   let ntn_for_interp = make_notation_key symbols in
   let symbols' = remove_curly_brackets symbols in
   let need_squash = (symbols <> symbols') in
@@ -962,7 +963,7 @@ let add_notation_in_scope local df c mods scope =
 
 let add_notation_interpretation_core local df names c scope onlyparse =
   let dfs = split_notation_string df in
-  let (extrarecvars,recvars,vars,symbs) = analyse_notation_tokens dfs in
+  let (extrarecvars,recvars,vars,symbs) = analyze_notation_tokens dfs in
   (* Redeclare pa/pp rules *)
   if not (is_numeral symbs) then begin
     let sy_rules = recover_notation_syntax (make_notation_key symbs) in
@@ -1016,19 +1017,6 @@ let add_infix local (inf,modifiers) pr sc =
   add_notation local c (df,modifiers) sc
 
 (**********************************************************************)
-(* Miscellaneous                                                      *)
-
-let standardize_locatable_notation ntn =
-  let unquote = function
-    | String s -> [unquote_notation_token s]
-    | _ -> [] in
-  if String.contains ntn ' ' then
-    String.concat " " 
-      (List.flatten (List.map unquote (split_notation_string ntn)))
-  else
-    unquote_notation_token ntn
-
-(**********************************************************************)
 (* Delimiters and classes bound to scopes                             *)
 
 type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 29dbcb4daa..7ebb818673 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -53,10 +53,6 @@ val add_syntax_extension :
 
 val print_grammar : string -> unit
 
-(* Removes quotes in a notation *)
-
-val standardize_locatable_notation : string -> string
-
 (* Evaluate whether a notation is not printable *)
 
 val is_not_printable : aconstr -> bool
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 739193f518..887d5a6168 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -44,7 +44,7 @@ type pcoq_hook = {
   solve : int -> unit;
   abort : string -> unit;
   search : searchable -> dir_path list * bool -> unit;
-  print_name : reference -> unit;
+  print_name : reference Genarg.or_by_notation -> unit;
   print_check : Environ.env -> Environ.unsafe_judgment -> unit;
   print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
     Environ.unsafe_judgment -> unit;
@@ -59,7 +59,7 @@ let set_pcoq_hook f = pcoq := Some f
 let cl_of_qualid = function
   | FunClass -> Classops.CL_FUN
   | SortClass -> Classops.CL_SORT
-  | RefClass r -> Class.class_of_global (global_with_alias r)
+  | RefClass r -> Class.class_of_global (Smartlocate.smart_global r)
 
 (*******************)
 (* "Show" commands *)
@@ -278,9 +278,9 @@ let print_located_module r =
 	str "No module is referred to by name ") ++ pr_qualid qid
   in msgnl msg  
 
-let global_with_alias r =
-  let gr = global_with_alias r in
-    Dumpglob.add_glob (loc_of_reference r) gr;
+let smart_global r =
+  let gr = Smartlocate.smart_global r in
+    Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr;
     gr
 
 (**********)
@@ -296,7 +296,7 @@ let vernac_bind_scope sc cll =
 let vernac_open_close_scope = Notation.open_close_scope
 
 let vernac_arguments_scope local r scl =
-  Notation.declare_arguments_scope local (global_with_alias r) scl
+  Notation.declare_arguments_scope local (smart_global r) scl
 
 let vernac_infix = Metasyntax.add_infix
 
@@ -596,14 +596,14 @@ let vernac_require import _ qidl =
 (* Coercions and canonical structures *)
 
 let vernac_canonical r =
-  Recordops.declare_canonical_structure (global_with_alias r)
+  Recordops.declare_canonical_structure (smart_global r)
 
 let vernac_coercion stre ref qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  let ref' = global_with_alias ref in
+  let ref' = smart_global ref in
   Class.try_add_new_coercion_with_target ref' stre source target;
-  if_verbose message ((string_of_reference ref) ^ " is now a coercion")
+  if_verbose msgnl (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion stre id qids qidt =
   let target = cl_of_qualid qidt in
@@ -764,10 +764,10 @@ let vernac_syntactic_definition lid =
   
 let vernac_declare_implicits local r = function
   | Some imps ->
-      Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false
+      Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
 	(List.map (fun (ex,b,f) -> ex, (b,true,f)) imps)
   | None -> 
-      Impargs.declare_implicits local (global_with_alias r)
+      Impargs.declare_implicits local (smart_global r)
 
 let vernac_reserve idl c =
   let t = Constrintern.interp_type Evd.empty (Global.env()) c in
@@ -975,7 +975,7 @@ let _ =
 
 let vernac_set_opacity local str =
   let glob_ref r =
-    match global_with_alias r with
+    match smart_global r with
       | ConstRef sp -> EvalConstRef sp
       | VarRef id -> EvalVarRef id
       | _ -> error
@@ -1064,11 +1064,10 @@ let vernac_print = function
   | PrintName qid -> 
       if !pcoq <> None then (Option.get !pcoq).print_name qid
       else msg (print_name qid)
-  | PrintOpaqueName qid -> msg (print_opaque_name qid)
   | PrintGraph -> ppnl (Prettyp.print_graph())
   | PrintClasses -> ppnl (Prettyp.print_classes())
   | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses())
-  | PrintInstances c -> ppnl (Prettyp.print_instances (global c))
+  | PrintInstances c -> ppnl (Prettyp.print_instances (smart_global c))
   | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> ppnl (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
@@ -1076,7 +1075,7 @@ let vernac_print = function
   | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ())
   | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ()))
   | PrintUniverses (Some s) -> dump_universes s
-  | PrintHint r -> Auto.print_hint_ref (global_with_alias r)
+  | PrintHint r -> Auto.print_hint_ref (smart_global r)
   | PrintHintGoal -> Auto.print_applicable_hint ()
   | PrintHintDbName s -> Auto.print_hint_db_by_name s
   | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
@@ -1091,7 +1090,7 @@ let vernac_print = function
   | PrintImplicit qid -> msg (print_impargs qid)
 (*spiwack: prints all the axioms and section variables used by a term *)
   | PrintAssumptions (o,r) ->
-      let cstr = constr_of_global (global_with_alias r) in
+      let cstr = constr_of_global (smart_global r) in
       let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ())
 	~add_opaque:o cstr (Global.env ()) in
       msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
@@ -1144,13 +1143,14 @@ let vernac_search s r =
       Search.search_about (List.map (on_snd interp_search_about_item) sl) r
 
 let vernac_locate = function
-  | LocateTerm qid -> msgnl (print_located_qualid qid)
+  | LocateTerm (Genarg.AN qid) -> msgnl (print_located_qualid qid)
+  | LocateTerm (Genarg.ByNotation (_,ntn,sc)) ->
+      ppnl
+        (Notation.locate_notation
+          (Constrextern.without_symbols pr_lrawconstr) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> print_located_module qid
   | LocateFile f -> locate_file f
-  | LocateNotation ntn ->
-      ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lrawconstr)
-	(Metasyntax.standardize_locatable_notation ntn))
 
 (********************)
 (* Proof management *)
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 6cbb536175..300ff44f8e 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -38,7 +38,7 @@ type pcoq_hook = {
   solve : int -> unit;
   abort : string -> unit;
   search : searchable -> dir_path list * bool -> unit;
-  print_name : Libnames.reference -> unit;
+  print_name : Libnames.reference Genarg.or_by_notation -> unit;
   print_check : Environ.env -> Environ.unsafe_judgment -> unit;
   print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
     Environ.unsafe_judgment -> unit;
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e563f66874..080acc7fcf 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -30,7 +30,7 @@ type lname = name located
 type lstring = string
 type lreference = reference
 
-type class_rawexpr = FunClass | SortClass | RefClass of reference
+type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
   
 type printable =
   | PrintTables
@@ -44,18 +44,17 @@ type printable =
   | PrintModuleType of reference
   | PrintMLLoadPath
   | PrintMLModules
-  | PrintName of reference
-  | PrintOpaqueName of reference
+  | PrintName of reference or_by_notation
   | PrintGraph
   | PrintClasses
   | PrintTypeClasses
-  | PrintInstances of reference
+  | PrintInstances of reference or_by_notation
   | PrintLtac of reference
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
   | PrintCanonicalConversions
   | PrintUniverses of string option
-  | PrintHint of reference
+  | PrintHint of reference or_by_notation
   | PrintHintGoal
   | PrintHintDbName of string
   | PrintRewriteHintDbName of string
@@ -63,9 +62,9 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference
-  | PrintImplicit of reference
-  | PrintAssumptions of bool * reference
+  | PrintAbout of reference or_by_notation
+  | PrintImplicit of reference or_by_notation
+  | PrintAssumptions of bool * reference or_by_notation
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr
@@ -78,11 +77,10 @@ type searchable =
   | SearchAbout of (bool * search_about_item) list
 
 type locatable =
-  | LocateTerm of reference
+  | LocateTerm of reference or_by_notation
   | LocateLibrary of reference
   | LocateModule of reference
   | LocateFile of string
-  | LocateNotation of notation
 
 type goable =
   | GoTo of int
@@ -188,8 +186,8 @@ type proof_end =
   | Proved of opacity_flag * (lident * theorem_kind option) option
 
 type scheme =
-  | InductionScheme of bool * lreference * sort_expr
-  | EqualityScheme of lreference
+  | InductionScheme of bool * reference or_by_notation * sort_expr
+  | EqualityScheme of reference or_by_notation
 
 type vernac_expr =
   (* Control *)
@@ -204,7 +202,8 @@ type vernac_expr =
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * lstring
   | VernacBindScope of scope_name * class_rawexpr list
-  | VernacArgumentsScope of locality_flag * lreference * scope_name option list
+  | VernacArgumentsScope of locality_flag * reference or_by_notation * 
+      scope_name option list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
       constr_expr * scope_name option
   | VernacNotation of
@@ -232,8 +231,9 @@ type vernac_expr =
   | VernacRequire of
       export_flag option * specif_flag option * lreference list
   | VernacImport of export_flag * lreference list
-  | VernacCanonical of lreference
-  | VernacCoercion of locality * lreference * class_rawexpr * class_rawexpr
+  | VernacCanonical of reference or_by_notation
+  | VernacCoercion of locality * reference or_by_notation * 
+      class_rawexpr * class_rawexpr
   | VernacIdentityCoercion of locality * lident * 
       class_rawexpr * class_rawexpr
 
@@ -297,11 +297,11 @@ type vernac_expr =
   | VernacHints of locality_flag * lstring list * hints_expr
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
-  | VernacDeclareImplicits of locality_flag * lreference * 
+  | VernacDeclareImplicits of locality_flag * reference or_by_notation * 
       (explicitation * bool * bool) list option
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of
-      locality_flag * (Conv_oracle.level * lreference list) list
+      locality_flag * (Conv_oracle.level * reference or_by_notation list) list
   | VernacUnsetOption of bool option * Goptions.option_name
   | VernacSetOption of bool option * Goptions.option_name * option_value
   | VernacAddOption of Goptions.option_name * option_ref_value list
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index b844f03ca1..b7db4b431d 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -217,7 +217,7 @@ END
 VERNAC COMMAND EXTEND Whelp
 | [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] 
 | [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] 
-| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (global_inductive_with_alias r) ] 
+| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (Smartlocate.global_inductive_with_alias r) ] 
 | [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
 END