--- a/thys2/blexer2.sc Thu Apr 21 14:58:51 2022 +0100
+++ b/thys2/blexer2.sc Mon Apr 25 17:00:18 2022 +0100
@@ -479,6 +479,35 @@
}
}
+def strongBsimp5(r: ARexp): ARexp =
+{
+ // println("was this called?")
+ r match {
+ case ASEQ(bs1, r1, r2) => (strongBsimp5(r1), strongBsimp5(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(strongBsimp5(_))
+
+ val flat_res = flats(rs_simp)
+
+ val dist_res = distinctBy5(flat_res)//distinctBy(flat_res, erase)
+
+ dist_res match {
+ case Nil => AZERO
+ case s :: Nil => fuse(bs1, s)
+ case rs => AALTS(bs1, rs)
+ }
+
+ }
+ case r => r
+ }
+}
+
def bders (s: List[Char], r: ARexp) : ARexp = s match {
case Nil => r
case c::s => bders(s, bder(c, r))
@@ -552,14 +581,101 @@
case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
}
-
}
}
+// fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
+// where
+// "pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) ⊆ (L (erase (AALTs [] rsa))) then AZERO else
+// case r of (ASEQ bs r1 r2) ⇒
+// bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ (erase r2) ( ctx) )) r2 |
+// (AALTs bs rs) ⇒
+// bsimp_AALTs bs (flts (map (λr. pAKC_aux rsa r ( ctx) ) rs) ) |
+// r ⇒ r
+
+// def canonicalSeq(rs: List[Rexp], acc: Rexp) = rs match {
+// case r::Nil => SEQ(r, acc)
+// case Nil => acc
+// case r1::r2::Nil => SEQ(SEQ(r1, r2), acc)
+// }
+
+
+//the "fake" Language interpretation: just concatenates!
+def L(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
+ case Nil => acc
+ case r :: rs1 =>
+ if(acc == ONE)
+ L(r, rs1)
+ else
+ L(SEQ(acc, r), rs1)
+}
+
+def pAKC(rs: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
+ if (breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(rs.contains)) {//rs.flatMap(breakIntoTerms
+ AZERO
+ }
+ else{
+ r match {
+ case ASEQ(bs, r1, r2) =>
+ (pAKC(rs, 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"rs is ")
+ // rs.foreach(r => println(shortRexpOutput(r)))
+ rs0.map(r => pAKC(rs, 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 distinctBy5(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)){
+ distinctBy5(xs, acc)
+ }
+ else{
+ val pruned = pAKC(acc, x, Nil)
+ val newTerms = breakIntoTerms(erase(pruned))
+ pruned match {
+ case AZERO =>
+ distinctBy5(xs, acc)
+ case xPrime =>
+ xPrime :: distinctBy5(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))
case ALTS(r1, r2) => breakIntoTerms(r1) ::: breakIntoTerms(r2)
+ case ZERO => Nil
case _ => r::Nil
}
@@ -583,7 +699,7 @@
}
case (STAR(r1), S::bs) => {
val (v, bs1) = decode_aux(r1, bs)
- //println(v)
+ //(v)
val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
(Stars(v::vs), bs2)
}
@@ -614,10 +730,19 @@
decode(r, strong_blex_simp(internalise(r), s.toList))
}
+def strong_blexing_simp5(r: Rexp, s: String) : Val = {
+ decode(r, strong_blex_simp5(internalise(r), s.toList))
+}
+
+
def strongBlexer(r: Rexp, s: String) : Val = {
Try(strong_blexing_simp(r, s)).getOrElse(Failure)
}
+def strongBlexer5(r: Rexp, s: String): Val = {
+ Try(strong_blexing_simp5(r, s)).getOrElse(Failure)
+}
+
def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
case Nil => {
if (bnullable(r)) {
@@ -635,15 +760,36 @@
}
}
+def strong_blex_simp5(r: ARexp, s: List[Char]) : Bits = s match {
+ case Nil => {
+ if (bnullable(r)) {
+ //println(asize(r))
+ val bits = mkepsBC(r)
+ bits
+ }
+ else
+ throw new Exception("Not matched")
+ }
+ case c::cs => {
+ val der_res = bder(c,r)
+ val simp_res = strongBsimp5(der_res)
+ strong_blex_simp5(simp_res, cs)
+ }
+}
def bders_simp(s: List[Char], r: ARexp) : ARexp = s match {
case Nil => r
case c::s =>
- println(erase(r))
+ //println(erase(r))
bders_simp(s, bsimp(bder(c, r)))
}
+ def bdersStrong5(s: List[Char], r: ARexp) : ARexp = s match {
+ case Nil => r
+ case c::s => bdersStrong5(s, strongBsimp5(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 {
@@ -913,58 +1059,54 @@
}
def generator_test() {
- // println("XXX generates 10 random integers in the range 0..2")
- // println(range(0, 3).gen(10).mkString("\n"))
-
- // println("XXX gnerates random lists and trees")
- // println(lists.generate())
- // println(trees(chars).generate())
-
- // println("XXX generates 10 random characters")
- // println(chars.gen(10).mkString("\n"))
- // println("XXX generates 10 random leaf-regexes")
- // println(leaf_rexp().gen(10).mkString("\n"))
-
- // println("XXX generates 1000 regexes of maximal 10 height")
- // println(rexp(10).gen(1000).mkString("\n"))
-
- // println("XXX generates 1000 regexes and tests an always true-test")
- // test(rexp(10), 1000) { _ => true }
- // println("XXX generates regexes and tests a valid predicate")
- // test(rexp(10), 1000) { r => height(r) <= size(r) }
- // println("XXX faulty test")
- // test(rexp(10), 100) { r => height(r) <= size_faulty(r) }
-
+ // test(rexp(7), 1000) { (r: Rexp) =>
+ // val ss = stringsFromRexp(r)
+ // val boolList = ss.map(s => {
+ // val simpVal = simpBlexer(r, s)
+ // val strongVal = strongBlexer(r, s)
+ // // println(simpVal)
+ // // println(strongVal)
+ // (simpVal == strongVal) && (simpVal != None)
+ // })
+ // !boolList.exists(b => b == false)
+ // }
+ // test(single(STAR(ALTS(STAR(CHAR('c')),ALTS(CHAR('c'),ZERO)))), 100000) { (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))
+ // // println(shortRexpOutput(r))
+ // // println(s)
+ // // println(strongVal)
+ // // println(strongVal5)
+ // // (strongVal == strongVal5)
- /* For inspection of counterexamples should they arise*/
-// println("testing strongbsimp against bsimp")
-// val r = 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'))),
-// SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
-
-// val ss = stringsFromRexp(r)
-// val boolList = ss.map(s => {
-// val simpVal = simpBlexer(r, s)
-// val strongVal = strongBlexer(r, s)
-// println(simpVal)
-// println(strongVal)
-// (simpVal == strongVal) && (simpVal != None)
-// })
-// println(boolList)
-// println(boolList.exists(b => b == false))
-
-
- test(rexp(9), 100000) { (r: Rexp) =>
+ // if(asize(bdStrong5) > asize(bdStrong)){
+ // println(s)
+ // println(shortRexpOutput(erase(bdStrong5)))
+ // println(shortRexpOutput(erase(bdStrong)))
+ // }
+ // asize(bdStrong5) <= asize(bdStrong)
+ // })
+ // !boolList.exists(b => b == false)
+ // }
+ //test(rexp(3), 10000000) { (r: Rexp) =>
+ test(single(STAR(SEQ(SEQ(ALTS(CHAR('b'),STAR(CHAR('b'))),CHAR('b')),ALTS(ALTS(STAR(CHAR('c')),SEQ(CHAR('a'),CHAR('c'))),ALTS(ZERO,ONE))))), 1) {(r: Rexp) =>
val ss = stringsFromRexp(r)
val boolList = ss.map(s => {
- val simpVal = simpBlexer(r, s)
- val strongVal = strongBlexer(r, s)
- // println(simpVal)
- // println(strongVal)
- (simpVal == strongVal) && (simpVal != None)
+ val bdStrong = bdersStrong(s.toList, internalise(r))
+ val bdStrong5 = bdersStrong5(s.toList, internalise(r))
+ val size5 = asize(bdStrong5)
+ val size0 = asize(bdStrong)
+ println(s)
+ println(shortRexpOutput(erase(bdStrong5)))
+ println(shortRexpOutput(erase(bdStrong)))
+ println(size5, size0)
+ // println(s)
+ size5 <= size0
})
+ // println(boolList)
!boolList.exists(b => b == false)
}