author | wenzelm |
Tue, 22 Apr 2014 23:57:17 +0200 | |
changeset 56663 | 2d09b437c168 |
parent 55980 | 36fd4981c119 |
child 56821 | 2e6d46a3a617 |
permissions | -rw-r--r-- |
31648 | 1 |
/* Title: Pure/General/scan.scala |
2 |
Author: Makarius |
|
3 |
||
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40290
diff
changeset
|
4 |
Efficient scanning of keywords and tokens. |
31648 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
9 |
|
55980 | 10 |
import scala.annotation.tailrec |
46627
fbe2cb05bdb3
avoid trait Addable, which is deprecated in scala-2.9.x;
wenzelm
parents:
45900
diff
changeset
|
11 |
import scala.collection.{IndexedSeq, TraversableOnce} |
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
12 |
import scala.collection.immutable.PagedSeq |
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
13 |
import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader} |
31648 | 14 |
import scala.util.parsing.combinator.RegexParsers |
15 |
||
48409 | 16 |
import java.io.{File => JFile, BufferedInputStream, FileInputStream} |
34187
7b659c1561f1
added byte_reader, which works without decoding and enables efficient length operation (for scala.util.parsing.input.Reader);
wenzelm
parents:
34157
diff
changeset
|
17 |
|
31648 | 18 |
|
19 |
object Scan |
|
20 |
{ |
|
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
21 |
/** context of partial line-oriented scans **/ |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
22 |
|
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
23 |
abstract class Line_Context |
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
24 |
case object Finished extends Line_Context |
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
25 |
case class Quoted(quote: String) extends Line_Context |
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
26 |
case object Verbatim extends Line_Context |
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
27 |
case class Cartouche(depth: Int) extends Line_Context |
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
28 |
case class Comment(depth: Int) extends Line_Context |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
29 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
30 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
31 |
|
55492
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
32 |
/** parser combinators **/ |
31650 | 33 |
|
55492
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
34 |
object Parsers extends Parsers |
36011
3ff725ac13a4
adapted to Scala 2.8.0 Beta1 -- with notable changes to scala.collection;
wenzelm
parents:
34316
diff
changeset
|
35 |
|
55492
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
36 |
trait Parsers extends RegexParsers |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
37 |
{ |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
38 |
override val whiteSpace = "".r |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
39 |
|
34137 | 40 |
|
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
41 |
/* optional termination */ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
42 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
43 |
def opt_term[T](p: => Parser[T]): Parser[Option[T]] = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
44 |
p ^^ (x => Some(x)) | """\z""".r ^^ (_ => None) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
45 |
|
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
46 |
|
55497 | 47 |
/* repeated symbols */ |
34137 | 48 |
|
55497 | 49 |
def repeated(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] = |
34140 | 50 |
new Parser[String] |
34135 | 51 |
{ |
34137 | 52 |
def apply(in: Input) = |
53 |
{ |
|
54 |
val start = in.offset |
|
55 |
val end = in.source.length |
|
56 |
val matcher = new Symbol.Matcher(in.source) |
|
57 |
||
58 |
var i = start |
|
59 |
var count = 0 |
|
60 |
var finished = false |
|
55034 | 61 |
while (!finished && i < end && count < max_count) { |
62 |
val n = matcher(i, end) |
|
63 |
val sym = in.source.subSequence(i, i + n).toString |
|
64 |
if (pred(sym)) { i += n; count += 1 } |
|
34137 | 65 |
else finished = true |
66 |
} |
|
34140 | 67 |
if (count < min_count) Failure("bad input", in) |
68 |
else Success(in.source.subSequence(start, i).toString, in.drop(i - start)) |
|
34137 | 69 |
} |
55497 | 70 |
}.named("repeated") |
34137 | 71 |
|
43696 | 72 |
def one(pred: Symbol.Symbol => Boolean): Parser[String] = |
55497 | 73 |
repeated(pred, 1, 1) |
43696 | 74 |
|
75 |
def many(pred: Symbol.Symbol => Boolean): Parser[String] = |
|
55497 | 76 |
repeated(pred, 0, Integer.MAX_VALUE) |
43696 | 77 |
|
78 |
def many1(pred: Symbol.Symbol => Boolean): Parser[String] = |
|
55497 | 79 |
repeated(pred, 1, Integer.MAX_VALUE) |
80 |
||
81 |
||
82 |
/* character */ |
|
83 |
||
84 |
def character(pred: Char => Boolean): Symbol.Symbol => Boolean = |
|
85 |
(s: Symbol. Symbol) => s.length == 1 && pred(s.charAt(0)) |
|
34140 | 86 |
|
87 |
||
34143 | 88 |
/* quoted strings */ |
34140 | 89 |
|
43696 | 90 |
private def quoted_body(quote: Symbol.Symbol): Parser[String] = |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
91 |
{ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
92 |
rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" | |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
93 |
(("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
94 |
} |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
95 |
|
55494 | 96 |
def quoted(quote: Symbol.Symbol): Parser[String] = |
34143 | 97 |
{ |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
98 |
quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z } |
34143 | 99 |
}.named("quoted") |
34140 | 100 |
|
43696 | 101 |
def quoted_content(quote: Symbol.Symbol, source: String): String = |
34140 | 102 |
{ |
103 |
require(parseAll(quoted(quote), source).successful) |
|
34189 | 104 |
val body = source.substring(1, source.length - 1) |
105 |
if (body.exists(_ == '\\')) { |
|
106 |
val content = |
|
40523
1050315f6ee2
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
wenzelm
parents:
40290
diff
changeset
|
107 |
rep(many1(sym => sym != quote && sym != "\\") | |
34189 | 108 |
"\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString })) |
109 |
parseAll(content ^^ (_.mkString), body).get |
|
110 |
} |
|
111 |
else body |
|
34140 | 112 |
} |
113 |
||
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
114 |
def quoted_line(quote: Symbol.Symbol, ctxt: Line_Context): Parser[(String, Line_Context)] = |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
115 |
{ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
116 |
ctxt match { |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
117 |
case Finished => |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
118 |
quote ~ quoted_body(quote) ~ opt_term(quote) ^^ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
119 |
{ case x ~ y ~ Some(z) => (x + y + z, Finished) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
120 |
case x ~ y ~ None => (x + y, Quoted(quote)) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
121 |
case Quoted(q) if q == quote => |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
122 |
quoted_body(quote) ~ opt_term(quote) ^^ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
123 |
{ case x ~ Some(y) => (x + y, Finished) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
124 |
case x ~ None => (x, ctxt) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
125 |
case _ => failure("") |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
126 |
} |
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
127 |
}.named("quoted_line") |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
128 |
|
48763
de68fc11c245
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
wenzelm
parents:
48754
diff
changeset
|
129 |
def recover_quoted(quote: Symbol.Symbol): Parser[String] = |
de68fc11c245
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
wenzelm
parents:
48754
diff
changeset
|
130 |
quote ~ quoted_body(quote) ^^ { case x ~ y => x + y } |
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48409
diff
changeset
|
131 |
|
34140 | 132 |
|
34143 | 133 |
/* verbatim text */ |
134 |
||
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
135 |
private def verbatim_body: Parser[String] = |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
136 |
rep(many1(sym => sym != "*") | """\*(?!\})""".r) ^^ (_.mkString) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
137 |
|
55494 | 138 |
def verbatim: Parser[String] = |
34143 | 139 |
{ |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
140 |
"{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z } |
34143 | 141 |
}.named("verbatim") |
34140 | 142 |
|
143 |
def verbatim_content(source: String): String = |
|
144 |
{ |
|
145 |
require(parseAll(verbatim, source).successful) |
|
146 |
source.substring(2, source.length - 2) |
|
147 |
} |
|
148 |
||
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
149 |
def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] = |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
150 |
{ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
151 |
ctxt match { |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
152 |
case Finished => |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
153 |
"{*" ~ verbatim_body ~ opt_term("*}") ^^ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
154 |
{ case x ~ y ~ Some(z) => (x + y + z, Finished) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
155 |
case x ~ y ~ None => (x + y, Verbatim) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
156 |
case Verbatim => |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
157 |
verbatim_body ~ opt_term("*}") ^^ |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
158 |
{ case x ~ Some(y) => (x + y, Finished) |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
159 |
case x ~ None => (x, Verbatim) } |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
160 |
case _ => failure("") |
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
161 |
} |
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
162 |
}.named("verbatim_line") |
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
42718
diff
changeset
|
163 |
|
48763
de68fc11c245
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
wenzelm
parents:
48754
diff
changeset
|
164 |
val recover_verbatim: Parser[String] = |
de68fc11c245
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
wenzelm
parents:
48754
diff
changeset
|
165 |
"{*" ~ verbatim_body ^^ { case x ~ y => x + y } |
48743
a72f8ffecf31
refined recovery of scan errors: longest prefix of delimited token after failure, otherwise just one symbol;
wenzelm
parents:
48409
diff
changeset
|
166 |
|
34140 | 167 |
|
55033 | 168 |
/* nested text cartouches */ |
169 |
||
170 |
private def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] |
|
171 |
{ |
|
172 |
require(depth >= 0) |
|
173 |
||
174 |
def apply(in: Input) = |
|
175 |
{ |
|
176 |
val start = in.offset |
|
177 |
val end = in.source.length |
|
178 |
val matcher = new Symbol.Matcher(in.source) |
|
179 |
||
180 |
var i = start |
|
181 |
var d = depth |
|
182 |
var finished = false |
|
55034 | 183 |
while (!finished && i < end) { |
184 |
val n = matcher(i, end) |
|
185 |
val sym = in.source.subSequence(i, i + n).toString |
|
186 |
if (Symbol.is_open(sym)) { i += n; d += 1 } |
|
187 |
else if (d > 0) { i += n; if (Symbol.is_close(sym)) d -= 1 } |
|
55033 | 188 |
else finished = true |
189 |
} |
|
190 |
if (i == start) Failure("bad input", in) |
|
191 |
else Success((in.source.subSequence(start, i).toString, d), in.drop(i - start)) |
|
192 |
} |
|
193 |
}.named("cartouche_depth") |
|
194 |
||
195 |
def cartouche: Parser[String] = |
|
196 |
cartouche_depth(0) ^? { case (x, d) if d == 0 => x } |
|
197 |
||
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
198 |
def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] = |
55033 | 199 |
{ |
200 |
val depth = |
|
201 |
ctxt match { |
|
202 |
case Finished => 0 |
|
203 |
case Cartouche(d) => d |
|
204 |
case _ => -1 |
|
205 |
} |
|
206 |
if (depth >= 0) |
|
207 |
cartouche_depth(depth) ^^ |
|
208 |
{ case (x, 0) => (x, Finished) |
|
209 |
case (x, d) => (x, Cartouche(d)) } |
|
210 |
else failure("") |
|
211 |
} |
|
212 |
||
213 |
val recover_cartouche: Parser[String] = |
|
214 |
cartouche_depth(0) ^^ (_._1) |
|
215 |
||
216 |
def cartouche_content(source: String): String = |
|
217 |
{ |
|
218 |
def err(): Nothing = error("Malformed text cartouche: " + quote(source)) |
|
219 |
val source1 = |
|
220 |
Library.try_unprefix(Symbol.open_decoded, source) orElse |
|
221 |
Library.try_unprefix(Symbol.open, source) getOrElse err() |
|
222 |
Library.try_unsuffix(Symbol.close_decoded, source1) orElse |
|
223 |
Library.try_unsuffix(Symbol.close, source1) getOrElse err() |
|
224 |
} |
|
225 |
||
226 |
||
34143 | 227 |
/* nested comments */ |
228 |
||
43412 | 229 |
private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] |
34143 | 230 |
{ |
43412 | 231 |
require(depth >= 0) |
232 |
||
34143 | 233 |
val comment_text = |
42441
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset
|
234 |
rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r) |
34143 | 235 |
|
236 |
def apply(in: Input) = |
|
237 |
{ |
|
238 |
var rest = in |
|
42441
781c622af16a
more robust scanning of iterated comments, such as "(* (**) (**) *)";
wenzelm
parents:
40523
diff
changeset
|
239 |
def try_parse[A](p: Parser[A]): Boolean = |
34143 | 240 |
{ |
56663
2d09b437c168
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
55980
diff
changeset
|
241 |
parse(p ^^^ (()), rest) match { |
34143 | 242 |
case Success(_, next) => { rest = next; true } |
243 |
case _ => false |
|
244 |
} |
|
245 |
} |
|
43412 | 246 |
var d = depth |
34143 | 247 |
var finished = false |
248 |
while (!finished) { |
|
43412 | 249 |
if (try_parse("(*")) d += 1 |
250 |
else if (d > 0 && try_parse("*)")) d -= 1 |
|
251 |
else if (d == 0 || !try_parse(comment_text)) finished = true |
|
34143 | 252 |
} |
43412 | 253 |
if (in.offset < rest.offset) |
254 |
Success((in.source.subSequence(in.offset, rest.offset).toString, d), rest) |
|
34143 | 255 |
else Failure("comment expected", in) |
256 |
} |
|
43412 | 257 |
}.named("comment_depth") |
258 |
||
259 |
def comment: Parser[String] = |
|
260 |
comment_depth(0) ^? { case (x, d) if d == 0 => x } |
|
261 |
||
55510
1585a65aad64
tuned signature -- emphasize line-oriented aspect;
wenzelm
parents:
55499
diff
changeset
|
262 |
def comment_line(ctxt: Line_Context): Parser[(String, Line_Context)] = |
43412 | 263 |
{ |
264 |
val depth = |
|
265 |
ctxt match { |
|
266 |
case Finished => 0 |
|
267 |
case Comment(d) => d |
|
268 |
case _ => -1 |
|
269 |
} |
|
270 |
if (depth >= 0) |
|
271 |
comment_depth(depth) ^^ |
|
272 |
{ case (x, 0) => (x, Finished) |
|
273 |
case (x, d) => (x, Comment(d)) } |
|
274 |
else failure("") |
|
275 |
} |
|
34143 | 276 |
|
48763
de68fc11c245
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
wenzelm
parents:
48754
diff
changeset
|
277 |
val recover_comment: Parser[String] = |
de68fc11c245
more precise recover_quoted, recover_verbatim, recover_comment (cf. ML version) -- NB: context parsers expect explicit termination;
wenzelm
parents:
48754
diff
changeset
|
278 |
comment_depth(0) ^^ (_._1) |
34143 | 279 |
|
55033 | 280 |
def comment_content(source: String): String = |
281 |
{ |
|
282 |
require(parseAll(comment, source).successful) |
|
283 |
source.substring(2, source.length - 2) |
|
284 |
} |
|
285 |
||
34143 | 286 |
|
55492
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
287 |
/* keyword */ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
288 |
|
55497 | 289 |
def literal(lexicon: Lexicon): Parser[String] = new Parser[String] |
55492
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
290 |
{ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
291 |
def apply(in: Input) = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
292 |
{ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
293 |
val result = lexicon.scan(in) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
294 |
if (result.isEmpty) Failure("keyword expected", in) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
295 |
else Success(result, in.drop(result.length)) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
296 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
297 |
}.named("keyword") |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
298 |
} |
55492
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
299 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
300 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
301 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
302 |
/** Lexicon -- position tree **/ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
303 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
304 |
object Lexicon |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
305 |
{ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
306 |
/* representation */ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
307 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
308 |
private sealed case class Tree(val branches: Map[Char, (String, Tree)]) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
309 |
private val empty_tree = Tree(Map()) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
310 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
311 |
val empty: Lexicon = new Lexicon(empty_tree) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
312 |
def apply(elems: String*): Lexicon = empty ++ elems |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
313 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
314 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
315 |
final class Lexicon private(rep: Lexicon.Tree) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
316 |
{ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
317 |
/* auxiliary operations */ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
318 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
319 |
private def content(tree: Lexicon.Tree, result: List[String]): List[String] = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
320 |
(result /: tree.branches.toList) ((res, entry) => |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
321 |
entry match { case (_, (s, tr)) => |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
322 |
if (s.isEmpty) content(tr, res) else content(tr, s :: res) }) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
323 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
324 |
private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
325 |
{ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
326 |
val len = str.length |
55980 | 327 |
@tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] = |
55492
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
328 |
{ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
329 |
if (i < len) { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
330 |
tree.branches.get(str.charAt(i)) match { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
331 |
case Some((s, tr)) => look(tr, !s.isEmpty, i + 1) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
332 |
case None => None |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
333 |
} |
55980 | 334 |
} |
335 |
else Some(tip, tree) |
|
55492
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
336 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
337 |
look(rep, false, 0) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
338 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
339 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
340 |
def completions(str: CharSequence): List[String] = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
341 |
lookup(str) match { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
342 |
case Some((true, tree)) => content(tree, List(str.toString)) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
343 |
case Some((false, tree)) => content(tree, Nil) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
344 |
case None => Nil |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
345 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
346 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
347 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
348 |
/* pseudo Set methods */ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
349 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
350 |
def iterator: Iterator[String] = content(rep, Nil).sorted.iterator |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
351 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
352 |
override def toString: String = iterator.mkString("Lexicon(", ", ", ")") |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
353 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
354 |
def empty: Lexicon = Lexicon.empty |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
355 |
def isEmpty: Boolean = rep.branches.isEmpty |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
356 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
357 |
def contains(elem: String): Boolean = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
358 |
lookup(elem) match { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
359 |
case Some((tip, _)) => tip |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
360 |
case _ => false |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
361 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
362 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
363 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
364 |
/* add elements */ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
365 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
366 |
def + (elem: String): Lexicon = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
367 |
if (contains(elem)) this |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
368 |
else { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
369 |
val len = elem.length |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
370 |
def extend(tree: Lexicon.Tree, i: Int): Lexicon.Tree = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
371 |
if (i < len) { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
372 |
val c = elem.charAt(i) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
373 |
val end = (i + 1 == len) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
374 |
tree.branches.get(c) match { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
375 |
case Some((s, tr)) => |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
376 |
Lexicon.Tree(tree.branches + |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
377 |
(c -> (if (end) elem else s, extend(tr, i + 1)))) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
378 |
case None => |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
379 |
Lexicon.Tree(tree.branches + |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
380 |
(c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1)))) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
381 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
382 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
383 |
else tree |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
384 |
new Lexicon(extend(rep, 0)) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
385 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
386 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
387 |
def ++ (elems: TraversableOnce[String]): Lexicon = (this /: elems)(_ + _) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
388 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
389 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
390 |
/* scan */ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
391 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
392 |
def scan(in: Reader[Char]): String = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
393 |
{ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
394 |
val source = in.source |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
395 |
val offset = in.offset |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
396 |
val len = source.length - offset |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
397 |
|
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
398 |
def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String = |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
399 |
{ |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
400 |
if (i < len) { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
401 |
tree.branches.get(source.charAt(offset + i)) match { |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
402 |
case Some((s, tr)) => scan_tree(tr, if (s.isEmpty) result else s, i + 1) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
403 |
case None => result |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
404 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
405 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
406 |
else result |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
407 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
408 |
scan_tree(rep, "", 0) |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
409 |
} |
28d4db6c6e79
tuned signature -- separate Lexicon from Parsers (in accordance to ML version);
wenzelm
parents:
55034
diff
changeset
|
410 |
} |
31648 | 411 |
} |