Adding a token "index" representing positions (1st, 2nd, etc.).

6 files changed, 33 insertions, 6 deletions

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 84da9c424..b3cd93926 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -32,7 +32,7 @@ let my_int_of_string loc s =
 
 GEXTEND Gram
   GLOBAL:
-    bigint natural integer identref name ident var preident
+    bigint natural index integer identref name ident var preident
     fullyqualid qualid reference dirpath ne_lstring
     ne_string string pattern_ident pattern_identref by_notation smart_global;
   preident:
@@ -113,6 +113,9 @@ GEXTEND Gram
   natural:
     [ [ i = INT -> my_int_of_string (!@loc) i ] ]
   ;
+  index:
+    [ [ i = INDEX -> my_int_of_string (!@loc) i ] ]
+  ;
   bigint: (* Negative numbers are dealt with specially *)
     [ [ i = INT -> (Bigint.of_string i) ] ]
   ;
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 23bd74da9..d7941bedb 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -262,9 +262,23 @@ let rec ident_tail len = parser
           ident_tail (nstore n len s) s
       | _ -> len
 
-let rec number len = parser
-  | [< ' ('0'..'9' as c); s >] -> number (store len c) s
-  | [< >] -> len
+let check_no_char s =
+  match Stream.npeek 3 s with
+  | [_;_;('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_')] -> false
+  | [_;_;_] -> true
+  | [_;_] -> true
+  | _ -> assert false
+
+let rec number_or_index c len = parser
+  | [< ' ('0'..'9' as c); s >] -> number_or_index c (store len c) s
+  | [< s >] ->
+      match Stream.npeek 2 s with
+      | ['s';'t'] when c = '1' && check_no_char s -> njunk 2 s; false, len
+      | ['n';'d'] when c = '2' && check_no_char s -> njunk 2 s; false, len
+      | ['r';'d'] when c = '3' && check_no_char s -> njunk 2 s; false, len
+      | ['t';'h'] when not (len=1 && c='0') && check_no_char s ->
+        njunk 2 s; false, len
+      | _ -> true, len
 
 let rec string in_comments bp len = parser
   | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] ->
@@ -513,9 +527,9 @@ let rec next_token = parser bp
       let id = get_buff len in
       comment_stop bp;
       (try find_keyword id s with Not_found -> IDENT id), (bp, ep)
-  | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
+  | [< ' ('0'..'9' as c); (b,len) = number_or_index c (store 0 c) >] ep ->
       comment_stop bp;
-      (INT (get_buff len), (bp, ep))
+      (if b then INT (get_buff len) else INDEX (get_buff len)), (bp, ep)
   | [< ''\"'; len = string None bp 0 >] ep ->
       comment_stop bp;
       (STRING (get_buff len), (bp, ep))
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 4565b87a0..df0d26206 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -298,6 +298,7 @@ module Prim =
     let preident = gec_gen (rawwit wit_pre_ident) "preident"
     let ident = gec_gen (rawwit wit_ident) "ident"
     let natural = gec_gen (rawwit wit_int) "natural"
+    let index = gec_gen (rawwit wit_int) "index"
     let integer = gec_gen (rawwit wit_int) "integer"
     let bigint = Gram.entry_create "Prim.bigint"
     let string = gec_gen (rawwit wit_string) "string"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index c224dbad9..ad4d9e501 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -173,6 +173,7 @@ module Prim :
     val pattern_identref : Id.t located Gram.entry
     val base_ident : Id.t Gram.entry
     val natural : int Gram.entry
+    val index : int Gram.entry
     val bigint : Bigint.bigint Gram.entry
     val integer : int Gram.entry
     val string : string Gram.entry
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 12140f403..427080788 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -15,6 +15,7 @@ type t =
   | IDENT of string
   | FIELD of string
   | INT of string
+  | INDEX of string
   | STRING of string
   | LEFTQMARK
   | BULLET of string
@@ -28,6 +29,7 @@ let equal t1 t2 = match t1, t2 with
 | IDENT s1, IDENT s2 -> CString.equal s1 s2
 | FIELD s1, FIELD s2 -> CString.equal s1 s2
 | INT s1, INT s2 -> CString.equal s1 s2
+| INDEX s1, INDEX s2 -> CString.equal s1 s2
 | STRING s1, STRING s2 -> CString.equal s1 s2
 | LEFTQMARK, LEFTQMARK -> true
 | BULLET s1, BULLET s2 -> CString.equal s1 s2
@@ -42,6 +44,7 @@ let extract_string = function
   | PATTERNIDENT s -> s
   | FIELD s -> s
   | INT s -> s
+  | INDEX s -> s
   | LEFTQMARK -> "?"
   | BULLET s -> s
   | EOI -> ""
@@ -53,6 +56,7 @@ let to_string = function
   | PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s
   | FIELD s -> Format.sprintf "FIELD %S" s
   | INT s -> Format.sprintf "INT %s" s
+  | INDEX s -> Format.sprintf "INDEX %s" s
   | STRING s -> Format.sprintf "STRING %S" s
   | LEFTQMARK -> "LEFTQMARK"
   | BULLET s -> Format.sprintf "STRING %S" s
@@ -76,6 +80,7 @@ let of_pattern = function
   | "PATTERNIDENT", s -> PATTERNIDENT s
   | "FIELD", s -> FIELD s
   | "INT", s -> INT s
+  | "INDEX", s -> INDEX s
   | "STRING", s -> STRING s
   | "LEFTQMARK", _ -> LEFTQMARK
   | "BULLET", s -> BULLET s
@@ -89,6 +94,7 @@ let to_pattern = function
   | PATTERNIDENT s -> "PATTERNIDENT", s
   | FIELD s -> "FIELD", s
   | INT s -> "INT", s
+  | INDEX s -> "INDEX", s
   | STRING s -> "STRING", s
   | LEFTQMARK -> "LEFTQMARK", ""
   | BULLET s -> "BULLET", s
@@ -103,6 +109,7 @@ let match_pattern =
     | "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ())
     | "FIELD", "" -> (function FIELD s -> s | _ -> err ())
     | "INT", "" -> (function INT s -> s | _ -> err ())
+    | "INDEX", "" -> (function INDEX s -> s | _ -> err ())
     | "STRING", "" -> (function STRING s -> s | _ -> err ())
     | "LEFTQMARK", "" -> (function LEFTQMARK -> ""  | _ -> err ())
     | "BULLET", "" ->  (function BULLET s -> s  | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index feee1983d..3414de36b 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -15,6 +15,7 @@ type t =
   | IDENT of string
   | FIELD of string
   | INT of string
+  | INDEX of string
   | STRING of string
   | LEFTQMARK
   | BULLET of string