26 val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
26 val repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
27 val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
27 val repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
28 val max_of: ('a -> ('b * string) * 'a) -> ('a -> ('b * string) * 'a) |
28 val max_of: ('a -> ('b * string) * 'a) -> ('a -> ('b * string) * 'a) |
29 -> 'a -> ('b * string) option * 'a |
29 -> 'a -> ('b * string) option * 'a |
30 val scan_id: string list -> string * string list |
30 val scan_id: string list -> string * string list |
|
31 val scan_longid: string list -> string * string list |
31 val scan_tid: string list -> string * string list |
32 val scan_tid: string list -> string * string list |
32 val scan_nat: string list -> string * string list |
33 val scan_nat: string list -> string * string list |
33 type lexicon |
34 type lexicon |
34 val dest_lexicon: lexicon -> string list |
35 val dest_lexicon: lexicon -> string list |
35 val empty_lexicon: lexicon |
36 val empty_lexicon: lexicon |
134 |
138 |
135 |
139 |
136 (* terminal arguments *) |
140 (* terminal arguments *) |
137 |
141 |
138 val idT = Type ("id", []); |
142 val idT = Type ("id", []); |
|
143 val longidT = Type ("longid", []); |
139 val varT = Type ("var", []); |
144 val varT = Type ("var", []); |
140 val tidT = Type ("tid", []); |
145 val tidT = Type ("tid", []); |
141 val tvarT = Type ("tvar", []); |
146 val tvarT = Type ("tvar", []); |
142 |
147 |
143 val terminals = ["id", "var", "tid", "tvar", "xnum", "xstr"]; |
148 val terminals = ["id", "longid", "var", "tid", "tvar", "xnum", "xstr"]; |
144 |
149 |
145 fun is_terminal s = s mem terminals; |
150 fun is_terminal s = s mem terminals; |
146 |
151 |
147 |
152 |
148 (* str_of_token *) |
153 (* str_of_token *) |
149 |
154 |
150 fun str_of_token (Token s) = s |
155 fun str_of_token (Token s) = s |
151 | str_of_token (IdentSy s) = s |
156 | str_of_token (IdentSy s) = s |
|
157 | str_of_token (LongIdentSy s) = s |
152 | str_of_token (VarSy s) = s |
158 | str_of_token (VarSy s) = s |
153 | str_of_token (TFreeSy s) = s |
159 | str_of_token (TFreeSy s) = s |
154 | str_of_token (TVarSy s) = s |
160 | str_of_token (TVarSy s) = s |
155 | str_of_token (NumSy s) = s |
161 | str_of_token (NumSy s) = s |
156 | str_of_token (StrSy s) = s |
162 | str_of_token (StrSy s) = s |
159 |
165 |
160 (* display_token *) |
166 (* display_token *) |
161 |
167 |
162 fun display_token (Token s) = quote s |
168 fun display_token (Token s) = quote s |
163 | display_token (IdentSy s) = "id(" ^ s ^ ")" |
169 | display_token (IdentSy s) = "id(" ^ s ^ ")" |
|
170 | display_token (LongIdentSy s) = "longid(" ^ s ^ ")" |
164 | display_token (VarSy s) = "var(" ^ s ^ ")" |
171 | display_token (VarSy s) = "var(" ^ s ^ ")" |
165 | display_token (TFreeSy s) = "tid(" ^ s ^ ")" |
172 | display_token (TFreeSy s) = "tid(" ^ s ^ ")" |
166 | display_token (TVarSy s) = "tvar(" ^ s ^ ")" |
173 | display_token (TVarSy s) = "tvar(" ^ s ^ ")" |
167 | display_token (NumSy s) = "xnum(" ^ s ^ ")" |
174 | display_token (NumSy s) = "xnum(" ^ s ^ ")" |
168 | display_token (StrSy s) = "xstr(" ^ s ^ ")" |
175 | display_token (StrSy s) = "xstr(" ^ s ^ ")" |
171 |
178 |
172 (* matching_tokens *) |
179 (* matching_tokens *) |
173 |
180 |
174 fun matching_tokens (Token x, Token y) = (x = y) |
181 fun matching_tokens (Token x, Token y) = (x = y) |
175 | matching_tokens (IdentSy _, IdentSy _) = true |
182 | matching_tokens (IdentSy _, IdentSy _) = true |
|
183 | matching_tokens (LongIdentSy _, LongIdentSy _) = true |
176 | matching_tokens (VarSy _, VarSy _) = true |
184 | matching_tokens (VarSy _, VarSy _) = true |
177 | matching_tokens (TFreeSy _, TFreeSy _) = true |
185 | matching_tokens (TFreeSy _, TFreeSy _) = true |
178 | matching_tokens (TVarSy _, TVarSy _) = true |
186 | matching_tokens (TVarSy _, TVarSy _) = true |
179 | matching_tokens (NumSy _, NumSy _) = true |
187 | matching_tokens (NumSy _, NumSy _) = true |
180 | matching_tokens (StrSy _, StrSy _) = true |
188 | matching_tokens (StrSy _, StrSy _) = true |
196 |
204 |
197 (* valued_token *) |
205 (* valued_token *) |
198 |
206 |
199 fun valued_token (Token _) = false |
207 fun valued_token (Token _) = false |
200 | valued_token (IdentSy _) = true |
208 | valued_token (IdentSy _) = true |
|
209 | valued_token (LongIdentSy _) = true |
201 | valued_token (VarSy _) = true |
210 | valued_token (VarSy _) = true |
202 | valued_token (TFreeSy _) = true |
211 | valued_token (TFreeSy _) = true |
203 | valued_token (TVarSy _) = true |
212 | valued_token (TVarSy _) = true |
204 | valued_token (NumSy _) = true |
213 | valued_token (NumSy _) = true |
205 | valued_token (StrSy _) = true |
214 | valued_token (StrSy _) = true |
207 |
216 |
208 |
217 |
209 (* predef_term *) |
218 (* predef_term *) |
210 |
219 |
211 fun predef_term "id" = Some (IdentSy "id") |
220 fun predef_term "id" = Some (IdentSy "id") |
|
221 | predef_term "longid" = Some (LongIdentSy "longid") |
212 | predef_term "var" = Some (VarSy "var") |
222 | predef_term "var" = Some (VarSy "var") |
213 | predef_term "tid" = Some (TFreeSy "tid") |
223 | predef_term "tid" = Some (TFreeSy "tid") |
214 | predef_term "tvar" = Some (TVarSy "tvar") |
224 | predef_term "tvar" = Some (TVarSy "tvar") |
215 | predef_term "xnum" = Some (NumSy "xnum") |
225 | predef_term "xnum" = Some (NumSy "xnum") |
216 | predef_term "xstr" = Some (StrSy "xstr") |
226 | predef_term "xstr" = Some (StrSy "xstr") |
344 |
354 |
345 val scan_digits1 = scan_any1 is_digit; |
355 val scan_digits1 = scan_any1 is_digit; |
346 |
356 |
347 val scan_id = scan_letter_letdigs >> implode; |
357 val scan_id = scan_letter_letdigs >> implode; |
348 |
358 |
|
359 val scan_longid = scan_id ^^ (repeat1 ($$ "." ^^ scan_id) >> implode); |
|
360 |
349 val scan_id_nat = |
361 val scan_id_nat = |
350 scan_id ^^ ($$ "." ^^ (scan_digits1 >> implode) || scan_empty >> K ""); |
362 scan_id ^^ ($$ "." ^^ (scan_digits1 >> implode) || scan_empty >> K ""); |
351 |
363 |
352 val scan_tid = $$ "'" ^^ scan_id; |
364 val scan_tid = $$ "'" ^^ scan_id; |
353 |
365 |
387 val scan_val = |
399 val scan_val = |
388 $$ "?" ^^ $$ "'" ^^ scan_id_nat >> pair TVarSy || |
400 $$ "?" ^^ $$ "'" ^^ scan_id_nat >> pair TVarSy || |
389 $$ "?" ^^ scan_id_nat >> pair VarSy || |
401 $$ "?" ^^ scan_id_nat >> pair VarSy || |
390 $$ "'" ^^ scan_id >> pair TFreeSy || |
402 $$ "'" ^^ scan_id >> pair TFreeSy || |
391 $$ "#" ^^ scan_int >> pair NumSy || |
403 $$ "#" ^^ scan_int >> pair NumSy || |
|
404 scan_longid >> pair LongIdentSy || |
392 scan_xid >> pair IdentSy; |
405 scan_xid >> pair IdentSy; |
393 |
406 |
394 fun scan_str ("'" :: "'" :: cs) = ([], cs) |
407 fun scan_str ("'" :: "'" :: cs) = ([], cs) |
395 | scan_str ("\\" :: c :: cs) = apfst (cons c) (scan_str cs) |
408 | scan_str ("\\" :: c :: cs) = apfst (cons c) (scan_str cs) |
396 | scan_str (c :: cs) = apfst (cons c) (scan_str cs) |
409 | scan_str (c :: cs) = apfst (cons c) (scan_str cs) |