Traitement plus clair, notamment pour Locate, de quand quoter les composantes de notations + contournement du fait que Lexer arrive apres Symbol

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

5 files changed, 153 insertions, 113 deletions

diff --git a/interp/symbols.ml b/interp/symbols.ml
index 427524c74d..44237b6c99 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -382,36 +382,6 @@ let find_arguments_scope r =
   try Refmap.find r !arguments_scope
   with Not_found -> []
 
-(* Analysing *)
-
-type symbol_token = WhiteSpace of int | String of string
-
-let split str =
-  let push_token beg i l =
-    if beg = i then l else String (String.sub str beg (i - beg)) :: l 
-  in
-  let push_whitespace beg i l =
-    if beg = i then l else WhiteSpace (i-beg) :: l 
-  in
-  let rec loop beg i =
-    if i < String.length str then
-      if str.[i] = ' ' then
-	push_token beg i (loop_on_whitespace (i+1) (i+1))
-      else
-	loop beg (i+1)
-    else
-      push_token beg i []
-  and loop_on_whitespace beg i =
-    if i < String.length str then
-      if str.[i] <> ' ' then
-	push_whitespace beg i (loop i (i+1))
-      else
-	loop_on_whitespace beg (i+1)
-    else
-      push_whitespace beg i []
-  in
-  loop 0 0
-
 (**********************************************************************)
 (* Mapping classes to scopes *)
 
@@ -451,6 +421,39 @@ let declare_ref_arguments_scope ref =
   let t = Global.type_of_global ref in
   declare_arguments_scope ref (compute_ref_arguments_scope t)
 
+(********************************)
+(* Encoding notations as string *)
+
+type symbol =
+  | Terminal of string
+  | NonTerminal of identifier
+  | Break of int
+
+let string_of_symbol = function
+  | NonTerminal _ -> ["_"]
+  | Terminal s -> [s]
+  | Break _ -> []
+
+let make_notation_key symbols =
+  String.concat " " (List.flatten (List.map string_of_symbol symbols))
+
+let decompose_notation_key s =
+  let len = String.length s in
+  let rec decomp_ntn dirs n =
+    if n>=len then dirs else
+    let pos =
+      try
+	String.index_from s n ' ' 
+      with Not_found -> len
+    in
+    let tok =
+      match String.sub s n (pos-n) with
+      | "_" -> NonTerminal (id_of_string "_")
+      | s -> Terminal s in
+    decomp_ntn (tok::dirs) (pos+1)	  
+  in
+    decomp_ntn [] 0
+
 (************)
 (* Printing *)
 
@@ -514,16 +517,12 @@ let factorize_entries = function
       (ntn,l_of_ntn)::rest
 
 let is_ident s = (* Poor analysis *)
-  String.length s <> 0 & is_letter s.[0] 
+  String.length s <> 0 & is_letter s.[0]
 
 let browse_notation ntn map =
   let find =
-    if is_ident ntn then
-      fun ntn' -> List.mem (String ntn) (split ntn')
-    else if
-      String.contains ntn '_' then (=) ntn
-    else
-      fun ntn' -> string_string_contains ~where:ntn' ~what:ntn in
+    if String.contains ntn ' ' then (=) ntn
+    else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in
   let l =
     Stringmap.fold 
       (fun scope_name sc ->
@@ -538,7 +537,7 @@ let locate_notation prraw ntn =
   if ntns = [] then
     str "Unknown notation"
   else
-    t (str "Notation                               " ++
+    t (str "Notation            " ++
     tab () ++ str "Scope     " ++ tab () ++ fnl () ++ 
     prlist (fun (ntn,l) ->
       let scope = find_default ntn !scope_stack in
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 051b0aa3cb..ffd82c8084 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -126,9 +126,15 @@ val find_arguments_scope : global_reference -> scope_name option list
 val declare_class_scope : scope_name -> Classops.cl_typ -> unit
 val declare_ref_arguments_scope : global_reference -> unit
 
-(* Analysing notation *)
-type symbol_token = WhiteSpace of int | String of string
-val split : notation -> symbol_token list
+(* Building notation key *)
+
+type symbol =
+  | Terminal of string
+  | NonTerminal of identifier
+  | Break of int
+
+val make_notation_key : symbol list -> notation
+val decompose_notation_key : notation -> symbol list
 
 (* Prints scopes (expect a pure aconstr printer *)
 val pr_scope : (rawconstr -> std_ppcmds) -> scope_name -> std_ppcmds
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ad29c28e86..a18659cc25 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -219,7 +219,8 @@ let print_grammar univ entry =
 	| _ -> error "Unknown or unprintable grammar entry" in
     Gram.Entry.print te
 
-(* Parse a format *)
+(* Parse a format (every terminal starting with a letter or a single
+   quote (except a single quote alone) must be quoted) *)
 
 let parse_format (loc,str) =
   let str = " "^str in
@@ -300,10 +301,6 @@ let parse_format (loc,str) =
       (* Parse a ' *)
       |	'\'' when i+1 >= String.length str or str.[i+1] = ' ' ->
 	  push_white (n-1) (push_token (UnpTerminal "'") (parse_token (i+1)))
-      (* Parse a ' followed by one character *)
-      |	'\'' when i+2 >= String.length str or str.[i+2] = ' ' ->
-	  push_white (n-1)
-            (push_token (UnpTerminal (String.sub str i 2)) (parse_token (i+2)))
       (* Parse the beginning of a quoted expression *)
       |	'\'' ->
           parse_quoted (n-1) (i+1)
@@ -321,16 +318,73 @@ let parse_format (loc,str) =
   with e ->
     Stdpp.raise_with_loc loc e
 
+(***********************)
+(* Analysing notations *)
+
+open Symbols
+
+type symbol_token = WhiteSpace of int | String of string
+
+let split_notation_string str =
+  let push_token beg i l =
+    if beg = i then l else
+      let s = String.sub str beg (i - beg) in
+      String s :: l 
+  in
+  let push_whitespace beg i l =
+    if beg = i then l else WhiteSpace (i-beg) :: l 
+  in
+  let rec loop beg i =
+    if i < String.length str then
+      if str.[i] = ' ' then
+	push_token beg i (loop_on_whitespace (i+1) (i+1))
+      else
+	loop beg (i+1)
+    else
+      push_token beg i []
+  and loop_on_whitespace beg i =
+    if i < String.length str then
+      if str.[i] <> ' ' then
+	push_whitespace beg i (loop i (i+1))
+      else
+	loop_on_whitespace beg (i+1)
+    else
+      push_whitespace beg i []
+  in
+  loop 0 0
+
+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
+
+(* To protect alphabetic tokens and quotes from being seen as variables *)
+let quote_notation_token x =
+  let n = String.length x in
+  if (n > 0 & Lexer.is_normal_token x) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
+  else x
+
+let rec analyse_notation_tokens = function
+  | []    -> [], []
+  | String x :: sl when Lexer.is_normal_token x ->
+      Lexer.check_ident x;
+      let id = Names.id_of_string x in
+      let (vars,l) = analyse_notation_tokens sl in
+      if List.mem id vars then
+	error ("Variable "^x^" occurs more than once");
+      (id::vars, NonTerminal id :: l)
+  | String s :: sl ->
+      Lexer.check_special_token s;
+      let (vars,l) = analyse_notation_tokens sl in
+      (vars, Terminal (unquote_notation_token s) :: l)
+  | WhiteSpace n :: sl ->
+      let (vars,l) = analyse_notation_tokens sl in
+      (vars, Break n :: l)
+
 (* Build the syntax and grammar rules *)
 
 type printing_precedence = int * parenRelation
 type parsing_precedence = int option
 
-type symbol =
-  | Terminal of string
-  | NonTerminal of identifier
-  | Break of int
-
 let prec_assoc = function
   | Gramext.RightA -> (L,E)
   | Gramext.LeftA -> (E,L)
@@ -339,8 +393,6 @@ let prec_assoc = function
 (* For old ast printer *)
 let meta_pattern m = Pmeta(m,Tany)
 
-open Symbols
-
 type white_status = Juxtapose | Separate of int | NextIsTerminal
 
 let precedence_of_entry_type from = function
@@ -481,22 +533,13 @@ let make_hunks etyps symbols from =
 
   in make NoBreak symbols
 
-let strip s =
-  let n = String.length s in
-  if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
-
-(* To protect alphabetic tokens and quotes from being seen as variables *)
-let quote x =
-  let n = String.length x in
-  if (n > 0 & Lexer.is_normal_token x) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
-  else x
-
 let hunks_of_format (from,(vars,typs) as vt) symfmt = 
   let rec aux = function
   | symbs, (UnpTerminal s' as u) :: fmt
       when s' = String.make (String.length s') ' ' ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
-  | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt when s = strip s' ->
+  | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt
+      when s = unquote_notation_token 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
@@ -518,11 +561,6 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt =
 let string_of_prec (n,p) =
   (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")
 
-let string_of_symbol = function
-  | NonTerminal _ -> ["_"]
-  | Terminal s -> [s]
-  | Break _ -> []
-
 let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
 
 let string_of_assoc = function
@@ -530,11 +568,8 @@ let string_of_assoc = function
   | Some(Gramext.LeftA) | None -> "LEFTA"
   | Some(Gramext.NonA) -> "NONA"
 
-let make_anon_notation symbols =
-  String.concat " " (List.flatten (List.map string_of_symbol symbols))
-
 let make_symbolic n symbols etyps =
-  ((n,List.map (assoc_of_type n) etyps), make_anon_notation symbols)
+  ((n,List.map (assoc_of_type n) etyps), make_notation_key symbols)
 
 let is_not_small_constr = function
     ETConstr _ -> true
@@ -571,21 +606,6 @@ let make_production etyps symbols =
       symbols [] in
   define_keywords prod
 
-let rec analyse_tokens = function
-  | []    -> [], []
-  | String x :: sl when Lexer.is_normal_token x ->
-      Lexer.check_ident x;
-      let id = Names.id_of_string x in
-      let (vars,l) = analyse_tokens sl in
-      if List.mem id vars then
-	error ("Variable "^x^" occurs more than once");
-      (id::vars, NonTerminal id :: l)
-  | String s :: sl ->
-      Lexer.check_special_token s;
-      let (vars,l) = analyse_tokens sl in (vars, Terminal (strip s) :: l)
-  | WhiteSpace n :: sl ->
-      let (vars,l) = analyse_tokens sl in (vars, Break n :: l)
-
 let rec find_symbols c_current c_next c_last = function
   | [] -> []
   | NonTerminal id :: sl ->
@@ -833,9 +853,9 @@ let compute_syntax_data forv7 (df,modifiers) =
   let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
   (* Notation defaults to NONA *)
   let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
-  let toks = split df in
+  let toks = split_notation_string df in
   let innerlevel = NumLevel (if forv7 then 10 else 200) in
-  let (vars,symbols) = analyse_tokens toks in
+  let (vars,symbols) = analyse_notation_tokens toks in
   check_rule_reversibility symbols;
   let n =
     if !Options.v7 then find_precedence_v7 n etyps symbols
@@ -1003,7 +1023,7 @@ let build_old_pp_rule notation scope symbs (r,vars) =
 
 let add_notation_interpretation_core local symbs for_old df a scope onlyparse 
   onlypp =
-  let notation = make_anon_notation symbs in
+  let notation = make_notation_key symbs in
   let old_pp_rule = 
     if !Options.v7 then 
       option_app (build_old_pp_rule notation scope symbs) for_old
@@ -1012,8 +1032,8 @@ let add_notation_interpretation_core local symbs for_old df a scope onlyparse
     (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp,df))
 
 let add_notation_interpretation df names c sc =
-  let (vars,symbs) = analyse_tokens (split df) in
-  check_notation_existence (make_anon_notation symbs);
+  let (vars,symbs) = analyse_notation_tokens (split_notation_string df) in
+  check_notation_existence (make_notation_key symbs);
   let a = interp_aconstr names vars c in
   let a_for_old = interp_rawconstr_with_implicits (Global.env()) vars names c 
   in
@@ -1032,7 +1052,7 @@ let add_notation_in_scope_v8only local df c mv8 scope toks =
     (inNotation(local,None,notation,scope,a,onlyparse,true,df))
 
 let add_notation_v8only local c (df,modifiers) sc =
-  let toks = split df in
+  let toks = split_notation_string df in
   match toks with 
     | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
 	(* This is a ident to be declared as a rule *)
@@ -1045,7 +1065,7 @@ let add_notation_v8only local c (df,modifiers) sc =
 		error "Parsing rule for this notation includes no level"
 	      else
 	        (* Declare only interpretation *)
-		let (vars,symbs) = analyse_tokens toks in
+		let (vars,symbs) = analyse_notation_tokens toks in
 		let onlyparse = modifiers = [SetOnlyParsing] in
 		let a = interp_aconstr [] vars c in
 		let a_for_old = interp_global_rawconstr_with_vars vars c in
@@ -1060,19 +1080,20 @@ let add_notation_v8only local c (df,modifiers) sc =
 	      add_notation_in_scope_v8only local df c mods sc toks
 
 let is_quoted_ident x =
-  let x' = strip x in x <> x' & try Lexer.check_ident x'; true with _ -> false
+  let x' = unquote_notation_token x in
+  x <> x' & try Lexer.check_ident x'; true with _ -> false
 
 let add_notation local c dfmod mv8 sc =
   match dfmod with
   | None -> add_notation_v8only local c (out_some mv8) sc
   | Some (df,modifiers) ->
-  let toks = split df in
+  let toks = split_notation_string df in
   match toks with 
     | [String x] when is_quoted_ident x 
 	(* This is an ident that can be qualified: a syntactic definition *)
 	& (modifiers = [] or modifiers = [SetOnlyParsing]) ->
         (* Means a Syntactic Definition *)
-        let ident = id_of_string (strip x) in
+        let ident = id_of_string (unquote_notation_token x) in
 	let c = snd (interp_aconstr [] [] c) in
 	let onlyparse = !Options.v7_only or modifiers = [SetOnlyParsing] in
         Syntax_def.declare_syntactic_definition local ident onlyparse c
@@ -1087,8 +1108,8 @@ let add_notation local c dfmod mv8 sc =
 		error "Parsing rule for this notation includes no level"
 	      else
 	        (* Declare only interpretation *)
-		let (vars,symbs) = analyse_tokens toks in
-		check_notation_existence (make_anon_notation symbs);
+		let (vars,symbs) = analyse_notation_tokens toks in
+		check_notation_existence (make_notation_key symbs);
 		let onlyparse = modifiers = [SetOnlyParsing] in
 		let a = interp_aconstr [] vars c in
 		let a_for_old = interp_global_rawconstr_with_vars vars c in
@@ -1112,12 +1133,12 @@ let rec rename x vars n = function
       let xn = x^(string_of_int n) in
       ((inject_var xn)::vars,xn::l)
   | String y::l ->
-      let (vars,l) = rename x vars n l in (vars,(quote y)::l)
+      let (vars,l) = rename x vars n l in (vars,(quote_notation_token y)::l)
   | WhiteSpace _::l ->
       rename x vars n l
 
 let translate_distfix assoc df r = 
-  let (vars,l) = rename "x" [] 1 (split df) in
+  let (vars,l) = rename "x" [] 1 (split_notation_string df) in
   let df = String.concat " " l in
   let a = mkAppC (mkRefC r, vars) in
   let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
@@ -1125,11 +1146,12 @@ let translate_distfix assoc df r =
 
 let add_distfix local assoc n df r sc =
   (* "x" cannot clash since r is globalized (included section vars) *)
-  let (vars,l) = rename "x" [] 1 (split df) in
+  let (vars,l) = rename "x" [] 1 (split_notation_string df) in
   let df = String.concat " " l in
   let a = mkAppC (mkRefC r, vars) in
   let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
-  add_notation_in_scope local df a [SetAssoc assoc;SetLevel n] None sc (split df)
+  add_notation_in_scope local df a [SetAssoc assoc;SetLevel n] None sc
+    (split_notation_string df)
 
 let add_infix local (inf,modl) pr mv8 sc =
   if inf="" (* Code for V8Infix only *) then
@@ -1137,11 +1159,11 @@ let add_infix local (inf,modl) pr mv8 sc =
     let (a8,n8,onlyparse,fmt) = interp_infix_modifiers mv8 in
     let metas = [inject_var "x"; inject_var "y"] in
     let a = mkAppC (mkRefC pr,metas) in
-    let df = "x "^(quote p8)^" y" in
-    let toks = split df in
+    let df = "x "^(quote_notation_token p8)^" y" in
+    let toks = split_notation_string df in
     if a8=None & n8=None & fmt=None then
       (* Declare only interpretation *)
-      let (vars,symbs) = analyse_tokens toks in
+      let (vars,symbs) = analyse_notation_tokens toks in
       let a' = interp_aconstr [] vars a in
       let a_for_old = interp_global_rawconstr_with_vars vars a in
       add_notation_interpretation_core local symbs None df a' sc 
@@ -1163,14 +1185,14 @@ let add_infix local (inf,modl) pr mv8 sc =
   *)
   let metas = [inject_var "x"; inject_var "y"] in
   let a = mkAppC (mkRefC pr,metas) in
-  let df = "x "^(quote inf)^" y" in
-  let toks = split df in
+  let df = "x "^(quote_notation_token inf)^" y" in
+  let toks = split_notation_string df in
   if not !Options.v7 & n=None & assoc=None then
     (* En v8, une notation sans information de parsing signifie *)
     (* de ne déclarer que l'interprétation *)
     (* Declare only interpretation *)
-    let (vars,symbs) = analyse_tokens toks in
-    check_notation_existence (make_anon_notation symbs);
+    let (vars,symbs) = analyse_notation_tokens toks in
+    check_notation_existence (make_notation_key symbs);
     let a' = interp_aconstr [] vars a in
     let a_for_old = interp_global_rawconstr_with_vars vars a in
     let for_old = Some (a_for_old,vars) in
@@ -1185,10 +1207,20 @@ let add_infix local (inf,modl) pr mv8 sc =
     | Some(s8,mv8) ->
 	if List.for_all (function SetLevel _ -> false | _ -> true) mv8 then
 	  error "Needs a level"
-	else Some (("x "^quote s8^" y"),mv8) in
+	else Some (("x "^quote_notation_token s8^" y"),mv8) in
   add_notation_in_scope local df a mv mv8 sc toks
   end
 
+let standardise_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 74b199ed71..8f6b49d0e5 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -59,3 +59,5 @@ val merge_modifiers : Gramext.g_assoc option -> int option ->
 
 val interp_infix_modifiers : syntax_modifier list ->
   Gramext.g_assoc option * precedence option * bool * string located option
+
+val standardise_locatable_notation : string -> string
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 67da01408d..d888edc9d9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -918,7 +918,8 @@ let vernac_locate = function
   | LocateLibrary qid -> print_located_library qid
   | LocateFile f -> locate_file f
   | LocateNotation ntn ->
-      ppnl (Symbols.locate_notation (Constrextern.without_symbols pr_rawterm) ntn)
+      ppnl (Symbols.locate_notation (Constrextern.without_symbols pr_rawterm)
+	(Metasyntax.standardise_locatable_notation ntn))
 
 (********************)
 (* Proof management *)