1 (* Title: Pure/General/lazy_scan.ML |
|
2 ID: $Id$ |
|
3 Author: Sebastian Skalberg, TU Muenchen |
|
4 |
|
5 Scanner combinators for lazy sequences. |
|
6 *) |
|
7 |
|
8 signature LAZY_SCAN = |
|
9 sig |
|
10 |
|
11 exception SyntaxError |
|
12 |
|
13 type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq |
|
14 |
|
15 val :-- : ('a,'b) scanner * ('b -> ('a,'c) scanner) |
|
16 -> ('a,'b*'c) scanner |
|
17 val -- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b*'c) scanner |
|
18 val >> : ('a,'b) scanner * ('b -> 'c) -> ('a,'c) scanner |
|
19 val --| : ('a,'b) scanner * ('a,'c) scanner -> ('a,'b) scanner |
|
20 val |-- : ('a,'b) scanner * ('a,'c) scanner -> ('a,'c) scanner |
|
21 val ^^ : ('a,string) scanner * ('a,string) scanner |
|
22 -> ('a,string) scanner |
|
23 val || : ('a,'b) scanner * ('a,'b) scanner -> ('a,'b) scanner |
|
24 val one : ('a -> bool) -> ('a,'a) scanner |
|
25 val succeed : 'b -> ('a,'b) scanner |
|
26 val any : ('a -> bool) -> ('a,'a list) scanner |
|
27 val any1 : ('a -> bool) -> ('a,'a list) scanner |
|
28 val optional : ('a,'b) scanner -> 'b -> ('a,'b) scanner |
|
29 val option : ('a,'b) scanner -> ('a,'b option) scanner |
|
30 val repeat : ('a,'b) scanner -> ('a,'b list) scanner |
|
31 val repeat1 : ('a,'b) scanner -> ('a,'b list) scanner |
|
32 val ahead : ('a,'b) scanner -> ('a,'b) scanner |
|
33 val unless : ('a LazySeq.seq -> bool) -> ('a,'b) scanner -> ('a,'b) scanner |
|
34 val $$ : ''a -> (''a,''a) scanner |
|
35 val !! : ('a LazySeq.seq -> string) -> ('a,'b) scanner -> ('a,'b) scanner |
|
36 val scan_full: ('a,'b) scanner -> 'a LazySeq.seq -> 'b LazySeq.seq |
|
37 |
|
38 end |
|
39 |
|
40 structure LazyScan :> LAZY_SCAN = |
|
41 struct |
|
42 |
|
43 infix 7 |-- --| |
|
44 infix 5 :-- -- ^^ |
|
45 infix 3 >> |
|
46 infix 0 || |
|
47 |
|
48 exception SyntaxError |
|
49 exception Fail of string |
|
50 |
|
51 type ('a,'b) scanner = 'a LazySeq.seq -> 'b * 'a LazySeq.seq |
|
52 |
|
53 fun (sc1 :-- sc2) toks = |
|
54 let |
|
55 val (x,toks2) = sc1 toks |
|
56 val (y,toks3) = sc2 x toks2 |
|
57 in |
|
58 ((x,y),toks3) |
|
59 end |
|
60 |
|
61 fun (sc1 -- sc2) toks = |
|
62 let |
|
63 val (x,toks2) = sc1 toks |
|
64 val (y,toks3) = sc2 toks2 |
|
65 in |
|
66 ((x,y),toks3) |
|
67 end |
|
68 |
|
69 fun (sc >> f) toks = |
|
70 let |
|
71 val (x,toks2) = sc toks |
|
72 in |
|
73 (f x,toks2) |
|
74 end |
|
75 |
|
76 fun (sc1 --| sc2) toks = |
|
77 let |
|
78 val (x,toks2) = sc1 toks |
|
79 val (_,toks3) = sc2 toks2 |
|
80 in |
|
81 (x,toks3) |
|
82 end |
|
83 |
|
84 fun (sc1 |-- sc2) toks = |
|
85 let |
|
86 val (_,toks2) = sc1 toks |
|
87 in |
|
88 sc2 toks2 |
|
89 end |
|
90 |
|
91 fun (sc1 ^^ sc2) toks = |
|
92 let |
|
93 val (x,toks2) = sc1 toks |
|
94 val (y,toks3) = sc2 toks2 |
|
95 in |
|
96 (x^y,toks3) |
|
97 end |
|
98 |
|
99 fun (sc1 || sc2) toks = |
|
100 (sc1 toks) |
|
101 handle SyntaxError => sc2 toks |
|
102 |
|
103 fun one p toks = |
|
104 case LazySeq.getItem toks of |
|
105 NONE => raise SyntaxError |
|
106 | SOME(t,toks) => if p t |
|
107 then (t,toks) |
|
108 else raise SyntaxError |
|
109 |
|
110 fun succeed e toks = (e,toks) |
|
111 |
|
112 fun any p toks = |
|
113 case LazySeq.getItem toks of |
|
114 NONE => ([],toks) |
|
115 | SOME(x,toks2) => if p x |
|
116 then |
|
117 let |
|
118 val (xs,toks3) = any p toks2 |
|
119 in |
|
120 (x::xs,toks3) |
|
121 end |
|
122 else ([],toks) |
|
123 |
|
124 fun any1 p toks = |
|
125 let |
|
126 val (x,toks2) = one p toks |
|
127 val (xs,toks3) = any p toks2 |
|
128 in |
|
129 (x::xs,toks3) |
|
130 end |
|
131 |
|
132 fun optional sc def = sc || succeed def |
|
133 fun option sc = (sc >> SOME) || succeed NONE |
|
134 |
|
135 (* |
|
136 fun repeat sc = |
|
137 let |
|
138 fun R toks = |
|
139 let |
|
140 val (x,toks2) = sc toks |
|
141 val (xs,toks3) = R toks2 |
|
142 in |
|
143 (x::xs,toks3) |
|
144 end |
|
145 handle SyntaxError => ([],toks) |
|
146 in |
|
147 R |
|
148 end |
|
149 *) |
|
150 |
|
151 (* A tail-recursive version of repeat. It is (ever so) slightly slower |
|
152 * than the above, non-tail-recursive version (due to the garbage generation |
|
153 * associated with the reversal of the list). However, this version will be |
|
154 * able to process input where the former version must give up (due to stack |
|
155 * overflow). The slowdown seems to be around the one percent mark. |
|
156 *) |
|
157 fun repeat sc = |
|
158 let |
|
159 fun R xs toks = |
|
160 case SOME (sc toks) handle SyntaxError => NONE of |
|
161 SOME (x,toks2) => R (x::xs) toks2 |
|
162 | NONE => (List.rev xs,toks) |
|
163 in |
|
164 R [] |
|
165 end |
|
166 |
|
167 fun repeat1 sc toks = |
|
168 let |
|
169 val (x,toks2) = sc toks |
|
170 val (xs,toks3) = repeat sc toks2 |
|
171 in |
|
172 (x::xs,toks3) |
|
173 end |
|
174 |
|
175 fun ahead (sc:'a->'b*'a) toks = (#1 (sc toks),toks) |
|
176 |
|
177 fun unless test sc toks = |
|
178 let |
|
179 val test_failed = (test toks;false) handle SyntaxError => true |
|
180 in |
|
181 if test_failed |
|
182 then sc toks |
|
183 else raise SyntaxError |
|
184 end |
|
185 |
|
186 fun $$ arg = one (fn x => x = arg) |
|
187 |
|
188 fun !! f sc toks = (sc toks |
|
189 handle SyntaxError => raise Fail (f toks)) |
|
190 |
|
191 fun scan_full sc toks = |
|
192 let |
|
193 fun F toks = |
|
194 if LazySeq.null toks |
|
195 then NONE |
|
196 else |
|
197 let |
|
198 val (x,toks') = sc toks |
|
199 in |
|
200 SOME(x,LazySeq.make (fn () => F toks')) |
|
201 end |
|
202 in |
|
203 LazySeq.make (fn () => F toks) |
|
204 end |
|
205 |
|
206 end |
|