# HG changeset patch
# User Chengsong
# Date 1573493844 0
# Node ID 4fd50a6844aaac414de314cca706b68403ddfc88
# Parent  15bcf9b8f4d6d23a00b85c740da74f705bf4376c
got it

diff -r 15bcf9b8f4d6 -r 4fd50a6844aa Spiral.scala
--- a/Spiral.scala	Thu Aug 22 12:44:48 2019 +0200
+++ b/Spiral.scala	Mon Nov 11 17:37:24 2019 +0000
@@ -597,14 +597,90 @@
       printf("%d  %f\n",i, (end - start)/1.0e9)
     }
   }
+  /*
+  lemma retrieve_encode_STARS:
+  assumes "∀v∈set vs. ⊨ v : r ∧ code v = retrieve (intern r) v"
+  shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)"
+  */
+  def retrieve_encode_STARS(){
+    val r =  ALT(CHAR('a'), SEQ(CHAR('a'),CHAR('b')) ) 
+    //val v =  Stars(List(Sequ(Chr('a'), Chr('b')),  Chr('a')) )
+    val v1 = Right(Sequ(Chr('a'), Chr('b')))
+    val v2 = Left(Chr('a'))
+    val compressed1 = code(v1)
+    val compressed2 = code(v2)
+    val xompressed1 = retrieve(internalise(r), v1)
+    val xompressed2 = retrieve(internalise(r), v2)
+    println(compressed1, compressed2, xompressed1, xompressed2)
+    val v = Stars(List(v1, v2))
+    val compressed = code(v)
+    val a = ASTAR(List(), internalise(r))
+    val xompressed = retrieve(a, v)
+    println(compressed, xompressed)
+  }
+  //what does contains7 do?
+  //it causes exception
+  //relation between retreive, bder and injection
+  // a match error occurs when doing the injection
+  def contains7(){
+    val r = STAR( SEQ(CHAR('a'),CHAR('b')) )
+    val v = Sequ(Chr('b'), Stars(List(Sequ(Chr('a'), Chr('b')))))
+    val a = internalise(r)
+    val c = 'a'
+    val v_aug = inj(r, c, v)
+    println("bder c r:")
+    println(bder(c, a))
+    println("r:")
+    println(a)
+    println("bits they can both produce:")
+    println(retrieve(a, v_aug))
+  }
+  def der_seq(r:ARexp, s: List[Char],acc: List[ARexp]) : List[ARexp] = s match{
+    case Nil => acc ::: List(r)
+    case c::cs => der_seq(bder(c, r), cs, acc ::: List(r))
+  }
+  def der_seq_rev(r:ARexp, s: List[Char], acc: List[ARexp]): List[ARexp] = s match{
+    case Nil => r::acc
+    case c::cs =>der_seq_rev(r, cs, bders(s, r) :: acc  )
+  }
+  def re_close(l1: List[ARexp], l2: List[ARexp], re_init: ARexp): ARexp = l1 match {
+    case Nil => re_init
+    case c::cs => if(bnullable(c)) re_close(cs, l2.tail, AALTS(List(), List(re_init, fuse(mkepsBC(c), l2.head)) ) ) 
+    else re_close(cs, l2.tail, re_init)
+  }
+  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))
+    print(Re)
+    val Comp = bders( s.toList, ASEQ(List(), r1, r2))
+    print(Comp  )
+    if(Re != Comp){
+      println("boooooooooooooooo!joihniuguyfuyftyftyufuyids gheioueghrigdhxilj")
+    }
+    Re
+  }
+  def newxp1(){
+    val r1 = internalise("ab"|"")
+    val r2 = internalise(("b")%)
+    val s = "abbbbb"
+    val s2= "bbbbb"
+    val s3 = "aaaaaa"
+    //closed_string_der(r1, r2, s)
+    //closed_string_der(r1, r2, s2)
+    closed_string_der(r1, r2, s3)
+  }
   def main(args: Array[String]) {
+    newxp1()
+  //contains7()
+  //retrieve_encode_STARS()
     //check_all()   
     //radical_correctness()
     //correctness_proof_convenient_path()
     //retrieve_experience()
     //neat_retrieve()
     //test_bsimp2()
-    christian_def2()
+    //christian_def2()
     //christian_def()
     //essence_posix()
     //speed_test()