--- a/Spiral.scala	Wed May 08 22:09:59 2019 +0100
+++ b/Spiral.scala	Tue Jun 25 18:56:52 2019 +0100
@@ -488,49 +488,56 @@
       println("frect v = ")
       println(frectv)
     }
-    */
-  def retrieve_experience(){
-    for(i <- 1 to 100){
-      val rg = internalise(balanced_struct_gen(1))//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 = "ab"//"abaab"
-      val r_der_s = ders(st.toList, erase(rg))
-      if(nullable(r_der_s)){
-        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(internalise(r_der_s), unsimplified_vl)
-        println("The property: ")
-        println("retrieve ar v = retrieve (bsimp ar) (decode erase(bsimp(ar)) code(v)) if |- v : r")
-        println("does not hold.")
-        println("Here v == mkeps r\\s and r == r\\s")
-        println("regular expression is")
-        println(rg)
-        println("string is")
-        println(st)
-        println("derivative without simplification is ")
-        
-        println(r_bder_s)
+    *///KH8W5BXL
+  def nice_lex(r: Rexp, s: List[Char], ar: ARexp) : Val = s match {
+    case Nil => 
+    if (nullable(r)){
+      val vr = mkeps(r)
+      val bits1 = retrieve(ar, vr)
+      val av = bsimp2(ar, vr)
+      val bits2 = retrieve(av._1, av._2)
+      if(bits1 != bits2) throw new Exception("bsimp2 does not work")
+      vr
+    }  
+    else throw new Exception("Not matched")
+    case c::cs => { 
+      val vr = inj(r, c, nice_lex(der(c, r), cs, bder(c, ar)));
+      val bits1 = retrieve(ar, vr);
+      val av = bsimp2(ar, vr);
+      val bits2 = retrieve(av._1, av._2);
+      if(bits1 != bits2) throw new Exception("bsimp2 does not work");
+      vr 
+    }
+  }
+  def test_bsimp2(){
+    for(i <- 1 to 1000){
+      val rg = (balanced_struct_gen(9))//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 = rd_string_gen(3, 4)
+      val a = internalise(rg)
+      val final_derivative = ders(st.toList, rg)
+      if(nullable(final_derivative))
+        nice_lex(rg, st.toList, a)
+    }
+  }
 
-        println("after erase of this derivative")
-        println(erase(r_bder_s))
-        println("simplification of derivative (bsimp(ar))")
-        println(s_r_bder_s)
-        println("after erase of simplified derivative (erase(bsimp(ar))")
-        println(erase(s_r_bder_s))
-        println("decode says the above regex and the below bits(code(v)) are not decodable")
-        println(unsimplified_vl)
-        println(code(unsimplified_vl))
-        println(bits1)
-        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 neat_retrieve(){
+    for(i <- 1 to 1000){
+      val rg = internalise(balanced_struct_gen(6))//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 = rd_string_gen(3, 5)
+      val final_derivative = ders(st.toList, erase(rg))
+      if(nullable(final_derivative)){
+        val unsimplified_vl = mkeps(final_derivative)
+        val arexp_for_retrieve = bders( st.toList, rg)
+        val simp_ar_vl = bsimp2(arexp_for_retrieve, unsimplified_vl)
+        val bits1 = retrieve(arexp_for_retrieve, unsimplified_vl)
+        val bits2 = retrieve(simp_ar_vl._1, simp_ar_vl._2)
+        if(bits1 != bits2){
+          println("nOOOOOOOOOO!")
         }
       }
     }
+  }
+
   def radical_correctness(){
     enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
     random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet
@@ -539,16 +546,18 @@
     val r = ALTS(List(SEQ(ZERO,CHAR('b')), ONE))
     val v = Right(Empty)
     val a = internalise(r)
-    val as = bsimp(a)
+    val a_v = bsimp2(a,v)
     println(s"Testing ${r} and ${v}")
     println(s"internalise(r) = ${a}")
+    println(s"a_v = ${a_v}")
     val bs1 = retrieve(a, v)
     println(bs1)
-    println(s"as = ${as}")
+    println(s"as = ${a_v._1}")
     //val bs2 = retrieve(as, decode(erase(as), bs1))
-    val bs3 = retrieve(as, decode(erase(as), bs1.tail))
-    println(decode(erase(as), bs1.tail))
-    println(bs3)
+    val bs3 = retrieve(a_v._1, a_v._2)//decode(erase(as), bs1) does not work
+    //println(decode(erase(as), bs1))
+    println(s"bs1=${bs1}, bs3=${bs3}")
+    //println(decode(erase(a_v._1), bs3))
   }
   def essence_posix(){
     //val s = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
@@ -567,8 +576,10 @@
     //radical_correctness()
     //correctness_proof_convenient_path()
     //retrieve_experience()
+    //neat_retrieve()
+    test_bsimp2()
     //christian_def()
-    essence_posix()
+    //essence_posix()
   } 
 }