aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/lexer.mll
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/lexer.mll')
-rw-r--r--parsing/lexer.mll290
1 files changed, 0 insertions, 290 deletions
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
deleted file mode 100644
index 06531fb0f..000000000
--- a/parsing/lexer.mll
+++ /dev/null
@@ -1,290 +0,0 @@
-
-(* $Id$ *)
-
-{
-open Util
-
-type error =
- | Illegal_character
- | Unterminated_comment
- | Unterminated_string
-
-exception Error of error
-
-(* token trees *)
-
-module Charmap = Map.Make (struct type t = char let compare = compare end)
-
-type ttree = { node : string option; branch : ttree Charmap.t }
-
-let ttree_empty = { node = None; branch = Charmap.empty }
-
-let ttree_add ttree str =
- let n = String.length str in
- let rec insert tt i =
- if i == n then
- { node = Some str; branch = tt.branch }
- else
- let c = str.[i] in
- let br =
- match
- try Some (Charmap.find c tt.branch) with Not_found -> None
- with
- | Some tt' ->
- Charmap.add c (insert tt' (i + 1)) (Charmap.remove c tt.branch)
- | None ->
- let tt' = { node = None; branch = Charmap.empty } in
- Charmap.add c (insert tt' (i + 1)) tt.branch
- in
- { node = tt.node; branch = br }
- in
- insert ttree 0
-
-let ttree_find ttree str =
- let n = String.length str in
- let rec proc_rec tt i =
- if i == n then
- match tt.node with
- | Some s -> s
- | None -> raise Not_found
- else
- proc_rec (Charmap.find str.[i] tt.branch) (i+1)
- in
- proc_rec ttree 0
-
-let kw_table = ref ttree_empty
-
-let init () =
- kw_table := ttree_empty;
- List.iter
- (fun kw -> kw_table := ttree_add !kw_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" ]
-
-let _ = init ()
-
-let add_keyword s = kw_table := ttree_add !kw_table s
-
-let is_keyword s =
- try let _ = ttree_find !kw_table s in true with Not_found -> false
-
-type frozen_t = ttree
-
-let freeze () = !kw_table
-
-let unfreeze ft = kw_table := ft
-
-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 = ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#']
-let extrachar = symbolchar | ['\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' '\'']
-let decimal_literal = ['0'-'9']+
-let hex_literal = '0' ['x' 'X'] ['0'-'9' 'A'-'F' 'a'-'f']+
-let oct_literal = '0' ['o' 'O'] ['0'-'7']+
-let bin_literal = '0' ['b' 'B'] ['0'-'1']+
-
-rule token = parse
- | blank+
- { token lexbuf }
- | "$" identchar*
- { ("METAIDENT",Lexing.lexeme lexbuf) }
- | firstchar identchar*
- { let s = Lexing.lexeme lexbuf in
- if is_keyword s then ("",s) else ("IDENT",s) }
- | decimal_literal | hex_literal | oct_literal | bin_literal
- { ("INT", Lexing.lexeme lexbuf) }
- | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "``" | "()"
- | "->" | "\\/" | "/\\" | "|-" | ":=" | "<->" | '\'' | extrachar
- { ("", Lexing.lexeme lexbuf) }
- | "." blank
- { ("", ".") }
- | "." firstchar identchar*
- { let s = Lexing.lexeme lexbuf in
- ("FIELD", String.sub s 1 (String.length s - 1)) }
- | ('\\'(symbolchar | '\\' | '-' | '>' | '|' | ':' | '?' | '=' | '<' | '~')+ |
- '/' (symbolchar | '/' | '-' | '>' | '|' | ':' | '?' | '=' | '<' | '~')+ |
- '-' (symbolchar | '\\' | '/' | '-' | '|' | ':' | '?' | '=' | '<' | '~')+ |
- '|' (symbolchar | '\\' | '/' | '|' | '>' | ':' | '?' | '=' | '<' | '~')+ |
- '=' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' | '~')+ |
- '<' (symbolchar | '\\' | '/' | '|' | '>' | '?' | ':' | '=' | '<' | '~')+ |
- "<-"(symbolchar | '\\' | '/' | '|' | '-' | '?' | ':' | '=' | '<' | '~')+ |
- '~' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' )+ |
- ':' (symbolchar | '\\' | '/' | '|' | '-' | '>' | ':' | '=' | '<' )+ |
- '\'' symbolchar+ | '>' | '?') extrachar* | "<-"
- { ("", Lexing.lexeme lexbuf) }
- | symbolchar+ extrachar*
- { ("", Lexing.lexeme lexbuf) }
- (***
- | '`' [^'`']* '`'
- { let s = Lexing.lexeme lexbuf in
- ("QUOTED", String.sub s 1 (String.length s - 2)) }
- ***)
- | "\""
- { 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 }
- | eof
- { ("EOI","") }
- | _ { let loc = (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf) in
- raise (Stdpp.Exc_located (loc, Error Illegal_character)) }
-
-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
- { let loc = (!comment_start_pos, !comment_start_pos+2) in
- raise (Stdpp.Exc_located (loc, Error Unterminated_comment)) }
- | _
- { 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
- { let loc = (!string_start_pos, !string_start_pos+1) in
- raise (Stdpp.Exc_located (loc, Error Unterminated_string)) }
- | _
- { 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 is_ident s =
- String.length s > 0 &&
- (match s.[0] with
- | 'A'..'Z' | 'a'..'z' | '\192'..'\214' | '\216'..'\246'
- | '\248'..'\255' -> true
- | _ -> false)
-
-let add_token = function
- | ("",kw) -> if is_ident kw then add_keyword kw
- | _ -> ()
-
-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) =
- None
- (*i etait en ocaml 2.xx :
- if p_prm = "" then
- parser [< '(con, prm) when con = p_con >] -> prm
- else
- parser [< '(con, prm) when con = p_con && prm = p_prm >] -> prm
- i*)
-
-}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 10:10:56 +0000