author | wenzelm |
Tue, 21 Mar 2006 12:18:15 +0100 | |
changeset 19305 | 5c16895d548b |
parent 19002 | 2fbb3d809026 |
child 19482 | 9f11af8f7ef9 |
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 |
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
12 |
val implode_xstr: string list -> string |
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
13 |
val explode_xstr: string -> string list |
4703 | 14 |
val scan_id: string list -> string * string list |
15 |
val scan_longid: string list -> string * string list |
|
16 |
val scan_var: string list -> string * string list |
|
17 |
val scan_tid: string list -> string * string list |
|
4902 | 18 |
val scan_tvar: string list -> string * string list |
4703 | 19 |
val scan_nat: string list -> string * string list |
20 |
val scan_int: string list -> string * string list |
|
18 | 21 |
val string_of_vname: indexname -> string |
2583
690835a06cf2
added string_of_vname' (treats neg. index as free);
wenzelm
parents:
2363
diff
changeset
|
22 |
val string_of_vname': indexname -> string |
15443
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
23 |
val indexname: string -> indexname |
4703 | 24 |
val read_var: string -> term |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
25 |
val read_variable: string -> indexname option |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
26 |
val const: string -> term |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
27 |
val free: string -> term |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
28 |
val var: indexname -> term |
9289 | 29 |
val internal: string -> string |
30 |
val dest_internal: string -> string |
|
5260 | 31 |
val skolem: string -> string |
5286 | 32 |
val dest_skolem: string -> string |
5860 | 33 |
val read_nat: string -> int option |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
34 |
val read_xnum: string -> IntInf.int |
7784 | 35 |
val read_idents: string -> string list |
19002 | 36 |
val fixedN: string |
37 |
val constN: string |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
38 |
end; |
0 | 39 |
|
40 |
signature LEXICON = |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
41 |
sig |
18 | 42 |
include LEXICON0 |
43 |
val is_xid: string -> bool |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
44 |
val is_tid: string -> bool |
18 | 45 |
datatype token = |
46 |
Token of string | |
|
47 |
IdentSy of string | |
|
3828 | 48 |
LongIdentSy of string | |
18 | 49 |
VarSy of string | |
50 |
TFreeSy of string | |
|
51 |
TVarSy of string | |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
52 |
NumSy of string | |
11697 | 53 |
XNumSy of string | |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
54 |
StrSy of string | |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
55 |
EndToken |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
56 |
val idT: typ |
3828 | 57 |
val longidT: typ |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
58 |
val varT: typ |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
59 |
val tidT: typ |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
60 |
val tvarT: typ |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
61 |
val terminals: string list |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
62 |
val is_terminal: string -> bool |
18 | 63 |
val str_of_token: token -> string |
64 |
val display_token: token -> string |
|
65 |
val matching_tokens: token * token -> bool |
|
66 |
val valued_token: token -> bool |
|
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
67 |
val predef_term: string -> token option |
4703 | 68 |
val tokenize: Scan.lexicon -> bool -> string list -> token list |
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
69 |
end; |
0 | 70 |
|
14679 | 71 |
structure Lexicon: LEXICON = |
0 | 72 |
struct |
73 |
||
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
74 |
|
18 | 75 |
(** is_identifier etc. **) |
76 |
||
16150 | 77 |
val is_identifier = Symbol.is_ident o Symbol.explode; |
18 | 78 |
|
14679 | 79 |
fun is_ascii_identifier s = |
80 |
let val cs = Symbol.explode s |
|
16150 | 81 |
in forall Symbol.is_ascii cs andalso Symbol.is_ident cs end; |
14679 | 82 |
|
18 | 83 |
fun is_xid s = |
4703 | 84 |
(case Symbol.explode s of |
16150 | 85 |
"_" :: cs => Symbol.is_ident cs |
86 |
| cs => Symbol.is_ident cs); |
|
18 | 87 |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
88 |
fun is_tid s = |
4703 | 89 |
(case Symbol.explode s of |
16150 | 90 |
"'" :: cs => Symbol.is_ident cs |
18 | 91 |
| _ => false); |
92 |
||
0 | 93 |
|
94 |
||
4703 | 95 |
(** basic scanners **) |
96 |
||
97 |
val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::; |
|
98 |
val scan_digits1 = Scan.any1 Symbol.is_digit; |
|
99 |
||
100 |
val scan_id = scan_letter_letdigs >> implode; |
|
101 |
val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode); |
|
102 |
val scan_tid = $$ "'" ^^ scan_id; |
|
103 |
||
104 |
val scan_nat = scan_digits1 >> implode; |
|
5513 | 105 |
val scan_int = $$ "-" ^^ scan_nat || scan_nat; |
4703 | 106 |
|
107 |
val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) ""; |
|
108 |
val scan_var = $$ "?" ^^ scan_id_nat; |
|
4902 | 109 |
val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat; |
4703 | 110 |
|
111 |
||
112 |
||
18 | 113 |
(** string_of_vname **) |
0 | 114 |
|
14783 | 115 |
val string_of_vname = Term.string_of_vname; |
116 |
val string_of_vname' = Term.string_of_vname'; |
|
2583
690835a06cf2
added string_of_vname' (treats neg. index as free);
wenzelm
parents:
2363
diff
changeset
|
117 |
|
18 | 118 |
|
0 | 119 |
|
18 | 120 |
(** datatype token **) |
0 | 121 |
|
18 | 122 |
datatype token = |
123 |
Token of string | |
|
124 |
IdentSy of string | |
|
3828 | 125 |
LongIdentSy of string | |
18 | 126 |
VarSy of string | |
127 |
TFreeSy of string | |
|
128 |
TVarSy of string | |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
129 |
NumSy of string | |
11697 | 130 |
XNumSy of string | |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
131 |
StrSy of string | |
18 | 132 |
EndToken; |
0 | 133 |
|
134 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
135 |
(* terminal arguments *) |
0 | 136 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
137 |
val idT = Type ("id", []); |
3828 | 138 |
val longidT = Type ("longid", []); |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
139 |
val varT = Type ("var", []); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
140 |
val tidT = Type ("tid", []); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
141 |
val tvarT = Type ("tvar", []); |
0 | 142 |
|
11697 | 143 |
val terminals = ["id", "longid", "var", "tid", "tvar", "num", "xnum", "xstr"]; |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
144 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
145 |
fun is_terminal s = s mem terminals; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
146 |
|
0 | 147 |
|
18 | 148 |
(* str_of_token *) |
0 | 149 |
|
18 | 150 |
fun str_of_token (Token s) = s |
151 |
| str_of_token (IdentSy s) = s |
|
3828 | 152 |
| str_of_token (LongIdentSy s) = s |
18 | 153 |
| str_of_token (VarSy s) = s |
154 |
| str_of_token (TFreeSy s) = s |
|
155 |
| str_of_token (TVarSy s) = s |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
156 |
| str_of_token (NumSy s) = s |
11697 | 157 |
| str_of_token (XNumSy s) = s |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
158 |
| str_of_token (StrSy s) = s |
376
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
159 |
| str_of_token EndToken = "EOF"; |
0 | 160 |
|
18 | 161 |
|
162 |
(* display_token *) |
|
0 | 163 |
|
18 | 164 |
fun display_token (Token s) = quote s |
165 |
| display_token (IdentSy s) = "id(" ^ s ^ ")" |
|
3828 | 166 |
| display_token (LongIdentSy s) = "longid(" ^ s ^ ")" |
18 | 167 |
| 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
|
168 |
| display_token (TFreeSy s) = "tid(" ^ s ^ ")" |
18 | 169 |
| display_token (TVarSy s) = "tvar(" ^ s ^ ")" |
11697 | 170 |
| display_token (NumSy s) = "num(" ^ s ^ ")" |
171 |
| display_token (XNumSy s) = "xnum(" ^ s ^ ")" |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
172 |
| display_token (StrSy s) = "xstr(" ^ s ^ ")" |
18 | 173 |
| display_token EndToken = ""; |
0 | 174 |
|
18 | 175 |
|
176 |
(* matching_tokens *) |
|
0 | 177 |
|
18 | 178 |
fun matching_tokens (Token x, Token y) = (x = y) |
179 |
| matching_tokens (IdentSy _, IdentSy _) = true |
|
3828 | 180 |
| matching_tokens (LongIdentSy _, LongIdentSy _) = true |
18 | 181 |
| matching_tokens (VarSy _, VarSy _) = true |
182 |
| matching_tokens (TFreeSy _, TFreeSy _) = true |
|
183 |
| matching_tokens (TVarSy _, TVarSy _) = true |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
184 |
| matching_tokens (NumSy _, NumSy _) = true |
11697 | 185 |
| matching_tokens (XNumSy _, XNumSy _) = true |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
186 |
| matching_tokens (StrSy _, StrSy _) = true |
18 | 187 |
| matching_tokens (EndToken, EndToken) = true |
188 |
| matching_tokens _ = false; |
|
0 | 189 |
|
190 |
||
18 | 191 |
(* valued_token *) |
0 | 192 |
|
18 | 193 |
fun valued_token (Token _) = false |
194 |
| valued_token (IdentSy _) = true |
|
3828 | 195 |
| valued_token (LongIdentSy _) = true |
18 | 196 |
| valued_token (VarSy _) = true |
197 |
| valued_token (TFreeSy _) = true |
|
198 |
| valued_token (TVarSy _) = true |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
199 |
| valued_token (NumSy _) = true |
11697 | 200 |
| valued_token (XNumSy _) = true |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
201 |
| valued_token (StrSy _) = true |
18 | 202 |
| valued_token EndToken = false; |
0 | 203 |
|
204 |
||
18 | 205 |
(* predef_term *) |
0 | 206 |
|
15531 | 207 |
fun predef_term "id" = SOME (IdentSy "id") |
208 |
| predef_term "longid" = SOME (LongIdentSy "longid") |
|
209 |
| predef_term "var" = SOME (VarSy "var") |
|
210 |
| predef_term "tid" = SOME (TFreeSy "tid") |
|
211 |
| predef_term "tvar" = SOME (TVarSy "tvar") |
|
212 |
| predef_term "num" = SOME (NumSy "num") |
|
213 |
| predef_term "xnum" = SOME (XNumSy "xnum") |
|
214 |
| predef_term "xstr" = SOME (StrSy "xstr") |
|
215 |
| predef_term _ = NONE; |
|
0 | 216 |
|
217 |
||
4703 | 218 |
(* xstr tokens *) |
18 | 219 |
|
14730 | 220 |
fun lex_err msg prfx (cs, _) = |
221 |
"Inner lexical error: " ^ msg ^ " at " ^ quote (prfx ^ Symbol.beginning 10 cs); |
|
222 |
||
223 |
val scan_chr = |
|
224 |
$$ "\\" |-- Scan.one Symbol.not_eof || |
|
19305 | 225 |
Scan.one (fn s => s <> "'" andalso Symbol.not_eof s) || |
226 |
$$ "'" --| Scan.ahead (~$$ "'"); |
|
14730 | 227 |
|
228 |
val scan_str = |
|
229 |
$$ "'" |-- $$ "'" |-- !! (lex_err "missing end of string" "''") |
|
230 |
(Scan.repeat scan_chr --| $$ "'" --| $$ "'"); |
|
231 |
||
0 | 232 |
|
4703 | 233 |
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs)); |
18 | 234 |
|
4703 | 235 |
fun explode_xstr str = |
5868 | 236 |
(case Scan.read Symbol.stopper scan_str (Symbol.explode str) of |
15531 | 237 |
SOME cs => cs |
5868 | 238 |
| _ => error ("Inner lexical error: literal string expected at " ^ quote str)); |
18 | 239 |
|
240 |
||
14730 | 241 |
(* nested comments *) |
242 |
||
243 |
val scan_cmt = |
|
244 |
Scan.depend (fn d => $$ "(" ^^ $$ "*" >> pair (d + 1)) || |
|
245 |
Scan.depend (fn 0 => Scan.fail | d => $$ "*" ^^ $$ ")" >> pair (d - 1)) || |
|
19305 | 246 |
Scan.lift ($$ "*" --| Scan.ahead (~$$ ")")) || |
247 |
Scan.lift (Scan.one (fn s => s <> "*" andalso Symbol.not_eof s)); |
|
14730 | 248 |
|
14783 | 249 |
val scan_comment = |
250 |
$$ "(" -- $$ "*" -- !! (lex_err "missing end of comment" "(*") |
|
14730 | 251 |
(Scan.pass 0 (Scan.repeat scan_cmt) -- $$ "*" -- $$ ")") |
14783 | 252 |
>> K (); |
14730 | 253 |
|
254 |
||
18 | 255 |
|
256 |
(** tokenize **) |
|
257 |
||
2363 | 258 |
fun tokenize lex xids chs = |
18 | 259 |
let |
260 |
val scan_xid = |
|
261 |
if xids then $$ "_" ^^ scan_id || scan_id |
|
262 |
else scan_id; |
|
263 |
||
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
264 |
val scan_val = |
4902 | 265 |
scan_tvar >> pair TVarSy || |
4703 | 266 |
scan_var >> pair VarSy || |
267 |
scan_tid >> pair TFreeSy || |
|
11697 | 268 |
scan_int >> pair NumSy || |
269 |
$$ "#" ^^ scan_int >> pair XNumSy || |
|
3828 | 270 |
scan_longid >> pair LongIdentSy || |
18 | 271 |
scan_xid >> pair IdentSy; |
272 |
||
4703 | 273 |
val scan_lit = Scan.literal lex >> (pair Token o implode); |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
274 |
|
4703 | 275 |
val scan_token = |
15531 | 276 |
scan_comment >> K NONE || |
277 |
Scan.max (op <= o pairself snd) scan_lit scan_val >> (fn (tk, s) => SOME (tk s)) || |
|
278 |
scan_str >> (SOME o StrSy o implode_xstr) || |
|
279 |
Scan.one Symbol.is_blank >> K NONE; |
|
18 | 280 |
in |
4938 | 281 |
(case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of |
15570 | 282 |
(toks, []) => List.mapPartial I toks @ [EndToken] |
4703 | 283 |
| (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs))) |
18 | 284 |
end; |
285 |
||
286 |
||
287 |
||
288 |
(** scan variables **) |
|
289 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
290 |
(* scan_indexname *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
291 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
292 |
local |
18 | 293 |
|
294 |
fun scan_vname chrs = |
|
295 |
let |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
296 |
fun nat n [] = n |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
297 |
| nat n (c :: cs) = nat (n * 10 + (ord c - ord "0")) cs; |
18 | 298 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
299 |
fun idxname cs ds = (implode (rev cs), nat 0 ds); |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
300 |
fun chop_idx [] ds = idxname [] ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
301 |
| chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
302 |
| chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
303 |
| chop_idx (c :: cs) ds = |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
304 |
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
|
305 |
else idxname (c :: cs) ds; |
18 | 306 |
|
307 |
val scan = |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
308 |
scan_letter_letdigs -- Scan.optional ($$ "." |-- scan_digits1 >> nat 0) ~1; |
18 | 309 |
in |
310 |
(case scan chrs of |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
311 |
((cs, ~1), cs') => (chop_idx (rev cs) [], cs') |
18 | 312 |
| ((cs, i), cs') => ((implode cs, i), cs')) |
313 |
end; |
|
314 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
315 |
in |
18 | 316 |
|
15443
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
317 |
val scan_indexname = |
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
318 |
$$ "'" |-- scan_vname >> (fn (x, i) => ("'" ^ x, i)) |
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
319 |
|| scan_vname; |
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
320 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
321 |
end; |
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 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
324 |
(* indexname *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
325 |
|
4703 | 326 |
fun indexname cs = |
15443
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
327 |
(case Scan.read Symbol.stopper scan_indexname (Symbol.explode cs) of |
15531 | 328 |
SOME xi => xi |
15443
07f78cc82a73
indexname function now parses type variables as well; changed input
berghofe
parents:
14981
diff
changeset
|
329 |
| _ => error ("Lexical error in variable name: " ^ quote cs)); |
18 | 330 |
|
331 |
||
4703 | 332 |
(* read_var *) |
18 | 333 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
334 |
fun const c = Const (c, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
335 |
fun free x = Free (x, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
336 |
fun var xi = Var (xi, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
337 |
|
4703 | 338 |
fun read_var str = |
18 | 339 |
let |
340 |
val scan = |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
341 |
$$ "?" |-- scan_indexname --| Scan.ahead (Scan.one Symbol.is_eof) >> var || |
4703 | 342 |
Scan.any Symbol.not_eof >> (free o implode); |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
343 |
in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
344 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
345 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
346 |
(* read_variable *) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
347 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
348 |
fun read_variable str = |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
349 |
let val scan = $$ "?" |-- scan_indexname || scan_indexname |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
350 |
in Scan.read Symbol.stopper scan (Symbol.explode str) end; |
4587 | 351 |
|
352 |
||
19002 | 353 |
(* specific identifiers *) |
5260 | 354 |
|
9289 | 355 |
val internal = suffix "_"; |
356 |
val dest_internal = unsuffix "_"; |
|
357 |
||
5286 | 358 |
val skolem = suffix "__"; |
359 |
val dest_skolem = unsuffix "__"; |
|
5260 | 360 |
|
19002 | 361 |
val constN = "\\<^const>"; |
362 |
val fixedN = "\\<^fixed>"; |
|
363 |
||
5260 | 364 |
|
5860 | 365 |
(* read_nat *) |
366 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
367 |
fun read_nat s = |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
368 |
Option.map (#1 o Library.read_int) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
369 |
(Scan.read Symbol.stopper scan_digits1 (Symbol.explode s)); |
5860 | 370 |
|
371 |
||
9326 | 372 |
(* read_xnum *) |
373 |
||
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
374 |
local |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
375 |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
376 |
fun read_intinf cs : IntInf.int * string list = |
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
377 |
let |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
378 |
val zero = ord "0"; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
379 |
val limit = zero + 10; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
380 |
fun scan (num, []) = (num, []) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
381 |
| scan (num, c :: cs) = |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
382 |
if zero <= ord c andalso ord c < limit |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
383 |
then scan (10 * num + IntInf.fromInt (ord c - zero), cs) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
384 |
else (num, c :: cs) |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
385 |
in scan (0, cs) end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
386 |
|
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
387 |
in |
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
388 |
|
9326 | 389 |
fun read_xnum str = |
390 |
let |
|
391 |
val (sign, digs) = |
|
392 |
(case Symbol.explode str of |
|
393 |
"#" :: "-" :: cs => (~1, cs) |
|
394 |
| "#" :: cs => (1, cs) |
|
11697 | 395 |
| "-" :: cs => (~1, cs) |
396 |
| cs => (1, cs)); |
|
15965
f422f8283491
Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents:
15570
diff
changeset
|
397 |
in sign * #1 (read_intinf digs) end; |
9326 | 398 |
|
15991
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
399 |
end; |
670f8e4b5a98
added read_variable: optional question mark on input;
wenzelm
parents:
15965
diff
changeset
|
400 |
|
9326 | 401 |
|
7784 | 402 |
(* read_ident(s) *) |
403 |
||
404 |
fun read_idents str = |
|
405 |
let |
|
406 |
val blanks = Scan.any Symbol.is_blank; |
|
407 |
val junk = Scan.any Symbol.not_eof; |
|
408 |
val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk; |
|
409 |
in |
|
410 |
(case Scan.read Symbol.stopper idents (Symbol.explode str) of |
|
15531 | 411 |
SOME (ids, []) => ids |
412 |
| SOME (_, bad) => error ("Bad identifier: " ^ quote (implode bad)) |
|
413 |
| NONE => error ("No identifier found in: " ^ quote str)) |
|
7784 | 414 |
end; |
415 |
||
0 | 416 |
end; |