author | wenzelm |
Tue, 23 Jun 2009 17:43:51 +0200 | |
changeset 31764 | e767fee21b22 |
parent 31762 | 20745ab5b79a |
child 32450 | 375db037f4d2 |
permissions | -rw-r--r-- |
31648 | 1 |
/* Title: Pure/General/scan.scala |
2 |
Author: Makarius |
|
3 |
||
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
4 |
Efficient scanning of keywords. |
31648 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
import scala.util.parsing.combinator.RegexParsers |
|
10 |
||
11 |
||
12 |
object Scan |
|
13 |
{ |
|
14 |
||
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
15 |
/** Lexicon -- position tree **/ |
31648 | 16 |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
17 |
object Lexicon |
31648 | 18 |
{ |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
19 |
private case class Tree(val branches: Map[Char, (String, Tree)]) |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
20 |
private val empty_tree = Tree(Map()) |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
21 |
|
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
22 |
val empty: Lexicon = new Lexicon |
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
23 |
def apply(elems: String*): Lexicon = empty ++ elems |
31648 | 24 |
} |
25 |
||
31764 | 26 |
class Lexicon extends scala.collection.Set[String] with RegexParsers |
31648 | 27 |
{ |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
28 |
/* representation */ |
31648 | 29 |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
30 |
import Lexicon.Tree |
31764 | 31 |
protected val main_tree: Tree = Lexicon.empty_tree |
31648 | 32 |
|
33 |
||
31650 | 34 |
/* auxiliary operations */ |
35 |
||
36 |
private def content(tree: Tree, result: List[String]): List[String] = |
|
37 |
(result /: tree.branches.toList) ((res, entry) => |
|
38 |
entry match { case (_, (s, tr)) => |
|
39 |
if (s.isEmpty) content(tr, res) else content(tr, s :: res) }) |
|
40 |
||
41 |
private def lookup(str: CharSequence): Option[(Boolean, Tree)] = |
|
42 |
{ |
|
43 |
val len = str.length |
|
44 |
def look(tree: Tree, tip: Boolean, i: Int): Option[(Boolean, Tree)] = |
|
45 |
{ |
|
46 |
if (i < len) { |
|
47 |
tree.branches.get(str.charAt(i)) match { |
|
48 |
case Some((s, tr)) => look(tr, !s.isEmpty, i + 1) |
|
49 |
case None => None |
|
50 |
} |
|
51 |
} else Some(tip, tree) |
|
52 |
} |
|
53 |
look(main_tree, false, 0) |
|
54 |
} |
|
55 |
||
56 |
def completions(str: CharSequence): List[String] = |
|
31764 | 57 |
lookup(str) match { |
31650 | 58 |
case Some((true, tree)) => content(tree, List(str.toString)) |
59 |
case Some((false, tree)) => content(tree, Nil) |
|
60 |
case None => Nil |
|
31764 | 61 |
} |
31650 | 62 |
|
63 |
||
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
64 |
/* Set methods */ |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
65 |
|
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
66 |
override def stringPrefix = "Lexicon" |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
67 |
|
31753 | 68 |
override def isEmpty: Boolean = { main_tree.branches.isEmpty } |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
69 |
|
31650 | 70 |
def size: Int = content(main_tree, Nil).length |
71 |
def elements: Iterator[String] = content(main_tree, Nil).sort(_ <= _).elements |
|
31648 | 72 |
|
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
73 |
def contains(elem: String): Boolean = |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
74 |
lookup(elem) match { |
31650 | 75 |
case Some((tip, _)) => tip |
76 |
case _ => false |
|
77 |
} |
|
31648 | 78 |
|
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
79 |
def + (elem: String): Lexicon = |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
80 |
if (contains(elem)) this |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
81 |
else { |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
82 |
val len = elem.length |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
83 |
def extend(tree: Tree, i: Int): Tree = |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
84 |
if (i < len) { |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
85 |
val c = elem.charAt(i) |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
86 |
val end = (i + 1 == len) |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
87 |
tree.branches.get(c) match { |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
88 |
case Some((s, tr)) => |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
89 |
Tree(tree.branches + |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
90 |
(c -> (if (end) elem else s, extend(tr, i + 1)))) |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
91 |
case None => |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
92 |
Tree(tree.branches + |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
93 |
(c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1)))) |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
94 |
} |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
95 |
} else tree |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
96 |
val old = this |
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
97 |
new Lexicon { override val main_tree = extend(old.main_tree, 0) } |
31648 | 98 |
} |
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
99 |
|
31764 | 100 |
def + (elem1: String, elem2: String, elems: String*): Lexicon = |
31762
20745ab5b79a
more precise implementation of trait methods -- oddly this seems to require copy/paste for +, ++;
wenzelm
parents:
31753
diff
changeset
|
101 |
this + elem1 + elem2 ++ elems |
31764 | 102 |
def ++ (elems: Iterable[String]): Lexicon = (this /: elems) ((s, elem) => s + elem) |
103 |
def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem) |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
104 |
|
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
105 |
|
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
106 |
/* RegexParsers methods */ |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
107 |
|
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
108 |
override val whiteSpace = "".r |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
109 |
|
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
110 |
def keyword: Parser[String] = new Parser[String] { |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
111 |
def apply(in: Input) = |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
112 |
{ |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
113 |
val source = in.source |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
114 |
val offset = in.offset |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
115 |
val len = source.length - offset |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
116 |
|
31650 | 117 |
def scan(tree: Tree, text: String, i: Int): String = |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
118 |
{ |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
119 |
if (i < len) { |
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
120 |
tree.branches.get(source.charAt(offset + i)) match { |
31650 | 121 |
case Some((s, tr)) => scan(tr, if (s.isEmpty) text else s, i + 1) |
122 |
case None => text |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
123 |
} |
31650 | 124 |
} else text |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
125 |
} |
31650 | 126 |
val text = scan(main_tree, "", 0) |
127 |
if (text.isEmpty) Failure("keyword expected", in) |
|
128 |
else Success(text, in.drop(text.length)) |
|
31648 | 129 |
} |
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
130 |
}.named("keyword") |
31648 | 131 |
|
31649
a11ea667d676
reorganized and abstracted version, via Set trait;
wenzelm
parents:
31648
diff
changeset
|
132 |
} |
31648 | 133 |
} |
134 |