import Element.elem
import RexpRelated._
import RexpRelated.Rexp._
import Partial._
import BRexp._
import scala.collection.mutable.ListBuffer
object Spiral{

  val space = elem(" ")
  val corner = elem("+")

  def spiral(nEdges: Int, direction: Int): Element = {
    if(nEdges == 1)
      elem("+")
    else {
      val sp = spiral(nEdges - 1, (direction + 3) % 4)
      def verticalBar = elem('|', 1, sp.height)
      def horizontalBar = elem('-', sp.width, 1)
      if(direction == 0)
        (corner beside horizontalBar) above sp//(sp beside space)
      else if (direction == 1)
        sp beside (corner above verticalBar)
      else if (direction == 2)
        (space beside sp) above (horizontalBar beside corner)
      else
        (verticalBar above corner) beside (space above sp)
    }
  }
  val alphabet = ("""abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789.:"=()\;-+*!<>\/%{} """+"\n\t").toSet//Set('a','b','c')
  def bregx_tree(r: BRexp): Element = regx_tree(berase(r))
  def regx_tree(r: Rexp): Element = aregx_tree(internalise(r))
  def annotated_tree(r: ARexp): Element = {
    r match {
      case ACHAR(bs, d) => {
        //val Some(d) = alphabet.find(f)
        d match {
          case '\n' => elem("\\n")
          case '\t' => elem("\\t")
          case ' ' => elem("space")
          case d => if(bs.isEmpty)  elem(d.toString) else elem(d.toString++" ") beside elem(bs.toString)
        }   
      }
      case AONE(bs) => {
        if(bs.isEmpty)  elem("ONE") else elem("ONE ") beside elem(bs.toString)
      }
      case AZERO => {
        elem("ZERO") 
      }
      case ASEQ(bs, r1, r2) => {
        annotated_binary_print("SEQ", r1, r2, bs)
      }
      case AALTS(bs, rs) => {
        //elem("Awaiting completion")
        annotated_list_print("ALT", rs, bs)  
      }
      case ASTAR(bs, r) => {
        annotated_list_print("STA", List(r), bs)
      }
    } 
  }
  def aregx_tree(r: ARexp): Element = {
    r match {
      case ACHAR(bs, d) => {
        //val Some(d) = alphabet.find(f)
        d match {
          case '\n' => elem("\\n")
          case '\t' => elem("\\t")
          case ' ' => elem("space")
          case d => elem(d.toString)
        }   
      }
      case AONE(bs) => {
        elem("ONE")
      }
      case AZERO => {
        elem("ZERO")
      }
      case ASEQ(bs, r1, r2) => {
        binary_print("SEQ", r1, r2)
      }
      case AALTS(bs, rs) => {
        //elem("Awaiting completion")
        list_print("ALT", rs)
      }
      case ASTAR(bs, r) => {
        list_print("STA", List(r))
      }
    }
  }
  val port = elem(" └-")
  def list_print(name: String, rs: List[ARexp]): Element = {
    rs match {
      case r::Nil => {
        val pref = aregx_tree(r)
        val head = elem(name)
        (head left_align (port up_align pref) ) 
      }
      case r2::r1::Nil => {
        binary_print(name, r2, r1)
      }
      case r::rs1 => {
        val pref = aregx_tree(r)
        val head = elem(name)
        if (pref.height > 1){
          val link = elem('|', 1, pref.height - 1)
          (head left_align ((port above link) beside pref)) left_align tail_print(rs1)    
        }
        else{
          (head left_align (port beside pref) ) left_align tail_print(rs1)
        }
      }
    }
  }
    def annotated_list_print(name: String, rs: List[ARexp], bs: List[Bit]): Element = {
    rs match {
      case r::Nil => {
        val pref = annotated_tree(r)
        val head = if(bs.isEmpty) elem(name) else elem(name ++ " ") beside elem(bs.toString)
        (head left_align (port up_align pref) ) 
      }
      case r2::r1::Nil => {
        annotated_binary_print(name, r2, r1, bs)
      }
      case r::rs1 => {
        val pref = annotated_tree(r)
        val head = if (bs.isEmpty) elem(name) else elem(name ++ " ") beside elem(bs.toString)
        if (pref.height > 1){
          val link = elem('|', 1, pref.height - 1)
          (head left_align ((port above link) beside pref)) left_align annotated_tail_print(rs1)    
        }
        else{
          (head left_align (port beside pref) ) left_align annotated_tail_print(rs1)
        }
      }
    }
  }

  def annotated_tail_print(rs: List[ARexp]): Element = {
    rs match {
      case r2::r1::Nil => {
        val pref = annotated_tree(r2)
        val suff = annotated_tree(r1)
        if (pref.height > 1){
          val link = elem('|', 1, pref.height - 1)
          ((port above link) beside pref) left_align (port up_align suff)
        }
        else{
          (port beside pref) left_align (port up_align suff)
        } 
      }
      case r2::rs1 => {
        val pref = annotated_tree(r2)
        
        if (pref.height > 1){
          val link = elem('|', 1, pref.height - 1)
          ((port above link) beside pref) left_align annotated_tail_print(rs1)//(port up_align tail_print(rs1) )
        }
        else{
          (port beside pref) left_align annotated_tail_print(rs1)//(port up_align tail_print(rs1))
        } 
        //pref left_align tail_print(rs1)
      }
    }
  }

  def tail_print(rs: List[ARexp]): Element = {
    rs match {
      case r2::r1::Nil => {
        val pref = aregx_tree(r2)
        val suff = aregx_tree(r1)
        if (pref.height > 1){
          val link = elem('|', 1, pref.height - 1)
          ((port above link) beside pref) left_align (port up_align suff)
        }
        else{
          (port beside pref) left_align (port up_align suff)
        } 
      }
      case r2::rs1 => {
        val pref = aregx_tree(r2)
        
        if (pref.height > 1){
          val link = elem('|', 1, pref.height - 1)
          ((port above link) beside pref) left_align tail_print(rs1)//(port up_align tail_print(rs1) )
        }
        else{
          (port beside pref) left_align tail_print(rs1)//(port up_align tail_print(rs1))
        } 
        //pref left_align tail_print(rs1)
      }
    }
  }

  def binary_print(name: String, r1: ARexp, r2: ARexp): Element = {
    val pref = aregx_tree(r1)
    val suff = aregx_tree(r2)
    val head = elem(name) 
    if (pref.height > 1){
      val link = elem('|', 1, pref.height - 1)
      (head left_align ((port above link) beside pref) ) left_align (port up_align suff)
    }
    else{
      (head left_align (port beside pref) ) left_align (port up_align suff)
    }
  }
  def annotated_binary_print(name: String, r1: ARexp, r2: ARexp, bs: List[Bit]): Element = {
    val pref = annotated_tree(r1)
    val suff = annotated_tree(r2)
    val head = if (bs.isEmpty) elem(name) else elem(name ++ " ") beside elem(bs.toString)
    if (pref.height > 1){
      val link = elem('|', 1, pref.height - 1)
      (head left_align ((port above link) beside pref) ) left_align (port up_align suff)
    }
    else{
      (head left_align (port beside pref) ) left_align (port up_align suff)
    }
  }

  val arr_of_size = ListBuffer.empty[Int]

  def pC(r: Rexp): Set[Rexp] = {//PD's companion
    r match {
      case SEQ(r1, r2) => pC(r2)
      case ALTS(rs) => rs.flatMap(a => pC(a) ).toSet
      case CHAR(c) => Set(r)
      case r => Set()
    }
  }
  def illustration(r: Rexp, s: String){
    var i_like_imperative_style = internalise(r)
    val all_chars = s.toList
    for (i <- 0 to s.length - 1){
      val der_res =  bder(all_chars(i), i_like_imperative_style)
      val simp_res = bsimp(der_res)
      println("The original regex, the regex after derivative w.r.t " + all_chars(i) + " and the simplification of the derivative.")
      println(aregx_tree(i_like_imperative_style) up_align aregx_tree(der_res) up_align aregx_tree(simp_res))
      //println(asize(i_like_imperative_style), asize(der_res), asize(simp_res))
      arr_of_size += asize(i_like_imperative_style)
      //println(asize(simp_res), asize(simp_res) / arr_of_size(0) )
      i_like_imperative_style = simp_res
    }
    arr_of_size += asize(i_like_imperative_style)
  }
  val ran = scala.util.Random
  var alphabet_size = 3
  def balanced_seq_star_gen(depth: Int, star: Boolean): Rexp = {
    if(depth == 1){
      ((ran.nextInt(4) + 97).toChar).toString
    }
    else if(star){
      STAR(balanced_seq_star_gen(depth - 1, false))
    }
    else{
      SEQ(balanced_seq_star_gen(depth - 1, true), balanced_seq_star_gen(depth - 1, true))
    }
  }
  def max(i: Int, j: Int): Int = {
    if(i > j)
      i
    else 
      j
  }
  def random_struct_gen(depth:Int): Rexp = {
    val dice = ran.nextInt(3)
    val dice2 = ran.nextInt(3)
    (dice, depth) match {
      case (_, 0) => ((ran.nextInt(3) + 97).toChar).toString
      case (0, i) => STAR(random_struct_gen(max(0, i - 1 - dice2)))
      case (1, i) => SEQ(random_struct_gen(max(0, i - 1 - dice2)), random_struct_gen(max(0, i - 1 - dice2)))
      case (2, i) => ALTS( List(random_struct_gen(max(0, i - 1 - dice2)), random_struct_gen(max(0, i - 1 - dice2))) )
    }
  }
  def balanced_struct_gen(depth: Int): Rexp = {
    val dice = ran.nextInt(3)
    (dice, depth) match {
      case (_, 0) => ((ran.nextInt(3) + 97).toChar).toString
      case (0, i) => STAR(random_struct_gen(depth - 1))
      case (1, i) => SEQ(random_struct_gen(depth - 1), random_struct_gen(depth - 1))
      case (2, i) => ALTS( List(random_struct_gen(depth - 1), random_struct_gen(depth - 1) ) )
    }
  }
  def random_pool(n: Int, d: Int) : Stream[Rexp] = n match {
    case 0 => (for (i <- 1 to 10) yield balanced_struct_gen(d)).toStream
    case n => {  
      val rs = random_pool(n - 1, d)
      rs #:::
      (for (i <- (1 to 10).toStream) yield balanced_struct_gen(d)) #::: 
      (for (i <- (1 to 10).toStream) yield random_struct_gen(d))
    }
  }

  def rd_string_gen(alp_size: Int, len: Int): String = {
    if( len > 0)
      ((ran.nextInt(alp_size) + 97).toChar).toString + rd_string_gen(alp_size, len - 1)
    else
      ((ran.nextInt(alp_size) + 97).toChar).toString
  }
  def plot(b: List[Int]){
    println(b(0),b.max)

  }
  def dep_exp(depth: List[Int]){
    for(i <- depth){
      arr_of_size.clear()
      val s = rd_string_gen(alphabet_size, (i-8)*(i-8)+10)
      val r = random_struct_gen(i)
      println("depth: "+i)
      illustration(r, s) //"abcabadaaadcabdbabcdaadbabbcbbdabdabbcbdbabdbcdb") 
      //println("depth: " + i + " general stats:"+ arr_of_size(0), arr_of_size.max, arr_of_size.max/arr_of_size(0))
      //println("x y label alignment")
      /*for(i <- 0 to s.length - 1){
        if(s(i) == '\n')
          println(i+" "+arr_of_size(i)+" "+"nl"+" -140")
        else if(s(i) ==  ' ')
          println(i+" "+arr_of_size(i)+" "+"sp"+" -140")
        else
          println(i+" "+arr_of_size(i)+" "+s(i)+" -140")
      }*/
      //println(s.length + " " + arr_of_size(s.length) + " ]" + " -140")
    }
  }
  def case_study(ss: List[String], r: Rexp){
    for(s <- ss){
      arr_of_size.clear()
      illustration(r, s)
      println("x y label alignment")
      for(i <- 0 to s.length - 1){
        if(s(i) == '\n')
          println(i+" "+arr_of_size(i)+" "+"nl"+" -140")
        else if(s(i) ==  ' ')
          println(i+" "+arr_of_size(i)+" "+"sp"+" -140")
        else
          println(i+" "+arr_of_size(i)+" "+s(i)+" -140")
      }
    }
  }
  def star_gen(dp: Int): Rexp = {
    if(dp > 0)
      STAR(star_gen(dp - 1))
    else
      "a"
  }
  def strs_gen(len: Int, num: Int): List[String] = {
    if(num > 0){
      rd_string_gen(3, len)::strs_gen(len, num - 1)
    }
    else{
      Nil
    }
  }
  def regx_print(r: Rexp): String = {
    r match {
      case ZERO =>
        "ZERO"
      case CHAR(c) => {
         //val Some(c) = alphabet.find(f)
         "\"" + c.toString + "\""
      }
      case ONE => {
        "ONE"
      }
      case ALTS(rs) => {
        "ALTS(List("+(rs.map(regx_print)).foldLeft("")((a, b) => if(a == "") b else a + "," + b)+"))"
      }
      case SEQ(r1, r2) => {
        "SEQ(" + regx_print(r1) + "," + regx_print(r2) + ")"
      }
      case STAR(r) => {
        "STAR(" + regx_print(r) + ")"
      }
    }
  }
  val mkst = "abcdefghijklmnopqrstuvwxyz"
  def weak_sub_check(r: Rexp, s: String, i: Int, f: (List[Rexp], Set[Rexp]) => Boolean){
    //we first compute pders over the set of all strings on the alphabet
    val pd = pderas(Set(r), i + 4)
    //then "b-internalise" the regular expression into a brexp(this is essentially 
    //attaching a bit Z to every alts to signify that they come from the original regular expression)
    var old = brternalise(r)
    //this is for comparison between normal simp and the weakened version of simp
    //normal simp will be performed on syncold
    //weakend simp will be performed on old
    var syncold = internalise(r)
    val all_chars = s.toList
    for (i <- 0 to s.length - 1){
      val syncder_res = bder(all_chars(i), syncold)
      val syncsimp_res = super_bsimp(syncder_res)
      //see brder for detailed explanation
      //just changes bit Z to S when deriving an ALTS, 
      //signifying that the structure has been "touched" and
      //therefore able to be spilled in the bspill function
      val der_res =  brder(all_chars(i), old)
      val simp_res = br_simp(der_res)
      val anatomy = bspill(simp_res)
      //track if the number of regular expressions exceeds those in the PD set(remember PD means the pders over A*)
      if(f(List(berase(simp_res)), pd)  == false ){
        println(size(erase(syncsimp_res)))
        println(size(berase(simp_res)))
        println(bregx_tree(simp_res))
        println(s)
        println(i)
        println(r)
        println(anatomy.map(size).sum)
        println(pd.map(size).sum)
      }  
      old = simp_res
      syncold = syncsimp_res
    }
  }
  def inclusion_truth(anatomy: List[Rexp], pd: Set[Rexp]): Boolean = {
    val aset = anatomy.toSet
    if(aset subsetOf pd){
      true
    }
    else{
      println("inclusion not true")
      false
    }
  }
  def size_comp(anatomy: List[Rexp], pd: Set[Rexp]):Boolean = {println("size of PD and bspilled simp regx: ", pd.size, anatomy.size); true}
  def size_expansion_rate(r: List[Rexp], pd: Set[Rexp]): Boolean = if(size(r(0)) > (pd.map(size).sum) * 3 ) { false }else {true}
  def ders_simp(r: ARexp, s: List[Char]): ARexp = {
    s match {
      case Nil => r 
      case c::cs => ders_simp(bsimp(bder(c, r)), cs)
    }
  }
  val big_panda = STAR(STAR(STAR(ALTS(List(ALTS(List(CHAR('c'), CHAR('b'))), SEQ(CHAR('c'),CHAR('c')))))))
  val str_panda = "ccccb"
  def check_all(){

        weak_sub_check(big_panda, str_panda, 6, size_expansion_rate)

  }
  //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))))
    case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
    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){
          val ss = s.slice(0, j+ 1)
          val nangao = ders_simp(internalise(r), ss.toList)
          val easy = bsimp(bders(ss.toList, internalise(r)))
          if(!(nangao == easy || pushbits(nangao) == (easy))){
            println(j)
            println("not equal")
            println("string")
            println(ss)
            println("original regex")
            println(regx_tree(r))
            println("regex after ders simp")
            println(annotated_tree(nangao))
            println("regex after ders")
            println(annotated_tree(bders(ss.toList, internalise(r))))//flats' fuse when opening up AALTS causes the difference
            println("regex after ders and then a single simp")
            println(annotated_tree(easy))
          }
        }
    }
  }
  /*    if(bts == cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
      println(bts)
      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)
    }
    *///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)
    }
  }

  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
  }
  def christian_def(){
    val r = ALTS(List(SEQ(ZERO,CHAR('b')), ONE))
    val v = Right(Empty)
    val a = internalise(r)
    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 = ${a_v._1}")
    //val bs2 = retrieve(as, decode(erase(as), bs1))
    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 christian_def2(){
    val a = AALTS(List(S), List(AZERO, ASEQ(List(S), AALTS(List(S), List(AONE(List(S)), ACHAR(List(S), 'c'))), ACHAR(List(S),'c') )) )
    //AALTS(List(Z), List(AZERO, ASEQ(List(), AALTS(List(),List(AONE(List()), ACHAR(Nil, 'b'))), ACHAR(Nil, 'b'))  )   )
    val unsimp = bsimp(bder('c',a))
    val simped = bsimp(bder('c', bsimp(a))           )
    println(bsimp(a))
    if(unsimp != simped){
      println(s"bsimp(bder c r) = ${unsimp}, whereas bsimp(bder c bsimp r) = ${simped}")
    }
  }
  def essence_posix(){
    //val s = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
    val s0 = "a"
    val r = SEQ(STAR(ALT("a", "aa")), "b")//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(i <- 1 to 40){
      val s = s0*i
      //printf("%d  %d\n",i, size(ders(s.toList, r)))
      printf("%d  %d\n",i, asize(ders_simp( internalise(r), s.toList)))
      //println(asize(ders_simp( internalise(r), s.toList)))
    }
  }

  def speed_test(){
    val s0 = "a"*1000
    val r = SEQ(STAR("a"), "b")
    for(i <- 1 to 30){
      val s = s0*i
      val start = System.nanoTime()
      try{
        blex_simp(internalise(r), s.toList)
      }
      catch{
        case x: Exception =>
      }
      val end = System.nanoTime()
      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_def()
    //essence_posix()
    //speed_test()
  } 
}