updated
authorChristian Urban <urbanc@in.tum.de>
Sat, 16 Mar 2019 11:15:22 +0000
changeset 316 0eaa1851a5b6
parent 315 ab7fe342e004
child 317 db0ff630bbb7
updated
exps/bit.scala
thys/BitCoded.thy
--- 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")
--- 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 \<Rightarrow> bit list \<Rightarrow> (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 \<Rightarrow> val \<Rightarrow> val"
+  where
+  "vsimp (ASEQ _ (AONE _) r) (Seq v1 v2) = vsimp r v1"
+| "vsimp _ v = v" 
+
+lemma fuse_vsimp:
+  assumes "\<Turnstile> 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 "\<exists>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 "\<And>r v. \<lbrakk>r \<in> set rs; \<Turnstile> v : erase r\<rbrakk> \<Longrightarrow> 
+              \<exists>v'. \<Turnstile> v' : erase (bsimp r) \<and> retrieve (bsimp r) v' = retrieve r v"
+          "\<Turnstile> v : erase (AALTs bs rs)"
+        shows "\<exists>v'. \<Turnstile> v' : erase (bsimp_AALTs bs (flts (map bsimp rs))) \<and>
+                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 "\<Turnstile> v : erase r" 
+  shows "\<Turnstile> 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 "\<exists>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 "\<Turnstile> v : erase r" 
+  shows "\<Turnstile> (vsimp (bsimp r) v : erase (bsimp r)  \<and> 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 "\<exists>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 "\<Turnstile> v : ders s r"
-  shows "retrieve (bders (intern r) s) v = retrieve (bsimp (bders (intern r) s)) v"
+  shows "\<exists>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)