# HG changeset patch
# User Chengsong
# Date 1555168703 -3600
# Node ID 610f14009c0b0ae88536978e12273d2a2f957b4d
# Parent  4868c26268aad49cb871e72a9c062df7473630ff
the property
retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r
does not hold

diff -r 4868c26268aa -r 610f14009c0b Spiral.scala
--- a/Spiral.scala	Fri Apr 12 19:26:13 2019 +0100
+++ b/Spiral.scala	Sat Apr 13 16:18:23 2019 +0100
@@ -469,20 +469,45 @@
       println(cdbts)
       println("code v = retrieve internalise(r) v if |- v : r")
     }
+
+
+        val r_der_s = bders(st.toList, rg)
+    println(aregx_tree(r_der_s))
+    val bts = retrieve(r_der_s, unsimplified_vl)
+    val cdbts = code(unsimplified_vl)
+    val simprg = bsimp(r_der_s)
+    val frectv = decode(erase(simprg), cdbts)
+    val simpbts = retrieve(simprg, frectv)
+    if(bts == simpbts){
+      println("retrieve r v = retrieve (bsimp r) (decode bsimp(r) code(v))")
+      println("bits:")
+      //println(bts)
+      println(simpbts)
+      println("v = ")
+      println(unsimplified_vl)
+      println("frect v = ")
+      println(frectv)
+    }
     */
   def retrieve_experience(){
     val rg = ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) 
     val st = "abaab"
-    val vl = blexing_simp(erase(rg), st)
-    //println(vl)
-    val bts = retrieve(rg, vl)
-    val cdbts = code(vl)
-    val simprg = bsimp(rg)
-    val simpbts = retrieve(simprg, decode(erase(simprg), cdbts))
-    if(bts == simpbts){
-      println("retrieve r v = retrieve (bsimp r) (decode bsimp(r) code(v))")
-      println(bts)
-      println(simpbts)
+    val r_der_s = ders(st.toList, erase(rg))
+    val unsimplified_vl = mkeps(r_der_s)
+    val r_bder_s = bders( st.toList, rg)
+    val s_r_bder_s = bsimp(r_bder_s)
+    val bits1 = retrieve(r_bder_s, unsimplified_vl)
+    println(r_bder_s)
+    println(erase(r_bder_s))
+    println(s_r_bder_s)
+    println(erase(s_r_bder_s))
+    println(code(unsimplified_vl))
+    val bits2 = retrieve(s_r_bder_s, decode(erase(s_r_bder_s), code(unsimplified_vl)))
+    if(bits1 == bits2){
+      println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r")
+      println("Here v == mkeps r\\s and r == r\\s")
+      println(r_der_s, unsimplified_vl)
+      println(s_r_bder_s, erase(s_r_bder_s), code(unsimplified_vl))
     }
   }
   def radical_correctness(){
diff -r 4868c26268aa -r 610f14009c0b lex_blex_Frankensteined.scala
--- a/lex_blex_Frankensteined.scala	Fri Apr 12 19:26:13 2019 +0100
+++ b/lex_blex_Frankensteined.scala	Sat Apr 13 16:18:23 2019 +0100
@@ -140,9 +140,9 @@
   def retrieve(r: ARexp, v: Val): Bits = (r,v) match {
     case (AONE(bs), Empty) => bs
     case (ACHAR(bs, c), Chr(d)) => bs
+    case (AALTS(bs, a::Nil), v) => bs ++ retrieve(a, v)
     case (AALTS(bs, as), Left(v)) => bs ++ retrieve(as.head,v)
     case (AALTS(bs, as), Right(v)) => bs ++ retrieve(AALTS(Nil,as.tail),v)
-    case (AALTS(bs, a::Nil), v) => bs ++ retrieve(a, v)
     case (ASEQ(bs, a1, a2), Sequ(v1, v2)) => bs ++ retrieve(a1, v1) ++ retrieve(a2, v2)
     case (ASTAR(bs, a), Stars(Nil)) => bs ++ List(Z) 
     case (ASTAR(bs, a), Stars(v::vs)) => bs ++ List(S) ++ retrieve(a, v) ++ retrieve(ASTAR(Nil, a), Stars(vs))
@@ -457,13 +457,13 @@
     case r => r
   }
     
-  
-  //----------------------------------------------------------------------------experiment bsimp
-  /*
   def bders_simp (s: List[Char], r: ARexp) : ARexp = s match {
     case Nil => r
     case c::s => bders_simp(s, bsimp(bder(c, r)))
   }
+  //----------------------------------------------------------------------------experiment bsimp
+  /*
+
   */
   /*
   def time[T](code: => T) = {
@@ -484,7 +484,7 @@
   }
 
   def bpre_lexing(r: Rexp, s: String) = blex(internalise(r), s.toList)
-  //def blexing(r: Rexp, s: String) : Val = decode(r, blex(internalise(r), s.toList))
+  def blexing(r: Rexp, s: String) : Val = decode(r, blex(internalise(r), s.toList))
 
   var bder_time = 0L
   var bsimp_time = 0L