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