# HG changeset patch
# User Chengsong
# Date 1554910474 -3600
# Node ID 9c1ca6d6e1902d83cf3700e09f228d6289ff1a74
# Parent  2b95bcd2ac735dbaa7dcdef41bc162c7714fc20f
The C(Char) construct is incompatible with the code and retrieve in Fahad's thesis.
This causes the exception.
Two ways of fixing this: delete C(C) construct (easy way around) or amend retrieve code etc.
since the C(C) construct is intended for decoding Pred, and we don't use pred now, we shall delete this.
This is the last veersion that contains C(CHAR)

diff -r 2b95bcd2ac73 -r 9c1ca6d6e190 Spiral.scala
--- a/Spiral.scala	Sat Mar 23 11:53:09 2019 +0000
+++ b/Spiral.scala	Wed Apr 10 16:34:34 2019 +0100
@@ -434,14 +434,15 @@
   }
   //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(fuse(bs, _)))
+    case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
+    case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
     case r => r
   }
   def correctness_proof_convenient_path(){
-    for(i <- 1 to 1)
+    for(i <- 1 to 10000)
     {
-        val s = "baa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
-        val r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),'c'), ACHAR(List(S),'b'))),ASEQ(List(),ASTAR(List(),ACHAR(List(),'a')),AALTS(List(),List(ACHAR(List(Z),'a'), ACHAR(List(S),'a'))))))//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)
+        val s = rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
+        val r = 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){
           val ss = s.slice(0, j+ 1)
           val nangao = ders_simp(r, ss.toList)
@@ -463,6 +464,18 @@
         }
     }
   }
+  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)
+    val bts = retrieve(rg, vl)
+    val cdbts = code(vl)
+    if(bts != cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
+      println(bts)
+      println(cdbts)
+      println("NOoooooo.....!")
+    }
+  }
   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
@@ -470,7 +483,8 @@
   def main(args: Array[String]) {
     //check_all()   
     //radical_correctness()
-    correctness_proof_convenient_path()
+    //correctness_proof_convenient_path()
+    retrieve_experience()
   } 
 }
 
diff -r 2b95bcd2ac73 -r 9c1ca6d6e190 corr_pr_sketch.pdf
Binary file corr_pr_sketch.pdf has changed
diff -r 2b95bcd2ac73 -r 9c1ca6d6e190 corr_pr_sketch.tex
--- a/corr_pr_sketch.tex	Sat Mar 23 11:53:09 2019 +0000
+++ b/corr_pr_sketch.tex	Wed Apr 10 16:34:34 2019 +0100
@@ -314,50 +314,129 @@
 
 \begin{theorem}{
 This is a very strong claim that has yet to be more carefully examined and proved. However, experiments suggest a very good hope for this.}\\
-Define pushbits as the following:\\
-$pushbits(r) = if( r == ALTS(bs, rs) )\ then\ ALTS(Nil, rs.map(fuse(bs,\_)))  \ else\ r$.\\
+Define pushbits as the following:\\  
+\begin{verbatim}
+def pushbits(r: ARexp): ARexp = r match {
+    case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
+    case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
+    case r => r
+  }
+  \end{verbatim}
 Then we have \mbox{\boldmath$pushbits(ders\_simp(ar, s) ) == simp(ders(ar,s)) \ or\ ders\_simp(ar, s) == simp(ders(ar, s))$}.\\
 Unfortunately this does not hold. A counterexample is\\
 \begin{verbatim}
-r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),c), ACHAR(List(S),b))),ASEQ(List(),ASTAR(List(),ACHAR(List(),a)),AALTS(List(),List(ACHAR(List(Z),a), ACHAR(List(S),a))))))
+baa
+original regex
+STA
+ └-ALT
+    └-STA List(Z)
+    |  └-a
+    └-ALT List(S)
+       └-b List(Z)
+       └-a List(S)
 regex after ders simp
-
-SEQ
- └-ALT List(S, S, C(b))
- |  └-SEQ
- |  |  └-STA List(S, C(a), S, C(a))
- |  |  |  └-a
- |  |  └-a List(Z)
- |  └-ONE List(S, C(a), Z, Z, C(a))
- └-STA
+ALT List(S, S, Z, C(b))
+ └-SEQ
+ |  └-STA List(S, Z, S, C(a), S, C(a))
+ |  |  └-a
+ |  └-STA
+ |     └-ALT
+ |        └-STA List(Z)
+ |        |  └-a
+ |        └-ALT List(S)
+ |           └-b List(Z)
+ |           └-a List(S)
+ └-SEQ List(S, Z, S, C(a), Z)
+    └-ALT List(S)
+    |  └-STA List(Z, S, C(a))
+    |  |  └-a
+    |  └-ONE List(S, S, C(a))
+    └-STA
+       └-ALT
+          └-STA List(Z)
+          |  └-a
+          └-ALT List(S)
+             └-b List(Z)
+             └-a List(S)
+regex after ders
+ALT
+ └-SEQ
+ |  └-ALT List(S)
+ |  |  └-SEQ List(Z)
+ |  |  |  └-ZERO
+ |  |  |  └-STA
+ |  |  |     └-a
+ |  |  └-ALT List(S)
+ |  |     └-ZERO
+ |  |     └-ZERO
+ |  └-STA
+ |     └-ALT
+ |        └-STA List(Z)
+ |        |  └-a
+ |        └-ALT List(S)
+ |           └-b List(Z)
+ |           └-a List(S)
+ └-ALT List(S, S, Z, C(b))
     └-SEQ
-       └-ALT
-       |  └-c List(Z)
-       |  └-b List(S)
-       └-SEQ
-          └-STA
-          |  └-a
+    |  └-ALT List(S)
+    |  |  └-ALT List(Z)
+    |  |  |  └-SEQ
+    |  |  |  |  └-ZERO
+    |  |  |  |  └-STA
+    |  |  |  |     └-a
+    |  |  |  └-SEQ List(S, C(a))
+    |  |  |     └-ONE List(S, C(a))
+    |  |  |     └-STA
+    |  |  |        └-a
+    |  |  └-ALT List(S)
+    |  |     └-ZERO
+    |  |     └-ZERO
+    |  └-STA
+    |     └-ALT
+    |        └-STA List(Z)
+    |        |  └-a
+    |        └-ALT List(S)
+    |           └-b List(Z)
+    |           └-a List(S)
+    └-SEQ List(S, Z, S, C(a), Z)
+       └-ALT List(S)
+       |  └-SEQ List(Z)
+       |  |  └-ONE List(S, C(a))
+       |  |  └-STA
+       |  |     └-a
+       |  └-ALT List(S)
+       |     └-ZERO
+       |     └-ONE List(S, C(a))
+       └-STA
           └-ALT
-             └-a List(Z)
-             └-a List(S)
+             └-STA List(Z)
+             |  └-a
+             └-ALT List(S)
+                └-b List(Z)
+                └-a List(S)
 regex after ders and then a single simp
-SEQ
- └-ALT List(S)
- |  └-SEQ List(S, C(b))
- |  |  └-STA List(S, C(a), S, C(a))
- |  |  |  └-a
- |  |  └-a List(Z)
- |  └-ONE List(S, C(b), S, C(a), Z, Z, C(a))
- └-STA
-    └-SEQ
+ALT
+ └-SEQ List(S, S, Z, C(b))
+ |  └-STA List(S, Z, S, C(a), S, C(a))
+ |  |  └-a
+ |  └-STA
+ |     └-ALT
+ |        └-STA List(Z)
+ |        |  └-a
+ |        └-ALT List(S)
+ |           └-b List(Z)
+ |           └-a List(S)
+ └-SEQ List(S, S, Z, C(b), S, Z, S, C(a), Z)
+    └-ALT List(S)
+    |  └-STA List(Z, S, C(a))
+    |  |  └-a
+    |  └-ONE List(S, S, C(a))
+    └-STA
        └-ALT
-       |  └-c List(Z)
-       |  └-b List(S)
-       └-SEQ
-          └-STA
+          └-STA List(Z)
           |  └-a
-          └-ALT
-             └-a List(Z)
+          └-ALT List(S)
+             └-b List(Z)
              └-a List(S)
 \end{verbatim}
 \end{theorem}
diff -r 2b95bcd2ac73 -r 9c1ca6d6e190 lex_blex_Frankensteined.scala
--- a/lex_blex_Frankensteined.scala	Sat Mar 23 11:53:09 2019 +0000
+++ b/lex_blex_Frankensteined.scala	Wed Apr 10 16:34:34 2019 +0100
@@ -92,7 +92,7 @@
   def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
     case (ONE, bs) => (Empty, bs)
     case (CHAR(f), C(c)::bs) => (Chr(c), bs)
-    case (ALTS(r::Nil), bs) => decode_aux(r, bs)//this case seems tailor made for those who want to simplify the regex before der or simp
+    //case (ALTS(r::Nil), bs) => decode_aux(r, bs)//this case seems only used when we simp a regex before derivatives and it contains things like alt("a")
     case (ALTS(rs), bs) => bs match {
       case Z::bs1 => {
         val (v, bs2) = decode_aux(rs.head, bs1)
@@ -126,7 +126,25 @@
     case _ => throw new Exception("Not decodable")
   }
 
+  def code(v: Val): Bits = v match {
+    case Empty => Nil
+    case Left(v) => Z :: code(v)
+    case Right(v) => S :: code(v)
+    case Sequ(v1, v2) => code(v1) ::: code(v2)
+    case Stars(Nil) => Z::Nil
+    case Stars(v::vs) => S::code(v) ::: code(Stars(vs))
+  }
 
+
+  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, as), Left(v)) => bs ++ retrieve(as.head,v)
+    case (AALTS(bs, as), Right(v)) => bs ++ retrieve(AALTS(Nil,as.tail),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))
+  }
   //erase function: extracts the regx from Aregex
   def erase(r:ARexp): Rexp = r match{
     case AZERO => ZERO
@@ -397,8 +415,8 @@
     case ASEQ(bs1, r1, r2) => (super_bsimp(r1), super_bsimp(r2)) match {
         case (AZERO, _) => AZERO
         case (_, AZERO) => AZERO
-        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
-        case (AALTS(bs2, rs), r2) => AALTS(bs1 ++ bs2, rs.map(r => r match {case AONE(bs3) => fuse(bs3, r2) case r => ASEQ(Nil, r, r2)}) ) 
+        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)//万一是(r1, alts(rs))这种形式呢
+        case (AALTS(bs2, rs), r2) => AALTS(bs1 ++ bs2, rs.map(r => r match {case AONE(bs3) => fuse(bs3, r2) case r => ASEQ(Nil, r, r2)} ) ) 
         case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
     }
     case AALTS(bs1, rs) => {