author | Chengsong |
Tue, 14 Jun 2022 18:06:33 +0100 | |
changeset 542 | a7344c9afbaf |
parent 436 | 222333d2bdc2 |
permissions | -rw-r--r-- |
436 | 1 |
|
2 |
||
3 |
||
4 |
||
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
import scala.language.implicitConversions |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
import scala.language.reflectiveCalls |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
7 |
import scala.annotation.tailrec |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
8 |
|
360 | 9 |
// standard regular expressions |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
10 |
abstract class Rexp |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
11 |
case object ZERO extends Rexp |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
12 |
case object ONE extends Rexp |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
13 |
case class CHAR(c: Char) extends Rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
14 |
case class ALT(r1: Rexp, r2: Rexp) extends Rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
15 |
case class SEQ(r1: Rexp, r2: Rexp) extends Rexp |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
16 |
case class STAR(r: Rexp) extends Rexp |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
17 |
|
359 | 18 |
abstract class Bit |
19 |
case object Z extends Bit |
|
20 |
case object S extends Bit |
|
21 |
||
22 |
type Bits = List[Bit] |
|
23 |
||
360 | 24 |
// annotated regular expressions |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
25 |
abstract class ARexp |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
26 |
case object AZERO extends ARexp |
359 | 27 |
case class AONE(bs: Bits) extends ARexp |
28 |
case class ACHAR(bs: Bits, c: Char) extends ARexp |
|
29 |
case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp |
|
30 |
case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp |
|
31 |
case class ASTAR(bs: Bits, r: ARexp) extends ARexp |
|
32 |
||
360 | 33 |
// an abbreviation for binary alternatives |
359 | 34 |
def AALT(bs: Bits, r1: ARexp, r2: ARexp) = AALTS(bs, List(r1, r2)) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
abstract class Val |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
37 |
case object Empty extends Val |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
38 |
case class Chr(c: Char) extends Val |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
39 |
case class Sequ(v1: Val, v2: Val) extends Val |
13
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
40 |
case class Left(v: Val) extends Val |
62fe79ee2726
fixed the scala implementation
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
3
diff
changeset
|
41 |
case class Right(v: Val) extends Val |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
42 |
case class Stars(vs: List[Val]) extends Val |
360 | 43 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
// some convenience for typing in regular expressions |
359 | 46 |
def charlist2rexp(s: List[Char]): Rexp = s match { |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
47 |
case Nil => ONE |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
48 |
case c::Nil => CHAR(c) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
case c::s => SEQ(CHAR(c), charlist2rexp(s)) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
50 |
} |
359 | 51 |
implicit def string2rexp(s: String) : Rexp = charlist2rexp(s.toList) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
53 |
implicit def RexpOps(r: Rexp) = new { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
def | (s: Rexp) = ALT(r, s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
def % = STAR(r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
56 |
def ~ (s: Rexp) = SEQ(r, s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
57 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
58 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
implicit def stringOps(s: String) = new { |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
60 |
def | (r: Rexp) = ALT(s, r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
61 |
def | (r: String) = ALT(s, r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
62 |
def % = STAR(s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
63 |
def ~ (r: Rexp) = SEQ(s, r) |
81
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
64 |
def ~ (r: String) = SEQ(s, r) |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
65 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
66 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
67 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
68 |
// Bitcoded + Annotation |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
69 |
//======================= |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
70 |
|
360 | 71 |
//erase function: extracts the Rexp from ARexp |
359 | 72 |
def erase(r:ARexp): Rexp = r match{ |
73 |
case AZERO => ZERO |
|
74 |
case AONE(_) => ONE |
|
75 |
case ACHAR(bs, c) => CHAR(c) |
|
76 |
case AALTS(bs, Nil) => ZERO |
|
77 |
case AALTS(bs, r::Nil) => erase(r) |
|
78 |
case AALTS(bs, r::rs) => ALT(erase(r), erase(AALTS(bs, rs))) |
|
79 |
case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2)) |
|
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
80 |
case ASTAR(cs, ASTAR(ds, r))=> STAR(erase(r)) |
359 | 81 |
case ASTAR(cs, r)=> STAR(erase(r)) |
82 |
} |
|
83 |
||
84 |
def fuse(bs: Bits, r: ARexp) : ARexp = r match { |
|
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
85 |
case AZERO => AZERO |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
86 |
case AONE(cs) => AONE(bs ++ cs) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
87 |
case ACHAR(cs, c) => ACHAR(bs ++ cs, c) |
359 | 88 |
case AALTS(cs, rs) => AALTS(bs ++ cs, rs) |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
89 |
case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
90 |
case ASTAR(cs, r) => ASTAR(bs ++ cs, r) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
91 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
92 |
|
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
93 |
def internalise(r: Rexp) : ARexp = r match { |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
94 |
case ZERO => AZERO |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
95 |
case ONE => AONE(Nil) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
96 |
case CHAR(c) => ACHAR(Nil, c) |
359 | 97 |
case ALT(r1, r2) => AALT(Nil, fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2))) |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
98 |
case SEQ(r1, r2) => ASEQ(Nil, internalise(r1), internalise(r2)) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
99 |
case STAR(r) => ASTAR(Nil, internalise(r)) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
100 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
101 |
|
294 | 102 |
|
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
103 |
internalise(("a" | "ab") ~ ("b" | "")) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
104 |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
105 |
|
360 | 106 |
// decoding of a value from a bitsequence |
359 | 107 |
def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match { |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
108 |
case (ONE, bs) => (Empty, bs) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
109 |
case (CHAR(c), bs) => (Chr(c), bs) |
359 | 110 |
case (ALT(r1, r2), Z::bs) => { |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
111 |
val (v, bs1) = decode_aux(r1, bs) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
112 |
(Left(v), bs1) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
113 |
} |
359 | 114 |
case (ALT(r1, r2), S::bs) => { |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
115 |
val (v, bs1) = decode_aux(r2, bs) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
116 |
(Right(v), bs1) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
117 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
118 |
case (SEQ(r1, r2), bs) => { |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
119 |
val (v1, bs1) = decode_aux(r1, bs) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
120 |
val (v2, bs2) = decode_aux(r2, bs1) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
121 |
(Sequ(v1, v2), bs2) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
122 |
} |
359 | 123 |
case (STAR(r1), Z::bs) => { |
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
124 |
val (v, bs1) = decode_aux(r1, bs) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
125 |
val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1) |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
126 |
(Stars(v::vs), bs2) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
127 |
} |
359 | 128 |
case (STAR(_), S::bs) => (Stars(Nil), bs) |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
129 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
130 |
|
359 | 131 |
def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match { |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
132 |
case (v, Nil) => v |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
133 |
case _ => throw new Exception("Not decodable") |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
134 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
135 |
|
359 | 136 |
def encode(v: Val) : Bits = v match { |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
137 |
case Empty => Nil |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
138 |
case Chr(c) => Nil |
359 | 139 |
case Left(v) => Z :: encode(v) |
140 |
case Right(v) => S :: encode(v) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
141 |
case Sequ(v1, v2) => encode(v1) ::: encode(v2) |
359 | 142 |
case Stars(Nil) => List(S) |
143 |
case Stars(v::vs) => Z :: encode(v) ::: encode(Stars(vs)) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
144 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
145 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
146 |
|
360 | 147 |
// nullable function: tests whether the an (annotated) |
148 |
// regular expression can recognise the empty string |
|
359 | 149 |
def bnullable (r: ARexp) : Boolean = r match { |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
150 |
case AZERO => false |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
151 |
case AONE(_) => true |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
152 |
case ACHAR(_,_) => false |
359 | 153 |
case AALTS(_, rs) => rs.exists(bnullable) |
154 |
case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2) |
|
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
155 |
case ASTAR(_, _) => true |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
156 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
157 |
|
359 | 158 |
def bmkeps(r: ARexp) : Bits = r match { |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
159 |
case AONE(bs) => bs |
359 | 160 |
case AALTS(bs, r::Nil) => bs ++ bmkeps(r) |
161 |
case AALTS(bs, r::rs) => |
|
162 |
if (bnullable(r)) bs ++ bmkeps(r) else bmkeps(AALTS(bs, rs)) |
|
163 |
case ASEQ(bs, r1, r2) => bs ++ bmkeps(r1) ++ bmkeps(r2) |
|
164 |
case ASTAR(bs, r) => bs ++ List(S) |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
165 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
166 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
167 |
// derivative of a regular expression w.r.t. a character |
359 | 168 |
def bder(c: Char, r: ARexp) : ARexp = r match { |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
169 |
case AZERO => AZERO |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
170 |
case AONE(_) => AZERO |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
171 |
case ACHAR(bs, d) => if (c == d) AONE(bs) else AZERO |
359 | 172 |
case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _))) |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
173 |
case ASEQ(bs, r1, r2) => |
359 | 174 |
if (bnullable(r1)) AALT(bs, ASEQ(Nil, bder(c, r1), r2), fuse(bmkeps(r1), bder(c, r2))) |
175 |
else ASEQ(bs, bder(c, r1), r2) |
|
176 |
case ASTAR(bs, r) => ASEQ(bs, fuse(List(Z), bder(c, r)), ASTAR(Nil, r)) |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
177 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
178 |
|
360 | 179 |
// derivative w.r.t. a string (iterates bder) |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
180 |
@tailrec |
359 | 181 |
def bders (s: List[Char], r: ARexp) : ARexp = s match { |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
182 |
case Nil => r |
359 | 183 |
case c::s => bders(s, bder(c, r)) |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
184 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
185 |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
186 |
// main unsimplified lexing function (produces a value) |
359 | 187 |
def blex(r: ARexp, s: List[Char]) : Bits = s match { |
188 |
case Nil => if (bnullable(r)) bmkeps(r) else throw new Exception("Not matched") |
|
189 |
case c::cs => blex(bder(c, r), cs) |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
190 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
191 |
|
359 | 192 |
def pre_blexing(r: ARexp, s: String) : Bits = blex(r, s.toList) |
193 |
def blexing(r: Rexp, s: String) : Val = decode(r, pre_blexing(internalise(r), s)) |
|
194 |
||
195 |
||
196 |
// example by Tudor |
|
360 | 197 |
//val reg = ((("a".%)) ~ ("b" | "c")).% |
359 | 198 |
|
360 | 199 |
//println(blexing(reg, "aab")) |
359 | 200 |
|
201 |
||
202 |
//======================= |
|
203 |
// simplification |
|
204 |
// |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
205 |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
206 |
|
359 | 207 |
def flts(rs: List[ARexp]) : List[ARexp] = rs match { |
208 |
case Nil => Nil |
|
209 |
case AZERO :: rs => flts(rs) |
|
210 |
case AALTS(bs, rs1) :: rs => rs1.map(fuse(bs, _)) ++ flts(rs) |
|
211 |
case r1 :: rs => r1 :: flts(rs) |
|
212 |
} |
|
213 |
||
214 |
def distinctBy[B, C](xs: List[B], |
|
215 |
f: B => C, |
|
216 |
acc: List[C] = Nil): List[B] = xs match { |
|
217 |
case Nil => Nil |
|
218 |
case x::xs => { |
|
219 |
val res = f(x) |
|
220 |
if (acc.contains(res)) distinctBy(xs, f, acc) |
|
221 |
else x::distinctBy(xs, f, res::acc) |
|
222 |
} |
|
223 |
} |
|
224 |
||
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
225 |
def flats(rs: List[ARexp]): List[ARexp] = rs match { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
226 |
case Nil => Nil |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
227 |
case AZERO :: rs1 => flats(rs1) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
228 |
case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
229 |
case r1 :: rs2 => r1 :: flats(rs2) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
230 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
231 |
|
359 | 232 |
def bsimp(r: ARexp): ARexp = r match { |
233 |
case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match { |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
234 |
case (AZERO, _) => AZERO |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
235 |
case (_, AZERO) => AZERO |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
236 |
case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
237 |
case (r1s, r2s) => ASEQ(bs1, r1s, r2s) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
238 |
} |
360 | 239 |
case AALTS(bs1, rs) => (flts(rs.map(bsimp))).distinctBy(erase) match { |
359 | 240 |
case Nil => AZERO |
241 |
case r::Nil => fuse(bs1, r) |
|
242 |
case rs => AALTS(bs1, rs) |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
243 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
244 |
case r => r |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
245 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
246 |
|
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
247 |
def bders_simp(r: ARexp, s: List[Char]) : ARexp = s match { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
248 |
case Nil => r |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
249 |
case c::cs => bders_simp(bsimp(bder(c, r)), cs) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
250 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
251 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
252 |
|
359 | 253 |
def blex_simp(r: ARexp, s: List[Char]) : Bits = s match { |
254 |
case Nil => if (bnullable(r)) bmkeps(r) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
255 |
else throw new Exception("Not matched") |
436 | 256 |
case c::cs => blex_simp(bsimp(bder(c, r)), cs) |
359 | 257 |
} |
258 |
||
259 |
def blexing_simp(r: Rexp, s: String) : Val = |
|
260 |
decode(r, blex_simp(internalise(r), s.toList)) |
|
261 |
||
436 | 262 |
////////////////////// |
263 |
// new simplification |
|
264 |
||
265 |
// collects first components of sequences. |
|
266 |
def coll(r: Rexp, rs: List[Rexp]) : List[Rexp] = rs match { |
|
267 |
case Nil => Nil |
|
268 |
case SEQ(r1, r2) :: rs => |
|
269 |
if (r == r2) r1 :: coll(r, rs) else coll(r, rs) |
|
270 |
case r1 :: rs => coll(r, rs) |
|
271 |
} |
|
272 |
||
273 |
def bsimp_ASEQ1(bs: Bits, r1: ARexp, r2: ARexp) : ARexp = r1 match { |
|
274 |
case AZERO => AZERO |
|
275 |
case AONE(bs1) => fuse(bs ::: bs1, r2) |
|
276 |
case _ => ASEQ(bs, r1, r2) |
|
277 |
} |
|
278 |
||
279 |
def bsimp_AALTs(bs: Bits, rs: List[ARexp]) : ARexp = rs match { |
|
280 |
case Nil => AZERO |
|
281 |
case r::Nil => fuse(bs, r) |
|
282 |
case _ => AALTS(bs, rs) |
|
283 |
} |
|
284 |
||
285 |
def prune(r: ARexp, all: List[Rexp]) : ARexp = r match { |
|
286 |
case ASEQ(bs, r1, r2) => { |
|
287 |
val termsTruncated = coll(erase(r2), all) |
|
288 |
val pruned = prune(r1, termsTruncated) |
|
289 |
bsimp_ASEQ1(bs, pruned, r2) |
|
290 |
} |
|
291 |
case AALTS(bs, rs) => { |
|
292 |
val rsp = rs.map(prune(_, all)).filter(_ != AZERO) |
|
293 |
bsimp_AALTs(bs, rsp) |
|
294 |
} |
|
295 |
case r => |
|
296 |
if (all.contains(erase(r))) r else AZERO |
|
297 |
} |
|
298 |
||
299 |
def oneSimp(r: Rexp) : Rexp = r match { |
|
300 |
case SEQ(ONE, r) => r |
|
301 |
case SEQ(r1, r2) => SEQ(oneSimp(r1), r2) |
|
302 |
case r => r |
|
303 |
} |
|
304 |
||
305 |
def breakup(r: Rexp) : List[Rexp] = r match { |
|
306 |
case SEQ(r1, r2) => breakup(r1).map(SEQ(_, r2)) |
|
307 |
case ALT(r1, r2) => breakup(r1) ::: breakup(r2) |
|
308 |
case _ => r::Nil |
|
309 |
} |
|
310 |
||
311 |
def addToAcc(r: ARexp, acc: List[Rexp]) : List[Rexp] = |
|
312 |
breakup(erase(r)).filterNot(r => acc.contains(oneSimp(r))) |
|
313 |
||
314 |
def dBStrong(rs: List[ARexp], acc: List[Rexp]) : List[ARexp] = rs match { |
|
315 |
case Nil => Nil |
|
316 |
case r::rs => if (acc.contains(erase(r))) dBStrong(rs, acc) |
|
317 |
else prune(r, addToAcc(r, acc)) match { |
|
318 |
case AZERO => dBStrong(rs, addToAcc(r, acc) ::: acc) |
|
319 |
case r1 => r1 :: dBStrong(rs, addToAcc(r, acc) ::: acc) |
|
320 |
} |
|
321 |
} |
|
322 |
||
323 |
def bsimp_ASEQ(bs: Bits, r1: ARexp, r2: ARexp) : ARexp = (r1, r2) match { |
|
324 |
case (AZERO, _) => AZERO |
|
325 |
case (_, AZERO) => AZERO |
|
326 |
case (AONE(bs1), r2) => fuse(bs ::: bs1, r2) |
|
327 |
case _ => ASEQ(bs, r1, r2) |
|
328 |
} |
|
329 |
||
330 |
def bsimp2(r: ARexp): ARexp = r match { |
|
331 |
case ASEQ(bs1, r1, r2) => bsimp_ASEQ(bs1, bsimp2(r1), bsimp2(r2)) |
|
332 |
case AALTS(bs1, rs) => bsimp_AALTs(bs1, dBStrong(flts(rs.map(bsimp2(_))), Nil)) |
|
333 |
case r => r |
|
334 |
} |
|
335 |
||
336 |
def bders_simp2(r: ARexp, s: List[Char]) : ARexp = s match { |
|
337 |
case Nil => r |
|
338 |
case c::cs => bders_simp2(bsimp2(bder(c, r)), cs) |
|
339 |
} |
|
340 |
||
341 |
||
342 |
def blex_simp2(r: ARexp, s: List[Char]) : Bits = s match { |
|
343 |
case Nil => if (bnullable(r)) bmkeps(r) |
|
344 |
else throw new Exception("Not matched") |
|
345 |
case c::cs => blex_simp2(bsimp2(bder(c, r)), cs) |
|
346 |
} |
|
347 |
||
348 |
def blexing_simp2(r: Rexp, s: String) : Val = |
|
349 |
decode(r, blex_simp2(internalise(r), s.toList)) |
|
350 |
||
360 | 351 |
//println(blexing_simp(reg, "aab")) |
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
352 |
|
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
353 |
|
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
354 |
// extracts a string from value |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
355 |
def flatten(v: Val) : String = v match { |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
356 |
case Empty => "" |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
357 |
case Chr(c) => c.toString |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
358 |
case Left(v) => flatten(v) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
359 |
case Right(v) => flatten(v) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
360 |
case Sequ(v1, v2) => flatten(v1) + flatten(v2) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
361 |
case Stars(vs) => vs.map(flatten).mkString |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
362 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
363 |
|
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
364 |
// extracts an environment from a value |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
365 |
def env(v: Val) : List[(String, String)] = v match { |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
366 |
case Empty => Nil |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
367 |
case Chr(c) => Nil |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
368 |
case Left(v) => env(v) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
369 |
case Right(v) => env(v) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
370 |
case Sequ(v1, v2) => env(v1) ::: env(v2) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
371 |
case Stars(vs) => vs.flatMap(env) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
372 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
373 |
|
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
374 |
def nullable(r: Rexp) : Boolean = r match { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
375 |
case ZERO => false |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
376 |
case ONE => true |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
377 |
case CHAR(_) => false |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
378 |
case ALT(r1, r2) => nullable(r1) || nullable(r2) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
379 |
case SEQ(r1, r2) => nullable(r1) && nullable(r2) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
380 |
case STAR(_) => true |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
381 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
382 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
383 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
384 |
def pder(c: Char, r: Rexp) : Set[Rexp] = r match { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
385 |
case ZERO => Set() |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
386 |
case ONE => Set() |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
387 |
case CHAR(d) => if (c == d) Set(ONE) else Set() |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
388 |
case ALT(r1, r2) => pder(c, r1) ++ pder(c, r2) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
389 |
case SEQ(r1, r2) => { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
390 |
(for (pr1 <- pder(c, r1)) yield SEQ(pr1, r2)) ++ |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
391 |
(if (nullable(r1)) pder(c, r2) else Set()) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
392 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
393 |
case STAR(r1) => { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
394 |
for (pr1 <- pder(c, r1)) yield SEQ(pr1, STAR(r1)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
395 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
396 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
397 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
398 |
def pders(s: List[Char], rs: Set[Rexp]) : Set[Rexp] = s match { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
399 |
case Nil => rs |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
400 |
case c::s => pders(s, rs.flatMap(pder(c, _))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
401 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
402 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
403 |
def size(r: Rexp): Int = r match { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
404 |
case ZERO => 1 |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
405 |
case ONE => 1 |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
406 |
case CHAR(_) => 1 |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
407 |
case ALT(r1, r2) => 1 + size(r1) + size (r2) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
408 |
case SEQ(r1, r2) => 1 + size(r1) + size (r2) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
409 |
case STAR(r1) => 1 + size(r1) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
410 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
411 |
|
436 | 412 |
def asize(r: ARexp) : Int = size(erase(r)) |
413 |
def psize(rs: Set[Rexp]) : Int = rs.map(size(_)).sum |
|
414 |
||
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
415 |
def pp(r: ARexp): String = r match { |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
416 |
case ASEQ(_, ACHAR(_, a1),ASEQ(_, r1, r2)) => s"${a1}${pp(r1)}${pp(r2)}" |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
417 |
case ASEQ(_, ACHAR(_, a1),ACHAR(_, a2)) => s"${a1}${a2}" |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
418 |
case AZERO => "0" |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
419 |
case AONE(_) => "1" |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
420 |
case ACHAR(_, a) => a.toString |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
421 |
case AALTS(_, rs) => s"ALTs(${rs.map(pp(_)).mkString(",")})" |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
422 |
case ASEQ(_, r1, r2) => s"SEQ(${pp(r1)}, ${pp(r2)})" |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
423 |
case ASTAR(_, r1) => s"(${pp(r1)})*" |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
424 |
} |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
425 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
426 |
|
436 | 427 |
val TEST = STAR("a" | "aa") |
428 |
println(asize(bders(("a" * 0).toList, internalise(TEST)))) |
|
429 |
println(asize(bders(("a" * 1).toList, internalise(TEST)))) |
|
430 |
println(asize(bders(("a" * 2).toList, internalise(TEST)))) |
|
431 |
println(asize(bders(("a" * 3).toList, internalise(TEST)))) |
|
432 |
println(asize(bders(("a" * 4).toList, internalise(TEST)))) |
|
433 |
||
434 |
println(asize(bders_simp(internalise(TEST), ("a" * 0).toList))) |
|
435 |
println(asize(bders_simp(internalise(TEST), ("a" * 1).toList))) |
|
436 |
println(asize(bders_simp(internalise(TEST), ("a" * 2).toList))) |
|
437 |
println(asize(bders_simp(internalise(TEST), ("a" * 3).toList))) |
|
438 |
println(asize(bders_simp(internalise(TEST), ("a" * 4).toList))) |
|
439 |
||
440 |
||
441 |
println(asize(bders_simp2(internalise(TEST), ("a" * 0).toList))) |
|
442 |
println(asize(bders_simp2(internalise(TEST), ("a" * 1).toList))) |
|
443 |
println(asize(bders_simp2(internalise(TEST), ("a" * 2).toList))) |
|
444 |
println(asize(bders_simp2(internalise(TEST), ("a" * 3).toList))) |
|
445 |
println(asize(bders_simp2(internalise(TEST), ("a" * 4).toList))) |
|
446 |
println(asize(bders_simp2(internalise(TEST), ("a" * 5).toList))) |
|
447 |
||
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
448 |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
449 |
// Some Tests |
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
450 |
//============ |
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
451 |
val ST = STAR(STAR("a")) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
452 |
println(pp(internalise(ST))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
453 |
println(bders(("a" * 1).toList, internalise(ST))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
454 |
println(bders_simp(internalise(ST), ("a" * 1).toList)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
455 |
println(pp(bders(("a" * 1).toList, internalise(ST)))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
456 |
println(pp(bders_simp(internalise(ST), ("a" * 1).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
457 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
458 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
459 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
460 |
println(pp(bders_simp(internalise(ST), ("a" * 1).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
461 |
println(pp(bders_simp(internalise(ST), ("a" * 2).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
462 |
println(pp(bders_simp(internalise(ST), ("a" * 3).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
463 |
println(pp(bders_simp(internalise(ST), ("a" * 4).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
464 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
465 |
println(blexing(ST, "a" * 1)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
466 |
println(blexing_simp(ST, "a" * 1)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
467 |
println(blexing(ST, "a" * 2)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
468 |
println(blexing_simp(ST, "a" * 2)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
469 |
println(blexing(ST, "a" * 3)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
470 |
println(blexing_simp(ST, "a" * 3)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
471 |
println(blexing(ST, "a" * 4)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
472 |
println(blexing_simp(ST, "a" * 4)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
473 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
474 |
val STARREG = ((STAR("a") | STAR("aaa")) | STAR("aaaaa")).% |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
475 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
476 |
println(blexing(STARREG, "a" * 3)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
477 |
println(blexing_simp(STARREG, "a" * 3)) |
436 | 478 |
println(pders(List(STARREG), "a" * 3)) |
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
479 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
480 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
481 |
size(STARREG) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
482 |
size(erase(bders_simp(internalise(STARREG), ("a" * 1).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
483 |
size(erase(bders_simp(internalise(STARREG), ("a" * 2).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
484 |
size(erase(bders_simp(internalise(STARREG), ("a" * 3).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
485 |
size(erase(bders_simp(internalise(STARREG), ("a" * 4).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
486 |
size(erase(bders_simp(internalise(STARREG), ("a" * 5).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
487 |
size(erase(bders_simp(internalise(STARREG), ("a" * 6).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
488 |
size(erase(bders_simp(internalise(STARREG), ("a" * 7).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
489 |
size(erase(bders_simp(internalise(STARREG), ("a" * 8).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
490 |
size(erase(bders_simp(internalise(STARREG), ("a" * 9).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
491 |
size(erase(bders_simp(internalise(STARREG), ("a" * 100).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
492 |
size(erase(bders_simp(internalise(STARREG), ("a" * 101).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
493 |
size(erase(bders_simp(internalise(STARREG), ("a" * 102).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
494 |
size(erase(bders_simp(internalise(STARREG), ("a" * 103).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
495 |
|
436 | 496 |
size(erase(bders_simp2(internalise(STARREG), ("a" * 103).toList))) |
497 |
psize(pders(("a" * 103).toList, Set(STARREG))) |
|
498 |
||
416
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
499 |
println(bders_simp(internalise(STARREG), ("a" * 1).toList)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
500 |
println(bders_simp(internalise(STARREG), ("a" * 2).toList)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
501 |
println(bders_simp(internalise(STARREG), ("a" * 3).toList)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
502 |
println(bders_simp(internalise(STARREG), ("a" * 4).toList)) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
503 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
504 |
println(erase(bders_simp(internalise(STARREG), ("a" * 1).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
505 |
println(erase(bders_simp(internalise(STARREG), ("a" * 2).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
506 |
println(erase(bders_simp(internalise(STARREG), ("a" * 3).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
507 |
println(erase(bders_simp(internalise(STARREG), ("a" * 4).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
508 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
509 |
println(pp(internalise(STARREG))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
510 |
println(pp(bders_simp(internalise(STARREG), ("a" * 1).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
511 |
println(pp(bders_simp(internalise(STARREG), ("a" * 2).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
512 |
println(pp(bders_simp(internalise(STARREG), ("a" * 3).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
513 |
println(pp(bders_simp(internalise(STARREG), ("a" * 4).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
514 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
515 |
val STARR = (STAR("a") | STAR("aa") | |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
516 |
STAR("aaa") | STAR("aaaa") | |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
517 |
STAR("aaaaa") | STAR("aaaaaa") | |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
518 |
STAR("aaaaaaa") | STAR("aaaaaaaa")).% |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
519 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
520 |
size(STARR) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
521 |
size(erase(bders_simp(internalise(STARR), ("a" * 1).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
522 |
size(erase(bders_simp(internalise(STARR), ("a" * 2).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
523 |
size(erase(bders_simp(internalise(STARR), ("a" * 3).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
524 |
size(erase(bders_simp(internalise(STARR), ("a" * 4).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
525 |
size(erase(bders_simp(internalise(STARR), ("a" * 5).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
526 |
size(erase(bders_simp(internalise(STARR), ("a" * 6).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
527 |
size(erase(bders_simp(internalise(STARR), ("a" * 7).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
528 |
size(erase(bders_simp(internalise(STARR), ("a" * 8).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
529 |
size(erase(bders_simp(internalise(STARR), ("a" * 9).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
530 |
size(erase(bders_simp(internalise(STARR), ("a" * 1000).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
531 |
size(erase(bders_simp(internalise(STARR), ("a" * 1001).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
532 |
size(erase(bders_simp(internalise(STARR), ("a" * 1002).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
533 |
size(erase(bders_simp(internalise(STARR), ("a" * 1010).toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
534 |
size(erase(bders_simp(internalise(STARR), ("a" * 1010 ++ "b").toList))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
535 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
536 |
val r0 = ("a" | "ab") ~ ("b" | "") |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
537 |
println(pre_blexing(internalise(r0), "ab")) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
538 |
println(blexing(r0, "ab")) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
539 |
println(blexing_simp(r0, "ab")) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
540 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
541 |
println(pders("a".toList, Set(r0))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
542 |
println(pders("ab".toList, Set(r0))) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
543 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
544 |
val r00 = ("a" ~ ("b" | "")) | ("ab" ~ ("b" | "")) |
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
545 |
|
57182b36ec01
more with the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
360
diff
changeset
|
546 |
|
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
547 |
|
359 | 548 |
/* |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
549 |
def time_needed[T](i: Int, code: => T) = { |
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
550 |
val start = System.nanoTime() |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
551 |
for (j <- 1 to i) code |
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
552 |
val end = System.nanoTime() |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
553 |
(end - start)/(i * 1.0e9) |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
554 |
} |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
555 |
|
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
556 |
|
359 | 557 |
val evil1 = (("a").%) ~ "b" |
558 |
val evil2 = (((("a").%).%).%) ~ "b" |
|
559 |
val evil3 = (("a"~"a") | ("a")).% |
|
560 |
||
561 |
for(i <- 1 to 10000 by 1000) { |
|
562 |
println(time_needed(1, blex_simp(internalise(evil1), ("a"*i + "b").toList))) |
|
563 |
} |
|
564 |
||
565 |
for(i <- 1 to 10000 by 1000) { |
|
566 |
println(time_needed(1, blexing_simp(evil1, "a"*i + "b"))) |
|
567 |
} |
|
568 |
||
569 |
for(i <- 1 to 10000 by 1000) { |
|
570 |
println(time_needed(1, blexing_simp(evil2, "a"*i + "b"))) |
|
571 |
} |
|
572 |
||
573 |
for(i <- 1 to 10000 by 1000) { |
|
574 |
println(time_needed(1, blexing_simp(evil3, "a"*i))) |
|
575 |
} |
|
576 |
*/ |
|
577 |
||
578 |
||
579 |
||
580 |
||
581 |
||
582 |
///////////////////////// |
|
583 |
///////////////////////// |
|
584 |
///// Below not relevant |
|
585 |
||
586 |
/* |
|
204
cd9e40280784
added paper about size derivatives
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
159
diff
changeset
|
587 |
val rf = ("a" | "ab") ~ ("ab" | "") |
359 | 588 |
println(pre_blexing(internalise(rf), "ab")) |
589 |
println(blexing(rf, "ab")) |
|
590 |
println(blexing_simp(rf, "ab")) |
|
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
591 |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
592 |
val r0 = ("a" | "ab") ~ ("b" | "") |
359 | 593 |
println(pre_blexing(internalise(r0), "ab")) |
594 |
println(blexing(r0, "ab")) |
|
595 |
println(blexing_simp(r0, "ab")) |
|
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
596 |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
597 |
val r1 = ("a" | "ab") ~ ("bcd" | "cd") |
359 | 598 |
println(blexing(r1, "abcd")) |
599 |
println(blexing_simp(r1, "abcd")) |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
600 |
|
359 | 601 |
println(blexing((("" | "a") ~ ("ab" | "b")), "ab")) |
602 |
println(blexing_simp((("" | "a") ~ ("ab" | "b")), "ab")) |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
603 |
|
359 | 604 |
println(blexing((("" | "a") ~ ("b" | "ab")), "ab")) |
605 |
println(blexing_simp((("" | "a") ~ ("b" | "ab")), "ab")) |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
606 |
|
359 | 607 |
println(blexing((("" | "a") ~ ("c" | "ab")), "ab")) |
608 |
println(blexing_simp((("" | "a") ~ ("c" | "ab")), "ab")) |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
609 |
|
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
610 |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
611 |
// Sulzmann's tests |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
612 |
//================== |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
613 |
|
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
614 |
val sulzmann = ("a" | "b" | "ab").% |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
615 |
|
359 | 616 |
println(blexing(sulzmann, "a" * 10)) |
617 |
println(blexing_simp(sulzmann, "a" * 10)) |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
618 |
|
359 | 619 |
for (i <- 0 to 4000 by 500) { |
620 |
println(i + ": " + "%.5f".format(time_needed(1, blexing_simp(sulzmann, "a" * i)))) |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
621 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
622 |
|
359 | 623 |
for (i <- 0 to 15 by 5) { |
624 |
println(i + ": " + "%.5f".format(time_needed(1, blexing_simp(sulzmann, "ab" * i)))) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
625 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
626 |
|
359 | 627 |
*/ |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
628 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
629 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
630 |
// some automatic testing |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
631 |
|
359 | 632 |
/* |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
633 |
def clear() = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
634 |
print("") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
635 |
//print("\33[H\33[2J") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
636 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
637 |
|
359 | 638 |
def merge[A](l1: LazyList[A], l2: LazyList[A], l3: LazyList[A]) : LazyList[A] = |
639 |
l1.head #:: l2.head #:: l3.head #:: merge(l1.tail, l2.tail, l3.tail) |
|
640 |
||
641 |
||
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
642 |
// enumerates regular expressions until a certain depth |
359 | 643 |
def enum(rs: LazyList[Rexp]) : LazyList[Rexp] = { |
644 |
rs #::: enum( (for (r1 <- rs; r2 <- rs) yield ALT(r1, r2)) ++ |
|
645 |
(for (r1 <- rs; r2 <- rs) yield SEQ(r1, r2)) ++ |
|
646 |
(for (r1 <- rs) yield STAR(r1))) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
647 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
648 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
649 |
|
359 | 650 |
enum(LazyList(ZERO, ONE, CHAR('a'), CHAR('b'))).take(200).force.mkString("\n") |
651 |
enum(LazyList(ZERO, ONE, CHAR('a'), CHAR('b'))).take(200_000).force |
|
652 |
||
653 |
||
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
654 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
655 |
import scala.util.Try |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
656 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
657 |
def test_mkeps(r: Rexp) = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
658 |
val res1 = Try(Some(mkeps(r))).getOrElse(None) |
359 | 659 |
val res2 = Try(Some(decode(r, bmkeps(internalise(r))))).getOrElse(None) |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
660 |
if (res1 != res2) println(s"Mkeps disagrees on ${r}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
661 |
if (res1 != res2) Some(r) else (None) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
662 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
663 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
664 |
println("Testing mkeps") |
359 | 665 |
enum(LazyList(ZERO, ONE, CHAR('a'), CHAR('b'))).take(100).exists(test_mkeps(_).isDefined) |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
666 |
//enum(3, "ab").map(test_mkeps).toSet |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
667 |
//enum(3, "abc").map(test_mkeps).toSet |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
668 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
669 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
670 |
//enumerates strings of length n over alphabet cs |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
671 |
def strs(n: Int, cs: String) : Set[String] = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
672 |
if (n == 0) Set("") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
673 |
else { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
674 |
val ss = strs(n - 1, cs) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
675 |
ss ++ |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
676 |
(for (s <- ss; c <- cs.toList) yield c + s) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
677 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
678 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
679 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
680 |
//tests lexing and lexingB |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
681 |
def tests_inj(ss: Set[String])(r: Rexp) = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
682 |
clear() |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
683 |
println(s"Testing ${r}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
684 |
for (s <- ss.par) yield { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
685 |
val res1 = Try(Some(alexing(r, s))).getOrElse(None) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
686 |
val res2 = Try(Some(alexing_simp(r, s))).getOrElse(None) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
687 |
if (res1 != res2) println(s"Disagree on ${r} and ${s}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
688 |
if (res1 != res2) println(s" ${res1} != ${res2}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
689 |
if (res1 != res2) Some((r, s)) else None |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
690 |
} |
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
691 |
} |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
692 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
693 |
//println("Testing lexing 1") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
694 |
//enum(2, "ab").map(tests_inj(strs(2, "ab"))).toSet |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
695 |
//println("Testing lexing 2") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
696 |
//enum(2, "ab").map(tests_inj(strs(3, "abc"))).toSet |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
697 |
//println("Testing lexing 3") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
698 |
//enum(3, "ab").map(tests_inj(strs(3, "abc"))).toSet |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
699 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
700 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
701 |
def tests_alexer(ss: Set[String])(r: Rexp) = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
702 |
clear() |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
703 |
println(s"Testing ${r}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
704 |
for (s <- ss.par) yield { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
705 |
val d = der('b', r) |
359 | 706 |
val ad = bder('b', internalise(r)) |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
707 |
val res1 = Try(Some(encode(inj(r, 'a', alexing(d, s))))).getOrElse(None) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
708 |
val res2 = Try(Some(pre_alexing(ad, s))).getOrElse(None) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
709 |
if (res1 != res2) println(s"Disagree on ${r} and 'a'::${s}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
710 |
if (res1 != res2) println(s" ${res1} != ${res2}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
711 |
if (res1 != res2) Some((r, s)) else None |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
712 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
713 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
714 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
715 |
println("Testing alexing 1") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
716 |
println(enum(2, "ab").map(tests_alexer(strs(2, "ab"))).toSet) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
717 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
718 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
719 |
def values(r: Rexp) : Set[Val] = r match { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
720 |
case ZERO => Set() |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
721 |
case ONE => Set(Empty) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
722 |
case CHAR(c) => Set(Chr(c)) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
723 |
case ALT(r1, r2) => (for (v1 <- values(r1)) yield Left(v1)) ++ |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
724 |
(for (v2 <- values(r2)) yield Right(v2)) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
725 |
case SEQ(r1, r2) => for (v1 <- values(r1); v2 <- values(r2)) yield Sequ(v1, v2) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
726 |
case STAR(r) => (Set(Stars(Nil)) ++ |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
727 |
(for (v <- values(r)) yield Stars(List(v)))) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
728 |
// to do more would cause the set to be infinite |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
729 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
730 |
|
359 | 731 |
def tests_bder(c: Char)(r: Rexp) = { |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
732 |
val d = der(c, r) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
733 |
val vals = values(d) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
734 |
for (v <- vals) { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
735 |
println(s"Testing ${r} and ${v}") |
359 | 736 |
val res1 = retrieve(bder(c, internalise(r)), v) |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
737 |
val res2 = encode(inj(r, c, decode(d, retrieve(internalise(der(c, r)), v)))) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
738 |
if (res1 != res2) println(s"Disagree on ${r}, ${v} and der = ${d}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
739 |
if (res1 != res2) println(s" ${res1} != ${res2}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
740 |
if (res1 != res2) Some((r, v)) else None |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
741 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
742 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
743 |
|
359 | 744 |
println("Testing bder/der") |
745 |
println(enum(2, "ab").map(tests_bder('a')).toSet) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
746 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
747 |
val er = SEQ(ONE,CHAR('a')) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
748 |
val ev = Right(Empty) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
749 |
val ed = ALT(SEQ(ZERO,CHAR('a')),ONE) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
750 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
751 |
retrieve(internalise(ed), ev) // => [true] |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
752 |
internalise(er) |
359 | 753 |
bder('a', internalise(er)) |
754 |
retrieve(bder('a', internalise(er)), ev) // => [] |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
755 |
decode(ed, List(true)) // gives the value for derivative |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
756 |
decode(er, List()) // gives the value for original value |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
757 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
758 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
759 |
val dr = STAR(CHAR('a')) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
760 |
val dr_der = SEQ(ONE,STAR(CHAR('a'))) // derivative of dr |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
761 |
val dr_val = Sequ(Empty,Stars(List())) // value of dr_def |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
762 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
763 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
764 |
val res1 = retrieve(internalise(der('a', dr)), dr_val) // => [true] |
359 | 765 |
val res2 = retrieve(bder('a', internalise(dr)), dr_val) // => [false, true] |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
766 |
decode(dr_der, res1) // gives the value for derivative |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
767 |
decode(dr, res2) // gives the value for original value |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
768 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
769 |
encode(inj(dr, 'a', decode(dr_der, res1))) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
770 |
|
359 | 771 |
*/ |
436 | 772 |
|
773 |
||
774 |
||
775 |
||
776 |
||
777 |
||
778 |
||
779 |
/* |
|
780 |
def star(n: Long) = if ((n & 1L) == 1L) "*" else " " |
|
781 |
def stars(n: Long): String = if (n == 0L) "" else star(n) + " " + stars(n >> 1) |
|
782 |
def spaces(n: Int) = " " * n |
|
783 |
||
784 |
||
785 |
def sierpinski(n: Int) { |
|
786 |
((1 << n) - 1 to 0 by -1).foldLeft(1L) { |
|
787 |
case (bitmap, remainingLines) => |
|
788 |
println(spaces(remainingLines) + stars(bitmap)) |
|
789 |
(bitmap << 1) ^ bitmap |
|
790 |
} |
|
791 |
} |
|
792 |
||
793 |
*/ |