-
Notifications
You must be signed in to change notification settings - Fork 3
/
lexer.mll
executable file
·153 lines (133 loc) · 4.28 KB
/
lexer.mll
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
{
(** The lexer. *)
open Parser
let reserved = [
("forall", FORALL);
("fun", FUN);
("Type", TYPE);
("impossible", IMPOSSIBLE);
("on", ON) ;
("yields", YIELDS) ;
("On", SET_ON) ;
("Off", SET_OFF) ;
("hrefl", REFL) ;
("hsubst", SUBST)
]
let directives = [
("Check", CHECK) ;
("Definition", DEFINITION) ;
("Recursive", RECURSIVE) ;
("Split", SPLIT) ;
("Eval", EVAL) ;
("Whnf", WHNF) ;
("Help", HELP) ;
("Version", VERSION) ;
("Axiom", AXIOM);
("Context", CONTEXT) ;
("Inductive", INDUCTIVE) ;
("Load", LOAD) ;
("Reset", RESET) ;
("Set", SET) ;
("Get", GET) ;
("Quit", QUIT)
]
let position_of_lex lex =
Common.Position (Lexing.lexeme_start_p lex, Lexing.lexeme_end_p lex)
(* To buffer string literals *)
let string_buffer = ref ""
let reset_string_buffer () =
string_buffer := ""
let store_string_char c =
string_buffer := !string_buffer ^ Char.escaped c
let store_string s =
string_buffer := !string_buffer ^ s
let store_lexeme lexbuf =
store_string (Lexing.lexeme lexbuf)
let get_stored_string () = !string_buffer
}
let name = ['a'-'z' 'A'-'Z'] ['_' '-' 'a'-'z' 'A'-'Z' '0'-'9' '\'']*
let numeral = ['0'-'9']+
rule token = parse
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| [' ' '\r' '\t'] { token lexbuf }
| numeral { NUMERAL (int_of_string (Lexing.lexeme lexbuf)) }
| "\""
{ reset_string_buffer();
string lexbuf;
STRING (get_stored_string())
}
| "CommandLine" { option lexbuf}
| name { let s = Lexing.lexeme lexbuf in
try
List.assoc s reserved
with Not_found ->
(try
List.assoc s directives
with Not_found -> NAME s)
}
| '(' { LPAREN }
| ')' { RPAREN }
| '[' { LSQ }
| ']' { RSQ }
| "." { PERIOD }
| ':' { COLON }
| ',' { COMMA }
| ';' { SEMICOLON }
| "->" { ARROW }
| "=>" { DARROW }
| ":=" { COLONEQUAL }
| '=' { EQUAL }
| "|" { BAR }
| "(*" { comments 0 lexbuf }
| eof { EOF }
and comments level = parse
| "*)" { if level = 0 then token lexbuf else comments (level-1) lexbuf }
| "(*" { comments (level+1) lexbuf }
| '\n' { Lexing.new_line lexbuf; comments level lexbuf }
| _ { comments level lexbuf }
| eof { print_endline "comments are not closed";
raise End_of_file }
and string = parse
| '"' { () }
| "\\\"" { store_string_char '"' ; string lexbuf }
| eof { Error.violation "Unterminated String" }
| _ { store_string_char(Lexing.lexeme_char lexbuf 0); string lexbuf }
and option = parse
| [^'\n''.']* { OPTION (Lexing.lexeme lexbuf) }
| '.' { PERIOD }
| '\n' { Lexing.new_line lexbuf; token lexbuf }
{
let read_file parser fn =
try
let fh = open_in fn in
let lex = Lexing.from_channel fh in
lex.Lexing.lex_curr_p <- {lex.Lexing.lex_curr_p with Lexing.pos_fname = fn};
try
let terms = parser lex in
close_in fh;
terms
with
(* Close the file in case of any parsing errors. *)
Error.Error err -> close_in fh; raise (Error.Error err)
with
(* Any errors when opening or closing a file are fatal. *)
Sys_error msg -> Error.fatal ~loc:Common.Nowhere "%s" msg
let read_toplevel parser () =
let ends_with_period str =
let i = ref (String.length str - 1) in
while !i >= 0 && List.mem str.[!i] [' '; '\n'; '\t'; '\r'] do decr i done ;
!i >= 0 && str.[!i] = '.'
in
let rec read_more prompt acc =
if ends_with_period acc
then acc
else begin
print_string prompt ;
let str = read_line () in
read_more " " (acc ^ "\n" ^ str)
end
in
let str = read_more "# " "" in
let lex = Lexing.from_string (str ^ "\n") in
parser lex
}