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

          val easy = bsimp(bders(ss.toList, r))

          if(!(nangao == easy || pushbits(nangao) == (easy))){

            println(j)

            println("not equal")

            println("string")

            println(ss)

            println("original regex")

            println(annotated_tree(r))

            println("regex after ders simp")

            println(annotated_tree(nangao))

            println("regex after ders")

            println(annotated_tree(bders(ss.toList, r)))//flats' fuse when opening up AALTS causes the difference

            println("regex after ders and then a single simp")

            println(annotated_tree(easy))

          }

        }

    }

  }

  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)

      println(bts)

      println(cdbts)

    }

  }

  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 main(args: Array[String]) {

    //check_all()   

    //radical_correctness()

    //correctness_proof_convenient_path()

    retrieve_experience()

  } 

}