# HG changeset patch # User Chengsong # Date 1650902418 -3600 # Node ID c730d018ebfaaa4709317034f4e998d5dbdd46aa # Parent 1481f465e6ead6d5235a628690ace7b27b22ccc6 blexer2 diff -r 1481f465e6ea -r c730d018ebfa thys2/SizeBoundStrong.thy --- a/thys2/SizeBoundStrong.thy Thu Apr 21 14:58:51 2022 +0100 +++ b/thys2/SizeBoundStrong.thy Mon Apr 25 17:00:18 2022 +0100 @@ -701,18 +701,28 @@ apply(simp_all) done +lemma bdersStrong_append: + shows "bdersStrong r (s1 @ s2) = bdersStrong (bdersStrong r s1) s2" + apply(induct s1 arbitrary: r) + apply simp+ + done + + lemma L_bsimp_ASEQ: "L (SEQ (erase r1) (erase r2)) = L (erase (bsimp_ASEQ bs r1 r2))" apply(induct bs r1 r2 rule: bsimp_ASEQ.induct) apply(simp_all) by (metis erase_fuse fuse.simps(4)) + + lemma L_bsimp_AALTs: "L (erase (AALTs bs rs)) = L (erase (bsimp_AALTs bs rs))" apply(induct bs rs rule: bsimp_AALTs.induct) apply(simp_all add: erase_fuse) done + lemma L_erase_AALTs: shows "L (erase (AALTs bs rs)) = \ (L ` erase ` (set rs))" apply(induct rs) @@ -971,18 +981,19 @@ 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 r1) ( ctx) )) 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)) | + bsimp_AALTs bs (filter (\r. r \ AZERO) (map (\r. pAKC_aux rsa r ( ctx) ) rs) ) | r \ r )" - inductive rrewrite:: "arexp \ arexp \ bool" ("_ \ _" [99, 99] 99) -where - "ASEQ bs AZERO r2 \ AZERO" + where + "pAKC_aux rsa a2 ONE = a2' \ AALTs bs (rsa @ [a2] @ rsb) \ AALTs bs (rsa @ [a2'] @ rsb)" + +| "ASEQ bs AZERO r2 \ AZERO" | "ASEQ bs r1 AZERO \ AZERO" | "ASEQ bs1 (AONE bs2) r \ fuse (bs1@bs2) r" | "r1 \ r2 \ ASEQ bs r1 r3 \ ASEQ bs r2 r3" @@ -994,7 +1005,6 @@ | "AALTs bs [] \ AZERO" | "AALTs bs [r] \ fuse bs r" | "erase a1 = erase a2 \ AALTs bs (rsa@[a1]@rsb@[a2]@rsc) \ AALTs bs (rsa@[a1]@rsb@rsc)" -| "pAKC_aux rsa a2 ONE = a2' \ AALTs bs (rsa @ [a2] @ rsb) \ AALTs bs (rsa @ [a2'] @ rsb)" inductive @@ -1040,13 +1050,15 @@ lemma contextrewrites1: "r \* r' \ (AALTs bs (r#rs)) \* (AALTs bs (r'#rs))" apply(induct r r' rule: rrewrites.induct) apply simp - by (metis append_Cons append_Nil rrewrite.intros(6) rs2) + + oops lemma contextrewrites2: "r \* r' \ (AALTs bs (rs1@[r]@rs)) \* (AALTs bs (rs1@[r']@rs))" apply(induct r r' rule: rrewrites.induct) apply simp - using rrewrite.intros(6) by blast + using rrewrite.intros(6) + oops diff -r 1481f465e6ea -r c730d018ebfa thys2/blexer2.sc --- 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) }