author | nipkow |
Fri, 07 Feb 2003 15:36:12 +0100 | |
changeset 13808 | f67a53bf63bc |
parent 12785 | 27debaf2112d |
child 14679 | 6ed90bd68eda |
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 |
12785 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
0 | 5 |
|
4703 | 6 |
Lexer for the inner Isabelle syntax (terms and types). |
18 | 7 |
*) |
0 | 8 |
|
9 |
signature LEXICON0 = |
|
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
10 |
sig |
0 | 11 |
val is_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 |
4703 | 23 |
val indexname: string list -> indexname |
24 |
val read_var: string -> term |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
25 |
val const: string -> term |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
26 |
val free: string -> term |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
27 |
val var: indexname -> term |
9289 | 28 |
val internal: string -> string |
29 |
val dest_internal: string -> string |
|
5260 | 30 |
val skolem: string -> string |
5286 | 31 |
val dest_skolem: string -> string |
5860 | 32 |
val read_nat: string -> int option |
9326 | 33 |
val read_xnum: string -> int |
7784 | 34 |
val read_idents: string -> string list |
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 |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
41 |
val is_tid: string -> bool |
18 | 42 |
datatype token = |
43 |
Token of string | |
|
44 |
IdentSy of string | |
|
3828 | 45 |
LongIdentSy of string | |
18 | 46 |
VarSy of string | |
47 |
TFreeSy of string | |
|
48 |
TVarSy of string | |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
49 |
NumSy of string | |
11697 | 50 |
XNumSy of string | |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
51 |
StrSy of string | |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
52 |
EndToken |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
53 |
val idT: typ |
3828 | 54 |
val longidT: typ |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
55 |
val varT: typ |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
56 |
val tidT: typ |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
57 |
val tvarT: typ |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
58 |
val terminals: string list |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
59 |
val is_terminal: string -> bool |
18 | 60 |
val str_of_token: token -> string |
61 |
val display_token: token -> string |
|
62 |
val matching_tokens: token * token -> bool |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
63 |
val token_assoc: (token option * 'a list) list * token -> 'a list |
18 | 64 |
val valued_token: token -> bool |
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
65 |
val predef_term: string -> token option |
4703 | 66 |
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
|
67 |
end; |
0 | 68 |
|
1507 | 69 |
structure Lexicon : LEXICON = |
0 | 70 |
struct |
71 |
||
4247
9bba9251bb4d
added implode_xstr: string list -> string, explode_xstr: string -> string list;
wenzelm
parents:
3828
diff
changeset
|
72 |
|
18 | 73 |
(** is_identifier etc. **) |
74 |
||
75 |
fun is_ident [] = false |
|
4703 | 76 |
| is_ident (c :: cs) = Symbol.is_letter c andalso forall Symbol.is_letdig cs; |
18 | 77 |
|
4703 | 78 |
val is_identifier = is_ident o Symbol.explode; |
18 | 79 |
|
80 |
fun is_xid s = |
|
4703 | 81 |
(case Symbol.explode s of |
18 | 82 |
"_" :: cs => is_ident cs |
83 |
| cs => is_ident cs); |
|
84 |
||
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
85 |
fun is_tid s = |
4703 | 86 |
(case Symbol.explode s of |
18 | 87 |
"'" :: cs => is_ident cs |
88 |
| _ => false); |
|
89 |
||
0 | 90 |
|
91 |
||
4703 | 92 |
(** basic scanners **) |
93 |
||
94 |
val scan_letter_letdigs = Scan.one Symbol.is_letter -- Scan.any Symbol.is_letdig >> op ::; |
|
95 |
val scan_digits1 = Scan.any1 Symbol.is_digit; |
|
96 |
||
97 |
val scan_id = scan_letter_letdigs >> implode; |
|
98 |
val scan_longid = scan_id ^^ (Scan.repeat1 ($$ "." ^^ scan_id) >> implode); |
|
99 |
val scan_tid = $$ "'" ^^ scan_id; |
|
100 |
||
101 |
val scan_nat = scan_digits1 >> implode; |
|
5513 | 102 |
val scan_int = $$ "-" ^^ scan_nat || scan_nat; |
4703 | 103 |
|
104 |
val scan_id_nat = scan_id ^^ Scan.optional ($$ "." ^^ scan_nat) ""; |
|
105 |
val scan_var = $$ "?" ^^ scan_id_nat; |
|
4902 | 106 |
val scan_tvar = $$ "?" ^^ $$ "'" ^^ scan_id_nat; |
4703 | 107 |
|
108 |
||
109 |
||
18 | 110 |
(** string_of_vname **) |
0 | 111 |
|
18 | 112 |
fun string_of_vname (x, i) = |
113 |
let |
|
114 |
val si = string_of_int i; |
|
6962 | 115 |
val dot = if_none (try (Symbol.is_digit o last_elem o Symbol.explode) x) true; |
18 | 116 |
in |
4703 | 117 |
if dot then "?" ^ x ^ "." ^ si |
118 |
else if i = 0 then "?" ^ x |
|
119 |
else "?" ^ x ^ si |
|
18 | 120 |
end; |
0 | 121 |
|
4703 | 122 |
fun string_of_vname' (x, ~1) = x |
123 |
| string_of_vname' xi = string_of_vname xi; |
|
2583
690835a06cf2
added string_of_vname' (treats neg. index as free);
wenzelm
parents:
2363
diff
changeset
|
124 |
|
18 | 125 |
|
0 | 126 |
|
18 | 127 |
(** datatype token **) |
0 | 128 |
|
18 | 129 |
datatype token = |
130 |
Token of string | |
|
131 |
IdentSy of string | |
|
3828 | 132 |
LongIdentSy of string | |
18 | 133 |
VarSy of string | |
134 |
TFreeSy of string | |
|
135 |
TVarSy of string | |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
136 |
NumSy of string | |
11697 | 137 |
XNumSy of string | |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
138 |
StrSy of string | |
18 | 139 |
EndToken; |
0 | 140 |
|
141 |
||
237
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
142 |
(* terminal arguments *) |
0 | 143 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
144 |
val idT = Type ("id", []); |
3828 | 145 |
val longidT = Type ("longid", []); |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
146 |
val varT = Type ("var", []); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
147 |
val tidT = Type ("tid", []); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
148 |
val tvarT = Type ("tvar", []); |
0 | 149 |
|
11697 | 150 |
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
|
151 |
|
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
152 |
fun is_terminal s = s mem terminals; |
a7d3e712767a
MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables
wenzelm
parents:
164
diff
changeset
|
153 |
|
0 | 154 |
|
18 | 155 |
(* str_of_token *) |
0 | 156 |
|
18 | 157 |
fun str_of_token (Token s) = s |
158 |
| str_of_token (IdentSy s) = s |
|
3828 | 159 |
| str_of_token (LongIdentSy s) = s |
18 | 160 |
| str_of_token (VarSy s) = s |
161 |
| str_of_token (TFreeSy s) = s |
|
162 |
| str_of_token (TVarSy s) = s |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
163 |
| str_of_token (NumSy s) = s |
11697 | 164 |
| str_of_token (XNumSy s) = s |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
165 |
| str_of_token (StrSy s) = s |
376
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
166 |
| str_of_token EndToken = "EOF"; |
0 | 167 |
|
18 | 168 |
|
169 |
(* display_token *) |
|
0 | 170 |
|
18 | 171 |
fun display_token (Token s) = quote s |
172 |
| display_token (IdentSy s) = "id(" ^ s ^ ")" |
|
3828 | 173 |
| display_token (LongIdentSy s) = "longid(" ^ s ^ ")" |
18 | 174 |
| 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
|
175 |
| display_token (TFreeSy s) = "tid(" ^ s ^ ")" |
18 | 176 |
| display_token (TVarSy s) = "tvar(" ^ s ^ ")" |
11697 | 177 |
| display_token (NumSy s) = "num(" ^ s ^ ")" |
178 |
| display_token (XNumSy s) = "xnum(" ^ s ^ ")" |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
179 |
| display_token (StrSy s) = "xstr(" ^ s ^ ")" |
18 | 180 |
| display_token EndToken = ""; |
0 | 181 |
|
18 | 182 |
|
183 |
(* matching_tokens *) |
|
0 | 184 |
|
18 | 185 |
fun matching_tokens (Token x, Token y) = (x = y) |
186 |
| matching_tokens (IdentSy _, IdentSy _) = true |
|
3828 | 187 |
| matching_tokens (LongIdentSy _, LongIdentSy _) = true |
18 | 188 |
| matching_tokens (VarSy _, VarSy _) = true |
189 |
| matching_tokens (TFreeSy _, TFreeSy _) = true |
|
190 |
| matching_tokens (TVarSy _, TVarSy _) = true |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
191 |
| matching_tokens (NumSy _, NumSy _) = true |
11697 | 192 |
| matching_tokens (XNumSy _, XNumSy _) = true |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
193 |
| matching_tokens (StrSy _, StrSy _) = true |
18 | 194 |
| matching_tokens (EndToken, EndToken) = true |
195 |
| matching_tokens _ = false; |
|
0 | 196 |
|
197 |
||
376
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
198 |
(* token_assoc *) |
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
199 |
|
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
200 |
fun token_assoc (list, key) = |
376
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
201 |
let |
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
202 |
fun assoc [] = [] |
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
203 |
| assoc ((keyi, xi) :: pairs) = |
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
204 |
if is_none keyi orelse matching_tokens (the keyi, key) then |
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
205 |
assoc pairs @ xi |
d3d01131470f
extended signature SCANNER by some basic scanners and type lexicon;
wenzelm
parents:
330
diff
changeset
|
206 |
else assoc pairs; |
330
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
207 |
in assoc list end; |
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
208 |
|
2fda15dd1e0f
changed the way a grammar is generated to allow the new parser to work;
clasohm
parents:
237
diff
changeset
|
209 |
|
18 | 210 |
(* valued_token *) |
0 | 211 |
|
18 | 212 |
fun valued_token (Token _) = false |
213 |
| valued_token (IdentSy _) = true |
|
3828 | 214 |
| valued_token (LongIdentSy _) = true |
18 | 215 |
| valued_token (VarSy _) = true |
216 |
| valued_token (TFreeSy _) = true |
|
217 |
| valued_token (TVarSy _) = true |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
218 |
| valued_token (NumSy _) = true |
11697 | 219 |
| valued_token (XNumSy _) = true |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
220 |
| valued_token (StrSy _) = true |
18 | 221 |
| valued_token EndToken = false; |
0 | 222 |
|
223 |
||
18 | 224 |
(* predef_term *) |
0 | 225 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
226 |
fun predef_term "id" = Some (IdentSy "id") |
3828 | 227 |
| predef_term "longid" = Some (LongIdentSy "longid") |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
228 |
| predef_term "var" = Some (VarSy "var") |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
229 |
| predef_term "tid" = Some (TFreeSy "tid") |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
230 |
| predef_term "tvar" = Some (TVarSy "tvar") |
11697 | 231 |
| predef_term "num" = Some (NumSy "num") |
232 |
| predef_term "xnum" = Some (XNumSy "xnum") |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
233 |
| predef_term "xstr" = Some (StrSy "xstr") |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
234 |
| predef_term _ = None; |
0 | 235 |
|
236 |
||
13808 | 237 |
fun scan_enclosed(a1,a2,z1,z2,kind) = |
238 |
let val scan_chr = |
|
239 |
$$ "\\" |-- Scan.one Symbol.not_eof || |
|
240 |
Scan.one (not_equal z1 andf Symbol.not_eof) || |
|
241 |
$$ z1 --| Scan.ahead (Scan.one (not_equal z2)); |
|
242 |
in $$ a1 |-- $$ a2 |-- |
|
243 |
!! (fn (cs, _) => "Inner lexical error: missing end of " ^ kind ^ " at " ^ |
|
244 |
quote (a1 ^ a2 ^ Symbol.beginning cs)) |
|
245 |
(Scan.repeat scan_chr --| $$ z1 --| $$ z2) |
|
246 |
end; |
|
247 |
||
4703 | 248 |
(* xstr tokens *) |
18 | 249 |
|
13808 | 250 |
val scan_str = scan_enclosed("'","'","'","'","string") |
0 | 251 |
|
4703 | 252 |
fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs)); |
18 | 253 |
|
4703 | 254 |
fun explode_xstr str = |
5868 | 255 |
(case Scan.read Symbol.stopper scan_str (Symbol.explode str) of |
256 |
Some cs => cs |
|
257 |
| _ => error ("Inner lexical error: literal string expected at " ^ quote str)); |
|
18 | 258 |
|
259 |
||
13808 | 260 |
val scan_comment = scan_enclosed("(","*","*",")","comment") |
18 | 261 |
|
262 |
(** tokenize **) |
|
263 |
||
2363 | 264 |
fun tokenize lex xids chs = |
18 | 265 |
let |
266 |
val scan_xid = |
|
267 |
if xids then $$ "_" ^^ scan_id || scan_id |
|
268 |
else scan_id; |
|
269 |
||
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
270 |
val scan_val = |
4902 | 271 |
scan_tvar >> pair TVarSy || |
4703 | 272 |
scan_var >> pair VarSy || |
273 |
scan_tid >> pair TFreeSy || |
|
11697 | 274 |
scan_int >> pair NumSy || |
275 |
$$ "#" ^^ scan_int >> pair XNumSy || |
|
3828 | 276 |
scan_longid >> pair LongIdentSy || |
18 | 277 |
scan_xid >> pair IdentSy; |
278 |
||
4703 | 279 |
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
|
280 |
|
4703 | 281 |
val scan_token = |
13808 | 282 |
scan_comment >> K None || |
4703 | 283 |
Scan.max (op <= o pairself snd) scan_lit scan_val >> (fn (tk, s) => Some (tk s)) || |
284 |
scan_str >> (Some o StrSy o implode_xstr) || |
|
285 |
Scan.one Symbol.is_blank >> K None; |
|
18 | 286 |
in |
4938 | 287 |
(case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of |
4703 | 288 |
(toks, []) => mapfilter I toks @ [EndToken] |
289 |
| (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs))) |
|
18 | 290 |
end; |
291 |
||
292 |
||
293 |
||
294 |
(** scan variables **) |
|
295 |
||
296 |
(* scan_vname *) |
|
297 |
||
298 |
fun scan_vname chrs = |
|
299 |
let |
|
300 |
fun nat_of_chs n [] = n |
|
301 |
| nat_of_chs n (c :: cs) = nat_of_chs (n * 10 + (ord c - ord "0")) cs; |
|
302 |
||
4703 | 303 |
val nat = nat_of_chs 0; |
18 | 304 |
|
305 |
fun split_vname chs = |
|
4703 | 306 |
let val (cs, ds) = take_suffix Symbol.is_digit chs |
307 |
in (implode cs, nat ds) end |
|
18 | 308 |
|
309 |
val scan = |
|
4703 | 310 |
scan_letter_letdigs -- Scan.optional ($$ "." |-- scan_digits1 >> nat) ~1; |
18 | 311 |
in |
312 |
(case scan chrs of |
|
313 |
((cs, ~1), cs') => (split_vname cs, cs') |
|
314 |
| ((cs, i), cs') => ((implode cs, i), cs')) |
|
315 |
end; |
|
316 |
||
317 |
||
4703 | 318 |
(* indexname *) |
18 | 319 |
|
4703 | 320 |
fun indexname cs = |
5868 | 321 |
(case Scan.read Symbol.stopper scan_vname cs of |
322 |
Some xi => xi |
|
4703 | 323 |
| _ => error ("Lexical error in variable name: " ^ quote (implode cs))); |
18 | 324 |
|
325 |
||
4703 | 326 |
(* read_var *) |
18 | 327 |
|
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
328 |
fun const c = Const (c, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
329 |
fun free x = Free (x, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
330 |
fun var xi = Var (xi, dummyT); |
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
331 |
|
4703 | 332 |
fun read_var str = |
18 | 333 |
let |
550
353eea6ec232
replaced id, var, tid, tvar by idT, varT, tidT, tvarT;
wenzelm
parents:
376
diff
changeset
|
334 |
fun tvar (x, i) = var ("'" ^ x, i); |
18 | 335 |
|
336 |
val scan = |
|
4703 | 337 |
$$ "?" |-- $$ "'" |-- scan_vname >> tvar || |
338 |
$$ "?" |-- scan_vname >> var || |
|
339 |
Scan.any Symbol.not_eof >> (free o implode); |
|
5868 | 340 |
in the (Scan.read Symbol.stopper scan (Symbol.explode str)) end; |
4587 | 341 |
|
342 |
||
5260 | 343 |
(* variable kinds *) |
344 |
||
9289 | 345 |
val internal = suffix "_"; |
346 |
val dest_internal = unsuffix "_"; |
|
347 |
||
5286 | 348 |
val skolem = suffix "__"; |
349 |
val dest_skolem = unsuffix "__"; |
|
5260 | 350 |
|
351 |
||
5860 | 352 |
(* read_nat *) |
353 |
||
354 |
fun read_nat str = |
|
5868 | 355 |
apsome (#1 o Term.read_int) (Scan.read Symbol.stopper scan_digits1 (Symbol.explode str)); |
5860 | 356 |
|
357 |
||
9326 | 358 |
(* read_xnum *) |
359 |
||
360 |
fun read_xnum str = |
|
361 |
let |
|
362 |
val (sign, digs) = |
|
363 |
(case Symbol.explode str of |
|
364 |
"#" :: "-" :: cs => (~1, cs) |
|
365 |
| "#" :: cs => (1, cs) |
|
11697 | 366 |
| "-" :: cs => (~1, cs) |
367 |
| cs => (1, cs)); |
|
9326 | 368 |
in sign * #1 (Term.read_int digs) end; |
369 |
||
370 |
||
7784 | 371 |
(* read_ident(s) *) |
372 |
||
373 |
fun read_idents str = |
|
374 |
let |
|
375 |
val blanks = Scan.any Symbol.is_blank; |
|
376 |
val junk = Scan.any Symbol.not_eof; |
|
377 |
val idents = Scan.repeat1 (blanks |-- scan_id --| blanks) -- junk; |
|
378 |
in |
|
379 |
(case Scan.read Symbol.stopper idents (Symbol.explode str) of |
|
380 |
Some (ids, []) => ids |
|
381 |
| Some (_, bad) => error ("Bad identifier: " ^ quote (implode bad)) |
|
382 |
| None => error ("No identifier found in: " ^ quote str)) |
|
383 |
end; |
|
384 |
||
385 |
||
0 | 386 |
end; |