import Spiral._
import Element.elem
import RexpRelated._
import RexpRelated.Rexp._
//import Partial._
import scala.collection.mutable.ListBuffer

object Spiral{


  val alphabet = ("""abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789.:"=()\;-+*!<>\/%{} """+"\n\t").toSet//Set('a','b','c')
  
  val arr_of_size = ListBuffer.empty[Int]


  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 random_struct_gen(depth:Int): Rexp = {
    val dice = ran.nextInt(3)
    val dice2 = ran.nextInt(3)
    val new_depth = (List(0, depth - 1 - dice2)).max
    (dice, new_depth) match {
      case (_, 0) => ((ran.nextInt(3) + 97).toChar).toString
      case (0, i) => STAR(random_struct_gen(new_depth))
      case (1, i) => SEQ(random_struct_gen(new_depth), random_struct_gen(new_depth))
      case (2, i) => ALTS( List(random_struct_gen(new_depth), random_struct_gen(new_depth)) )
    }
  }
  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 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
    }
  }

  val mkst = "abcdefghijklmnopqrstuvwxyz"

  val big_panda = STAR(STAR(STAR(ALTS(List(ALTS(List(CHAR('c'), CHAR('b'))), SEQ(CHAR('c'),CHAR('c')))))))
  val str_panda = "ccccb"

  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 aregex_simple_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 
        aregex_simple_print(r))  )( (acc, r2) => acc beside ((elem(" + ") above elem("   ")) beside aregex_simple_print(r2) )) beside
        elem(")")
        case Nil => elem(' ', 1, 1)
      }
    }
    case ASEQ(bs, r1, r2) => {
      ((elem("[") left_align bstostick(bs)) beside  aregex_simple_print(r1) beside elem("~") beside aregex_simple_print(r2) beside (elem("]") above elem(" "))) 
    }
    case ASTAR(bs, r) => {
      r match {
        case AONE(_) | AZERO | ACHAR(_, _) => {
          (elem("{") left_align bstostick(bs)) beside (aregex_simple_print(r) beside elem("}*")) 
        }
        case _ => {
          (elem("{") left_align bstostick(bs)) beside (aregex_simple_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 regex_simple_print(r: Rexp): Unit = r match {
    case ALTS( r::rs ) => {
      print("(")
      regex_simple_print(r)
      rs.map(r2=>{      
        print(" + ")
        regex_simple_print(r2)
      })
      print(")")
    }
    case SEQ(r1, r2) => {
      regex_simple_print(r1)
      print("~")
      regex_simple_print(r2)
    }
    case STAR(r) => {
      r match {
        case ONE | ZERO | CHAR(_) => {
          regex_simple_print(r)
          print("*")
        }
        case _ => {
          print("[")
          regex_simple_print(r)
          print("]*")
        }
      }
    }
    case ONE => {
      print("1")
    }
    case ZERO => {
      print("0")
    }
    case CHAR(c) =>{
      print(c)
    }
  }
  //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")
        aregex_simple_print(bsimp(r1))
        aregex_simple_print(bsimp(r2))
      }
    case AALTS(bs, rs) => {
      println("rs.map(bsimp) equals *************")
      val rs_simp = rs.map(bsimp)
      for(r <- rs_simp){
        println(aregex_simple_print(r))
      }
      println("*************")
      println("flts(rs_simp)")
      val flat_res = flats(rs_simp)
      for(r <- flat_res){
        println(aregex_simple_print(r))
      }
      println("dB(flat_res)")
      val dist_res = distinctBy(flat_res, erase)
      for(r <- dist_res){
        println(aregex_simple_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")
  }


  //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 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 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)
  }
  //HERE
  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).tail, l2.tail, 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 string_der_test(){
    for(i <- 0 to 10){
      val s = rd_string_gen(alphabet_size, i).toList
      val r = random_struct_gen(2)
      if(ders(s, r) != ders2(s, r)){
        println(i)
        println(s)
        println(r)
        println(ders(s, r))
        println(ders2(s,r))
        println("neq") 
      }
    }
  }
  def have_fun(){
    val bis = List(S,S)
    val bits = List(S,S,Z)
    val reg = ("a" | (("a")%) )~("b")
    val res = decode_aux(reg, bis)
    val result = decode_aux(reg, bis) 
    val result1 = decode_aux(reg, List(Z))
    println(res)
    println(result)
    println(bsimp(bders( "a".toList, internalise(reg))))
    println(result1)
  }
  def finj_test0(c: Char, r: ARexp){
    val dr = (bder(c, r))
    val sdr = bsimp(dr)
    val v = if(bnullable(sdr)) mkeps(erase(sdr)) else mkchr(erase(sdr))
    val v0 = if(bnullable(sdr)) mkeps(erase(bder(c,r))) else mkchr(erase(bder(c, r)))
    val v1 = inj(erase(r), c, v0)
    val v2 = fuzzy_inj(r, c, v)
    println("regular expression original")
    println(aregex_simple_print(r))
    println("regular expression derivative")
    println(aregex_simple_print(dr))
    println("regular expression simped derivative")
    println(aregex_simple_print(sdr))
    println("simplified value")
    println(v)
    println("unsimplified value")
    println(v0)
    println("normal injection")
    println(v1)
    println("fuzzy injection")
    println(v2)
    println("inj "+r+c+v0)
    println("fuzzy_inj "+r+c+v)
  }
  def vunsimp_test(){
    /*val bdr = AALTS(
      List(), 
      List(
        AONE(List(S,Z)), 
        ASTAR(List(Z,Z,S), ACHAR(List(),'c')), 
        ASEQ(List(Z), ASTAR(List(S), ACHAR(List(), 'c')), ASTAR(List(S), ACHAR(List(), 'c') )    )
      )    
    )*/
    val bdr = AALTS(List(),List(AALTS(List(Z),List(ASEQ(List(),
    ASEQ(List(),AONE(List(S)),ASTAR(List(),ACHAR(List(),'c'))),ASTAR(List(),ACHAR(List(),'c'))),
     ASEQ(List(Z),AONE(List(S)),ASTAR(List(),ACHAR(List(),'c'))))), AALTS(List(S),List(AONE(List(Z)), AZERO))))
    val dr = erase(bdr)
    val dv = mkeps(dr)
    //val bdr = bder(c, internalise(r))
    //val dv = mkeps(dr)
    println(aregex_simple_print(bdr))
    println(dv)
    val target_vr = bsimp2(bdr, dv)
    println(aregex_simple_print(target_vr._1))
    println(target_vr._2)
    println(vunsimp(bdr, dv)(target_vr._2))
  }


  def main(args: Array[String]) {
    vunsimp_test()
  }
   
}