author | Christian Urban <christian.urban@kcl.ac.uk> |
Mon, 22 Feb 2021 03:22:26 +0000 | |
changeset 360 | e752d84225ec |
parent 359 | fedc16924b76 |
child 416 | 57182b36ec01 |
permissions | -rw-r--r-- |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
import scala.language.implicitConversions |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
import scala.language.reflectiveCalls |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
3 |
import scala.annotation.tailrec |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
|
360 | 5 |
// standard regular expressions |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
6 |
abstract class Rexp |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
7 |
case object ZERO extends Rexp |
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
8 |
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
|
9 |
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
|
10 |
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
|
11 |
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
|
12 |
case class STAR(r: Rexp) extends Rexp |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
13 |
|
359 | 14 |
abstract class Bit |
15 |
case object Z extends Bit |
|
16 |
case object S extends Bit |
|
17 |
||
18 |
type Bits = List[Bit] |
|
19 |
||
360 | 20 |
// annotated regular expressions |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
21 |
abstract class ARexp |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
22 |
case object AZERO extends ARexp |
359 | 23 |
case class AONE(bs: Bits) extends ARexp |
24 |
case class ACHAR(bs: Bits, c: Char) extends ARexp |
|
25 |
case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp |
|
26 |
case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp |
|
27 |
case class ASTAR(bs: Bits, r: ARexp) extends ARexp |
|
28 |
||
360 | 29 |
// an abbreviation for binary alternatives |
359 | 30 |
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
|
31 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
32 |
abstract class Val |
156
6a43ea9305ba
updated implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
81
diff
changeset
|
33 |
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
|
34 |
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
|
35 |
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
|
36 |
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
|
37 |
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
|
38 |
case class Stars(vs: List[Val]) extends Val |
360 | 39 |
|
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
// some convenience for typing in regular expressions |
359 | 42 |
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
|
43 |
case Nil => ONE |
3
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
44 |
case c::Nil => CHAR(c) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
45 |
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
|
46 |
} |
359 | 47 |
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
|
48 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
49 |
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
|
50 |
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
|
51 |
def % = STAR(r) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
52 |
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
|
53 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
54 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
def % = STAR(s) |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
59 |
def ~ (r: Rexp) = SEQ(s, r) |
81
7ac7782a7318
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
78
diff
changeset
|
60 |
def ~ (r: String) = SEQ(s, r) |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
61 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
62 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
63 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
64 |
// Bitcoded + Annotation |
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 |
|
360 | 67 |
//erase function: extracts the Rexp from ARexp |
359 | 68 |
def erase(r:ARexp): Rexp = r match{ |
69 |
case AZERO => ZERO |
|
70 |
case AONE(_) => ONE |
|
71 |
case ACHAR(bs, c) => CHAR(c) |
|
72 |
case AALTS(bs, Nil) => ZERO |
|
73 |
case AALTS(bs, r::Nil) => erase(r) |
|
74 |
case AALTS(bs, r::rs) => ALT(erase(r), erase(AALTS(bs, rs))) |
|
75 |
case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2)) |
|
76 |
case ASTAR(cs, r)=> STAR(erase(r)) |
|
77 |
} |
|
78 |
||
79 |
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
|
80 |
case AZERO => AZERO |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
81 |
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
|
82 |
case ACHAR(cs, c) => ACHAR(bs ++ cs, c) |
359 | 83 |
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
|
84 |
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
|
85 |
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
|
86 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
87 |
|
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
88 |
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
|
89 |
case ZERO => AZERO |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
90 |
case ONE => AONE(Nil) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
91 |
case CHAR(c) => ACHAR(Nil, c) |
359 | 92 |
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
|
93 |
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
|
94 |
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
|
95 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
96 |
|
294 | 97 |
|
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
98 |
internalise(("a" | "ab") ~ ("b" | "")) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
99 |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
100 |
|
360 | 101 |
// decoding of a value from a bitsequence |
359 | 102 |
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
|
103 |
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
|
104 |
case (CHAR(c), bs) => (Chr(c), bs) |
359 | 105 |
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
|
106 |
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
|
107 |
(Left(v), bs1) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
108 |
} |
359 | 109 |
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
|
110 |
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
|
111 |
(Right(v), bs1) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
112 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
113 |
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
|
114 |
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
|
115 |
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
|
116 |
(Sequ(v1, v2), bs2) |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
117 |
} |
359 | 118 |
case (STAR(r1), Z::bs) => { |
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
119 |
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
|
120 |
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
|
121 |
(Stars(v::vs), 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(_), 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
|
124 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
125 |
|
359 | 126 |
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
|
127 |
case (v, Nil) => v |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
128 |
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
|
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 encode(v: Val) : Bits = v match { |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
132 |
case Empty => Nil |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
133 |
case Chr(c) => Nil |
359 | 134 |
case Left(v) => Z :: encode(v) |
135 |
case Right(v) => S :: encode(v) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
136 |
case Sequ(v1, v2) => encode(v1) ::: encode(v2) |
359 | 137 |
case Stars(Nil) => List(S) |
138 |
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
|
139 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
140 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
141 |
|
360 | 142 |
// nullable function: tests whether the an (annotated) |
143 |
// regular expression can recognise the empty string |
|
359 | 144 |
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
|
145 |
case AZERO => false |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
146 |
case AONE(_) => true |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
147 |
case ACHAR(_,_) => false |
359 | 148 |
case AALTS(_, rs) => rs.exists(bnullable) |
149 |
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
|
150 |
case ASTAR(_, _) => true |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
151 |
} |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
152 |
|
359 | 153 |
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
|
154 |
case AONE(bs) => bs |
359 | 155 |
case AALTS(bs, r::Nil) => bs ++ bmkeps(r) |
156 |
case AALTS(bs, r::rs) => |
|
157 |
if (bnullable(r)) bs ++ bmkeps(r) else bmkeps(AALTS(bs, rs)) |
|
158 |
case ASEQ(bs, r1, r2) => bs ++ bmkeps(r1) ++ bmkeps(r2) |
|
159 |
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
|
160 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
161 |
|
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
162 |
// derivative of a regular expression w.r.t. a character |
359 | 163 |
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
|
164 |
case AZERO => AZERO |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
165 |
case AONE(_) => AZERO |
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
166 |
case ACHAR(bs, d) => if (c == d) AONE(bs) else AZERO |
359 | 167 |
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
|
168 |
case ASEQ(bs, r1, r2) => |
359 | 169 |
if (bnullable(r1)) AALT(bs, ASEQ(Nil, bder(c, r1), r2), fuse(bmkeps(r1), bder(c, r2))) |
170 |
else ASEQ(bs, bder(c, r1), r2) |
|
171 |
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
|
172 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
173 |
|
360 | 174 |
// 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
|
175 |
@tailrec |
359 | 176 |
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
|
177 |
case Nil => r |
359 | 178 |
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
|
179 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
180 |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
181 |
// main unsimplified lexing function (produces a value) |
359 | 182 |
def blex(r: ARexp, s: List[Char]) : Bits = s match { |
183 |
case Nil => if (bnullable(r)) bmkeps(r) else throw new Exception("Not matched") |
|
184 |
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
|
185 |
} |
94824659f6d7
added all toy implementations
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
186 |
|
359 | 187 |
def pre_blexing(r: ARexp, s: String) : Bits = blex(r, s.toList) |
188 |
def blexing(r: Rexp, s: String) : Val = decode(r, pre_blexing(internalise(r), s)) |
|
189 |
||
190 |
||
191 |
// example by Tudor |
|
360 | 192 |
//val reg = ((("a".%)) ~ ("b" | "c")).% |
359 | 193 |
|
360 | 194 |
//println(blexing(reg, "aab")) |
359 | 195 |
|
196 |
||
197 |
//======================= |
|
198 |
// simplification |
|
199 |
// |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
200 |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
201 |
|
359 | 202 |
def flts(rs: List[ARexp]) : List[ARexp] = rs match { |
203 |
case Nil => Nil |
|
204 |
case AZERO :: rs => flts(rs) |
|
205 |
case AALTS(bs, rs1) :: rs => rs1.map(fuse(bs, _)) ++ flts(rs) |
|
206 |
case r1 :: rs => r1 :: flts(rs) |
|
207 |
} |
|
208 |
||
209 |
def distinctBy[B, C](xs: List[B], |
|
210 |
f: B => C, |
|
211 |
acc: List[C] = Nil): List[B] = xs match { |
|
212 |
case Nil => Nil |
|
213 |
case x::xs => { |
|
214 |
val res = f(x) |
|
215 |
if (acc.contains(res)) distinctBy(xs, f, acc) |
|
216 |
else x::distinctBy(xs, f, res::acc) |
|
217 |
} |
|
218 |
} |
|
219 |
||
220 |
||
221 |
def bsimp(r: ARexp): ARexp = r match { |
|
222 |
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
|
223 |
case (AZERO, _) => AZERO |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
224 |
case (_, AZERO) => AZERO |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
225 |
case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) |
359 | 226 |
//case (AALTS(bs, rs), r2) => AALTS(bs, rs.map(ASEQ(Nil, _, r2))) |
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
227 |
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
|
228 |
} |
360 | 229 |
case AALTS(bs1, rs) => (flts(rs.map(bsimp))).distinctBy(erase) match { |
359 | 230 |
case Nil => AZERO |
231 |
case r::Nil => fuse(bs1, r) |
|
232 |
case rs => AALTS(bs1, rs) |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
233 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
234 |
case r => r |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
235 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
236 |
|
359 | 237 |
def blex_simp(r: ARexp, s: List[Char]) : Bits = s match { |
238 |
case Nil => if (bnullable(r)) bmkeps(r) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
239 |
else throw new Exception("Not matched") |
359 | 240 |
case c::cs => blex(bsimp(bder(c, r)), cs) |
241 |
} |
|
242 |
||
243 |
def blexing_simp(r: Rexp, s: String) : Val = |
|
244 |
decode(r, blex_simp(internalise(r), s.toList)) |
|
245 |
||
360 | 246 |
//println(blexing_simp(reg, "aab")) |
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
247 |
|
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
248 |
|
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
249 |
// extracts a string from value |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
250 |
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
|
251 |
case Empty => "" |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
252 |
case Chr(c) => c.toString |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
253 |
case Left(v) => flatten(v) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
254 |
case Right(v) => flatten(v) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
255 |
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
|
256 |
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
|
257 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
258 |
|
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
259 |
// extracts an environment from a value |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
260 |
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
|
261 |
case Empty => Nil |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
262 |
case Chr(c) => Nil |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
263 |
case Left(v) => env(v) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
264 |
case Right(v) => env(v) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
265 |
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
|
266 |
case Stars(vs) => vs.flatMap(env) |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
267 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
268 |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
269 |
// Some Tests |
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
270 |
//============ |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
271 |
|
359 | 272 |
/* |
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
273 |
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
|
274 |
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
|
275 |
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
|
276 |
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
|
277 |
(end - start)/(i * 1.0e9) |
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
278 |
} |
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
279 |
|
158
4e00dd2398ac
added bit-coded version
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
157
diff
changeset
|
280 |
|
359 | 281 |
val evil1 = (("a").%) ~ "b" |
282 |
val evil2 = (((("a").%).%).%) ~ "b" |
|
283 |
val evil3 = (("a"~"a") | ("a")).% |
|
284 |
||
285 |
for(i <- 1 to 10000 by 1000) { |
|
286 |
println(time_needed(1, blex_simp(internalise(evil1), ("a"*i + "b").toList))) |
|
287 |
} |
|
288 |
||
289 |
for(i <- 1 to 10000 by 1000) { |
|
290 |
println(time_needed(1, blexing_simp(evil1, "a"*i + "b"))) |
|
291 |
} |
|
292 |
||
293 |
for(i <- 1 to 10000 by 1000) { |
|
294 |
println(time_needed(1, blexing_simp(evil2, "a"*i + "b"))) |
|
295 |
} |
|
296 |
||
297 |
for(i <- 1 to 10000 by 1000) { |
|
298 |
println(time_needed(1, blexing_simp(evil3, "a"*i))) |
|
299 |
} |
|
300 |
*/ |
|
301 |
||
302 |
||
303 |
||
304 |
||
305 |
||
306 |
///////////////////////// |
|
307 |
///////////////////////// |
|
308 |
///// Below not relevant |
|
309 |
||
310 |
/* |
|
204
cd9e40280784
added paper about size derivatives
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
159
diff
changeset
|
311 |
val rf = ("a" | "ab") ~ ("ab" | "") |
359 | 312 |
println(pre_blexing(internalise(rf), "ab")) |
313 |
println(blexing(rf, "ab")) |
|
314 |
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
|
315 |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
316 |
val r0 = ("a" | "ab") ~ ("b" | "") |
359 | 317 |
println(pre_blexing(internalise(r0), "ab")) |
318 |
println(blexing(r0, "ab")) |
|
319 |
println(blexing_simp(r0, "ab")) |
|
75
f95a405c3180
updated
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
74
diff
changeset
|
320 |
|
157
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
321 |
val r1 = ("a" | "ab") ~ ("bcd" | "cd") |
359 | 322 |
println(blexing(r1, "abcd")) |
323 |
println(blexing_simp(r1, "abcd")) |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
324 |
|
359 | 325 |
println(blexing((("" | "a") ~ ("ab" | "b")), "ab")) |
326 |
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
|
327 |
|
359 | 328 |
println(blexing((("" | "a") ~ ("b" | "ab")), "ab")) |
329 |
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
|
330 |
|
359 | 331 |
println(blexing((("" | "a") ~ ("c" | "ab")), "ab")) |
332 |
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
|
333 |
|
1fe44fb6d0a4
cleaned up scala code
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
156
diff
changeset
|
334 |
|
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
335 |
// Sulzmann's tests |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
336 |
//================== |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
337 |
|
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
338 |
val sulzmann = ("a" | "b" | "ab").% |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
339 |
|
359 | 340 |
println(blexing(sulzmann, "a" * 10)) |
341 |
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
|
342 |
|
359 | 343 |
for (i <- 0 to 4000 by 500) { |
344 |
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
|
345 |
} |
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
346 |
|
359 | 347 |
for (i <- 0 to 15 by 5) { |
348 |
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
|
349 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
350 |
|
359 | 351 |
*/ |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
352 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
353 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
354 |
// some automatic testing |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
355 |
|
359 | 356 |
/* |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
357 |
def clear() = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
358 |
print("") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
359 |
//print("\33[H\33[2J") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
360 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
361 |
|
359 | 362 |
def merge[A](l1: LazyList[A], l2: LazyList[A], l3: LazyList[A]) : LazyList[A] = |
363 |
l1.head #:: l2.head #:: l3.head #:: merge(l1.tail, l2.tail, l3.tail) |
|
364 |
||
365 |
||
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
366 |
// enumerates regular expressions until a certain depth |
359 | 367 |
def enum(rs: LazyList[Rexp]) : LazyList[Rexp] = { |
368 |
rs #::: enum( (for (r1 <- rs; r2 <- rs) yield ALT(r1, r2)) ++ |
|
369 |
(for (r1 <- rs; r2 <- rs) yield SEQ(r1, r2)) ++ |
|
370 |
(for (r1 <- rs) yield STAR(r1))) |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
371 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
372 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
373 |
|
359 | 374 |
enum(LazyList(ZERO, ONE, CHAR('a'), CHAR('b'))).take(200).force.mkString("\n") |
375 |
enum(LazyList(ZERO, ONE, CHAR('a'), CHAR('b'))).take(200_000).force |
|
376 |
||
377 |
||
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
378 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
379 |
import scala.util.Try |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
380 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
381 |
def test_mkeps(r: Rexp) = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
382 |
val res1 = Try(Some(mkeps(r))).getOrElse(None) |
359 | 383 |
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
|
384 |
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
|
385 |
if (res1 != res2) Some(r) else (None) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
386 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
387 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
388 |
println("Testing mkeps") |
359 | 389 |
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
|
390 |
//enum(3, "ab").map(test_mkeps).toSet |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
391 |
//enum(3, "abc").map(test_mkeps).toSet |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
392 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
393 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
394 |
//enumerates strings of length n over alphabet cs |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
395 |
def strs(n: Int, cs: String) : Set[String] = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
396 |
if (n == 0) Set("") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
397 |
else { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
398 |
val ss = strs(n - 1, cs) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
399 |
ss ++ |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
400 |
(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
|
401 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
402 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
403 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
404 |
//tests lexing and lexingB |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
405 |
def tests_inj(ss: Set[String])(r: Rexp) = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
406 |
clear() |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
407 |
println(s"Testing ${r}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
408 |
for (s <- ss.par) yield { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
409 |
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
|
410 |
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
|
411 |
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
|
412 |
if (res1 != res2) println(s" ${res1} != ${res2}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
413 |
if (res1 != res2) Some((r, s)) else None |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
414 |
} |
159
940530087f30
updated programs
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
158
diff
changeset
|
415 |
} |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
416 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
417 |
//println("Testing lexing 1") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
418 |
//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
|
419 |
//println("Testing lexing 2") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
420 |
//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
|
421 |
//println("Testing lexing 3") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
422 |
//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
|
423 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
424 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
425 |
def tests_alexer(ss: Set[String])(r: Rexp) = { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
426 |
clear() |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
427 |
println(s"Testing ${r}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
428 |
for (s <- ss.par) yield { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
429 |
val d = der('b', r) |
359 | 430 |
val ad = bder('b', internalise(r)) |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
431 |
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
|
432 |
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
|
433 |
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
|
434 |
if (res1 != res2) println(s" ${res1} != ${res2}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
435 |
if (res1 != res2) Some((r, s)) else None |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
436 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
437 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
438 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
439 |
println("Testing alexing 1") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
440 |
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
|
441 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
442 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
443 |
def values(r: Rexp) : Set[Val] = r match { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
444 |
case ZERO => Set() |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
445 |
case ONE => Set(Empty) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
446 |
case CHAR(c) => Set(Chr(c)) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
447 |
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
|
448 |
(for (v2 <- values(r2)) yield Right(v2)) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
449 |
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
|
450 |
case STAR(r) => (Set(Stars(Nil)) ++ |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
451 |
(for (v <- values(r)) yield Stars(List(v)))) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
452 |
// 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
|
453 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
454 |
|
359 | 455 |
def tests_bder(c: Char)(r: Rexp) = { |
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
456 |
val d = der(c, r) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
457 |
val vals = values(d) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
458 |
for (v <- vals) { |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
459 |
println(s"Testing ${r} and ${v}") |
359 | 460 |
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
|
461 |
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
|
462 |
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
|
463 |
if (res1 != res2) println(s" ${res1} != ${res2}") |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
464 |
if (res1 != res2) Some((r, v)) else None |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
465 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
466 |
} |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
467 |
|
359 | 468 |
println("Testing bder/der") |
469 |
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
|
470 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
471 |
val er = SEQ(ONE,CHAR('a')) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
472 |
val ev = Right(Empty) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
473 |
val ed = ALT(SEQ(ZERO,CHAR('a')),ONE) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
474 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
475 |
retrieve(internalise(ed), ev) // => [true] |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
476 |
internalise(er) |
359 | 477 |
bder('a', internalise(er)) |
478 |
retrieve(bder('a', internalise(er)), ev) // => [] |
|
286
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
479 |
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
|
480 |
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
|
481 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
482 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
483 |
val dr = STAR(CHAR('a')) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
484 |
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
|
485 |
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
|
486 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
487 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
488 |
val res1 = retrieve(internalise(der('a', dr)), dr_val) // => [true] |
359 | 489 |
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
|
490 |
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
|
491 |
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
|
492 |
|
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
493 |
encode(inj(dr, 'a', decode(dr_der, res1))) |
804fbb227568
added proof for bitcoded algorithm
Christian Urban <urbanc@in.tum.de>
parents:
204
diff
changeset
|
494 |
|
359 | 495 |
*/ |