debut d'un lexer

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

2 files changed, 134 insertions, 0 deletions

diff --git a/parsing/.cvsignore b/parsing/.cvsignore
new file mode 100644
index 000000000..c1104f3ab
--- /dev/null
+++ b/parsing/.cvsignore
@@ -0,0 +1 @@
+lexer.ml
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
new file mode 100644
index 000000000..bdd8d8016
--- /dev/null
+++ b/parsing/lexer.mll
@@ -0,0 +1,133 @@
+
+(* $Id$ *)
+
+{
+open Util
+
+type error =
+  | Illegal_character
+  | Unterminated_comment
+  | Unterminated_string
+
+exception Error of error * int * int
+
+let is_keyword =
+  let table = Hashtbl.create 149 in
+  List.iter (fun kw -> Hashtbl.add table kw ())
+    [ "Grammar"; "Syntax"; "Quit"; "Load"; "Compile";
+      "of"; "with"; "end"; "as"; "in"; "using";
+      "Cases"; "Fixpoint"; "CoFixpoint";
+      "Definition"; "Inductive"; "CoInductive"; 
+      "Theorem"; "Variable"; "Axiom"; "Parameter"; "Hypothesis";
+      "Orelse"; "Proof"; "Qed";
+      "Prop"; "Set"; "Type" ];
+  fun s -> try Hashtbl.find table s; true with Not_found -> false
+      
+let char_for_backslash =
+  match Sys.os_type with
+  | "Unix" | "Win32" ->
+      begin function
+      | 'n' -> '\010'
+      | 'r' -> '\013'
+      | 'b' -> '\008'
+      | 't' -> '\009'
+      | c   -> c
+      end
+  | "MacOS" ->
+      begin function
+      | 'n' -> '\013'
+      | 'r' -> '\010'
+      | 'b' -> '\008'
+      | 't' -> '\009'
+      | c   -> c
+      end
+  | x -> error "Lexer: unknown system type"
+
+let char_for_decimal_code lexbuf i =
+  let c = 100 * (Char.code(Lexing.lexeme_char lexbuf i) - 48) +
+           10 * (Char.code(Lexing.lexeme_char lexbuf (i+1)) - 48) +
+                (Char.code(Lexing.lexeme_char lexbuf (i+2)) - 48) in  
+  Char.chr(c land 0xFF)
+
+let string_buffer = Buffer.create 80
+let string_start_pos = ref 0
+			 
+let comment_depth = ref 0
+let comment_start_pos = ref 0
+
+}
+
+let blank = [' ' '\010' '\013' '\009' '\012']
+let firstchar = 
+  ['A'-'Z' 'a'-'z' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+let identchar = 
+  ['A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let symbolchar =
+  ['!' '$' '%' '&' '*' '+' '-' '.' '/' ':' '<' '=' '>' '?' '@' '^' '|' '~']
+
+rule token = parse
+  | blank+ 
+      { token lexbuf }
+  | firstchar identchar* 
+      { let s = Lexing.lexeme lexbuf in
+	if is_keyword s then ("",s) else ("IDENT",s) }
+  | symbolchar+
+      { ("SPECIAL", Lexing.lexeme lexbuf) }
+  | '`' [^'`']* '`'
+      { ("QUOTED", Lexing.lexeme lexbuf) }
+  | "\""
+      { Buffer.reset string_buffer;
+        let string_start = Lexing.lexeme_start lexbuf in
+        string_start_pos := string_start;
+        string lexbuf;
+        ("STRING", Buffer.contents string_buffer) }
+  | "(*"
+      { comment_depth := 1;
+        comment_start_pos := Lexing.lexeme_start lexbuf;
+        comment lexbuf;
+        token lexbuf }
+
+and comment = parse
+    "(*"
+      { comment_depth := succ !comment_depth; comment lexbuf }
+  | "*)"
+      { comment_depth := pred !comment_depth;
+        if !comment_depth > 0 then comment lexbuf }
+  | "\""
+      { Buffer.reset string_buffer;
+        string_start_pos := Lexing.lexeme_start lexbuf;
+        string lexbuf;
+        comment lexbuf }
+  | "''"
+      { comment lexbuf }
+  | "'" [^ '\\' '\''] "'"
+      { comment lexbuf }
+  | "'\\" ['\\' '\'' 'n' 't' 'b' 'r'] "'"
+      { comment lexbuf }
+  | "'\\" ['0'-'9'] ['0'-'9'] ['0'-'9'] "'"
+      { comment lexbuf }
+  | eof
+      { raise (Error (Unterminated_comment,
+                      !comment_start_pos, !comment_start_pos+2)) }
+  | _
+      { comment lexbuf }
+
+and string = parse
+    '"'
+      { () }
+  | '\\' ("\010" | "\013" | "\013\010") [' ' '\009'] *
+      { string lexbuf }
+  | '\\' ['\\' '"' 'n' 't' 'b' 'r']
+      { let c = char_for_backslash (Lexing.lexeme_char lexbuf 1) in
+	Buffer.add_char string_buffer c;
+        string lexbuf }
+  | '\\' ['0'-'9'] ['0'-'9'] ['0'-'9']
+      { Buffer.add_char string_buffer (char_for_decimal_code lexbuf 1);
+        string lexbuf }
+  | eof
+      { raise (Error (Unterminated_string,
+                      !string_start_pos, !string_start_pos+1)) }
+  | _
+      { Buffer.add_char string_buffer (Lexing.lexeme_char lexbuf 0);
+        string lexbuf }
+