author | wenzelm |
Thu, 07 Aug 2008 13:45:13 +0200 | |
changeset 27773 | a52166b228b9 |
parent 27121 | 38367dbccae5 |
child 27800 | df444ddeff56 |
permissions | -rw-r--r-- |
18 | 1 |
(* Title: Pure/Syntax/lexicon.ML |
0 | 2 |
ID: $Id$ |
18 | 3 |
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
0 | 4 |
|
4703 | 5 |
Lexer for the inner Isabelle syntax (terms and types). |
18 | 6 |
*) |
0 | 7 |
|
8 |
signature LEXICON0 = |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
9 |
sig |
0 | 10 |
val is_identifier: string -> bool |
14679 | 11 |
val is_ascii_identifier: string -> bool |
20165 | 12 |
val is_tid: string -> bool |
27773 | 13 |
val scan_id: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
14 |
val scan_longid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
|
15 |
val scan_tid: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
|
16 |
val scan_nat: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
|
17 |
val scan_int: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
|
18 |
val scan_hex: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
|
19 |
val scan_bin: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
|
20 |
val scan_var: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
|
21 |
val scan_tvar: SymbolPos.T list -> SymbolPos.T list * SymbolPos.T list |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
22 |
val implode_xstr: string list -> string |
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
23 |
val explode_xstr: string -> string list |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
24 |
val read_indexname: string -> indexname |
4703 | 25 |
val read_var: string -> term |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
26 |
val read_variable: string -> indexname option |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
27 |
val const: string -> term |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
28 |
val free: string -> term |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
29 |
val var: indexname -> term |
5860 | 30 |
val read_nat: string -> int option |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
31 |
val read_int: string -> int option |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24583
diff
changeset
|
32 |
val read_xnum: string -> {radix: int, leading_zeros: int, value: int} |
19002 | 33 |
val fixedN: string |
34 |
val constN: string |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
35 |
end; |
0 | 36 |
|
37 |
signature LEXICON = |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
38 |
sig |
18 | 39 |
include LEXICON0 |
40 |
val is_xid: string -> bool |
|
41 |
datatype token = |
|
42 |
Token of string | |
|
43 |
IdentSy of string | |
|
3828 | 44 |
LongIdentSy of string | |
18 | 45 |
VarSy of string | |
46 |
TFreeSy of string | |
|
47 |
TVarSy of string | |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
48 |
NumSy of string | |
11697 | 49 |
XNumSy of string | |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
50 |
StrSy of string | |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
51 |
EndToken |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
52 |
val idT: typ |
3828 | 53 |
val longidT: typ |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
54 |
val varT: typ |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
55 |
val tidT: typ |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
56 |
val tvarT: typ |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
57 |
val terminals: string list |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
58 |
val is_terminal: string -> bool |
18 | 59 |
val str_of_token: token -> string |
60 |
val display_token: token -> string |
|
61 |
val matching_tokens: token * token -> bool |
|
62 |
val valued_token: token -> bool |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
63 |
val predef_term: string -> token option |
27773 | 64 |
val tokenize: Scan.lexicon -> bool -> SymbolPos.T list -> token list |
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
65 |
end; |
0 | 66 |
|
14679 | 67 |
structure Lexicon: LEXICON = |
0 | 68 |
struct |
69 |
||
18 | 70 |
(** is_identifier etc. **) |
71 |
||
16150 | 72 |
val is_identifier = Symbol.is_ident o Symbol.explode; |
18 | 73 |
|
14679 | 74 |
fun is_ascii_identifier s = |
75 |
let val cs = Symbol.explode s |
|
16150 | 76 |
in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end; |
14679 | 77 |
|
18 | 78 |
fun is_xid s = |
4703 | 79 |
(case Symbol.explode s of |
16150 | 80 |
"_" :: cs => Symbol.is_ident cs |
81 |
| cs => Symbol.is_ident cs); |
|
18 | 82 |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
83 |
fun is_tid s = |
4703 | 84 |
(case Symbol.explode s of |
16150 | 85 |
"'" :: cs => Symbol.is_ident cs |
18 | 86 |
| _ => false); |
87 |
||
0 | 88 |
|
89 |
||
4703 | 90 |
(** basic scanners **) |
91 |
||
27773 | 92 |
open BasicSymbolPos; |
93 |
||
94 |
fun !!! msg = SymbolPos.!!! ("Inner lexical error: " ^ msg); |
|
95 |
||
96 |
val scan_id = Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol); |
|
97 |
val scan_longid = scan_id @@@ (Scan.repeat1 ($$$ "." @@@ scan_id) >> flat); |
|
98 |
val scan_tid = $$$ "'" @@@ scan_id; |
|
4703 | 99 |
|
27773 | 100 |
val scan_nat = Scan.many1 (Symbol.is_digit o symbol); |
101 |
val scan_int = $$$ "-" @@@ scan_nat || scan_nat; |
|
102 |
val scan_hex = $$$ "0" @@@ $$$ "x" @@@ Scan.many1 (Symbol.is_ascii_hex o symbol); |
|
103 |
val scan_bin = $$$ "0" @@@ $$$ "b" @@@ Scan.many1 (fn (s, _) => s = "0" orelse s = "1"); |
|
4703 | 104 |
|
27773 | 105 |
val scan_id_nat = scan_id @@@ Scan.optional ($$$ "." @@@ scan_nat) []; |
106 |
val scan_var = $$$ "?" @@@ scan_id_nat; |
|
107 |
val scan_tvar = $$$ "?" @@@ $$$ "'" @@@ scan_id_nat; |
|
4703 | 108 |
|
109 |
||
110 |
||
18 | 111 |
(** datatype token **) |
0 | 112 |
|
18 | 113 |
datatype token = |
114 |
Token of string | |
|
115 |
IdentSy of string | |
|
3828 | 116 |
LongIdentSy of string | |
18 | 117 |
VarSy of string | |
118 |
TFreeSy of string | |
|
119 |
TVarSy of string | |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
120 |
NumSy of string | |
11697 | 121 |
XNumSy of string | |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
122 |
StrSy of string | |
18 | 123 |
EndToken; |
0 | 124 |
|
125 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
126 |
(* terminal arguments *) |
0 | 127 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
128 |
val idT = Type ("id", []); |
3828 | 129 |
val longidT = Type ("longid", []); |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
130 |
val varT = Type ("var", []); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
131 |
val tidT = Type ("tid", []); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
132 |
val tvarT = Type ("tvar", []); |
0 | 133 |
|
11697 | 134 |
val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"]; |
20664 | 135 |
val is_terminal = member (op =) terminals; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
136 |
|
0 | 137 |
|
18 | 138 |
(* str_of_token *) |
0 | 139 |
|
18 | 140 |
fun str_of_token (Token s) = s |
141 |
| str_of_token (IdentSy s) = s |
|
3828 | 142 |
| str_of_token (LongIdentSy s) = s |
18 | 143 |
| str_of_token (VarSy s) = s |
144 |
| str_of_token (TFreeSy s) = s |
|
145 |
| str_of_token (TVarSy s) = s |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
146 |
| str_of_token (NumSy s) = s |
11697 | 147 |
| str_of_token (XNumSy s) = s |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
148 |
| str_of_token (StrSy s) = s |
376
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
149 |
| str_of_token EndToken = "EOF"; |
0 | 150 |
|
18 | 151 |
|
152 |
(* display_token *) |
|
0 | 153 |
|
18 | 154 |
fun display_token (Token s) = quote s |
155 |
| display_token (IdentSy s) = "id(" ^ s ^ ")" |
|
3828 | 156 |
| display_token (LongIdentSy s) = "longid(" ^ s ^ ")" |
18 | 157 |
| display_token (VarSy s) = "var(" ^ s ^ ")" |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
158 |
| display_token (TFreeSy s) = "tid(" ^ s ^ ")" |
18 | 159 |
| display_token (TVarSy s) = "tvar(" ^ s ^ ")" |
11697 | 160 |
| display_token (NumSy s) = "num(" ^ s ^ ")" |
161 |
| display_token (XNumSy s) = "xnum(" ^ s ^ ")" |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
162 |
| display_token (StrSy s) = "xstr(" ^ s ^ ")" |
18 | 163 |
| display_token EndToken = ""; |
0 | 164 |
|
18 | 165 |
|
166 |
(* matching_tokens *) |
|
0 | 167 |
|
18 | 168 |
fun matching_tokens (Token x, Token y) = (x = y) |
169 |
| matching_tokens (IdentSy _, IdentSy _) = true |
|
3828 | 170 |
| matching_tokens (LongIdentSy _, LongIdentSy _) = true |
18 | 171 |
| matching_tokens (VarSy _, VarSy _) = true |
172 |
| matching_tokens (TFreeSy _, TFreeSy _) = true |
|
173 |
| matching_tokens (TVarSy _, TVarSy _) = true |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
174 |
| matching_tokens (NumSy _, NumSy _) = true |
11697 | 175 |
| matching_tokens (XNumSy _, XNumSy _) = true |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
176 |
| matching_tokens (StrSy _, StrSy _) = true |
18 | 177 |
| matching_tokens (EndToken, EndToken) = true |
178 |
| matching_tokens _ = false; |
|
0 | 179 |
|
180 |
||
18 | 181 |
(* valued_token *) |
0 | 182 |
|
18 | 183 |
fun valued_token (Token _) = false |
184 |
| valued_token (IdentSy _) = true |
|
3828 | 185 |
| valued_token (LongIdentSy _) = true |
18 | 186 |
| valued_token (VarSy _) = true |
187 |
| valued_token (TFreeSy _) = true |
|
188 |
| valued_token (TVarSy _) = true |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
189 |
| valued_token (NumSy _) = true |
11697 | 190 |
| valued_token (XNumSy _) = true |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
191 |
| valued_token (StrSy _) = true |
18 | 192 |
| valued_token EndToken = false; |
0 | 193 |
|
194 |
||
18 | 195 |
(* predef_term *) |
0 | 196 |
|
15531 | 197 |
fun predef_term "id" = SOME (IdentSy "id") |
198 |
| predef_term "longid" = SOME (LongIdentSy "longid") |
|
199 |
| predef_term "var" = SOME (VarSy "var") |
|
200 |
| predef_term "tid" = SOME (TFreeSy "tid") |
|
201 |
| predef_term "tvar" = SOME (TVarSy "tvar") |
|
202 |
| predef_term "num" = SOME (NumSy "num") |
|
203 |
| predef_term "xnum" = SOME (XNumSy "xnum") |
|
204 |
| predef_term "xstr" = SOME (StrSy "xstr") |
|
205 |
| predef_term _ = NONE; |
|
0 | 206 |
|
207 |
||
4703 | 208 |
(* xstr tokens *) |
18 | 209 |
|
14730 | 210 |
val scan_chr = |
27773 | 211 |
$$$ "\\" |-- $$$ "'" || |
212 |
Scan.one ((fn s => s <> "\\" andalso s <> "'" andalso Symbol.is_regular s) o symbol) >> single || |
|
213 |
$$$ "'" --| Scan.ahead (~$$$ "'"); |
|
14730 | 214 |
|
215 |
val scan_str = |
|
27773 | 216 |
$$$ "'" |-- $$$ "'" |-- !!! "missing end of string" |
217 |
((Scan.repeat scan_chr >> flat) --| $$$ "'" --| $$$ "'"); |
|
14730 | 218 |
|
0 | 219 |
|
4703 | 220 |
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs)); |
18 | 221 |
|
4703 | 222 |
fun explode_xstr str = |
27773 | 223 |
(case Scan.read SymbolPos.stopper scan_str (SymbolPos.explode (str, Position.none)) of |
224 |
SOME cs => map symbol cs |
|
5868 | 225 |
| _ => error ("Inner lexical error: literal string expected at " ^ quote str)); |
18 | 226 |
|
227 |
||
228 |
(** tokenize **) |
|
229 |
||
27773 | 230 |
fun tokenize lex xids inp = |
18 | 231 |
let |
27773 | 232 |
fun token kind ss = (kind, #1 (SymbolPos.implode ss)); |
26007
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
233 |
|
18 | 234 |
val scan_xid = |
27773 | 235 |
if xids then $$$ "_" @@@ scan_id || scan_id |
18 | 236 |
else scan_id; |
237 |
||
20096 | 238 |
val scan_num = scan_hex || scan_bin || scan_int; |
239 |
||
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
240 |
val scan_val = |
26007
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
241 |
scan_tvar >> token TVarSy || |
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
242 |
scan_var >> token VarSy || |
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
243 |
scan_tid >> token TFreeSy || |
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
244 |
scan_num >> token NumSy || |
27773 | 245 |
$$$ "#" @@@ scan_num >> token XNumSy || |
26007
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
246 |
scan_longid >> token LongIdentSy || |
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
247 |
scan_xid >> token IdentSy; |
18 | 248 |
|
26007
3760d3ff4cce
basic scanners: produce symbol list instead of imploded string;
wenzelm
parents:
24630
diff
changeset
|
249 |
val scan_lit = Scan.literal lex >> token Token; |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
250 |
|
4703 | 251 |
val scan_token = |
27773 | 252 |
SymbolPos.scan_comment !!! >> K NONE || |
15531 | 253 |
Scan.max (op <= o pairself snd) scan_lit scan_val >> (fn (tk, s) => SOME (tk s)) || |
27773 | 254 |
scan_str >> (SOME o StrSy o implode_xstr o map symbol) || |
255 |
Scan.one (Symbol.is_blank o symbol) >> K NONE; |
|
18 | 256 |
in |
27773 | 257 |
(case Scan.error |
258 |
(Scan.finite SymbolPos.stopper (Scan.repeat scan_token)) inp of |
|
24245 | 259 |
(toks, []) => map_filter I toks |
27773 | 260 |
| (_, cs) => |
261 |
let val (s, (pos, _)) = SymbolPos.implode cs |
|
262 |
in error ("Inner lexical error at: " ^ quote s ^ Position.str_of pos) end) |
|
18 | 263 |
end; |
264 |
||
265 |
||
266 |
||
267 |
(** scan variables **) |
|
268 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
269 |
(* scan_indexname *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
270 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
271 |
local |
18 | 272 |
|
27773 | 273 |
val scan_vname = |
18 | 274 |
let |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
275 |
fun nat n [] = n |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
276 |
| nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs; |
18 | 277 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
278 |
fun idxname cs ds = (implode (rev cs), nat 0 ds); |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
279 |
fun chop_idx [] ds = idxname [] ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
280 |
| chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
281 |
| chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
282 |
| chop_idx (c :: cs) ds = |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
283 |
if Symbol.is_digit c then chop_idx cs (c :: ds) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
284 |
else idxname (c :: cs) ds; |
18 | 285 |
|
27773 | 286 |
val scan = (scan_id >> map symbol) -- |
287 |
Scan.optional ($$$ "." |-- scan_nat >> (nat 0 o map symbol)) ~1; |
|
18 | 288 |
in |
27773 | 289 |
scan >> |
290 |
(fn (cs, ~1) => chop_idx (rev cs) [] |
|
291 |
| (cs, i) => (implode cs, i)) |
|
18 | 292 |
end; |
293 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
294 |
in |
18 | 295 |
|
27773 | 296 |
val scan_indexname = $$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) || scan_vname; |
15443
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
297 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
298 |
end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
299 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
300 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
301 |
(* indexname *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
302 |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
303 |
fun read_indexname s = |
27773 | 304 |
(case Scan.read SymbolPos.stopper scan_indexname (SymbolPos.explode (s, Position.none)) of |
15531 | 305 |
SOME xi => xi |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
306 |
| _ => error ("Lexical error in variable name: " ^ quote s)); |
18 | 307 |
|
308 |
||
4703 | 309 |
(* read_var *) |
18 | 310 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
311 |
fun const c = Const (c, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
312 |
fun free x = Free (x, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
313 |
fun var xi = Var (xi, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
314 |
|
4703 | 315 |
fun read_var str = |
18 | 316 |
let |
317 |
val scan = |
|
27773 | 318 |
$$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one SymbolPos.is_eof) >> var || |
319 |
Scan.many (Symbol.is_regular o symbol) >> (free o implode o map symbol); |
|
320 |
in the (Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none))) end; |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
321 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
322 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
323 |
(* read_variable *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
324 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
325 |
fun read_variable str = |
27773 | 326 |
let val scan = $$$ "?" |-- scan_indexname || scan_indexname |
327 |
in Scan.read SymbolPos.stopper scan (SymbolPos.explode (str, Position.none)) end; |
|
4587 | 328 |
|
329 |
||
19002 | 330 |
(* specific identifiers *) |
5260 | 331 |
|
19002 | 332 |
val constN = "\\<^const>"; |
333 |
val fixedN = "\\<^fixed>"; |
|
334 |
||
5260 | 335 |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
336 |
(* read numbers *) |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
337 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
338 |
local |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
339 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
340 |
fun nat cs = |
27773 | 341 |
Option.map (#1 o Library.read_int o map symbol) |
342 |
(Scan.read SymbolPos.stopper scan_nat cs); |
|
5860 | 343 |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
344 |
in |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
345 |
|
27773 | 346 |
fun read_nat s = nat (SymbolPos.explode (s, Position.none)); |
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
347 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
348 |
fun read_int s = |
27773 | 349 |
(case SymbolPos.explode (s, Position.none) of |
350 |
("-", _) :: cs => Option.map ~ (nat cs) |
|
20313
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
351 |
| cs => nat cs); |
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
352 |
|
bf9101cc4385
renamed Syntax.indexname to Syntax.read_indexname;
wenzelm
parents:
20165
diff
changeset
|
353 |
end; |
5860 | 354 |
|
355 |
||
20096 | 356 |
(* read_xnum: hex/bin/decimal *) |
9326 | 357 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
358 |
local |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
359 |
|
20096 | 360 |
val ten = ord "0" + 10; |
361 |
val a = ord "a"; |
|
362 |
val A = ord "A"; |
|
23802 | 363 |
val _ = a > A orelse sys_error "Bad ASCII"; |
20096 | 364 |
|
365 |
fun remap_hex c = |
|
366 |
let val x = ord c in |
|
367 |
if x >= a then chr (x - a + ten) |
|
368 |
else if x >= A then chr (x - A + ten) |
|
369 |
else c |
|
370 |
end; |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
371 |
|
21781 | 372 |
fun leading_zeros ["0"] = 0 |
373 |
| leading_zeros ("0" :: cs) = 1 + leading_zeros cs |
|
374 |
| leading_zeros _ = 0; |
|
375 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
376 |
in |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
377 |
|
9326 | 378 |
fun read_xnum str = |
379 |
let |
|
20096 | 380 |
val (sign, radix, digs) = |
381 |
(case Symbol.explode (perhaps (try (unprefix "#")) str) of |
|
382 |
"0" :: "x" :: cs => (1, 16, map remap_hex cs) |
|
383 |
| "0" :: "b" :: cs => (1, 2, cs) |
|
384 |
| "-" :: cs => (~1, 10, cs) |
|
385 |
| cs => (1, 10, cs)); |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24583
diff
changeset
|
386 |
val value = sign * #1 (Library.read_radix_int radix digs); |
21781 | 387 |
in {radix = radix, leading_zeros = leading_zeros digs, value = value} end; |
9326 | 388 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
389 |
end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
390 |
|
0 | 391 |
end; |