# HG changeset patch
# User Chengsong
# Date 1578608409 0
# Node ID d486c12deeab131f53d487e05e5894c404585692
# Parent  aaa2f2b52baff26534fcf00c97e5ab99c8c2f04b
h

diff -r aaa2f2b52baf -r d486c12deeab Spiral.scala
--- a/Spiral.scala	Wed Nov 27 14:15:00 2019 +0000
+++ b/Spiral.scala	Thu Jan 09 22:20:09 2020 +0000
@@ -432,6 +432,158 @@
         weak_sub_check(big_panda, str_panda, 6, size_expansion_rate)
 
   }
+  def bstostick(bs: List[Bit]): Element = bs match {
+    //case b::Nil => elem(b.toString)
+    case b::bs1 => elem(b.toString) beside bstostick(bs1)
+    case Nil => elem(' ', 1, 1)
+  }
+  def bits_print(r: ARexp): Element = r match {
+    case AALTS(bs,rs) => {
+      val bitstick = bstostick(bs)
+      rs match {
+        case r::rs1 =>  
+        rs1.foldLeft( 
+        ((elem("(") left_align bitstick) beside 
+        bits_print(r))  )( (acc, r2) => acc beside ((elem(" + ") above elem("   ")) beside bits_print(r2) )) beside
+        elem(")")
+        case Nil => elem(' ', 1, 1)
+      }
+    }
+    case ASEQ(bs, r1, r2) => {
+      ((elem("[") left_align bstostick(bs)) beside  bits_print(r1) beside elem("~") beside bits_print(r2)) 
+    }
+    case ASTAR(bs, r) => {
+      r match {
+        case AONE(_) | AZERO | ACHAR(_, _) => {
+          (elem("{") left_align bstostick(bs)) beside (bits_print(r) beside elem("}*")) 
+        }
+        case _ => {
+          (elem("{") left_align bstostick(bs)) beside (bits_print(r) beside elem("}*")) 
+        }
+      }
+    }
+    case AONE(bs) => {
+      elem("1") left_align bstostick(bs)
+    }
+    case ACHAR(bs, c) => {
+      elem(c, 1, 1) left_align bstostick(bs)
+    }
+    case AZERO =>
+    {
+      elem ("0") above elem(" ")
+    }
+  }
+  def happy_print(r: Rexp): Unit = r match {
+    case ALTS( r::rs ) => {
+      print("(")
+      happy_print(r)
+      rs.map(r2=>{      
+        print(" + ")
+        happy_print(r2)
+      })
+      print(")")
+    }
+    case SEQ(r1, r2) => {
+      happy_print(r1)
+      print("~")
+      happy_print(r2)
+    }
+    case STAR(r) => {
+      r match {
+        case ONE | ZERO | CHAR(_) => {
+          happy_print(r)
+          print("*")
+        }
+        case _ => {
+          print("[")
+          happy_print(r)
+          print("]*")
+        }
+      }
+    }
+    case ONE => {
+      print("1")
+    }
+    case ZERO => {
+      print("0")
+    }
+    case CHAR(c) =>{
+      print(c)
+    }
+  }
+  def bits_slide(s: String, r: Rexp){
+    val nangao = ders_simp(internalise(r), s.toList)
+    val easy = bsimp(bders(s.toList, internalise(r)))
+    println(s)
+    println(r)
+    happy_print(r)
+    println()
+    print(bits_print(nangao))
+    println()
+    print(bits_print(easy))
+    println()
+  }
+  //found r = SEQ(ALTS(List(CHAR(c), CHAR(a))),SEQ(ALTS(List(CHAR(a), CHAR(c))),ALTS(List(CHAR(b), CHAR(c))))) s = "aa"
+    def bsimp_print(r: ARexp): Unit = r match {
+    case ASEQ(bs, r1, r2) => 
+      {
+        println("0.r or r.0 to 0 or bs1 1.r to fuse bs++bs1 r")
+        bits_print(bsimp(r1))
+        bits_print(bsimp(r2))
+      }
+    case AALTS(bs, rs) => {
+      println("rs.map(bsimp) equals *************")
+      val rs_simp = rs.map(bsimp)
+      for(r <- rs_simp){
+        println(bits_print(r))
+      }
+      println("*************")
+      println("flts(rs_simp)")
+      val flat_res = flats(rs_simp)
+      for(r <- flat_res){
+        println(bits_print(r))
+      }
+      println("dB(flat_res)")
+      val dist_res = distinctBy(flat_res, erase)
+      for(r <- dist_res){
+        println(bits_print(r))
+      }
+      dist_res match {
+        case Nil => println("AZERO")
+        case r::Nil => println("fuse(bs, r)")
+        case rs => println("AALTS(bs, rs)")
+      }
+    }
+    case _ => println("No simp at this level")
+  }
+  def tellmewhy(){
+    //val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(ALTS(List(CHAR('a'), CHAR('a'))), STAR(CHAR('a'))))) 
+    val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(CHAR('a'), STAR(CHAR('a')) ) ))
+    //val r = ("a"|"b")~("a")
+    val s = "aa"
+    for(i <- 0 to s.length-1){
+      val ss = s.slice(0, i+1)
+      val nangao = ders_simp(internalise(r), ss.toList)
+      val easy = (bders(ss.toList, internalise(r)))
+      println(bits_print(nangao))
+      println(bits_print(easy))
+      println()
+      bsimp_print(easy)
+    }
+    println(bits_print(bsimp(bders(s.toList, internalise(r)))))
+    println(bits_print(ders_simp(internalise(r), s.toList))
+  }
+  def find_re(){
+    for (i <- 1 to 10000){
+      val r = balanced_struct_gen(3)
+      val s = rd_string_gen(2,1)
+      val nangao = ders_simp(internalise(r), s.toList)
+      val easy = bsimp(bders(s.toList, internalise(r)))
+      if(nangao != easy){
+        bits_slide(s, r)
+      }
+    }
+  }
   //simplified regex size 291, so called pd_simp size 70 (did not do simplification to terms in the PD set)
   def pushbits(r: ARexp): ARexp = r match {
     case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
@@ -439,8 +591,6 @@
     case r => r
   }
   def correctness_proof_convenient_path(){
-    for(i <- 1 to 10000)
-    {
         val s = "abab"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
         val r = ("ab"| SEQ(ONE, "ab"))//internalise(random_struct_gen(4))//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")))) //random_struct_gen(7)
         for(j <- 0 to s.length - 1){
@@ -462,7 +612,6 @@
             println(annotated_tree(easy))
           }
         }
-    }
   }
   /*    if(bts == cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
       println(bts)
@@ -652,7 +801,7 @@
   def closed_string_der(r1: ARexp, r2: ARexp, s: String): ARexp = {
     val l1 = der_seq(r1, s.toList, Nil)
     val l2 = der_seq_rev(r2, s.toList, Nil)
-    val Re = re_close(l1.reverse, l2, ASEQ(List(), l1.last, l2.head))
+    val Re = re_close((l1.reverse).tail, l2.tail, ASEQ(List(), l1.last, l2.head))
     print(Re)
     val Comp = bders( s.toList, ASEQ(List(), r1, r2))
     print(Comp  )
@@ -688,7 +837,10 @@
   }
 
   def main(args: Array[String]) {
-    string_der_test()
+    //println(S.toString)
+    //find_re()
+    tellmewhy()
+    //string_der_test()
     //comp(rd_string_gen(3,6).toList, random_struct_gen(7))
     //newxp1()
   //contains7()
@@ -705,4 +857,4 @@
     //speed_test()
   } 
 }
-
+//List(              ASTAR(List(Z),ACHAR(List(),a)),            AALTS(List(S),List(ACHAR(List(Z),b), ACHAR(List(S),a)))       )
diff -r aaa2f2b52baf -r d486c12deeab corr_pr_sketch.pdf
Binary file corr_pr_sketch.pdf has changed
diff -r aaa2f2b52baf -r d486c12deeab lex_blex_Frankensteined.scala
--- a/lex_blex_Frankensteined.scala	Wed Nov 27 14:15:00 2019 +0000
+++ b/lex_blex_Frankensteined.scala	Thu Jan 09 22:20:09 2020 +0000
@@ -203,6 +203,7 @@
     case c::cs => if(nullable(c)) re_closeo(cs, l2.tail, ALT(re_init,  l2.head)  ) 
     else re_closeo(cs, l2.tail, re_init)
   }
+
   //HERE
   def closed_string_dero(r1: Rexp, r2: Rexp, s: List[Char]): Rexp = {
     val l1 = der_seqo(r1, s, Nil)
@@ -473,13 +474,15 @@
       val dist_res = distinctBy(flat_res, erase)
       dist_res match {
         case Nil => AZERO
-        case s :: Nil => fuse(bs1, s)
+        case r :: Nil => fuse(bs1, r)
         case rs => AALTS(bs1, rs)  
       }
     }
     //case ASTAR(bs, r) => ASTAR(bs, bsimp(r))
     case r => r
   }
+  //only print at the top level
+
   def find_pos(v: Val, rs: List[ARexp]): Int = (v, rs) match{
     case (v, r::Nil) => 0
     case (Right(v), r::rs) => find_pos(v, rs) + 1
@@ -528,8 +531,6 @@
     case (AALTS(bs1, rs), v) => {
       //phase 1 transformation so that aalts(bs1, rs) => aalts(bs1, rsf) and v => vf
       val init_ind = find_pos(v, rs)
-      //println(rs)
-      //println(v)
       val vs = bsimp2(rs(init_ind), remove(v, rs))//remove all the outer layers of left and right in v to  match the regx rs[i]
       //println(vs)
       val rs_simp = rs.map(bsimp)
@@ -538,30 +539,17 @@
         case r => vs._2
       }
       val flat_res = flats(rs_simp)
-      //println(rs_simp)
-      //println(flat_res)
-      //println(init_ind)
       val vs_for_coating = if(isend(vs._2, rs_simp, init_ind)||flat_res.length == 1) vs_kernel else Left(vs_kernel)
-      //println(vs_for_coating)
       val r_s = rs_simp(init_ind)//or vs._1
       val shift = flats_vsimp(rs_simp, init_ind) + find_pos_aux(vs._2, rs_simp(init_ind))
-      //println(shift)
       val new_ind = init_ind + shift
-      //println("new ind:")
-      //println(new_ind)
       val vf = coat(vs_for_coating, new_ind)
-      //println("vf:")
-      //println(vf)
       //flats2 returns a list of regex and a single v
       //now |- vf: ALTS(bs1, flat_res)
-
       //phase 2 transformation so that aalts(bs1, rsf) => aalts(bs, rsdb) and vf => vdb
       val dist_res = distinctBy(flat_res, erase)
       val front_part = distinctBy(flat_res.slice(0, new_ind + 1), erase)
       //val size_reduction = new_ind + 1 - front_part.length
-      //println(flat_res.length)
-      //println(dist_res)
-      //println(front_part)
       val vdb = if(dist_res.length == front_part.length )//that means the regex we are interested in is at the end of the list
       {
         coat(vs_kernel, front_part.length - 1)