blob: 82ee78839a494dd0531ab7adb3155f223f2b00dd (
plain)
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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
|
(**************************************************************************)
(* *)
(* SMTCoq *)
(* Copyright (C) 2011 - 2022 *)
(* *)
(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
type lex_buff = {
buff : bytes;
mutable curr_char : int;
mutable buff_end : int;
in_ch : in_channel
}
let buff_length = 1024
let open_file s name =
try
let in_channel = open_in name in
let buff = Bytes.create buff_length in
let buff_end = input in_channel buff 0 buff_length in
{ buff = buff; curr_char = 0; buff_end = buff_end; in_ch = in_channel }
with _ ->
Printf.printf ("%s file %s does not exists.\n") s name;
exit 1
let close lb =
lb.buff_end <- 0;
close_in lb.in_ch
let eof lb = lb.buff_end == 0
let curr_char lb =
if eof lb then raise End_of_file
else Bytes.get lb.buff lb.curr_char
let refill lb =
let ne = input lb.in_ch lb.buff 0 buff_length in
lb.curr_char <- 0;
lb.buff_end <- ne
(* Unsafe function *)
let is_space c = c == ' ' || c == '\t'
let is_space_ret c = c == ' ' || c == '\n' || c == '\t'
let skip to_skip lb =
while not (eof lb) && to_skip (Bytes.get lb.buff lb.curr_char) do
while lb.curr_char < lb.buff_end && to_skip (Bytes.get lb.buff lb.curr_char) do
lb.curr_char <- lb.curr_char + 1
done;
if lb.curr_char = lb.buff_end then refill lb
done
let skip_space lb = skip is_space lb
let skip_blank lb = skip is_space_ret lb
let skip_string lb s =
let slen = String.length s in
let pos = ref 0 in
while !pos < slen && not (eof lb) && Bytes.get lb.buff lb.curr_char == s.[!pos] do
lb.curr_char <- lb.curr_char + 1;
incr pos;
while !pos < slen && lb.curr_char < lb.buff_end && Bytes.get lb.buff lb.curr_char == s.[!pos] do
lb.curr_char <- lb.curr_char + 1;
incr pos
done;
if lb.curr_char = lb.buff_end then refill lb
done;
!pos = slen
let match_string lb s =
if not (skip_string lb s) then raise (Invalid_argument ("match_string "^s))
let aux_buff = Bytes.create buff_length
let aux_be = ref 0
let aux_pi = ref 0
let aux_cc = ref 0
let save_lb lb =
aux_cc := lb.curr_char;
aux_be := lb.buff_end;
aux_pi := pos_in lb.in_ch;
Bytes.blit lb.buff !aux_cc aux_buff !aux_cc (!aux_be - !aux_cc)
let restore_lb lb =
lb.curr_char <- !aux_cc;
lb.buff_end <- !aux_be;
seek_in lb.in_ch !aux_pi;
Bytes.blit aux_buff !aux_cc lb.buff !aux_cc (!aux_be - !aux_cc)
let check_string lb s =
let slen = String.length s in
if String.length s <= lb.buff_end - lb.curr_char then
let cc = lb.curr_char in
let pos = ref 0 in
while !pos < slen && Bytes.get lb.buff lb.curr_char == s.[!pos] do
lb.curr_char <- lb.curr_char + 1;
incr pos
done;
if !pos = slen then begin
if lb.curr_char = lb.buff_end then refill lb;
true
end else begin
lb.curr_char <- cc;
false
end
else begin
save_lb lb;
let b = skip_string lb s in
if not b then restore_lb lb;
b
end
let blank_check_string lb s =
skip_blank lb;
check_string lb s
let blank_match_string lb s =
skip_blank lb;
match_string lb s
let is_digit c =
'0' <= c && c <= '9'
let is_start_int lb =
skip_blank lb;
not (eof lb) && (is_digit (Bytes.get lb.buff lb.curr_char) || Bytes.get lb.buff lb.curr_char == '-')
let input_int lb =
if eof lb then raise End_of_file
else begin
let sign =
if Bytes.get lb.buff lb.curr_char == '-' then begin
lb.curr_char <- lb.curr_char + 1;
if lb.curr_char = lb.buff_end then refill lb;
-1
end else
1 in
if eof lb then raise End_of_file;
if not (is_digit (Bytes.get lb.buff lb.curr_char)) then raise (Invalid_argument "input_int");
let n = ref (Char.code (Bytes.get lb.buff lb.curr_char) - Char.code '0') in
lb.curr_char <- lb.curr_char + 1;
if lb.curr_char = lb.buff_end then refill lb;
while not (eof lb) && is_digit (Bytes.get lb.buff lb.curr_char) do
while lb.curr_char < lb.buff_end && is_digit (Bytes.get lb.buff lb.curr_char) do
n := !n*10 + (Char.code (Bytes.get lb.buff lb.curr_char) - Char.code '0');
lb.curr_char <- lb.curr_char + 1
done;
if lb.curr_char = lb.buff_end then refill lb
done;
sign * !n
end
let input_blank_int lb =
skip_blank lb;
input_int lb
let skip_line lb =
let notfound = ref true in
while not (eof lb) && !notfound do
while lb.curr_char < lb.buff_end && !notfound do
if Bytes.get lb.buff lb.curr_char == '\n' then notfound := false;
lb.curr_char <- lb.curr_char + 1
done;
if lb.curr_char = lb.buff_end then refill lb
done
|
