author | blanchet |
Fri, 17 Sep 2010 01:58:21 +0200 | |
changeset 39502 | cffceed8e7fa |
parent 39501 | aaa7078fff55 |
child 45778 | df6e210fb44c |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* PARSING *) |
|
39502 | 3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure Parse :> Parse = |
|
7 |
struct |
|
8 |
||
9 |
open Useful; |
|
10 |
||
11 |
infixr 9 >>++ |
|
12 |
infixr 8 ++ |
|
13 |
infixr 7 >> |
|
14 |
infixr 6 || |
|
15 |
||
16 |
(* ------------------------------------------------------------------------- *) |
|
17 |
(* A "cannot parse" exception. *) |
|
18 |
(* ------------------------------------------------------------------------- *) |
|
19 |
||
20 |
exception NoParse; |
|
21 |
||
22 |
(* ------------------------------------------------------------------------- *) |
|
23 |
(* Recursive descent parsing combinators. *) |
|
24 |
(* ------------------------------------------------------------------------- *) |
|
25 |
||
26 |
val error : 'a -> 'b * 'a = fn _ => raise NoParse; |
|
27 |
||
28 |
fun op ++ (parser1,parser2) input = |
|
29 |
let |
|
30 |
val (result1,input) = parser1 input |
|
31 |
val (result2,input) = parser2 input |
|
32 |
in |
|
33 |
((result1,result2),input) |
|
34 |
end; |
|
35 |
||
36 |
fun op >> (parser : 'a -> 'b * 'a, treatment) input = |
|
37 |
let |
|
38 |
val (result,input) = parser input |
|
39 |
in |
|
40 |
(treatment result, input) |
|
41 |
end; |
|
42 |
||
43 |
fun op >>++ (parser,treatment) input = |
|
44 |
let |
|
45 |
val (result,input) = parser input |
|
46 |
in |
|
47 |
treatment result input |
|
48 |
end; |
|
49 |
||
50 |
fun op || (parser1,parser2) input = |
|
51 |
parser1 input handle NoParse => parser2 input; |
|
52 |
||
53 |
fun first [] _ = raise NoParse |
|
54 |
| first (parser :: parsers) input = (parser || first parsers) input; |
|
55 |
||
56 |
fun mmany parser state input = |
|
57 |
let |
|
58 |
val (state,input) = parser state input |
|
59 |
in |
|
60 |
mmany parser state input |
|
61 |
end |
|
62 |
handle NoParse => (state,input); |
|
63 |
||
64 |
fun many parser = |
|
65 |
let |
|
66 |
fun sparser l = parser >> (fn x => x :: l) |
|
67 |
in |
|
68 |
mmany sparser [] >> rev |
|
69 |
end; |
|
70 |
||
71 |
fun atLeastOne p = (p ++ many p) >> op::; |
|
72 |
||
73 |
fun nothing input = ((),input); |
|
74 |
||
75 |
fun optional p = (p >> SOME) || (nothing >> K NONE); |
|
76 |
||
77 |
(* ------------------------------------------------------------------------- *) |
|
78 |
(* Stream-based parsers. *) |
|
79 |
(* ------------------------------------------------------------------------- *) |
|
80 |
||
81 |
type ('a,'b) parser = 'a Stream.stream -> 'b * 'a Stream.stream |
|
82 |
||
83 |
fun maybe p Stream.Nil = raise NoParse |
|
84 |
| maybe p (Stream.Cons (h,t)) = |
|
85 |
case p h of SOME r => (r, t ()) | NONE => raise NoParse; |
|
86 |
||
87 |
fun finished Stream.Nil = ((), Stream.Nil) |
|
88 |
| finished (Stream.Cons _) = raise NoParse; |
|
89 |
||
90 |
fun some p = maybe (fn x => if p x then SOME x else NONE); |
|
91 |
||
92 |
fun any input = some (K true) input; |
|
93 |
||
94 |
(* ------------------------------------------------------------------------- *) |
|
95 |
(* Parsing whole streams. *) |
|
96 |
(* ------------------------------------------------------------------------- *) |
|
97 |
||
98 |
fun fromStream parser input = |
|
99 |
let |
|
100 |
val (res,_) = (parser ++ finished >> fst) input |
|
101 |
in |
|
102 |
res |
|
103 |
end; |
|
104 |
||
105 |
fun fromList parser l = fromStream parser (Stream.fromList l); |
|
106 |
||
107 |
fun everything parser = |
|
108 |
let |
|
109 |
fun parserOption input = |
|
110 |
SOME (parser input) |
|
111 |
handle e as NoParse => if Stream.null input then NONE else raise e |
|
112 |
||
113 |
fun parserList input = |
|
114 |
case parserOption input of |
|
115 |
NONE => Stream.Nil |
|
116 |
| SOME (result,input) => |
|
117 |
Stream.append (Stream.fromList result) (fn () => parserList input) |
|
118 |
in |
|
119 |
parserList |
|
120 |
end; |
|
121 |
||
122 |
(* ------------------------------------------------------------------------- *) |
|
123 |
(* Parsing lines of text. *) |
|
124 |
(* ------------------------------------------------------------------------- *) |
|
125 |
||
126 |
fun initialize {lines} = |
|
127 |
let |
|
128 |
val lastLine = ref (~1,"","","") |
|
129 |
||
130 |
val chars = |
|
131 |
let |
|
132 |
fun saveLast line = |
|
133 |
let |
|
134 |
val ref (n,_,l2,l3) = lastLine |
|
135 |
val () = lastLine := (n + 1, l2, l3, line) |
|
136 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
137 |
String.explode line |
39348 | 138 |
end |
139 |
in |
|
140 |
Stream.memoize (Stream.map saveLast lines) |
|
141 |
end |
|
142 |
||
143 |
fun parseErrorLocation () = |
|
144 |
let |
|
145 |
val ref (n,l1,l2,l3) = lastLine |
|
146 |
in |
|
147 |
(if n <= 0 then "at start" |
|
148 |
else "around line " ^ Int.toString n) ^ |
|
149 |
chomp (":\n" ^ l1 ^ l2 ^ l3) |
|
150 |
end |
|
151 |
in |
|
152 |
{chars = chars, |
|
153 |
parseErrorLocation = parseErrorLocation} |
|
154 |
end; |
|
155 |
||
156 |
fun exactChar (c : char) = some (equal c) >> K (); |
|
157 |
||
158 |
fun exactCharList cs = |
|
159 |
case cs of |
|
160 |
[] => nothing |
|
161 |
| c :: cs => (exactChar c ++ exactCharList cs) >> snd; |
|
162 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
163 |
fun exactString s = exactCharList (String.explode s); |
39348 | 164 |
|
165 |
fun escapeString {escape} = |
|
166 |
let |
|
167 |
fun isEscape c = mem c escape |
|
168 |
||
169 |
fun isNormal c = |
|
170 |
case c of |
|
171 |
#"\\" => false |
|
172 |
| #"\n" => false |
|
173 |
| #"\t" => false |
|
174 |
| _ => not (isEscape c) |
|
175 |
||
176 |
val escapeParser = |
|
177 |
(exactChar #"\\" >> K #"\\") || |
|
178 |
(exactChar #"n" >> K #"\n") || |
|
179 |
(exactChar #"t" >> K #"\t") || |
|
180 |
some isEscape |
|
181 |
||
182 |
val charParser = |
|
183 |
((exactChar #"\\" ++ escapeParser) >> snd) || |
|
184 |
some isNormal |
|
185 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
186 |
many charParser >> String.implode |
39348 | 187 |
end; |
188 |
||
189 |
local |
|
190 |
val isSpace = Char.isSpace; |
|
191 |
||
192 |
val space = some isSpace; |
|
193 |
in |
|
194 |
val manySpace = many space >> K (); |
|
195 |
||
196 |
val atLeastOneSpace = atLeastOne space >> K (); |
|
197 |
end; |
|
198 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
199 |
fun fromString parser s = fromList parser (String.explode s); |
39348 | 200 |
|
201 |
(* ------------------------------------------------------------------------- *) |
|
202 |
(* Infix operators. *) |
|
203 |
(* ------------------------------------------------------------------------- *) |
|
204 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
205 |
fun parseLayeredInfixes {tokens,assoc} mk tokParser subParser = |
39348 | 206 |
let |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
207 |
fun layerTokParser inp = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
208 |
let |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
209 |
val tok_rest as (tok,_) = tokParser inp |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
210 |
in |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
211 |
if StringSet.member tok tokens then tok_rest |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
212 |
else raise NoParse |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
213 |
end |
39348 | 214 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
215 |
fun layerMk (x,txs) = |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
216 |
case assoc of |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
217 |
Print.LeftAssoc => |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
218 |
let |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
219 |
fun inc ((t,y),z) = mk (t,z,y) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
220 |
in |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
221 |
List.foldl inc x txs |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
222 |
end |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
223 |
| Print.NonAssoc => |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
224 |
(case txs of |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
225 |
[] => x |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
226 |
| [(t,y)] => mk (t,x,y) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
227 |
| _ => raise NoParse) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
228 |
| Print.RightAssoc => |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
229 |
(case rev txs of |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
230 |
[] => x |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
231 |
| tx :: txs => |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
232 |
let |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
233 |
fun inc ((t,y),(u,z)) = (t, mk (u,y,z)) |
39348 | 234 |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
235 |
val (t,y) = List.foldl inc tx txs |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
236 |
in |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
237 |
mk (t,x,y) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
238 |
end) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
239 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
240 |
val layerParser = subParser ++ many (layerTokParser ++ subParser) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
241 |
in |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
242 |
layerParser >> layerMk |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
243 |
end; |
39348 | 244 |
|
245 |
fun parseInfixes ops = |
|
246 |
let |
|
247 |
val layeredOps = Print.layerInfixes ops |
|
248 |
||
249 |
val iparsers = List.map parseLayeredInfixes layeredOps |
|
250 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
251 |
fn mk => fn tokParser => fn subParser => |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
252 |
List.foldr (fn (p,sp) => p mk tokParser sp) subParser iparsers |
39348 | 253 |
end; |
254 |
||
255 |
(* ------------------------------------------------------------------------- *) |
|
256 |
(* Quotations. *) |
|
257 |
(* ------------------------------------------------------------------------- *) |
|
258 |
||
259 |
type 'a quotation = 'a frag list; |
|
260 |
||
261 |
fun parseQuotation printer parser quote = |
|
262 |
let |
|
263 |
fun expand (QUOTE q, s) = s ^ q |
|
264 |
| expand (ANTIQUOTE a, s) = s ^ printer a |
|
265 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39349
diff
changeset
|
266 |
val string = List.foldl expand "" quote |
39348 | 267 |
in |
268 |
parser string |
|
269 |
end; |
|
270 |
||
271 |
end |