--- a/thys2/blexer2.sc Fri May 20 18:52:03 2022 +0100
+++ b/thys2/blexer2.sc Thu May 26 20:51:40 2022 +0100
@@ -1,3 +1,5 @@
+//Strong Bsimp to obtain Antimirov's cubic bound
+
// A simple lexer inspired by work of Sulzmann & Lu
//==================================================
//
@@ -496,12 +498,37 @@
val rs_simp = rs.map(strongBsimp5(_))
val flat_res = flats(rs_simp)
var dist_res = distinctBy5(flat_res)//distinctBy(flat_res, erase)
- var dist2_res = distinctBy5(dist_res)
- while(dist_res != dist2_res){
- dist_res = dist2_res
- dist2_res = distinctBy5(dist_res)
+ // var dist2_res = distinctBy5(dist_res)
+ // while(dist_res != dist2_res){
+ // dist_res = dist2_res
+ // dist2_res = distinctBy5(dist_res)
+ // }
+ (dist_res) match {
+ case Nil => AZERO
+ case s :: Nil => fuse(bs1, s)
+ case rs => AALTS(bs1, rs)
}
- (dist2_res) match {
+ }
+ case r => r
+ }
+}
+
+def strongBsimp6(r: ARexp): ARexp =
+{
+ // println("was this called?")
+ r match {
+ case ASEQ(bs1, r1, r2) => (strongBsimp6(r1), strongBsimp6(r2)) match {
+ case (AZERO, _) => AZERO
+ case (_, AZERO) => AZERO
+ case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
+ case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
+ }
+ case AALTS(bs1, rs) => {
+ // println("alts case")
+ val rs_simp = rs.map(strongBsimp6(_))
+ val flat_res = flats(rs_simp)
+ var dist_res = distinctBy6(flat_res)//distinctBy(flat_res, erase)
+ (dist_res) match {
case Nil => AZERO
case s :: Nil => fuse(bs1, s)
case rs => AALTS(bs1, rs)
@@ -688,6 +715,90 @@
}
}
+def attachCtx(r: ARexp, ctx: List[Rexp]) : List[Rexp] = {
+ val res = breakIntoTerms(oneSimp(L(erase(r), ctx))).map(oneSimp)
+ res
+}
+
+def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, inclusionPred: (C, C) => Boolean) : Boolean = {
+ inclusionPred(f(a, b), c)
+}
+def rexpListInclusion(rs1: List[Rexp], rs2: List[Rexp]) : Boolean = {
+ rs1.forall(rs2.contains)
+}
+def pAKC6(acc: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
+ // println("pakc")
+ // println(shortRexpOutput(erase(r)))
+ // println("acc")
+ // rsprint(acc)
+ // println("ctx---------")
+ // rsprint(ctx)
+ // println("ctx---------end")
+ // rsprint(breakIntoTerms(L(erase(r), ctx)).map(oneSimp))
+
+ // rprint(L(erase(r), ctx))
+ //breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(acc.contains)
+ if (ABIncludedByC(r, ctx, acc, attachCtx, rexpListInclusion)) {//acc.flatMap(breakIntoTerms
+ //println("included in acc!!!")
+ AZERO
+ }
+ else{
+ r match {
+ case ASEQ(bs, r1, r2) =>
+ (pAKC6(acc, r1, erase(r2) :: ctx)) match{
+ case AZERO =>
+ AZERO
+ case AONE(bs1) =>
+ fuse(bs1, r2)
+ case r1p =>
+ ASEQ(bs, r1p, r2)
+ }
+ case AALTS(bs, rs0) =>
+ // println("before pruning")
+ // println(s"ctx is ")
+ // ctx.foreach(r => println(shortRexpOutput(r)))
+ // println(s"rs0 is ")
+ // rs0.foreach(r => println(shortRexpOutput(erase(r))))
+ // println(s"acc is ")
+ // acc.foreach(r => println(shortRexpOutput(r)))
+ rs0.map(r => pAKC6(acc, r, ctx)).filter(_ != AZERO) match {
+ case Nil =>
+ // println("after pruning Nil")
+ AZERO
+ case r :: Nil =>
+ // println("after pruning singleton")
+ // println(shortRexpOutput(erase(r)))
+ r
+ case rs0p =>
+ // println("after pruning non-singleton")
+ AALTS(bs, rs0p)
+ }
+ case r => r
+ }
+ }
+}
+
+
+def distinctBy6(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
+ case Nil =>
+ Nil
+ case x :: xs => {
+ val erased = erase(x)
+ if(acc.contains(erased)){
+ distinctBy6(xs, acc)
+ }
+ else{
+ val pruned = pAKC6(acc, x, Nil)
+ val newTerms = breakIntoTerms(erase(pruned))
+ pruned match {
+ case AZERO =>
+ distinctBy6(xs, acc)
+ case xPrime =>
+ xPrime :: distinctBy6(xs, newTerms.map(oneSimp) ::: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
+ }
+ }
+ }
+}
def breakIntoTerms(r: Rexp) : List[Rexp] = r match {
case SEQ(r1, r2) => breakIntoTerms(r1).map(r11 => SEQ(r11, r2))
@@ -806,7 +917,10 @@
case Nil => r
case c::s => bdersStrong5(s, strongBsimp5(bder(c, r)))
}
-
+ def bdersStrong6(s: List[Char], r: ARexp) : ARexp = s match {
+ case Nil => r
+ case c::s => bdersStrong6(s, strongBsimp6(bder(c, r)))
+ }
def bdersSimp(s: String, r: Rexp) : ARexp = bders_simp(s.toList, internalise(r))
def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
@@ -1024,13 +1138,13 @@
//val pderSTAR = pderUNIV(STARREG)
//val refSize = pderSTAR.map(size(_)).sum
- for(n <- 6 to 6){
+ for(n <- 5 to 5){
val STARREG = n_astar(n)
val iMax = (lcm((1 to n).toList))
- for(i <- 1 to iMax + 50){// 100, 400, 800, 840, 841, 900
+ for(i <- 1 to iMax + 2){// 100, 400, 800, 840, 841, 900
val prog0 = "a" * i
//println(s"test: $prog0")
- print(n)
+ print(i)
print(" ")
// print(i)
// print(" ")
@@ -1089,34 +1203,17 @@
//STAR(SEQ(ALTS(STAR(STAR(STAR(STAR(CHAR(c))))),ALTS(CHAR(c),CHAR(b))),ALTS(ZERO,SEQ(ALTS(ALTS(STAR(CHAR(c)),SEQ(CHAR(b),CHAR(a))),CHAR(c)),STAR(ALTS(ALTS(ONE,CHAR(a)),STAR(CHAR(c))))))))
//(depth5)
//STAR(SEQ(ALTS(ALTS(STAR(CHAR(b)),SEQ(ONE,CHAR(b))),SEQ(STAR(CHAR(a)),CHAR(b))),ALTS(ZERO,ALTS(STAR(CHAR(b)),STAR(CHAR(a))))))
- test(rexp(4), 10000000) { (r: Rexp) =>
+ test(rexp(4), 100000) { (r: Rexp) =>
// ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) =>
val ss = stringsFromRexp(r)
- val boolList = ss.map(s => {
- val bdStrong = bdersStrong(s.toList, internalise(r))
- val bdStrong5 = bdersStrong5(s.toList, internalise(r))
- val bdFurther5 = strongBsimp5(bdStrong5)
- val sizeFurther5 = asize(bdFurther5)
- val pdersSet = pderUNIV(r)
- val size5 = asize(bdStrong5)
- val size0 = asize(bdStrong)
+ val boolList = ss.filter(s => s != "").map(s => {
+ //val bdStrong = bdersStrong(s.toList, internalise(r))
+ val bdStrong6 = bdersStrong6(s.toList, internalise(r))
+ val bdStrong6Set = breakIntoTerms(erase(bdStrong6))
+ val pdersSet = pderUNIV(r).flatMap(r => breakIntoTerms(r))
// println(s)
- // println("pdersSet size")
- // println(pdersSet.size)
- // pdersSet.foreach(r => println(shortRexpOutput(r)))
- // println("after bdStrong5")
-
- // println(shortRexpOutput(erase(bdStrong5)))
- // println(breakIntoTerms(erase(bdStrong5)).size)
-
- // println("after bdStrong")
- // println(shortRexpOutput(erase(bdStrong)))
- // println(breakIntoTerms(erase(bdStrong)).size)
- // println(size5, size0, sizeFurther5)
- // aprint(strongBsimp5(bdStrong))
- // println(asize(strongBsimp5(bdStrong5)))
- // println(s)
- size5 <= size0
+ // println(bdStrong6Set.size, pdersSet.size)
+ bdStrong6Set.size <= pdersSet.size
})
// println(boolList)
//!boolList.exists(b => b == false)
@@ -1125,11 +1222,40 @@
}
-small()
-// generator_test()
+// small()
+generator_test()
+def counterexample_check() {
+ val r = STAR(SEQ(ALTS(ALTS(CHAR('b'),CHAR('c')),
+ SEQ(CHAR('b'),CHAR('b'))),ALTS(SEQ(ONE,CHAR('b')),CHAR('a'))))
+ val s = "bbbb"
+ val bdStrong5 = bdersStrong6(s.toList, internalise(r))
+ val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
+ val pdersSet = pderUNIV(r)//.map(oneSimp).flatMap(r => breakIntoTerms(r))
+ println("original regex ")
+ rprint(r)
+ println("after strong bsimp")
+ aprint(bdStrong5)
+ println("turned into a set %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ")
+ rsprint(bdStrong5Set)
+ println("after pderUNIV")
+ rsprint(pdersSet.toList)
+}
+// counterexample_check()
// 1
-
+def newStrong_test() {
+ val r2 = (CHAR('b') | ONE)
+ val r0 = CHAR('d')
+ val r1 = (ONE | CHAR('c'))
+ val expRexp = (SEQ(r2, r0) | SEQ(SEQ(r1, r2), r0))
+ println(s"original regex is: ")
+ rprint(expRexp)
+ val expSimp5 = strongBsimp5(internalise(expRexp))
+ val expSimp6 = strongBsimp6(internalise(expRexp))
+ aprint(expSimp5)
+ aprint(expSimp6)
+}
+// newStrong_test()
// SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))),
// SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))),
// STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))),