4 files changed, 88 insertions, 0 deletions
diff --git a/parsing/g_minicoq.g4 b/parsing/g_minicoq.g4
new file mode 100644
index 000000000..8ee3d5425
--- /dev/null
+++ b/parsing/g_minicoq.g4
@@ -0,0 +1,23 @@
+
+(* $Id$ *)
+
+open Names
+open Generic
+open Term
+
+let lexer = {
+  Token.func = Lexer.func;
+  Token.using = (fun _ -> ());
+  Token.removing = (fun _ -> ());
+  Token.tparse = Lexer.tparse;
+  Token.text = Lexer.token_text }
+  
+let gram = Grammar.create lexer
+
+let term = Grammar.Entry.create gram "term"
+let command = Grammar.Entry.create gram "command"
+
+EXTEND
+  term: [ [ id = IDENT -> VAR (id_of_string id) ] ];
+END
+
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
new file mode 100644
index 000000000..0b2ceb1e8
--- /dev/null
+++ b/parsing/g_minicoq.mli
@@ -0,0 +1,4 @@
+
+open Term
+
+val term : constr Grammar.Entry.e
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
new file mode 100644
index 000000000..670acaa25
--- /dev/null
+++ b/parsing/lexer.mli
@@ -0,0 +1,9 @@
+
+(* $Id$ *)
+
+val func : char Stream.t -> (string * string) Stream.t * (int -> int * int)
+
+val tparse : string * string -> (string * string) Stream.t -> string
+
+val token_text : string * string -> string
+
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index bdd8d8016..c0cbca3ba 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -131,3 +131,55 @@ and string = parse
       { Buffer.add_char string_buffer (Lexing.lexeme_char lexbuf 0);
         string lexbuf }
 
+{
+
+let create_loc_table () = ref (Array.create 1024 None)
+
+let find_loc t i = 
+  if i < 0 || i >= Array.length !t then invalid_arg "find_loc";
+  match Array.unsafe_get !t i with 
+    | None -> invalid_arg "find_loc" 
+    | Some l -> l
+
+let add_loc t i l =
+  while i >= Array.length !t do
+    let new_t = Array.create (2 * Array.length !t) None in
+    Array.blit !t 0 new_t 0 (Array.length !t);
+    t := new_t
+  done;
+  !t.(i) <- Some l
+  
+let func cs =
+  let loct = create_loc_table () in
+  let lexbuf = 
+    Lexing.from_function 
+      (fun s _ -> match cs with parser 
+	 | [< 'c >] -> String.unsafe_set s 0 c; 1
+	 | [< >] -> 0)
+  in
+  let next_token i = 
+    let tok = token lexbuf in
+    let loc = (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf) in
+    add_loc loct i loc; Some tok
+  in
+  let ts = Stream.from next_token in
+  (ts, find_loc loct)
+	 
+let token_text = function
+  | ("", t) -> "'" ^ t ^ "'"
+  | ("IDENT", "") -> "identifier"
+  | ("IDENT", t) -> "'" ^ t ^ "'"
+  | ("INT", "") -> "integer"
+  | ("INT", s) -> "'" ^ s ^ "'"
+  | ("STRING", "") -> "string"
+  | ("EOI", "") -> "end of input"
+  | (con, "") -> con
+  | (con, prm) -> con ^ " \"" ^ prm ^ "\""
+
+let tparse (p_con, p_prm) =
+  if p_prm = "" then
+    parser [< '(con, prm) when con = p_con >] -> prm
+  else
+    parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm
+
+}