author | Christian Urban <urbanc@in.tum.de> |
Tue, 20 Aug 2019 23:42:28 +0200 | |
changeset 343 | f139bdc0dcd5 |
parent 325 | 2a128087215f |
permissions | -rw-r--r-- |
298 | 1 |
|
2 |
import scala.language.implicitConversions |
|
3 |
import scala.language.reflectiveCalls |
|
4 |
import scala.annotation.tailrec |
|
5 |
import scala.util.Try |
|
6 |
||
314 | 7 |
// for escaping strings |
298 | 8 |
def escape(raw: String) : String = { |
9 |
import scala.reflect.runtime.universe._ |
|
10 |
Literal(Constant(raw)).toString |
|
11 |
} |
|
12 |
||
13 |
def esc2(r: (String, String)) = (escape(r._1), escape(r._2)) |
|
14 |
||
15 |
def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match { |
|
16 |
case Nil => Nil |
|
17 |
case (x::xs) => { |
|
18 |
val res = f(x) |
|
19 |
if (acc.contains(res)) distinctBy(xs, f, acc) |
|
20 |
else x::distinctBy(xs, f, res::acc) |
|
21 |
} |
|
22 |
} |
|
23 |
||
24 |
abstract class Bit |
|
25 |
case object Z extends Bit |
|
26 |
case object S extends Bit |
|
27 |
case class C(c: Char) extends Bit |
|
28 |
||
29 |
type Bits = List[Bit] |
|
30 |
||
318 | 31 |
// usual regular expressions with predicates |
298 | 32 |
abstract class Rexp |
33 |
case object ZERO extends Rexp |
|
34 |
case object ONE extends Rexp |
|
318 | 35 |
case class PRED(f: Char => Boolean, s: String = "_") extends Rexp { |
36 |
override def toString = s"PRED(${s})" |
|
37 |
} |
|
298 | 38 |
case class ALTS(rs: List[Rexp]) extends Rexp |
39 |
case class SEQ(r1: Rexp, r2: Rexp) extends Rexp |
|
40 |
case class STAR(r: Rexp) extends Rexp |
|
41 |
case class RECD(x: String, r: Rexp) extends Rexp |
|
42 |
||
43 |
||
44 |
// abbreviations |
|
305 | 45 |
def CHAR(c: Char) = PRED(_ == c, c.toString) |
298 | 46 |
def ALT(r1: Rexp, r2: Rexp) = ALTS(List(r1, r2)) |
47 |
def PLUS(r: Rexp) = SEQ(r, STAR(r)) |
|
312
8b0b414e71b0
added size bounds for partial derivatives
Christian Urban <urbanc@in.tum.de>
parents:
311
diff
changeset
|
48 |
val ANYCHAR = PRED(_ => true, ".") |
298 | 49 |
|
50 |
// annotated regular expressions |
|
51 |
abstract class ARexp |
|
52 |
case object AZERO extends ARexp |
|
53 |
case class AONE(bs: Bits) extends ARexp |
|
318 | 54 |
case class APRED(bs: Bits, f: Char => Boolean, s: String = "_") extends ARexp { |
55 |
override def toString = s"APRED(${bs}, ${s})" |
|
56 |
} |
|
298 | 57 |
case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp |
58 |
case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp |
|
59 |
case class ASTAR(bs: Bits, r: ARexp) extends ARexp |
|
60 |
||
61 |
// abbreviations |
|
62 |
def AALT(bs: Bits, r1: ARexp, r2: ARexp) = AALTS(bs, List(r1, r2)) |
|
63 |
||
64 |
// values |
|
65 |
abstract class Val |
|
66 |
case object Empty extends Val |
|
67 |
case class Chr(c: Char) extends Val |
|
68 |
case class Sequ(v1: Val, v2: Val) extends Val |
|
69 |
case class Left(v: Val) extends Val |
|
70 |
case class Right(v: Val) extends Val |
|
71 |
case class Stars(vs: List[Val]) extends Val |
|
72 |
case class Rec(x: String, v: Val) extends Val |
|
73 |
||
318 | 74 |
def flatten(v: Val) : String = v match { |
75 |
case Empty => "" |
|
76 |
case Chr(c) => c.toString |
|
77 |
case Left(v) => flatten(v) |
|
78 |
case Right(v) => flatten(v) |
|
79 |
case Sequ(v1, v2) => flatten(v1) + flatten(v2) |
|
80 |
case Stars(vs) => vs.map(flatten).mkString |
|
81 |
case Rec(_, v) => flatten(v) |
|
82 |
} |
|
83 |
||
84 |
// extracts an environment from a value |
|
85 |
def env(v: Val) : List[(String, String)] = v match { |
|
86 |
case Empty => Nil |
|
87 |
case Chr(c) => Nil |
|
88 |
case Left(v) => env(v) |
|
89 |
case Right(v) => env(v) |
|
90 |
case Sequ(v1, v2) => env(v1) ::: env(v2) |
|
91 |
case Stars(vs) => vs.flatMap(env) |
|
92 |
case Rec(x, v) => (x, flatten(v))::env(v) |
|
93 |
} |
|
298 | 94 |
|
95 |
||
96 |
// some convenience for typing in regular expressions |
|
97 |
def charlist2rexp(s : List[Char]): Rexp = s match { |
|
98 |
case Nil => ONE |
|
99 |
case c::Nil => CHAR(c) |
|
100 |
case c::s => SEQ(CHAR(c), charlist2rexp(s)) |
|
101 |
} |
|
102 |
implicit def string2rexp(s : String) : Rexp = charlist2rexp(s.toList) |
|
103 |
||
104 |
implicit def RexpOps(r: Rexp) = new { |
|
105 |
def | (s: Rexp) = ALT(r, s) |
|
106 |
def % = STAR(r) |
|
107 |
def ~ (s: Rexp) = SEQ(r, s) |
|
108 |
} |
|
109 |
||
110 |
implicit def stringOps(s: String) = new { |
|
111 |
def | (r: Rexp) = ALT(s, r) |
|
112 |
def | (r: String) = ALT(s, r) |
|
113 |
def % = STAR(s) |
|
114 |
def ~ (r: Rexp) = SEQ(s, r) |
|
115 |
def ~ (r: String) = SEQ(s, r) |
|
116 |
def $ (r: Rexp) = RECD(s, r) |
|
117 |
} |
|
118 |
||
119 |
||
318 | 120 |
// string of a regular expression - for testing purposes |
305 | 121 |
def string(r: Rexp): String = r match { |
122 |
case ZERO => "0" |
|
123 |
case ONE => "1" |
|
124 |
case PRED(_, s) => s |
|
125 |
case ALTS(rs) => rs.map(string).mkString("[", "|", "]") |
|
126 |
case SEQ(r1, r2) => s"(${string(r1)} ~ ${string(r2)})" |
|
127 |
case STAR(r) => s"{${string(r)}}*" |
|
128 |
case RECD(x, r) => s"(${x}! ${string(r)})" |
|
129 |
} |
|
130 |
||
318 | 131 |
// string of an annotated regular expression - for testing purposes |
305 | 132 |
def astring(a: ARexp): String = a match { |
133 |
case AZERO => "0" |
|
134 |
case AONE(_) => "1" |
|
135 |
case APRED(_, _, s) => s |
|
136 |
case AALTS(_, rs) => rs.map(astring).mkString("[", "|", "]") |
|
137 |
case ASEQ(_, r1, r2) => s"(${astring(r1)} ~ ${astring(r2)})" |
|
138 |
case ASTAR(_, r) => s"{${astring(r)}}*" |
|
139 |
} |
|
140 |
||
306
6756b026c5fe
added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents:
305
diff
changeset
|
141 |
//-------------------------------------------------------------------- |
298 | 142 |
// BITCODED PART |
143 |
||
318 | 144 |
def retrieve(r: ARexp, v: Val) : Bits = (r, v) match { |
314 | 145 |
case (AONE(bs), Empty) => bs |
318 | 146 |
case (APRED(bs, _, _), Chr(d)) => bs |
314 | 147 |
case (AALTS(bs, r::Nil), v) => bs ++ retrieve(r, v) |
148 |
case (AALTS(bs, r::rs), Left(v)) => bs ++ retrieve(r, v) |
|
149 |
case (AALTS(bs, r::rs), Right(v)) => bs ++ retrieve(AALTS(Nil, rs), v) |
|
150 |
case (ASEQ(bs, r1, r2), Sequ(v1, v2)) => |
|
151 |
bs ++ retrieve(r1, v1) ++ retrieve(r2, v2) |
|
152 |
case (ASTAR(bs, r), Stars(Nil)) => bs ++ List(S) |
|
153 |
case (ASTAR(bs, r), Stars(v::vs)) => |
|
154 |
bs ++ List(Z) ++ retrieve(r, v) ++ retrieve(ASTAR(Nil, r), Stars(vs)) |
|
155 |
} |
|
156 |
||
298 | 157 |
def fuse(bs: Bits, r: ARexp) : ARexp = r match { |
158 |
case AZERO => AZERO |
|
159 |
case AONE(cs) => AONE(bs ++ cs) |
|
305 | 160 |
case APRED(cs, f, s) => APRED(bs ++ cs, f, s) |
298 | 161 |
case AALTS(cs, rs) => AALTS(bs ++ cs, rs) |
162 |
case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2) |
|
163 |
case ASTAR(cs, r) => ASTAR(bs ++ cs, r) |
|
164 |
} |
|
165 |
||
166 |
// translation into ARexps |
|
167 |
def internalise(r: Rexp) : ARexp = r match { |
|
168 |
case ZERO => AZERO |
|
169 |
case ONE => AONE(Nil) |
|
305 | 170 |
case PRED(f, s) => APRED(Nil, f, s) |
298 | 171 |
case ALTS(List(r1, r2)) => |
172 |
AALTS(Nil, List(fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2)))) |
|
173 |
case ALTS(r1::rs) => { |
|
174 |
val AALTS(Nil, rs2) = internalise(ALTS(rs)) |
|
175 |
AALTS(Nil, fuse(List(Z), internalise(r1)) :: rs2.map(fuse(List(S), _))) |
|
176 |
} |
|
177 |
case SEQ(r1, r2) => ASEQ(Nil, internalise(r1), internalise(r2)) |
|
178 |
case STAR(r) => ASTAR(Nil, internalise(r)) |
|
179 |
case RECD(x, r) => internalise(r) |
|
180 |
} |
|
181 |
||
182 |
internalise(("a" | "ab") ~ ("b" | "")) |
|
183 |
||
184 |
// decoding of values from bit sequences |
|
185 |
def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match { |
|
186 |
case (ONE, bs) => (Empty, bs) |
|
305 | 187 |
case (PRED(f, _), C(c)::bs) => (Chr(c), bs) |
298 | 188 |
case (ALTS(r::Nil), bs) => decode_aux(r, bs) |
317 | 189 |
case (ALTS(rs), Z::bs1) => { |
298 | 190 |
val (v, bs2) = decode_aux(rs.head, bs1) |
191 |
(Left(v), bs2) |
|
192 |
} |
|
317 | 193 |
case (ALTS(rs), S::bs1) => { |
298 | 194 |
val (v, bs2) = decode_aux(ALTS(rs.tail), bs1) |
317 | 195 |
(Right(v), bs2) |
298 | 196 |
} |
197 |
case (SEQ(r1, r2), bs) => { |
|
198 |
val (v1, bs1) = decode_aux(r1, bs) |
|
199 |
val (v2, bs2) = decode_aux(r2, bs1) |
|
200 |
(Sequ(v1, v2), bs2) |
|
201 |
} |
|
202 |
case (STAR(r1), S::bs) => { |
|
203 |
val (v, bs1) = decode_aux(r1, bs) |
|
204 |
val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1) |
|
205 |
(Stars(v::vs), bs2) |
|
206 |
} |
|
207 |
case (STAR(_), Z::bs) => (Stars(Nil), bs) |
|
208 |
case (RECD(x, r1), bs) => { |
|
209 |
val (v, bs1) = decode_aux(r1, bs) |
|
210 |
(Rec(x, v), bs1) |
|
211 |
} |
|
212 |
} |
|
213 |
||
214 |
def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match { |
|
215 |
case (v, Nil) => v |
|
216 |
case _ => throw new Exception("Not decodable") |
|
217 |
} |
|
218 |
||
318 | 219 |
def encode(v: Val) : Bits = v match { |
220 |
case Empty => Nil |
|
221 |
case Chr(c) => Nil |
|
222 |
case Left(v) => Z :: encode(v) |
|
223 |
case Right(v) => S :: encode(v) |
|
224 |
case Sequ(v1, v2) => encode(v1) ::: encode(v2) |
|
225 |
case Stars(Nil) => List(S) |
|
226 |
case Stars(v::vs) => Z :: encode(v) ::: encode(Stars(vs)) |
|
227 |
} |
|
228 |
||
298 | 229 |
|
230 |
//erase function: extracts a Rexp from Arexp |
|
231 |
def erase(r: ARexp) : Rexp = r match{ |
|
232 |
case AZERO => ZERO |
|
233 |
case AONE(_) => ONE |
|
305 | 234 |
case APRED(bs, f, s) => PRED(f, s) |
298 | 235 |
case AALTS(bs, rs) => ALTS(rs.map(erase(_))) |
236 |
case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2)) |
|
237 |
case ASTAR(cs, r)=> STAR(erase(r)) |
|
238 |
} |
|
239 |
||
240 |
||
241 |
// bnullable function: tests whether the aregular |
|
242 |
// expression can recognise the empty string |
|
243 |
def bnullable (r: ARexp) : Boolean = r match { |
|
244 |
case AZERO => false |
|
245 |
case AONE(_) => true |
|
305 | 246 |
case APRED(_,_,_) => false |
298 | 247 |
case AALTS(_, rs) => rs.exists(bnullable) |
248 |
case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2) |
|
249 |
case ASTAR(_, _) => true |
|
250 |
} |
|
251 |
||
252 |
def bmkeps(r: ARexp) : Bits = r match { |
|
253 |
case AONE(bs) => bs |
|
254 |
case AALTS(bs, rs) => { |
|
255 |
val n = rs.indexWhere(bnullable) |
|
256 |
bs ++ bmkeps(rs(n)) |
|
257 |
} |
|
258 |
case ASEQ(bs, r1, r2) => bs ++ bmkeps(r1) ++ bmkeps(r2) |
|
259 |
case ASTAR(bs, r) => bs ++ List(Z) |
|
260 |
} |
|
261 |
||
262 |
// derivative of a regular expression w.r.t. a character |
|
263 |
def bder(c: Char, r: ARexp) : ARexp = r match { |
|
264 |
case AZERO => AZERO |
|
265 |
case AONE(_) => AZERO |
|
305 | 266 |
case APRED(bs, f, _) => if (f(c)) AONE(bs:::List(C(c))) else AZERO |
298 | 267 |
case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _))) |
268 |
case ASEQ(bs, r1, r2) => |
|
318 | 269 |
if (bnullable(r1)) |
270 |
AALT(bs, ASEQ(Nil, bder(c, r1), r2), fuse(bmkeps(r1), bder(c, r2))) |
|
298 | 271 |
else ASEQ(bs, bder(c, r1), r2) |
272 |
case ASTAR(bs, r) => ASEQ(bs, fuse(List(S), bder(c, r)), ASTAR(Nil, r)) |
|
273 |
} |
|
274 |
||
318 | 275 |
def blex(r: ARexp, s: List[Char]) : Bits = s match { |
276 |
case Nil => if (bnullable(r)) bmkeps(r) |
|
277 |
else throw new Exception("Not matched") |
|
278 |
case c::cs => blex(bder(c, r), cs) |
|
279 |
} |
|
280 |
||
281 |
def preblexing(r: ARexp, s: String) : Val = |
|
282 |
decode(erase(r), blex(r, s.toList)) |
|
283 |
||
284 |
def blexing(r: Rexp, s: String) : Val = |
|
285 |
decode(r, blex(internalise(r), s.toList)) |
|
286 |
||
298 | 287 |
|
288 |
// derivative w.r.t. a string (iterates bder) |
|
289 |
@tailrec |
|
290 |
def bders (s: List[Char], r: ARexp) : ARexp = s match { |
|
291 |
case Nil => r |
|
292 |
case c::s => bders(s, bder(c, r)) |
|
293 |
} |
|
294 |
||
295 |
def flats(rs: List[ARexp]): List[ARexp] = rs match { |
|
296 |
case Nil => Nil |
|
297 |
case AZERO :: rs1 => flats(rs1) |
|
298 |
case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2) |
|
299 |
case r1 :: rs2 => r1 :: flats(rs2) |
|
300 |
} |
|
301 |
||
318 | 302 |
/* |
303 |
def vsimp(r: ARexp, v: Val): Val = (r, v) match { |
|
304 |
case (ASEQ(bs1, r1, r2), Sequ(v1, v2)) => |
|
305 |
(bsimp(r1), bsimp(r2), vsimp(r1, v1), vsimp(r2, v2)) match { |
|
306 |
case (AZERO, _, _, _) => throw new Exception("error") |
|
307 |
case (_, AZERO, _, _) => throw new Exception("error") |
|
308 |
case (AONE(_), _, _, vp2) => vp2 |
|
309 |
case (r1s, r2s, vp1, vp2) => Sequ(vp1, vp2) |
|
310 |
} |
|
311 |
case (AALTS(bs1, rs), _) => distinctBy(flats(rs.map(bsimp)), erase) match { |
|
312 |
case Nil => throw new Exception("error") |
|
313 |
case r :: Nil => throw new Exception("error") |
|
314 |
case rs => throw new Exception("error") |
|
315 |
} |
|
316 |
case _ => v |
|
317 |
} |
|
318 |
*/ |
|
319 |
def vsimp(v: Val, a: ARexp): Val = (v, bsimp(a)) match { |
|
320 |
case (Sequ(v1, v2), ASEQ(_, a1, a2)) => |
|
321 |
(vsimp(v1, a1), vsimp(v2, a2)) match { |
|
322 |
case (Empty, vp2) => vp2 |
|
323 |
case (vp1, vp2) => Sequ(vp1, vp2) |
|
324 |
} |
|
325 |
case (Left(Left(v1)), AALTS(_, r::rs)) => Left(vsimp(v1, r)) |
|
326 |
case (Left(v1), AALTS(_, rs)) => |
|
327 |
if (rs.length == 1) vsimp(v1, rs.head) else Left(vsimp(v1, rs.head)) |
|
328 |
case (Right(v1), AALTS(bs, rs)) => |
|
329 |
if (rs.length == 1) vsimp(v1, rs.head) else Right(vsimp(v1, AALTS(bs, rs.tail))) |
|
330 |
case _ => v |
|
331 |
} |
|
332 |
||
333 |
||
298 | 334 |
def bsimp(r: ARexp): ARexp = r match { |
335 |
case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match { |
|
336 |
case (AZERO, _) => AZERO |
|
337 |
case (_, AZERO) => AZERO |
|
338 |
case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) |
|
339 |
case (r1s, r2s) => ASEQ(bs1, r1s, r2s) |
|
340 |
} |
|
341 |
case AALTS(bs1, rs) => distinctBy(flats(rs.map(bsimp)), erase) match { |
|
342 |
case Nil => AZERO |
|
300 | 343 |
case r :: Nil => fuse(bs1, r) |
298 | 344 |
case rs => AALTS(bs1, rs) |
345 |
} |
|
346 |
case r => r |
|
347 |
} |
|
348 |
||
349 |
def bders_simp (s: List[Char], r: ARexp) : ARexp = s match { |
|
350 |
case Nil => r |
|
351 |
case c::s => bders_simp(s, bsimp(bder(c, r))) |
|
352 |
} |
|
353 |
||
354 |
def blex_simp(r: ARexp, s: List[Char]) : Bits = s match { |
|
355 |
case Nil => if (bnullable(r)) bmkeps(r) |
|
356 |
else throw new Exception("Not matched") |
|
357 |
case c::cs => blex_simp(bsimp(bder(c, r)), cs) |
|
358 |
} |
|
359 |
||
360 |
||
361 |
def blexing_simp(r: Rexp, s: String) : Val = |
|
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
362 |
decode(r, blex_simp(internalise(r), s.toList)) |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
363 |
|
298 | 364 |
|
311 | 365 |
def btokenise_simp(r: Rexp, s: String) = |
366 |
env(blexing_simp(r, s)).map(esc2) |
|
298 | 367 |
|
314 | 368 |
// Quick example |
369 |
||
370 |
val r : Rexp = ZERO | "a" |
|
371 |
||
372 |
lexing(r, "a") |
|
373 |
||
374 |
val a0 = internalise(r) |
|
375 |
val a1 = bder('a', a0) |
|
376 |
val a1s = bsimp(bder('a', a0)) |
|
377 |
||
378 |
val a2 = bmkeps(a1) |
|
379 |
val a2s = bmkeps(a1s) |
|
380 |
||
381 |
val v = decode(r, a2) |
|
382 |
val vs = decode(r, a2s) |
|
383 |
||
384 |
||
385 |
||
386 |
val Rr : Rexp = ONE ~ "a" |
|
387 |
||
388 |
lexing(Rr, "a") |
|
389 |
||
390 |
val Ra0 = internalise(Rr) |
|
391 |
astring(Ra0) |
|
392 |
val Ra1 = bder('a', Ra0) |
|
393 |
astring(Ra1) |
|
394 |
val Ra1s = bsimp(bder('a', Ra0)) |
|
395 |
astring(Ra1s) |
|
396 |
||
397 |
val Ra2 = bmkeps(Ra1) |
|
398 |
val Ra2s = bmkeps(Ra1s) |
|
399 |
||
400 |
val Rv = decode(Rr, Ra2) |
|
401 |
val Rvs = decode(Rr, Ra2s) |
|
402 |
||
298 | 403 |
|
404 |
// Testing |
|
405 |
//============ |
|
406 |
||
407 |
def time[T](code: => T) = { |
|
408 |
val start = System.nanoTime() |
|
409 |
val result = code |
|
410 |
val end = System.nanoTime() |
|
411 |
((end - start)/1.0e9).toString |
|
412 |
} |
|
413 |
||
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
414 |
def timeR[T](code: => T) = { |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
415 |
val start = System.nanoTime() |
300 | 416 |
for (i <- 1 to 10) code |
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
417 |
val result = code |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
418 |
val end = System.nanoTime() |
300 | 419 |
(result, (end - start)) |
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
420 |
} |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
421 |
|
322 | 422 |
//size: of a Rrexp and ARexp for testing purposes |
298 | 423 |
def size(r: Rexp) : Int = r match { |
424 |
case ZERO => 1 |
|
425 |
case ONE => 1 |
|
305 | 426 |
case PRED(_,_) => 1 |
298 | 427 |
case SEQ(r1, r2) => 1 + size(r1) + size(r2) |
428 |
case ALTS(rs) => 1 + rs.map(size).sum |
|
429 |
case STAR(r) => 1 + size(r) |
|
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
430 |
case RECD(_, r) => size(r) |
298 | 431 |
} |
432 |
||
433 |
def asize(a: ARexp) = size(erase(a)) |
|
434 |
||
435 |
||
436 |
// Lexing Rules for a Small While Language |
|
437 |
||
438 |
//symbols |
|
305 | 439 |
val SYM = PRED("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ".contains(_), "SYM") |
298 | 440 |
//digits |
305 | 441 |
val DIGIT = PRED("0123456789".contains(_), "NUM") |
298 | 442 |
//identifiers |
443 |
val ID = SYM ~ (SYM | DIGIT).% |
|
444 |
//numbers |
|
445 |
val NUM = STAR(DIGIT) |
|
446 |
//keywords |
|
447 |
val KEYWORD : Rexp = "skip" | "while" | "do" | "if" | "then" | "else" | "read" | "write" | "true" | "false" |
|
448 |
//semicolons |
|
449 |
val SEMI: Rexp = ";" |
|
450 |
//operators |
|
451 |
val OP: Rexp = ":=" | "==" | "-" | "+" | "*" | "!=" | "<" | ">" | "<=" | ">=" | "%" | "/" |
|
452 |
//whitespaces |
|
453 |
val WHITESPACE = PLUS(" " | "\n" | "\t") |
|
454 |
//parentheses |
|
455 |
val RPAREN: Rexp = ")" |
|
456 |
val LPAREN: Rexp = "(" |
|
457 |
val BEGIN: Rexp = "{" |
|
458 |
val END: Rexp = "}" |
|
459 |
//strings...but probably needs not |
|
460 |
val STRING: Rexp = "\"" ~ SYM.% ~ "\"" |
|
461 |
||
462 |
||
463 |
||
464 |
val WHILE_REGS = (("k" $ KEYWORD) | |
|
465 |
("i" $ ID) | |
|
466 |
("o" $ OP) | |
|
467 |
("n" $ NUM) | |
|
468 |
("s" $ SEMI) | |
|
469 |
("str" $ STRING) | |
|
470 |
("p" $ (LPAREN | RPAREN)) | |
|
471 |
("b" $ (BEGIN | END)) | |
|
472 |
("w" $ WHITESPACE)).% |
|
473 |
||
474 |
||
475 |
// Some Small Tests |
|
476 |
//================== |
|
477 |
||
307
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
478 |
println("Small tests") |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
479 |
|
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
480 |
val re1 = STAR("a" | "aa") |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
481 |
println(astring(bders_simp("".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
482 |
println(astring(bders_simp("a".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
483 |
println(astring(bders_simp("aa".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
484 |
println(astring(bders_simp("aaa".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
485 |
println(astring(bders_simp("aaaaaa".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
486 |
println(astring(bders_simp("aaaaaaaaa".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
487 |
println(astring(bders_simp("aaaaaaaaaaaa".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
488 |
println(astring(bders_simp("aaaaaaaaaaaaaaaaaaaaaaaaa".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
489 |
println(astring(bders_simp("aaaaaabaaaabbbbbaaaaaaaaaaaaaaa".toList, internalise(re1)))) |
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
490 |
|
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
491 |
|
311 | 492 |
for (i <- 0 to 100 by 5) { |
493 |
//print("Old: " + time(tokenise_simp(re1, "a" * i))) |
|
494 |
print(" Bit: " + time(btokenise_simp(re1, "a" * i))) |
|
495 |
print(" Bit full simp: " + time(btokenise_simp_full(re1, "a" * i))) |
|
496 |
println(" Bit2: " + time(btokenise2_simp(re1, "a" * i))) |
|
497 |
} |
|
307
ee1caac29bb2
updated to Isabelle 2018
Christian Urban <urbanc@in.tum.de>
parents:
306
diff
changeset
|
498 |
|
311 | 499 |
Console.readLine |
298 | 500 |
|
501 |
||
502 |
// Bigger Tests |
|
503 |
//============== |
|
504 |
||
505 |
||
311 | 506 |
println("Big tests") |
507 |
||
298 | 508 |
val fib_prog = """ |
509 |
write "Fib"; |
|
510 |
read n; |
|
511 |
minus1 := 0; |
|
512 |
minus2 := 1; |
|
513 |
while n > 0 do { |
|
514 |
temp := minus2; |
|
515 |
minus2 := minus1 + minus2; |
|
516 |
minus1 := temp; |
|
517 |
n := n - 1 |
|
518 |
}; |
|
519 |
write "Result"; |
|
520 |
write minus2 |
|
521 |
""" |
|
522 |
||
523 |
||
524 |
println("fib prog tests :") |
|
525 |
println(tokenise_simp(WHILE_REGS, fib_prog)) |
|
526 |
println(btokenise_simp(WHILE_REGS, fib_prog)) |
|
527 |
println("equal? " + (tokenise_simp(WHILE_REGS, fib_prog) == btokenise_simp(WHILE_REGS, fib_prog))) |
|
528 |
||
300 | 529 |
for (i <- 1 to 20) { |
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
530 |
print("Old: " + time(tokenise_simp(WHILE_REGS, fib_prog * i))) |
300 | 531 |
print(" Bit: " + time(btokenise_simp(WHILE_REGS, fib_prog * i))) |
532 |
println(" Bit full simp: " + time(btokenise_simp_full(WHILE_REGS, fib_prog * i))) |
|
311 | 533 |
//println(" Bit2: " + time(btokenise2_simp(WHILE_REGS, fib_prog * i))) |
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
534 |
} |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
535 |
|
305 | 536 |
|
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
537 |
println("Original " + size(WHILE_REGS)) |
305 | 538 |
println("Size Bit " + asize(bders_simp((fib_prog * 1).toList, internalise(WHILE_REGS)))) |
539 |
println("Size Bitf " + asize(bders_simp_full((fib_prog * 1).toList, internalise(WHILE_REGS)))) |
|
311 | 540 |
println("Size Bit2 " + asize(bders2_simp((fib_prog * 1).toList, internalise(WHILE_REGS)))) |
305 | 541 |
println("Size Old " + size(ders_simp((fib_prog * 1).toList, WHILE_REGS))) |
306
6756b026c5fe
added partial derivatives to compare sizes
Christian Urban <urbanc@in.tum.de>
parents:
305
diff
changeset
|
542 |
println("Size Pder " + psize(pders_simp((fib_prog * 1).toList, WHILE_REGS))) |
298 | 543 |
|
305 | 544 |
System.exit(0) |
300 | 545 |
|
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
546 |
println("Internal sizes test OK or strange") |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
547 |
|
300 | 548 |
def perc(p1: Double, p2: Double) : String = |
549 |
f"${(((p1 - p2) / p2) * 100.0) }%5.0f" + "%" |
|
550 |
||
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
551 |
def ders_test(n: Int, s: List[Char], r: Rexp, a: ARexp) : (Rexp, ARexp) = s match { |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
552 |
case Nil => (r, a) |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
553 |
case c::s => { |
300 | 554 |
// derivative |
555 |
val (rd1, tr1) = timeR(der(c, r)) |
|
556 |
val (ad1, ta1) = timeR(bder(c, a)) |
|
557 |
val trs1 = f"${tr1}%.5f" |
|
558 |
val tas1 = f"${ta1}%.5f" |
|
559 |
if (tr1 < ta1) println(s"Time strange der (step) ${n} ${perc(ta1, tr1)} sizes der ${size(rd1)} ${asize(ad1)}") |
|
560 |
//simplification |
|
561 |
val (rd, tr) = timeR(simp(rd1)._1) |
|
562 |
val (ad, ta) = timeR(bsimp(ad1)) |
|
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
563 |
val trs = f"${tr}%.5f" |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
564 |
val tas = f"${ta}%.5f" |
300 | 565 |
//full simplification |
566 |
val (adf, taf) = timeR(bsimp_full(ad1)) |
|
567 |
if (tr < ta) println(s"Time strange simp (step) ${n} ${perc(ta, tr)} sizes simp ${size(rd)} ${asize(ad)}") |
|
568 |
if (n == 1749 || n == 1734) { |
|
569 |
println{s"Aregex before bder (size: ${asize(a)})\n ${string(erase(a))}"} |
|
570 |
println{s"Aregex after bder (size: ${asize(ad1)})\n ${string(erase(ad1))}"} |
|
571 |
println{s"Aregex after bsimp (size: ${asize(ad)})\n ${string(erase(ad))}"} |
|
572 |
println{s"Aregex after bsimp_full (size: ${asize(adf)})\n ${string(erase(adf))}"} |
|
573 |
} |
|
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
574 |
ders_test(n + 1, s, rd, ad) |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
575 |
} |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
576 |
} |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
577 |
|
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
578 |
val prg = (fib_prog * 10).toList |
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
579 |
ders_test(0, prg, WHILE_REGS, internalise(WHILE_REGS)) |
298 | 580 |
|
581 |
||
582 |
//testing the two lexings produce the same value |
|
583 |
//enumerates strings of length n over alphabet cs |
|
584 |
def strs(n: Int, cs: String) : Set[String] = { |
|
585 |
if (n == 0) Set("") |
|
586 |
else { |
|
587 |
val ss = strs(n - 1, cs) |
|
588 |
ss ++ |
|
589 |
(for (s <- ss; c <- cs.toList) yield c + s) |
|
590 |
} |
|
591 |
} |
|
318 | 592 |
|
298 | 593 |
def enum(n: Int, s: String) : Stream[Rexp] = n match { |
594 |
case 0 => ZERO #:: ONE #:: s.toStream.map(CHAR) |
|
595 |
case n => { |
|
596 |
val rs = enum(n - 1, s) |
|
597 |
rs #::: |
|
598 |
(for (r1 <- rs; r2 <- rs) yield ALT(r1, r2)) #::: |
|
599 |
(for (r1 <- rs; r2 <- rs) yield SEQ(r1, r2)) #::: |
|
600 |
(for (r1 <- rs) yield STAR(r1)) |
|
601 |
} |
|
602 |
} |
|
603 |
||
318 | 604 |
def benum(n: Int, s: String) = enum(n, s).map(internalise) |
605 |
||
606 |
def values(r: Rexp) : Set[Val] = r match { |
|
607 |
case ZERO => Set() |
|
608 |
case ONE => Set(Empty) |
|
609 |
case PRED(_, s) => Set(Chr(s.head)) |
|
610 |
case ALTS(List(r1, r2)) => (for (v1 <- values(r1)) yield Left(v1)) ++ |
|
611 |
(for (v2 <- values(r2)) yield Right(v2)) |
|
612 |
case SEQ(r1, r2) => for (v1 <- values(r1); v2 <- values(r2)) yield Sequ(v1, v2) |
|
613 |
case STAR(r) => (Set(Stars(Nil)) ++ |
|
614 |
(for (v <- values(r)) yield Stars(List(v)))) |
|
615 |
// to do more would cause the set to be infinite |
|
616 |
} |
|
617 |
||
618 |
||
619 |
// tests about retrieve |
|
620 |
||
621 |
def tests_retrieve(r: Rexp) = { |
|
622 |
val vs = values(r) |
|
623 |
val a = internalise(r) |
|
624 |
val as = bsimp(a) |
|
625 |
for (v <- vs) { |
|
626 |
println(s"Testing ${string(r)} and ${v}") |
|
627 |
val bs1 = retrieve(a, v) |
|
628 |
val bs2 = Try(Some(retrieve(as, decode(erase(as), bs1)))).getOrElse(None) |
|
629 |
if (Some(bs1) != bs2) println(s"Disagree on ${string(r)}, ${v}") |
|
630 |
if (Some(bs1) != bs2) Some((r, v)) else None |
|
631 |
} |
|
632 |
} |
|
633 |
||
634 |
println("Testing retrieve 1") |
|
635 |
println(enum(1, "ab").map(tests_retrieve).toList) |
|
636 |
||
637 |
// an example where the property fails |
|
638 |
val r = (ZERO ~ "b") | "a" |
|
639 |
val a = internalise(r) |
|
640 |
val as = bsimp(a) |
|
641 |
val v = Right(Chr('a')) |
|
642 |
||
643 |
println("arexp " ++ astring(a)) |
|
644 |
println("simplified " ++ astring(as)) |
|
645 |
||
646 |
val bs1 = retrieve(a, v) |
|
647 |
encode(v) |
|
648 |
retrieve(as, decode(erase(as), bs1)) |
|
649 |
||
650 |
//tests retrieve and vsimp |
|
651 |
||
652 |
def tests_retrieve_vsimp(ss: Set[String])(r: Rexp) = { |
|
653 |
val a = internalise(r) |
|
654 |
val as = bsimp(a) |
|
655 |
for (s <- ss.par) yield { |
|
656 |
val v = Try(Some(preblexing(a, s))).getOrElse(None) |
|
657 |
if (v.isDefined) { |
|
658 |
val bs1 = retrieve(a, v.get) |
|
659 |
val bs2 = Try(retrieve(as, vsimp(v.get, as))).getOrElse(Nil) |
|
660 |
if (bs1 != bs2) { |
|
661 |
println(s"Disagree on ${astring(a)}, ${astring(as)}, ${s}") |
|
662 |
println(s" ${v.get} and ${vsimp(v.get)}") |
|
663 |
println(s" ${bs1} and ${bs2}") |
|
664 |
Some(a, as, s, v.get, vsimp(v.get, as), bs1, bs2) |
|
665 |
} else None |
|
666 |
} else None |
|
667 |
} |
|
668 |
} |
|
669 |
||
670 |
println("Partial searching: ") |
|
671 |
enum(2, "abc").map(tests_retrieve_vsimp(strs(3, "abc"))). |
|
672 |
flatten.toSet.flatten.minBy(a => asize(a._1)) |
|
673 |
||
674 |
//tests derivatives and bsimp |
|
675 |
||
676 |
def tests_ders_bsimp(ss: Set[String])(r: Rexp) = { |
|
325 | 677 |
val a = fuse(List(Z,Z,S), internalise(r)) |
318 | 678 |
for (s <- ss.par) yield { |
679 |
val d1 = bsimp(bders(s.toList, bsimp(a))) |
|
680 |
val d2 = bsimp(bders(s.toList, a)) |
|
681 |
if (d1 != d2) { |
|
682 |
println(s"Disagree on ${astring(a)}") |
|
683 |
println(s" ${astring(d1)} and ${astring(d2)}") |
|
684 |
Some(a, d1, d2) |
|
685 |
} else None |
|
686 |
} |
|
687 |
} |
|
688 |
||
689 |
println("Partial searching: ") |
|
690 |
enum(2, "abc").map(tests_ders_bsimp(strs(1, "abc"))). |
|
325 | 691 |
flatten.toSet.flatten |
318 | 692 |
|
322 | 693 |
// tests about good |
323 | 694 |
def good(a: ARexp) : Boolean = a match { |
322 | 695 |
case AZERO => false |
696 |
case AONE(_) => true |
|
697 |
case APRED(_, _, _) => true |
|
698 |
case AALTS(_, Nil) => false |
|
699 |
case AALTS(_, rs) => rs.forall(good(_)) |
|
700 |
case ASEQ(_, r1, r2) => good(r1) & good(r2) |
|
701 |
case ASTAR(_, _) => true |
|
702 |
} |
|
703 |
||
704 |
def tests_good(r: Rexp) = { |
|
705 |
val a = bsimp(internalise(r)) |
|
706 |
if (! good(a) & a != AZERO) { |
|
707 |
println(s"Counter-example on ${astring(a)}") |
|
708 |
Some(a) |
|
709 |
} else None |
|
710 |
} |
|
711 |
||
712 |
enum(2, "abc").map(tests_good).toSet |
|
713 |
||
714 |
val g1 = AALTS(Nil, Nil) |
|
715 |
good(g1) |
|
716 |
good(bsimp(g1)) |
|
318 | 717 |
|
718 |
||
719 |
//tests retrieve and lexing |
|
720 |
||
721 |
def tests_retrieve_lex(ss: Set[String])(r: Rexp) = { |
|
722 |
val a = internalise(r) |
|
723 |
val as = bsimp(a) |
|
724 |
for (s <- ss.par) yield { |
|
725 |
val bs1 = Try(Some(blex(a, s.toList))).getOrElse(None) |
|
726 |
val bs2 = Try(Some(blex(as, s.toList))).getOrElse(None) |
|
727 |
if (bs1 != bs2) { |
|
728 |
println(s"Disagree on ${astring(a)}, ${astring(as)}, ${s}") |
|
729 |
println(s" ${bs1} and ${bs2}") |
|
730 |
Some(a, as, s) |
|
731 |
} else None |
|
732 |
} |
|
733 |
} |
|
734 |
||
735 |
println("Partial searching: ") |
|
736 |
enum(2, "abc").map(tests_retrieve_lex(strs(3, "abc"))).flatten.toSet |
|
737 |
||
738 |
//Disagree on [[c|b]|[a|c]], [c|b|a], a |
|
739 |
//Right(Left(Chr(a))) and Right(Left(Chr(a))) |
|
740 |
//List(S, Z) and List(Z, S) |
|
741 |
||
742 |
val s = "c" |
|
743 |
val ar : Rexp = "a" |
|
744 |
val br : Rexp = "b" |
|
745 |
val cr : Rexp = "c" |
|
746 |
val r1 : Rexp = ALT(ALT(cr, br), ALT(ar,cr)) |
|
747 |
val a1 = internalise(r1) |
|
748 |
val a2 = bsimp(a1) |
|
749 |
val a2a = internalise(erase(a2)) |
|
750 |
||
751 |
astring(a1) |
|
752 |
astring(a2) |
|
753 |
astring(a2a) |
|
754 |
||
755 |
blexing(r1 ,s) |
|
756 |
blexing_simp(r1 ,s) |
|
757 |
val v1 = preblexing(a1, s) |
|
758 |
val v2 = preblexing(a2a, s) |
|
759 |
retrieve(a1, v1) |
|
760 |
retrieve(a2, v2) |
|
761 |
||
762 |
||
298 | 763 |
//tests blexing and lexing |
764 |
def tests(ss: Set[String])(r: Rexp) = { |
|
765 |
//println(s"Testing ${r}") |
|
766 |
for (s <- ss.par) yield { |
|
767 |
val res1 = Try(Some(lexing_simp(r, s))).getOrElse(None) |
|
768 |
val res2 = Try(Some(blexing_simp(r, s))).getOrElse(None) |
|
769 |
if (res1 != res2) |
|
770 |
{ println(s"Disagree on ${r} and ${s}") |
|
771 |
println(s" ${res1} != ${res2}") |
|
772 |
Some((r, s)) } else None |
|
773 |
} |
|
774 |
} |
|
775 |
||
776 |
||
777 |
println("Partial searching: ") |
|
778 |
enum(2, "abc").map(tests(strs(3, "abc"))).toSet |
|
299
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
779 |
|
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
780 |
|
cae7eab03018
added some timing and size tests when doing the derivatives
Christian Urban <urbanc@in.tum.de>
parents:
298
diff
changeset
|
781 |
|
305 | 782 |