author | krauss |
Wed, 02 Feb 2011 08:47:45 +0100 | |
changeset 41686 | d8efc2490b8e |
parent 41589 | bbd861837ebc |
permissions | -rw-r--r-- |
19093 | 1 |
(* Title: HOL/Import/mono_scan.ML |
2 |
Author: Steven Obua, TU Muenchen |
|
3 |
||
41589 | 4 |
Monomorphic scanner combinators for monomorphic sequences. |
19093 | 5 |
*) |
6 |
||
7 |
signature MONO_SCANNER = |
|
8 |
sig |
|
9 |
||
10 |
include MONO_SCANNER_SEQ |
|
11 |
||
12 |
exception SyntaxError |
|
13 |
||
14 |
type 'a scanner = seq -> 'a * seq |
|
15 |
||
16 |
val :-- : 'a scanner * ('a -> 'b scanner) |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
17 |
-> ('a*'b) scanner |
19093 | 18 |
val -- : 'a scanner * 'b scanner -> ('a * 'b) scanner |
19 |
val >> : 'a scanner * ('a -> 'b) -> 'b scanner |
|
20 |
val --| : 'a scanner * 'b scanner -> 'a scanner |
|
21 |
val |-- : 'a scanner * 'b scanner -> 'b scanner |
|
22 |
val ^^ : string scanner * string scanner |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
23 |
-> string scanner |
19093 | 24 |
val || : 'a scanner * 'a scanner -> 'a scanner |
25 |
val one : (item -> bool) -> item scanner |
|
26 |
val anyone : item scanner |
|
27 |
val succeed : 'a -> 'a scanner |
|
28 |
val any : (item -> bool) -> item list scanner |
|
29 |
val any1 : (item -> bool) -> item list scanner |
|
30 |
val optional : 'a scanner -> 'a -> 'a scanner |
|
31 |
val option : 'a scanner -> 'a option scanner |
|
32 |
val repeat : 'a scanner -> 'a list scanner |
|
33 |
val repeat1 : 'a scanner -> 'a list scanner |
|
34 |
val repeat_fixed : int -> 'a scanner -> 'a list scanner |
|
35 |
val ahead : 'a scanner -> 'a scanner |
|
36 |
val unless : 'a scanner -> 'b scanner -> 'b scanner |
|
37 |
val !! : (seq -> string) -> 'a scanner -> 'a scanner |
|
38 |
||
39 |
end |
|
40 |
||
41 |
signature STRING_SCANNER = |
|
42 |
sig |
|
43 |
||
44 |
include MONO_SCANNER where type item = string |
|
45 |
||
46 |
val $$ : item -> item scanner |
|
47 |
||
48 |
val scan_id : string scanner |
|
49 |
val scan_nat : int scanner |
|
50 |
||
51 |
val this : item list -> item list scanner |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
52 |
val this_string : string -> string scanner |
19093 | 53 |
|
54 |
end |
|
55 |
||
56 |
functor MonoScanner (structure Seq : MONO_SCANNER_SEQ) : MONO_SCANNER = |
|
57 |
struct |
|
58 |
||
59 |
infix 7 |-- --| |
|
60 |
infix 5 :-- -- ^^ |
|
61 |
infix 3 >> |
|
62 |
infix 0 || |
|
63 |
||
64 |
exception SyntaxError |
|
65 |
exception Fail of string |
|
66 |
||
67 |
type seq = Seq.seq |
|
68 |
type item = Seq.item |
|
69 |
type 'a scanner = seq -> 'a * seq |
|
70 |
||
71 |
val pull = Seq.pull |
|
72 |
||
73 |
fun (sc1 :-- sc2) toks = |
|
74 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
75 |
val (x,toks2) = sc1 toks |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
76 |
val (y,toks3) = sc2 x toks2 |
19093 | 77 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
78 |
((x,y),toks3) |
19093 | 79 |
end |
80 |
||
81 |
fun (sc1 -- sc2) toks = |
|
82 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
83 |
val (x,toks2) = sc1 toks |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
84 |
val (y,toks3) = sc2 toks2 |
19093 | 85 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
86 |
((x,y),toks3) |
19093 | 87 |
end |
88 |
||
89 |
fun (sc >> f) toks = |
|
90 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
91 |
val (x,toks2) = sc toks |
19093 | 92 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
93 |
(f x,toks2) |
19093 | 94 |
end |
95 |
||
96 |
fun (sc1 --| sc2) toks = |
|
97 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
98 |
val (x,toks2) = sc1 toks |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
99 |
val (_,toks3) = sc2 toks2 |
19093 | 100 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
101 |
(x,toks3) |
19093 | 102 |
end |
103 |
||
104 |
fun (sc1 |-- sc2) toks = |
|
105 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
106 |
val (_,toks2) = sc1 toks |
19093 | 107 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
108 |
sc2 toks2 |
19093 | 109 |
end |
110 |
||
111 |
fun (sc1 ^^ sc2) toks = |
|
112 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
113 |
val (x,toks2) = sc1 toks |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
114 |
val (y,toks3) = sc2 toks2 |
19093 | 115 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
116 |
(x^y,toks3) |
19093 | 117 |
end |
118 |
||
119 |
fun (sc1 || sc2) toks = |
|
120 |
(sc1 toks) |
|
121 |
handle SyntaxError => sc2 toks |
|
122 |
||
123 |
fun anyone toks = case pull toks of NONE => raise SyntaxError | SOME x => x |
|
124 |
||
125 |
fun one p toks = case anyone toks of x as (t, toks) => if p t then x else raise SyntaxError |
|
126 |
||
127 |
fun succeed e toks = (e,toks) |
|
128 |
||
129 |
fun any p toks = |
|
130 |
case pull toks of |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
131 |
NONE => ([],toks) |
19093 | 132 |
| SOME(x,toks2) => if p x |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
133 |
then |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
134 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
135 |
val (xs,toks3) = any p toks2 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
136 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
137 |
(x::xs,toks3) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
138 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
139 |
else ([],toks) |
19093 | 140 |
|
141 |
fun any1 p toks = |
|
142 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
143 |
val (x,toks2) = one p toks |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
144 |
val (xs,toks3) = any p toks2 |
19093 | 145 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
146 |
(x::xs,toks3) |
19093 | 147 |
end |
148 |
||
149 |
fun optional sc def = sc || succeed def |
|
150 |
fun option sc = (sc >> SOME) || succeed NONE |
|
151 |
||
152 |
(* |
|
153 |
fun repeat sc = |
|
154 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
155 |
fun R toks = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
156 |
let |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
157 |
val (x,toks2) = sc toks |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
158 |
val (xs,toks3) = R toks2 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
159 |
in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
160 |
(x::xs,toks3) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
161 |
end |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
162 |
handle SyntaxError => ([],toks) |
19093 | 163 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
164 |
R |
19093 | 165 |
end |
166 |
*) |
|
167 |
||
168 |
(* A tail-recursive version of repeat. It is (ever so) slightly slower |
|
169 |
* than the above, non-tail-recursive version (due to the garbage generation |
|
170 |
* associated with the reversal of the list). However, this version will be |
|
171 |
* able to process input where the former version must give up (due to stack |
|
172 |
* overflow). The slowdown seems to be around the one percent mark. |
|
173 |
*) |
|
174 |
fun repeat sc = |
|
175 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
176 |
fun R xs toks = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
177 |
case SOME (sc toks) handle SyntaxError => NONE of |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
178 |
SOME (x,toks2) => R (x::xs) toks2 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
179 |
| NONE => (List.rev xs,toks) |
19093 | 180 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
181 |
R [] |
19093 | 182 |
end |
183 |
||
184 |
fun repeat1 sc toks = |
|
185 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
186 |
val (x,toks2) = sc toks |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
187 |
val (xs,toks3) = repeat sc toks2 |
19093 | 188 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
189 |
(x::xs,toks3) |
19093 | 190 |
end |
191 |
||
192 |
fun repeat_fixed n sc = |
|
193 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
194 |
fun R n xs toks = |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
195 |
if (n <= 0) then (List.rev xs, toks) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
196 |
else case (sc toks) of (x, toks2) => R (n-1) (x::xs) toks2 |
19093 | 197 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
198 |
R n [] |
19093 | 199 |
end |
200 |
||
201 |
fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks) |
|
202 |
||
203 |
fun unless test sc toks = |
|
204 |
let |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
205 |
val test_failed = (test toks;false) handle SyntaxError => true |
19093 | 206 |
in |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
207 |
if test_failed |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
208 |
then sc toks |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
209 |
else raise SyntaxError |
19093 | 210 |
end |
211 |
||
212 |
fun !! f sc toks = (sc toks |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
19093
diff
changeset
|
213 |
handle SyntaxError => raise Fail (f toks)) |
19093 | 214 |
|
215 |
end |
|
216 |
||
217 |
||
218 |
structure StringScanner : STRING_SCANNER = |
|
219 |
struct |
|
220 |
||
221 |
structure Scan = MonoScanner(structure Seq = StringScannerSeq) |
|
222 |
open Scan |
|
223 |
||
224 |
fun $$ arg = one (fn x => x = arg) |
|
225 |
||
226 |
val scan_id = one Symbol.is_letter ^^ (any Symbol.is_letdig >> implode); |
|
227 |
||
228 |
val nat_of_list = the o Int.fromString o implode |
|
229 |
||
230 |
val scan_nat = repeat1 (one Symbol.is_digit) >> nat_of_list |
|
231 |
||
232 |
fun this [] = (fn toks => ([], toks)) |
|
233 |
| this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs' |
|
234 |
||
40627
becf5d5187cc
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
wenzelm
parents:
32960
diff
changeset
|
235 |
fun this_string s = this (raw_explode s) >> K s |
19093 | 236 |
|
237 |
end |