# HG changeset patch # User Christian Urban # Date 1552734922 0 # Node ID 0eaa1851a5b6ce9a6e1b9816ca6ea06b603aa1b9 # Parent ab7fe342e0041c8be29bfe523ac61dc67a1c57fd updated diff -r ab7fe342e004 -r 0eaa1851a5b6 exps/bit.scala --- a/exps/bit.scala Wed Mar 13 12:31:03 2019 +0000 +++ b/exps/bit.scala Sat Mar 16 11:15:22 2019 +0000 @@ -32,7 +32,9 @@ abstract class Rexp case object ZERO extends Rexp case object ONE extends Rexp -case class PRED(f: Char => Boolean, s: String = "_") extends Rexp +case class PRED(f: Char => Boolean, s: String = "_") extends Rexp { + override def toString = "'" ++ s ++ "'" +} case class ALTS(rs: List[Rexp]) extends Rexp case class SEQ(r1: Rexp, r2: Rexp) extends Rexp case class STAR(r: Rexp) extends Rexp @@ -49,7 +51,9 @@ abstract class ARexp case object AZERO extends ARexp case class AONE(bs: Bits) extends ARexp -case class APRED(bs: Bits, f: Char => Boolean, s: String = "_") extends ARexp +case class APRED(bs: Bits, f: Char => Boolean, s: String = "_") extends ARexp { + override def toString = "'" ++ s ++ "'" +} case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp case class ASTAR(bs: Bits, r: ARexp) extends ARexp @@ -94,29 +98,39 @@ // string of a regular expressions - for testing purposes -def string(r: Rexp): String = r match { +def string(r: Rexp, s: String = ""): String = r match { case ZERO => "0" case ONE => "1" - case PRED(_, s) => s - case ALTS(rs) => rs.map(string).mkString("[", "|", "]") - case SEQ(r1, r2) => s"(${string(r1)} ~ ${string(r2)})" - case STAR(r) => s"{${string(r)}}*" - case RECD(x, r) => s"(${x}! ${string(r)})" + case PRED(_, s1) => s1 + case ALTS(rs) => rs.map(string(_, s ++ " ")).mkString("[", ",\n" ++ s ++ "|", "]") + case SEQ(r1, r2) => { + val s1 = string(r1, s) + val i = (s1 ++ "\n").toList.indexOf('\n') + val s2 = string(r2, (" " * i) + " ") + s"${s1} ~ ${s2}" + } + case STAR(r) => s"<${string(r, s ++ " ")}>*" + case RECD(x, r) => s"(${x}! ${string(r, s)})" } def strings(rs: Set[Rexp]): String = - rs.map(string).mkString("{", "|", "}") + rs.map(string(_, "")).mkString("{", ",\n|", "}") // string of an annotated regular expressions - for testing purposes - -def astring(a: ARexp): String = a match { +def astring(a: ARexp, s: String = ""): String = a match { case AZERO => "0" case AONE(_) => "1" case APRED(_, _, s) => s - case AALTS(_, rs) => rs.map(astring).mkString("[", "|", "]") - case ASEQ(_, r1, r2) => s"(${astring(r1)} ~ ${astring(r2)})" - case ASTAR(_, r) => s"{${astring(r)}}*" + case AALTS(_, rs) => rs.map(astring(_, s ++ " ")).mkString("[", ",\n" ++ s ++ "|", "]") + case ASEQ(_, r1, r2) => { + val s1 = astring(r1, s) + val i = (s1 ++ "\n").toList.indexOf('\n') + val s2 = astring(r2, (" " * i) + " ") + s"${s1} ~ ${s2}" + } + case ASTAR(_, r) => s"<${astring(r, s ++ " ")}>*" } + //-------------------------------------------------------------- @@ -302,8 +316,6 @@ case c::cs => pder(c, r).flatMap(pders_simp(cs, _)).map(simp(_)._1) } -def psize(rs: Set[Rexp]) = - rs.map(size).sum //-------------------------------------------------------------------- // BITCODED PART @@ -323,6 +335,8 @@ case ZERO => AZERO case ONE => AONE(Nil) case PRED(f, s) => APRED(Nil, f, s) + case ALTS(List(r1)) => + AALTS(Nil, List(fuse(List(Z), internalise(r1)))) case ALTS(List(r1, r2)) => AALTS(Nil, List(fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2)))) case ALTS(r1::rs) => { @@ -433,19 +447,24 @@ case r1 :: rs2 => r1 :: flats(rs2) } +def stack(r1: ARexp, r2: ARexp) = r1 match { + case AONE(bs2) => fuse(bs2, r2) + case _ => ASEQ(Nil, r1, r2) +} + def bsimp(r: ARexp): ARexp = r match { case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match { case (AZERO, _) => AZERO case (_, AZERO) => AZERO case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) - //case (AALTS(bs2, rs), r2s) => - // AALTS(bs1 ++ bs2, rs.map(ASEQ(Nil, _, r2s))) + case (AALTS(bs2, rs), r2s) => + AALTS(bs1 ++ bs2, rs.map(stack(_, r2s))) case (r1s, r2s) => ASEQ(bs1, r1s, r2s) } case AALTS(bs1, rs) => distinctBy(flats(rs.map(bsimp)), erase) match { case Nil => AZERO case r :: Nil => fuse(bs1, r) - case rs => AALTS(bs1, rs) + case rs2 => AALTS(bs1, rs2) } //case ASTAR(bs1, r1) => ASTAR(bs1, bsimp(r1)) case r => r @@ -479,8 +498,8 @@ case (AZERO, _) => AZERO case (_, AZERO) => AZERO case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s) - //case (AALTS(bs2, rs), r2s) => - // AALTS(bs1 ++ bs2, rs.map(ASEQ(Nil, _, r2s))) + case (AALTS(bs2, rs), r2s) => + AALTS(bs1 ++ bs2, rs.map(ASEQ(Nil, _, r2s))) case (r1s, r2s) => ASEQ(bs1, r1s, r2s) } case AALTS(bs1, rs) => distinctBy(flats(rs.map(bsimp_full)), erase) match { @@ -636,6 +655,8 @@ def asize(a: ARexp) = size(erase(a)) +def psize(rs: Set[Rexp]) = rs.map(size).sum + // Lexing Rules for a Small While Language @@ -679,10 +700,29 @@ // Some Small Tests //================== +// string of a regular expressions - for testing purposes + + +string(ALTS(List("a","b",ALTS(List("0","1","2")),"c"))) +string(ALTS(List("a","b",ALTS(List("0","1",ALTS(List("X","Y")),"2")),"c"))) +string(ALTS(List("aa","b",ALTS(List("0","1","2")),"c"))) +string(ALTS(List("aa","b",SEQ("Q", ALTS(List("0","1","2"))),"c"))) +string(ALTS(List("aa","b",SEQ(SEQ("Q", ALTS(List("0","1","2"))),"W"),"c"))) +string(ALTS(List("aa","b",SEQ("Q", STAR(ALTS(List("0","1","2")))),"c"))) +string(ALTS(List("aaa","bbbb",ALTS(List("000","1111","2222")),"ccccc"))) + println("Small tests") -val q = STAR(STAR("bb" | ("a" | "b"))) -val qs = "bb" +val q = STAR(STAR(STAR(ALTS(List(ALTS(List(CHAR('c'), CHAR('b'))), SEQ(CHAR('c'),CHAR('c'))))))) +val qs = "cccc" + +//val q = STAR(STAR("bb" | ("a" | "b"))) +//val qs = "bbbbbbb" + +println("Size Bit " + asize(bders_simp(qs.toList, internalise(q)))) +println("Size Pder " + psize(pders_simp(qs.toList, q))) +println(astring(bders_simp(qs.toList, internalise(q)))) +println(strings(pders_simp(qs.toList, q))) println("Size Bit " + asize(bders_simp(qs.toList, internalise(q)))) println("Size Bitf " + asize(bders_simp_full(qs.toList, internalise(q)))) @@ -692,11 +732,13 @@ println("Size Pder simp " + psize(pders_simp(qs.toList, q))) println(astring(bders_simp(qs.toList, internalise(q)))) -println(astring(bders_simp_full(qs.toList, internalise(q)))) -println(string(ders_simp(qs.toList, q))) -println(strings(pders(qs.toList, q))) +//println(astring(bders_simp_full(qs.toList, internalise(q)))) +//println(string(ders_simp(qs.toList, q))) +//println(strings(pders(qs.toList, q))) println(strings(pders_simp(qs.toList, q))) + + System.exit(0) val re1 = STAR("a" | "aa") diff -r ab7fe342e004 -r 0eaa1851a5b6 thys/BitCoded.thy --- a/thys/BitCoded.thy Wed Mar 13 12:31:03 2019 +0000 +++ b/thys/BitCoded.thy Sat Mar 16 11:15:22 2019 +0000 @@ -873,31 +873,152 @@ apply(simp) oops -function (sequential) bretrieve :: "arexp \ bit list \ (bit list) * (bit list)" where - "bretrieve (AZERO) bs1 = ([], bs1)" -| "bretrieve (AONE bs) bs1 = (bs, bs1)" -| "bretrieve (ACHAR bs c) bs1 = (bs, bs1)" -| "bretrieve (AALTs bs rs) [] = (bs, [])" -| "bretrieve (AALTs bs [r]) bs1 = - (let (bs2, bs3) = bretrieve r bs1 in (bs @ bs2, bs3))" -| "bretrieve (AALTs bs (r#rs)) (Z#bs1) = - (let (bs2, bs3) = bretrieve r bs1 in (bs @ [Z] @ bs2, bs3))" -| "bretrieve (AALTs bs (r#rs)) (S#bs1) = - (let (bs2, bs3) = bretrieve (AALTs [] rs) bs1 in (bs @ [S] @ bs2, bs3))" -| "bretrieve (ASEQ bs r1 r2) bs1 = - (let (bs2, bs3) = bretrieve r1 bs1 in - let (bs4, bs5) = bretrieve r2 bs3 in (bs @ bs2 @ bs4, bs5))" -| "bretrieve (ASTAR bs r) [] = (bs, [])" -| "bretrieve (ASTAR bs r) (S#bs1) = (bs @ [S], bs1)" -| "bretrieve (ASTAR bs r) (Z#bs1) = - (let (bs2, bs3) = bretrieve r bs1 in - let (bs4, bs5) = bretrieve (ASTAR [] r) bs3 in (bs @ bs2 @ [Z] @ bs4, bs5))" - by (pat_completeness) (auto) +fun vsimp :: "arexp \ val \ val" + where + "vsimp (ASEQ _ (AONE _) r) (Seq v1 v2) = vsimp r v1" +| "vsimp _ v = v" + +lemma fuse_vsimp: + assumes "\ v : (erase r)" + shows "vsimp (fuse bs r) v = vsimp r v" + using assms + apply(induct r arbitrary: v bs) + apply(simp_all) + apply(case_tac "\bs. r1 = AONE bs") + apply(auto) + apply (metis Prf_elims(2) vsimp.simps(1)) + apply(erule Prf_elims) + apply(auto) + apply(case_tac r1) + apply(auto) + done + + +lemma retrieve_XXX0: + assumes "\r v. \r \ set rs; \ v : erase r\ \ + \v'. \ v' : erase (bsimp r) \ retrieve (bsimp r) v' = retrieve r v" + "\ v : erase (AALTs bs rs)" + shows "\v'. \ v' : erase (bsimp_AALTs bs (flts (map bsimp rs))) \ + retrieve (bsimp_AALTs bs (flts (map bsimp rs))) v' = retrieve (AALTs bs rs) v" + using assms +apply(induct rs arbitrary: bs v taking: size rule: measure_induct) + apply(case_tac x) + apply(simp) + using Prf_elims(1) apply blast + apply(simp) + apply(case_tac list) + apply(simp_all) + apply(case_tac a) + apply(simp_all) + using Prf_elims(1) apply blast + apply (metis erase.simps(2) fuse.simps(2) retrieve_fuse2) + using Prf_elims(5) apply force + apply(erule Prf_elims) + apply(auto)[1] + + + + + apply(simp) + apply(erule Prf_elims) + using Prf_elims(1) apply b last + apply(auto) + apply (metis append_Ni l2 erase_fuse fuse.simps(4) retrieve_fuse2) + apply(case_tac rs) + apply(auto) + + + oops + +fun get where + "get (Some v) = v" -termination - sorry + +lemma retrieve_XXX: + assumes "\ v : erase r" + shows "\ get (decode (code v) (erase (bsimp r))) : erase (bsimp r)" + using assms +apply(induct r arbitrary: v) + apply(simp) + using Prf_elims(1) apply auto[1] + apply(simp) + apply (simp add: decode_code) + apply(simp) + apply (simp add: decode_code) + apply(simp) + apply(erule Prf_elims) + apply(simp) + apply(case_tac "r1 = AZERO") + apply(simp) + apply (meson Prf_elims(1) Prf_elims(2)) + apply(case_tac "r2 = AZERO") + apply(simp) + apply (meson Prf_elims(1) Prf_elims(2)) + apply(case_tac "\bs. bsimp r1 = AONE bs") + apply(clarify) + apply(simp) + apply(subst bsimp_ASEQ2) + apply(subst bsimp_ASEQ2) + apply(simp add: erase_fuse) + defer + apply(subst bsimp_ASEQ1) + using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce + using L_bsimp_erase L_ -thm Prf.intros +lemma retrieve_XXX: + assumes "\ v : erase r" + shows "\ (vsimp (bsimp r) v : erase (bsimp r) \ retrieve (bsimp r) (vsimp (bsimp r) v) = retrieve r v" + using assms + apply(induct r arbitrary: v) + apply(simp) + using Prf_elims(1) apply blast + apply(simp) + using Prf_elims(4) apply fastforce + apply(simp) + apply blast + apply simp + apply(case_tac "r1 = AZERO") + apply(simp) + apply (meson Prf_elims(1) Prf_elims(2)) + apply(case_tac "r2 = AZERO") + apply(simp) + apply (meson Prf_elims(1) Prf_elims(2)) + apply(erule Prf_elims) + apply(simp) + apply(case_tac "\bs. bsimp r1 = AONE bs") + apply(clarify) + apply(simp) + apply(subst bsimp_ASEQ2) + defer + apply(subst bsimp_ASEQ1) + using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce + using L_bsimp_erase L_flat_Prf1 L_flat_Prf2 apply fastforce + apply(simp) + apply(simp) + apply(drule_tac x="v1" in meta_spec) + apply(drule_tac x="v2" in meta_spec) + apply(simp) + apply(clarify) + apply(rule_tac x="Seq v' v'a" in exI) + apply(simp) + apply (metis Prf.intros(1) Prf_elims(1) bsimp_ASEQ1 erase.simps(1) retrieve.simps(6)) + prefer 3 + apply(drule_tac x="v1" in meta_spec) + apply(drule_tac x="v2" in meta_spec) + apply(simp) + apply(clarify) + apply(rule_tac x="v'a" in exI) + apply(subst bsimp_ASEQ2) + apply (metis Prf_elims(4) append_assoc erase_fuse retrieve.simps(1) retrieve_fuse2) + prefer 2 + apply(auto) + apply(case_tac "x2a") + apply(simp) + using Prf_elims(1) apply blast + apply(simp) + apply(case_tac "list") + apply(simp) + sorry lemma retrieve_XXX: @@ -958,10 +1079,11 @@ lemma TEST: assumes "\ v : ders s r" - shows "retrieve (bders (intern r) s) v = retrieve (bsimp (bders (intern r) s)) v" + shows "\v'. retrieve (bders (intern r) s) v' = retrieve (bsimp (bders (intern r) s)) v" using assms apply(induct s arbitrary: r v rule: rev_induct) apply(simp) + defer apply(simp add: ders_append) apply(frule Prf_injval)