--- a/thys2/blexer2.sc Thu Jun 09 22:08:06 2022 +0100
+++ b/thys2/blexer2.sc Sun Jun 12 17:03:09 2022 +0100
@@ -915,6 +915,11 @@
res.toSet
}
+def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] = {
+ val res = turnIntoTerms((L(r, ctx))).map(oneSimp)
+ res.toSet
+}
+
def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, subseteqPred: (C, C) => Boolean) : Boolean = {
subseteqPred(f(a, b), c)
}
@@ -923,7 +928,9 @@
res
}
def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
- if (ABIncludedByC(r, ctx, acc, attachCtx, rs1_subseteq_rs2)) {//acc.flatMap(breakIntoTerms
+ if (ABIncludedByC(a = r, b = ctx, c = acc,
+ f = attachCtx, subseteqPred = rs1_subseteq_rs2))
+ {//acc.flatMap(breakIntoTerms
AZERO
}
else{
@@ -951,6 +958,36 @@
}
}
+def prune6cc(acc: Set[Rexp], r: Rexp, ctx: List[Rexp]) : Rexp = {
+ if (ABIncludedByC(a = r, b = ctx, c = acc,
+ f = attachCtxcc, subseteqPred = rs1_subseteq_rs2))
+ {//acc.flatMap(breakIntoTerms
+ ZERO
+ }
+ else{
+ r match {
+ case SEQ(r1, r2) =>
+ (prune6cc(acc, r1, r2 :: ctx)) match{
+ case ZERO =>
+ ZERO
+ case ONE =>
+ r2
+ case r1p =>
+ SEQ(r1p, r2)
+ }
+ case ALTS(r1, r2) =>
+ List(r1, r2).map(r => prune6cc(acc, r, ctx)).filter(_ != AZERO) match {
+ case Nil =>
+ ZERO
+ case r :: Nil =>
+ r
+ case ra :: rb :: Nil =>
+ ALTS(ra, rb)
+ }
+ case r => r
+ }
+ }
+}
def distinctBy6(xs: List[ARexp], acc: Set[Rexp] = Set()) : List[ARexp] = xs match {
case Nil =>
@@ -973,6 +1010,26 @@
}
}
+def distinctByacc(xs: List[Rexp], acc: Set[Rexp] = Set()) : Set[Rexp] = xs match {
+ case Nil =>
+ acc
+ case x :: xs => {
+ if(acc.contains(x)){
+ distinctByacc(xs, acc)
+ }
+ else{
+ val pruned = prune6cc(acc, x, Nil)
+ val newTerms = turnIntoTerms(pruned)
+ pruned match {
+ case ZERO =>
+ distinctByacc(xs, acc)
+ case xPrime =>
+ distinctByacc(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)
@@ -1380,21 +1437,23 @@
// }
}
-naive_matcher()
+// naive_matcher()
def generator_test() {
- test(rexp(4), 1000000) { (r: Rexp) =>
+ test(single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
+ SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))), 1) { (r: Rexp) =>
// ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) =>
- val ss = Set("b")//stringsFromRexp(r)
- val boolList = ss.filter(s => s != "").map(s => {
+ val ss = stringsFromRexp(r)
+ val boolList = ss.map(s => {
//val bdStrong = bdersStrong(s.toList, internalise(r))
- val bdStrong6 = bdersStrong7(s.toList, internalise(r))
+ val bdStrong6 = bdersStrong6(s.toList, internalise(r))
val bdStrong6Set = turnIntoTerms(erase(bdStrong6))
val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
- bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size
+ rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList))
+ //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
+ //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size
})
- //println(boolList)
//!boolList.exists(b => b == false)
!boolList.exists(b => b == false)
}
@@ -1408,13 +1467,19 @@
// CHAR('c')))))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE)))//STAR(SEQ(ALTS(STAR(CHAR('c')),CHAR('c')),SEQ(ALTS(CHAR('c'),ONE),ONE)))
//counterexample1: STAR(SEQ(ALTS(STAR(ZERO),ALTS(CHAR(a),CHAR(b))),SEQ(ONE,ALTS(CHAR(a),CHAR(b)))))
//counterexample2: SEQ(ALTS(SEQ(CHAR(a),STAR(ONE)),STAR(ONE)),ALTS(CHAR(a),SEQ(ALTS(CHAR(c),CHAR(a)),CHAR(b))))
+
+//new ce1 : STAR(SEQ(ALTS(ALTS(ONE,CHAR(a)),SEQ(ONE,CHAR(b))),ALTS(CHAR(a),ALTS(CHAR(b),CHAR(a)))))
+//new ce2 : ALTS(CHAR(b),SEQ(ALTS(ZERO,ALTS(CHAR(b),CHAR(b))),ALTS(ALTS(CHAR(a),CHAR(b)),SEQ(CHAR(c),ONE))))
+//new ce3 : SEQ(CHAR(b),ALTS(ALTS(ALTS(ONE,CHAR(a)),SEQ(CHAR(c),ONE)),SEQ(STAR(ZERO),SEQ(ONE,CHAR(b)))))
def counterexample_check() {
- val r = SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
- ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
+ val r = SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
+ SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
+ //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
val s = "b"
val bdStrong5 = bdersStrong7(s.toList, internalise(r))
- val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
+ val bdStrong5Set = turnIntoTerms(erase(bdStrong5))
val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
+ val apdersSet = pdersSet.map(internalise)
println("original regex ")
rprint(r)
println("after strong bsimp")
@@ -1423,9 +1488,23 @@
rsprint(bdStrong5Set)
println("after pderUNIV")
rsprint(pdersSet.toList)
+ println("pderUNIV distinctBy6")
+ //asprint(distinctBy6(apdersSet.toList))
+ rsprint(distinctByacc(pdersSet.toList))
+ // rsprint(turnIntoTerms(pdersSet.toList(3)))
+ // println("NO 3 not into terms")
+ // rprint((pdersSet.toList()))
+ // println("after pderUNIV broken")
+ // rsprint(pdersSet.flatMap(r => turnIntoTerms(r)).toList)
}
-// counterexample_check()
+counterexample_check()
+
+def breakable(r: Rexp) : Boolean = r match {
+ case SEQ(ALTS(_, _), _) => true
+ case SEQ(r1, r2) => breakable(r1)
+ case _ => false
+}
def linform_test() {
val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) //