import Element.elem

import RexpRelated._

import RexpRelated.Rexp._

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)

      case (_, 0) => ((ran.nextInt(3) + 97).toChar).toString

    }

  }

  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)

  }

    case AALTS(bs,rs) => {

      val bitstick = bstostick(bs)

      rs match {

        case r::rs1 =>  

        rs1.foldLeft( 

        ((elem("(") left_align bitstick) beside 

        elem(")")

        case Nil => elem(' ', 1, 1)

      }

    }

    case ASEQ(bs, r1, r2) => {

    }

    case ASTAR(bs, r) => {

      r match {

        case AONE(_) | AZERO | ACHAR(_, _) => {

        }

        case _ => {

        }

      }

    }

    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(" ")

    }

  }

    case ALTS( r::rs ) => {

      print("(")

      rs.map(r2=>{      

        print(" + ")

      })

      print(")")

    }

    case SEQ(r1, r2) => {

      print("~")

    }

    case STAR(r) => {

      r match {

        case ONE | ZERO | CHAR(_) => {

          print("*")

        }

        case _ => {

          print("[")

          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")

      }

    case AALTS(bs, rs) => {

      println("rs.map(bsimp) equals *************")

      val rs_simp = rs.map(bsimp)

      for(r <- rs_simp){

      }

      println("*************")

      println("flts(rs_simp)")

      val flat_res = flats(rs_simp)

      for(r <- flat_res){

      }

      println("dB(flat_res)")

      val dist_res = distinctBy(flat_res, erase)

      for(r <- dist_res){

      }

      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("regular expression derivative")

    println("regular expression simped derivative")

    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(){

  }

  def main(args: Array[String]) {

    vunsimp_test()

  }

}