Be a bit less aggressive in declaring idents as keywords in notations

(an articulating ident needs to be a keyword if the constr entry that
 preceeds it is higher than the level of applications).

Also fixed is_ident_not_keyword which only looked at the first letter
and at the keyword status to decide if a token is an ident. This
allowed to simplified define_keywords in Metasyntax.

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

5 files changed, 23 insertions, 34 deletions

diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c94b42c28..581d151d1 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -205,6 +205,9 @@ let check_ident str =
   in
   loop_id false (Stream.of_string str)
 
+let is_ident str =
+  try let _ = check_ident str in true with Error.E _ -> false
+
 (* Keyword and symbol dictionary *)
 let token_tree = ref empty_ttree
 
@@ -609,7 +612,7 @@ END
 
 let is_ident_not_keyword s =
   match s.[0] with
-    | 'a'..'z' | 'A'..'Z' | '_' -> not (is_keyword s)
+    | 'a'..'z' | 'A'..'Z' | '_' -> is_ident s && not (is_keyword s)
     | _ -> false
 
 let is_number s =
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 0a40d0727..1899f7f4d 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -21,6 +21,7 @@ val location_table : unit -> location_table
 val restore_location_table : location_table -> unit
 
 val check_ident : string -> unit
+val is_ident : string -> bool
 val check_keyword : string -> unit
 
 type frozen_t
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 72264d082..8af9ca82c 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -2,10 +2,8 @@ true ? 0; 1
      : nat
 if true as x return (x ? nat; bool) then 0 else true
      : nat
-Defining 'proj1' as keyword
 fun e : nat * nat => proj1 e
      : nat * nat -> nat
-Defining 'decomp' as keyword
 decomp (true, true) as t, u in (t, u)
      : bool * bool
 !(0 = 0)
@@ -28,17 +26,14 @@ forall n n0 : nat, ###(n = n0)
      : list nat
 (1; 2, 4)
      : nat * nat * nat
-Defining 'ifzero' as keyword
 ifzero 3
      : bool
-Defining 'pred' as keyword
 pred 3
      : nat
 fun n : nat => pred n
      : nat -> nat
 fun n : nat => pred n
      : nat -> nat
-Defining 'ifn' as keyword
 Defining 'is' as keyword
 fun x : nat => ifn x is succ n then n else 0
      : nat -> nat
@@ -80,7 +75,6 @@ Nil
      : forall A : Type, list A
 NIL:list nat
      : list nat
-Defining 'I' as keyword
 (false && I 3)%bool /\ I 6
      : Prop
 [|1, 2, 3; 4, 5, 6|]
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index d92f8d694..f4eaeb478 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -30,7 +30,6 @@ let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
      : Type -> Prop
 λ A : Type, ∀ n p : A, n = p
      : Type -> Prop
-Defining 'let'' as keyword
 let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
      : bool -> nat
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 79b3dac5f..551ff302a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -308,16 +308,12 @@ let rec interp_list_parser hd = function
       xyl, List.rev_append hd tl'
   | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
 
-
 (* Find non-terminal tokens of notation *)
 
-let is_normal_token str =
-  try let _ = Lexer.check_ident str in true with Lexer.Error.E _ -> false
-
 (* To protect alphabetic tokens and quotes from being seen as variables *)
 let quote_notation_token x =
   let n = String.length x in
-  let norm = is_normal_token x in
+  let norm = is_ident x in
   if (n > 0 & norm) or (n > 2 & x.[0] = '\'') then "'"^x^"'"
   else x
 
@@ -325,7 +321,7 @@ 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 ->
+  | String x :: sl when is_ident x ->
       NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
       Terminal (drop_simple_quotes s) :: raw_analyze_notation_tokens sl
@@ -579,27 +575,23 @@ let hunks_of_format (from,(vars,typs)) symfmt =
 
 let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
 
-let is_not_small_constr = function
-    ETConstr _ -> true
-  | ETOther("constr","binder_constr") -> true
-  | _ -> false
-
-let rec define_keywords_aux = function
-  | GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal(IDENT k) :: l
-      when is_not_small_constr e ->
-      message ("Defining '"^k^"' as keyword");
-      Lexer.add_keyword k;
-      n1 :: GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
-  | n :: l -> n :: define_keywords_aux l
-  | [] -> []
+let constr_level n = function
+  | ETConstr (NextLevel,_) -> n-1
+  | ETConstr (NumLevel n,_) -> n
+  | ETOther("constr","binder_constr") -> 200
+  | _ -> 0
 
   (* Ensure that IDENT articulation terminal symbols are keywords *)
-let define_keywords = function
-  | GramConstrTerminal(IDENT k)::l ->
+let rec define_keywords n = function
+  | GramConstrNonTerminal(e,Some _) as x1 :: GramConstrTerminal(IDENT k) :: l
+      when constr_level n e > 9 ->
+      (* an entry can catch an ident coming next if it is at a level *)
+      (* higher than the level of applications which is 10 *)
       message ("Defining '"^k^"' as keyword");
       Lexer.add_keyword k;
-      GramConstrTerminal(KEYWORD k) :: define_keywords_aux l
-  | l -> define_keywords_aux l
+      x1 :: GramConstrTerminal(KEYWORD k) :: define_keywords n l
+  | x :: l -> x :: define_keywords  n l
+  | [] -> []
 
 let distribute a ll = List.map (fun l -> a @ l) ll
 
@@ -618,7 +610,7 @@ let rec expand_list_rule typ tkl x n i hds ll =
     distribute (GramConstrListMark (i+1,false) :: hds @ [main]) ll @
       expand_list_rule typ tkl x n (i+1) (main :: tks @ hds) ll
 
-let make_production etyps symbols =
+let make_production n etyps symbols =
   let prod =
     List.fold_right
       (fun t ll -> match t with
@@ -642,7 +634,7 @@ let make_production etyps symbols =
             | _ ->
                 error "Components of recursive patterns in notation must be terms or binders.")
       symbols [[]] in
-  List.map define_keywords prod
+  List.map (define_keywords n) prod
 
 let rec find_symbols c_current c_next c_last = function
   | [] -> []
@@ -1013,7 +1005,7 @@ let recover_notation_syntax rawntn =
 
 let make_pa_rule (n,typs,symbols,_) ntn =
   let assoc = recompute_assoc typs in
-  let prod = make_production typs symbols in
+  let prod = make_production n typs symbols in
   (n,assoc,ntn,prod)
 
 let make_pp_rule (n,typs,symbols,fmt) =