1 (* Title: Lexicon |
1 (* Title: Pure/Syntax/lexicon.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow, TU Muenchen |
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
4 Copyright 1993 TU Muenchen |
4 |
5 |
5 Scanner combinators and Isabelle's main lexer (used for terms and typs). |
6 The Isabelle Lexer |
|
7 |
|
8 Changes: |
|
9 TODO: |
|
10 Lexicon -> lexicon, Token -> token |
|
11 end_token -> EndToken ? |
|
12 *) |
6 *) |
|
7 |
|
8 infix 5 -- ^^; |
|
9 infix 3 >>; |
|
10 infix 0 ||; |
13 |
11 |
14 signature LEXICON0 = |
12 signature LEXICON0 = |
15 sig |
13 sig |
16 val is_identifier: string -> bool |
14 val is_identifier: string -> bool |
|
15 val string_of_vname: indexname -> string |
17 val scan_varname: string list -> indexname * string list |
16 val scan_varname: string list -> indexname * string list |
18 val string_of_vname: indexname -> string |
17 val scan_var: string -> term |
19 end; |
18 end; |
20 |
19 |
21 signature LEXICON = |
20 signature LEXICON = |
22 sig |
21 sig |
23 type Lexicon |
22 include LEXICON0 |
24 datatype Token = Token of string |
23 val is_xid: string -> bool |
25 | IdentSy of string |
24 val is_tfree: string -> bool |
26 | VarSy of string * int |
25 type lexicon |
27 | TFreeSy of string |
26 datatype token = |
28 | TVarSy of string * int |
27 Token of string | |
29 | end_token; |
28 IdentSy of string | |
30 val empty: Lexicon |
29 VarSy of string | |
31 val extend: Lexicon * string list -> Lexicon |
30 TFreeSy of string | |
32 val matching_tokens: Token * Token -> bool |
31 TVarSy of string | |
33 val mk_lexicon: string list -> Lexicon |
32 EndToken; |
34 val name_of_token: Token -> string |
33 val id: string |
35 val predef_term: string -> Token |
34 val var: string |
|
35 val tfree: string |
|
36 val tvar: string |
|
37 val str_of_token: token -> string |
|
38 val display_token: token -> string |
|
39 val matching_tokens: token * token -> bool |
|
40 val valued_token: token -> bool |
|
41 val predef_term: string -> token |
36 val is_terminal: string -> bool |
42 val is_terminal: string -> bool |
37 val tokenize: Lexicon -> string -> Token list |
43 val empty_lexicon: lexicon |
38 val token_to_string: Token -> string |
44 val extend_lexicon: lexicon -> string list -> lexicon |
39 val valued_token: Token -> bool |
45 val mk_lexicon: string list -> lexicon |
40 type 'b TokenMap |
46 val tokenize: lexicon -> bool -> string -> token list |
41 val mkTokenMap: ('b * Token list) list -> 'b TokenMap |
47 |
42 val applyTokenMap: 'b TokenMap * Token -> 'b list |
48 exception LEXICAL_ERROR |
43 include LEXICON0 |
49 val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c |
|
50 val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b |
|
51 val -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e |
|
52 val ^^ : ('a -> string * 'b) * ('b -> string * 'c) -> 'a -> string * 'c |
|
53 val $$ : ''a -> ''a list -> ''a * ''a list |
|
54 val scan_empty: 'a list -> 'b list * 'a list |
|
55 val scan_one: ('a -> bool) -> 'a list -> 'a * 'a list |
|
56 val scan_any: ('a -> bool) -> 'a list -> 'a list * 'a list |
|
57 val scan_any1: ('a -> bool) -> 'a list -> 'a list * 'a list |
|
58 val scan_end: 'a list -> 'b list * 'a list |
|
59 val optional: ('a -> 'b * 'a) -> 'a -> 'b option * 'a |
|
60 val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
|
61 val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
44 end; |
62 end; |
45 |
63 |
46 functor LexiconFun(Extension: EXTENSION): LEXICON = |
64 functor LexiconFun(): LEXICON = |
47 struct |
65 struct |
48 |
66 |
49 open Extension; |
67 |
50 |
68 (** is_identifier etc. **) |
51 |
69 |
52 datatype Token = Token of string |
70 fun is_ident [] = false |
53 | IdentSy of string |
71 | is_ident (c :: cs) = is_letter c andalso forall is_letdig cs; |
54 | VarSy of string * int |
72 |
55 | TFreeSy of string |
73 val is_identifier = is_ident o explode; |
56 | TVarSy of string * int |
74 |
57 | end_token; |
75 fun is_xid s = |
58 val no_token = ""; |
76 (case explode s of |
59 |
77 "_" :: cs => is_ident cs |
60 datatype dfa = Tip | Branch of string * string * dfa * dfa * dfa; |
78 | cs => is_ident cs); |
61 |
79 |
62 type Lexicon = dfa; |
80 fun is_tfree s = |
63 |
81 (case explode s of |
64 fun is_id(c::cs) = is_letter(c) andalso forall is_letdig cs |
82 "'" :: cs => is_ident cs |
65 | is_id([]) = false; |
83 | _ => false); |
66 |
84 |
67 fun is_identifier s = is_id(explode s); |
85 |
68 |
86 |
69 val empty = Tip; |
87 (** string_of_vname **) |
70 |
88 |
71 fun extend1(dfa, s) = |
89 fun string_of_vname (x, i) = |
72 let fun add(Branch(c, a, less, eq, gr), cs as (d::ds)) = |
90 let |
73 if c>d then Branch(c, a, add(less, cs), eq, gr) else |
91 val si = string_of_int i; |
74 if c<d then Branch(c, a, less, eq, add(gr, cs)) else |
92 in |
75 Branch(c, if null ds then s else a, less, add(eq, ds), gr) |
93 if is_digit (last_elem (explode x)) then "?" ^ x ^ "." ^ si |
76 | add(Tip, c::cs) = |
94 else if i = 0 then "?" ^ x |
77 Branch(c, if null cs then s else no_token, Tip, add(Tip, cs), Tip) |
95 else "?" ^ x ^ si |
78 | add(dfa, []) = dfa |
96 end; |
79 |
97 |
80 in add(dfa, explode s) end; |
98 |
81 |
99 |
82 val extend = foldl extend1; |
100 (** datatype token **) |
83 |
101 |
84 fun mk_lexicon ss = extend(empty, ss); |
102 datatype token = |
85 |
103 Token of string | |
86 fun next_dfa (Tip, _) = None |
104 IdentSy of string | |
87 | next_dfa (Branch(d, a, less, eq, gr), c) = |
105 VarSy of string | |
88 if c<d then next_dfa(less, c) else |
106 TFreeSy of string | |
89 if c>d then next_dfa(gr, c) else Some(a, eq); |
107 TVarSy of string | |
90 |
108 EndToken; |
91 exception ID of string * string list; |
109 |
92 |
110 |
93 val eof_id = "End of input - identifier expected.\n"; |
111 (* names of valued tokens *) |
94 |
112 |
95 (*A string of letters, digits, or ' _ *) |
113 val id = "id"; |
96 fun xscan_ident exn = |
114 val var = "var"; |
97 let fun scan [] = raise exn(eof_id, []) |
115 val tfree = "tfree"; |
98 | scan(c::cs) = |
116 val tvar = "tvar"; |
99 if is_letter c |
117 |
100 then let val (ds, tail) = take_prefix is_letdig cs |
118 |
101 in (implode(c::ds), tail) end |
119 (* str_of_token *) |
102 else raise exn("Identifier expected: ", c::cs) |
120 |
103 in scan end; |
121 fun str_of_token (Token s) = s |
104 |
122 | str_of_token (IdentSy s) = s |
105 (*Scan the offset of a Var, if present; otherwise ~1 *) |
123 | str_of_token (VarSy s) = s |
106 fun scan_offset cs = case cs of |
124 | str_of_token (TFreeSy s) = s |
107 ("."::[]) => (~1, cs) |
125 | str_of_token (TVarSy s) = s |
108 | ("."::(ds as c::cs')) => if is_digit c then scan_int ds else (~1, cs) |
126 | str_of_token EndToken = ""; |
109 | _ => (~1, cs); |
127 |
110 |
128 |
111 fun split_varname s = |
129 (* display_token *) |
112 let val (rpost, rpref) = take_prefix is_digit (rev(explode s)) |
130 |
113 val (i, _) = scan_int(rev rpost) |
131 fun display_token (Token s) = quote s |
114 in (implode(rev rpref), i) end; |
132 | display_token (IdentSy s) = "id(" ^ s ^ ")" |
115 |
133 | display_token (VarSy s) = "var(" ^ s ^ ")" |
116 fun xscan_varname exn cs : (string*int) * string list = |
134 | display_token (TFreeSy s) = "tfree(" ^ s ^ ")" |
117 let val (a, ds) = xscan_ident exn cs; |
135 | display_token (TVarSy s) = "tvar(" ^ s ^ ")" |
118 val (i, es) = scan_offset ds |
136 | display_token EndToken = ""; |
119 in if i = ~1 then (split_varname a, es) else ((a, i), es) end; |
137 |
120 |
138 |
121 fun scan_varname s = xscan_varname ID s |
139 (* matching_tokens *) |
122 handle ID(err, cs) => error(err^(implode cs)); |
140 |
123 |
141 fun matching_tokens (Token x, Token y) = (x = y) |
124 fun tokenize (dfa) (s:string) : Token list = |
142 | matching_tokens (IdentSy _, IdentSy _) = true |
125 let exception LEX_ERR; |
143 | matching_tokens (VarSy _, VarSy _) = true |
126 exception FAIL of string * string list; |
144 | matching_tokens (TFreeSy _, TFreeSy _) = true |
127 val lexerr = "Lexical error: "; |
145 | matching_tokens (TVarSy _, TVarSy _) = true |
128 |
146 | matching_tokens (EndToken, EndToken) = true |
129 fun tokenize1 (_:dfa, []:string list) : Token * string list = |
147 | matching_tokens _ = false; |
130 raise LEX_ERR |
148 |
131 | tokenize1(dfa, c::cs) = |
149 |
132 case next_dfa(dfa, c) of |
150 (* valued_token *) |
133 None => raise LEX_ERR |
151 |
134 | Some(a, dfa') => |
152 fun valued_token (Token _) = false |
135 if a=no_token then tokenize1(dfa', cs) |
153 | valued_token (IdentSy _) = true |
136 else (tokenize1(dfa', cs) handle LEX_ERR => |
154 | valued_token (VarSy _) = true |
137 if is_identifier a andalso not(null cs) andalso |
155 | valued_token (TFreeSy _) = true |
138 is_letdig(hd cs) |
156 | valued_token (TVarSy _) = true |
139 then raise LEX_ERR else (Token(a), cs)); |
157 | valued_token EndToken = false; |
140 |
158 |
141 fun token(cs) = tokenize1(dfa, cs) handle LEX_ERR => raise FAIL(lexerr, cs); |
159 |
142 |
160 (* predef_term *) |
143 fun id([]) = raise FAIL(eof_id, []) |
161 |
144 | id(cs as c::cs') = |
|
145 if is_letter(c) |
|
146 then let val (id, cs'') = xscan_ident FAIL cs |
|
147 in (IdentSy(id), cs'') end |
|
148 else |
|
149 if c = "?" |
|
150 then case cs' of |
|
151 "'"::xs => let val ((a, i), ys) = xscan_varname FAIL xs |
|
152 in (TVarSy("'"^a, i), ys) end |
|
153 | _ => let val ((a, i), ys) = xscan_varname FAIL cs' |
|
154 in (VarSy(a, i), ys) end |
|
155 else |
|
156 if c = "'" |
|
157 then let val (a, cs'') = xscan_ident FAIL cs' |
|
158 in (TFreeSy("'" ^ a), cs'') end |
|
159 else raise FAIL(lexerr, cs); |
|
160 |
|
161 fun tknize([], ts) = rev(ts) |
|
162 | tknize(cs as c::cs', ts) = |
|
163 if is_blank(c) then tknize(cs', ts) else |
|
164 let val (t, cs'') = |
|
165 if c="?" then id(cs) handle FAIL _ => token(cs) |
|
166 else (token(cs) handle FAIL _ => id(cs)) |
|
167 in tknize(cs'', t::ts) end |
|
168 |
|
169 in tknize(explode s, []) handle FAIL(s, cs) => error(s^(implode cs)) end; |
|
170 |
|
171 (*Variables have the form ?nameidx, or ?name.idx if "name" ends with a digit*) |
|
172 fun string_of_vname (a, idx) = case rev(explode a) of |
|
173 [] => "?NULL_VARIABLE_NAME" |
|
174 | c::_ => "?" ^ |
|
175 (if is_digit c then a ^ "." ^ string_of_int idx |
|
176 else if idx = 0 then a |
|
177 else a ^ string_of_int idx); |
|
178 |
|
179 fun token_to_string (Token(s)) = s |
|
180 | token_to_string (IdentSy(s)) = s |
|
181 | token_to_string (VarSy v) = string_of_vname v |
|
182 | token_to_string (TFreeSy a) = a |
|
183 | token_to_string (TVarSy v) = string_of_vname v |
|
184 | token_to_string end_token = "\n"; |
|
185 |
|
186 (* MMW *) |
|
187 fun name_of_token (Token s) = quote s |
|
188 | name_of_token (IdentSy _) = id |
|
189 | name_of_token (VarSy _) = var |
|
190 | name_of_token (TFreeSy _) = tfree |
|
191 | name_of_token (TVarSy _) = tvar; |
|
192 |
|
193 fun matching_tokens(Token(i), Token(j)) = (i=j) | |
|
194 matching_tokens(IdentSy(_), IdentSy(_)) = true | |
|
195 matching_tokens(VarSy _, VarSy _) = true | |
|
196 matching_tokens(TFreeSy _, TFreeSy _) = true | |
|
197 matching_tokens(TVarSy _, TVarSy _) = true | |
|
198 matching_tokens(end_token, end_token) = true | |
|
199 matching_tokens(_, _) = false; |
|
200 |
|
201 fun valued_token(end_token) = false |
|
202 | valued_token(Token _) = false |
|
203 | valued_token(IdentSy _) = true |
|
204 | valued_token(VarSy _) = true |
|
205 | valued_token(TFreeSy _) = true |
|
206 | valued_token(TVarSy _) = true; |
|
207 |
|
208 (* MMW *) |
|
209 fun predef_term name = |
162 fun predef_term name = |
210 if name = id then IdentSy name |
163 if name = id then IdentSy name |
211 else if name = var then VarSy (name, 0) |
164 else if name = var then VarSy name |
212 else if name = tfree then TFreeSy name |
165 else if name = tfree then TFreeSy name |
213 else if name = tvar then TVarSy (name, 0) |
166 else if name = tvar then TVarSy name |
214 else end_token; |
167 else EndToken; |
215 |
168 |
216 (* MMW *) |
169 |
|
170 (* is_terminal **) |
|
171 |
217 fun is_terminal s = s mem [id, var, tfree, tvar]; |
172 fun is_terminal s = s mem [id, var, tfree, tvar]; |
218 |
173 |
219 |
174 |
220 |
175 |
221 type 'b TokenMap = (Token * 'b list) list * 'b list; |
176 (** datatype lexicon **) |
222 val first_token = 0; |
177 |
223 |
178 datatype lexicon = |
224 fun int_of_token(Token(tk)) = first_token | |
179 Empty | |
225 int_of_token(IdentSy _) = first_token - 1 | |
180 Branch of string * string * lexicon * lexicon * lexicon; |
226 int_of_token(VarSy _) = first_token - 2 | |
181 |
227 int_of_token(TFreeSy _) = first_token - 3 | |
182 val no_token = ""; |
228 int_of_token(TVarSy _) = first_token - 4 | |
183 |
229 int_of_token(end_token) = first_token - 5; |
184 |
230 |
185 (* empty_lexicon *) |
231 fun lesstk(s, t) = int_of_token(s) < int_of_token(t) orelse |
186 |
232 (case (s, t) of (Token(a), Token(b)) => a<b | _ => false); |
187 val empty_lexicon = Empty; |
233 |
188 |
234 fun mkTokenMap(atll) = |
189 |
235 let val aill = atll; |
190 (* extend_lexicon *) |
236 val dom = sort lesstk (distinct(flat(map snd aill))); |
191 |
237 val mt = map fst (filter (null o snd) atll); |
192 fun extend_lexicon lexicon strs = |
238 fun mktm(i) = |
193 let |
239 let fun add(l, (a, il)) = if i mem il then a::l else l |
194 fun ext (lex, s) = |
240 in (i, foldl add ([], aill)) end; |
195 let |
241 in (map mktm dom, mt) end; |
196 fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) = |
242 |
197 if c < d then Branch (d, a, add lt chs, eq, gt) |
243 fun find_al (i) = |
198 else if c > d then Branch (d, a, lt, eq, add gt chs) |
244 let fun find((j, al)::l) = if lesstk(i, j) then [] else |
199 else Branch (d, if null cs then s else a, lt, add eq cs, gt) |
245 if matching_tokens(i, j) then al else find l | |
200 | add Empty [c] = |
246 find [] = []; |
201 Branch (c, s, Empty, Empty, Empty) |
247 in find end; |
202 | add Empty (c :: cs) = |
248 fun applyTokenMap((l, mt), tk:Token) = mt@(find_al tk l); |
203 Branch (c, no_token, Empty, add Empty cs, Empty) |
|
204 | add lex [] = lex; |
|
205 |
|
206 val cs = explode s; |
|
207 in |
|
208 if exists is_blank cs then |
|
209 error ("extend_lexicon: blank in literal " ^ quote s) |
|
210 else add lex cs |
|
211 end; |
|
212 in |
|
213 foldl ext (lexicon, strs) |
|
214 end; |
|
215 |
|
216 |
|
217 (* mk_lexicon *) |
|
218 |
|
219 val mk_lexicon = extend_lexicon empty_lexicon; |
|
220 |
|
221 |
|
222 |
|
223 (** scanners **) |
|
224 |
|
225 exception LEXICAL_ERROR; |
|
226 |
|
227 |
|
228 (* scanner combinators *) |
|
229 |
|
230 fun (scan >> f) cs = apfst f (scan cs); |
|
231 |
|
232 fun (scan1 || scan2) cs = scan1 cs handle LEXICAL_ERROR => scan2 cs; |
|
233 |
|
234 fun (scan1 -- scan2) cs = |
|
235 let |
|
236 val (x, cs') = scan1 cs; |
|
237 val (y, cs'') = scan2 cs'; |
|
238 in |
|
239 ((x, y), cs'') |
|
240 end; |
|
241 |
|
242 fun (scan1 ^^ scan2) = scan1 -- scan2 >> op ^; |
|
243 |
|
244 |
|
245 (* generic scanners *) |
|
246 |
|
247 fun $$ _ [] = raise LEXICAL_ERROR |
|
248 | $$ a (c :: cs) = |
|
249 if a = c then (c, cs) else raise LEXICAL_ERROR; |
|
250 |
|
251 fun scan_empty cs = ([], cs); |
|
252 |
|
253 fun scan_one _ [] = raise LEXICAL_ERROR |
|
254 | scan_one pred (c :: cs) = |
|
255 if pred c then (c, cs) else raise LEXICAL_ERROR; |
|
256 |
|
257 val scan_any = take_prefix; |
|
258 |
|
259 fun scan_any1 pred = scan_one pred -- scan_any pred >> op ::; |
|
260 |
|
261 fun scan_rest cs = (cs, []); |
|
262 |
|
263 fun scan_end [] = ([], []) |
|
264 | scan_end _ = raise LEXICAL_ERROR; |
|
265 |
|
266 fun optional scan = scan >> Some || scan_empty >> K None; |
|
267 |
|
268 fun repeat scan cs = (scan -- repeat scan >> op :: || scan_empty) cs; |
|
269 |
|
270 fun repeat1 scan = scan -- repeat scan >> op ::; |
|
271 |
|
272 |
|
273 (* other scanners *) |
|
274 |
|
275 val scan_letter_letdigs = scan_one is_letter -- scan_any is_letdig >> op ::; |
|
276 |
|
277 val scan_digits1 = scan_any1 is_digit; |
|
278 |
|
279 val scan_id = scan_letter_letdigs >> implode; |
|
280 |
|
281 val scan_id_nat = |
|
282 scan_id ^^ ($$ "." ^^ (scan_digits1 >> implode) || scan_empty >> K ""); |
|
283 |
|
284 |
|
285 (* scan_literal *) |
|
286 |
|
287 fun scan_literal lex chrs = |
|
288 let |
|
289 fun scan_lit _ s_cs [] = s_cs |
|
290 | scan_lit Empty s_cs _ = s_cs |
|
291 | scan_lit (Branch (d, a, lt, eq, gt)) s_cs (chs as c :: cs) = |
|
292 if c < d then scan_lit lt s_cs chs |
|
293 else if c > d then scan_lit gt s_cs chs |
|
294 else scan_lit eq (if a = no_token then s_cs else Some (a, cs)) cs; |
|
295 in |
|
296 (case scan_lit lex None chrs of |
|
297 None => raise LEXICAL_ERROR |
|
298 | Some s_cs => s_cs) |
|
299 end; |
|
300 |
|
301 |
|
302 |
|
303 (** tokenize **) |
|
304 |
|
305 fun tokenize lex xids str = |
|
306 let |
|
307 val scan_xid = |
|
308 if xids then $$ "_" ^^ scan_id || scan_id |
|
309 else scan_id; |
|
310 |
|
311 val scan_lit = scan_literal lex >> pair Token; |
|
312 |
|
313 val scan_ident = |
|
314 $$ "?" ^^ $$ "'" ^^ scan_id_nat >> pair TVarSy || |
|
315 $$ "?" ^^ scan_id_nat >> pair VarSy || |
|
316 $$ "'" ^^ scan_id >> pair TFreeSy || |
|
317 scan_xid >> pair IdentSy; |
|
318 |
|
319 fun scan_max_token cs = |
|
320 (case (optional scan_lit cs, optional scan_ident cs) of |
|
321 (tok1, (None, _)) => tok1 |
|
322 | ((None, _), tok2) => tok2 |
|
323 | (tok1 as (Some (_, s1), _), tok2 as (Some (_, s2), _)) => |
|
324 if size s1 >= size s2 then tok1 else tok2); |
|
325 |
|
326 fun scan_tokens [] rev_toks = rev (EndToken :: rev_toks) |
|
327 | scan_tokens (chs as c :: cs) rev_toks = |
|
328 if is_blank c then scan_tokens cs rev_toks |
|
329 else |
|
330 (case scan_max_token chs of |
|
331 (None, _) => error ("Lexical error at: " ^ quote (implode chs)) |
|
332 | (Some (tk, s), chs') => scan_tokens chs' (tk s :: rev_toks)); |
|
333 in |
|
334 scan_tokens (explode str) [] |
|
335 end; |
|
336 |
|
337 |
|
338 |
|
339 (** scan variables **) |
|
340 |
|
341 (* scan_vname *) |
|
342 |
|
343 fun scan_vname chrs = |
|
344 let |
|
345 fun nat_of_chs n [] = n |
|
346 | nat_of_chs n (c :: cs) = nat_of_chs (n * 10 + (ord c - ord "0")) cs; |
|
347 |
|
348 val nat_of = nat_of_chs 0; |
|
349 |
|
350 fun split_vname chs = |
|
351 let val (cs, ds) = take_suffix is_digit chs |
|
352 in (implode cs, nat_of ds) end |
|
353 |
|
354 val scan = |
|
355 scan_letter_letdigs -- |
|
356 ($$ "." -- scan_digits1 >> (nat_of o #2) || scan_empty >> K ~1); |
|
357 in |
|
358 (case scan chrs of |
|
359 ((cs, ~1), cs') => (split_vname cs, cs') |
|
360 | ((cs, i), cs') => ((implode cs, i), cs')) |
|
361 end; |
|
362 |
|
363 |
|
364 (* scan_varname *) |
|
365 |
|
366 fun scan_varname chs = |
|
367 scan_vname chs handle LEXICAL_ERROR |
|
368 => error ("scan_varname: bad varname " ^ quote (implode chs)); |
|
369 |
|
370 |
|
371 (* scan_var *) |
|
372 |
|
373 fun scan_var str = |
|
374 let |
|
375 fun tvar (x, i) = Var (("'" ^ x, i), dummyT); |
|
376 fun var x_i = Var (x_i, dummyT); |
|
377 fun free x = Free (x, dummyT); |
|
378 |
|
379 val scan = |
|
380 $$ "?" -- $$ "'" -- scan_vname -- scan_end >> (tvar o #2 o #1) || |
|
381 $$ "?" -- scan_vname -- scan_end >> (var o #2 o #1) || |
|
382 scan_rest >> (free o implode); |
|
383 in |
|
384 #1 (scan (explode str)) |
|
385 end; |
249 |
386 |
250 |
387 |
251 end; |
388 end; |
252 |
389 |