package isac.gui.mawen.scalaterm

import isac.gui.mawen.termtree.TreeNodeContent

import javax.swing.tree.DefaultMutableTreeNode

import edu.tum.cs.isabelle.api.XML

import edu.tum.cs.isabelle.pure._

import edu.tum.cs.isabelle._      // for Codec

object Util {

  def int(s: String): Integer = new Integer(s)

 /* Data for presentation of Const which are not contained in (Scala-) Term:

  * _1: string as shown by Isabelle's pretty printing

  * _2: string in LaTeX format with place-holders "#d", where d is a digit:

  *     number of place-holders determine arity;

  *     pre/post/mix-fix is read out from here also for _1

  * _3: infixl | infixr | prefix | postfix: the latter two are redundant with _2

  * _4: priority, which determines parentheses to be set

  * TODO: reconsider data representation: record, ...

  */

  val present = Map (

    "HOL.eq" -> (" = ", "#1=#2", "infixl", 50),                              //see ~~/src/HOL/HOL.thy

    "Groups.plus_class.plus" -> (" + ", "#1+#2", "infixl", 65),              //see ~~/src/HOL/Groups.thy

    "Groups.plus_class.minus" -> (" - ", "#1-#2", "infixl", 65),             //see ~~/src/HOL/Groups.thy

    "Groups.plus_class.uminus" -> (" -", "#1-#2", "prefix", 80),             //see ~~/src/HOL/Groups.thy

    "Groups.times_class.times" -> (" * ", "#1.#2", "infixl", 70),            //see ~~/src/HOL/Groups.thy

    //"Groups.plus_class.times"->("*", "#1\cdot#2", "infixl", 70),

    //...ERROR: implicit conversion found: Groups.plus_class.times => ...

    "Fields.inverse_class.divide" -> (" / ", "\frac{#1}{#2}", "infixl", 70), //see ~~/src/HOL/Fields.thy

    "Power.power_class.power" -> (" ^ ", "#1^{#2}", "infixr", 80)            //see ~~/src/HOL/Transcendental.thy

    //"Transcendental.sin" -> ("sin ", "\sin{#1}", "infixl", 70)

    //...ERROR: implicit conversion found: ...

    )

  /* so not every constant needs to be in Util.present */

  def ST_isa(str: String): String = {

    present.get(str) match {

      case Some((isa, _, _, _)) => isa 

      case None => str.substring(str.lastIndexOf(".") + 1) + " "}}

  def ST_latex(str: String): String = {

    present.get(str) match {

      case Some((_, latex, _, _)) => latex 

      case None => str.substring(str.lastIndexOf(".") + 1) + " "}}

  def ST_fix(str: String): String = {

    present.get(str) match {

      case Some((_, _, fix, _)) => fix 

      case None => "prefix"}}

  def ST_prior(str: String): Int = {

    present.get(str) match {

      case Some((_, _, _, prior)) => prior 

      case None => 99}}

  /* transform a Term into a String, which corresponds to Isabelle's 

   * pretty_printing within Isac's Knowledge.

   * mawen uses this for string representation of Terms.

   */

  def str_of(t: Term, prior: Int, l_r: String): String = t match {

    case App(App(Const("Product_Type.Pair", _), t1), t2) 

    => str_of(t1, prior, "none") + ", " + str_of(t2, prior, "none")

    case App(App(Const(str, _), t1), t2) 

    => { val pri = ST_prior(str)

      if (prior > pri) {

         ST_fix(str) match {

         case "infixl" => "(" + str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right") + ")"

         case "infixr" => "(" + str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right") + ")"

         case "prefix" => "(" + ST_isa(str) + str_of(t1, pri, "left") + " (2" + str_of(t2, pri, "right") + "2)" + ")"}

      }else{

         ST_fix(str) match {

         case "infixl" => {

           if (prior == pri & l_r == "right") {

             "(" + str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right") + ")"

           }else{

             str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right")

           }

         }

         case "infixr" => {

           if (prior == pri & l_r == "left") {

             "(" + str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right") + ")"

           }else{

             str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right")

           }

         }

         case "prefix" => ST_isa(str) + str_of(t1, pri, "none") + " " + str_of(t2, pri, "none")}

      }}

    case App(Const(str, _), t1) => ST_isa(str) + "(" + str_of(t1, prior, "none") + ")"

    case Free(str, _) =>  str

    case Const(str, _) => str

    case _ => throw new IllegalArgumentException("str_of WRONG arg: " + t)

  }

  // infix: "left" or "right" argument ----------vvvv

  def string_of(t: Term): String = str_of(t, 0, "none")

  def wrap_term (t: Term): XML.Tree =

    XML.Elem(("MATHML", Nil), List(

      XML.Elem(("ISA", Nil), List(XML.Text("aaa + bbb::real"))),

      XML.Elem(("TERM", Nil), List(Codec[Term].encode(t)))))

  def insert_nodes(t: Term, n: DefaultMutableTreeNode): DefaultMutableTreeNode = t match {

    case App(App(Const("Product_Type.Pair", _), t1), t2) 

    => n //TODO

    case App(App(Const(str, typ), t1), t2)

    => { val tmp1 = n.clone().asInstanceOf[DefaultMutableTreeNode]

         n.setUserObject(new TreeNodeContent(ST_isa(str), Util.string_of(App(App(Const(str, typ), t1), t2))))

         n.add(insert_nodes(t1, tmp1))

         val tmp2 = n.clone().asInstanceOf[DefaultMutableTreeNode]

         n.add(insert_nodes(t2, tmp2))

         n 

      }

    case App(Const(str, typ), t1) 

    => { val tmp = n.clone().asInstanceOf[DefaultMutableTreeNode]

         n.setUserObject(new TreeNodeContent(ST_isa(str), Util.string_of(App(Const(str, typ), t1))))

         n.add(insert_nodes(t1, tmp))

         n 

      }

    case Free(str, _) => { n.setUserObject(str); n }

    case Const(str, _) => { n.setUserObject(str); n }

    case _ => throw new IllegalArgumentException("jtree_of WRONG arg: " + t)

  }

  def jtree_of(t: Term): DefaultMutableTreeNode = insert_nodes(t, new DefaultMutableTreeNode)

  def sound_of_sub(t: Term, line: Integer, indent: Integer): Unit = t match {

    case App(App(Const("Product_Type.Pair", _), t1), t2) 

    => isac.gui.mawen.SoundUtils.tone(261, 500)

    case App(App(Const(str, typ), t1), t2)

    => { isac.gui.mawen.SoundUtils.repeatTone(261+(10*line), 500,indent) //tonhoehe: line, wiederholung: intent

         sound_of_sub(t1, line + 1, indent + 1)

         sound_of_sub(t2, line + 1, indent + 1)

      }

    case App(Const(str, typ), t1) 

    => { isac.gui.mawen.SoundUtils.repeatTone(261+(10*line), 500,indent) //tonhoehe: line, wiederholung: intent

         sound_of_sub(t1, line + 1, indent + 1)

      }

    case Free(str, _) => { 

       isac.gui.mawen.SoundUtils.repeatTone(1000+(10*line), 500,indent)

      }

    case Const(str, _) => { 

       isac.gui.mawen.SoundUtils.repeatTone(2000+(10*line), 500,indent)

      }

    case _ => throw new IllegalArgumentException("sound_of WRONG arg: " + t)

  }

  def sound_of(t: Term) = sound_of_sub(t, 0, 0)

  def is_numeral(s: String): Boolean = {

    try {

      s.toInt; true

    } catch {

      case e: Exception => false

    }

  }

  def matml_of(t: Term, prior: Int, l_r: String): String = t match {

    case App(App(Const("Product_Type.Pair", _), t1), t2) 

    => matml_of(t1, prior, "none") + ", " + matml_of(t2, prior, "none")

    case App(App(Const("Fields.inverse_class.divide", _), t1), t2) 

    => { 

      val str = "Fields.inverse_class.divide"

      val pri = ST_prior(str)

      "<mfrac><mrow>" + matml_of(t1, pri, "left") + "</mrow><mrow>" + matml_of(t2, pri, "right") + "</mrow></mfrac>"

    }

    case App(App(Const(str, _), t1), t2) 

    => { val pri = ST_prior(str)

      if (prior > pri) {

         ST_fix(str) match {

         case "prefix" => "<mfenced separators=\'\'>" + "<mo>" + ST_isa(str) + "</mo>" + matml_of(t1, pri, "left") + 

           "<mfenced separators=\'\'>" + matml_of(t2, pri, "right") + "</mfenced>" + "</mfenced>"

         case _ => "<mfenced separators=\'\'>" + matml_of(t1, pri, "left") + "<mo>" + 

           ST_isa(str) + "</mo>" + matml_of(t2, pri, "right") + "</mfenced>"

         }

      }else{

         ST_fix(str) match {

         case "prefix" => "<mo>" + ST_isa(str) + "</mo>" + matml_of(t1, pri, "none") + " " + matml_of(t2, pri, "none")

         case _ => {

           if (prior == pri & l_r == "right") {

             matml_of(t1, pri, "left") + "<mo>" + ST_isa(str) + "</mo>" + matml_of(t2, pri, "right")

           }else{

             matml_of(t1, pri, "left") + "<mo>" + ST_isa(str) + "</mo>" + matml_of(t2, pri, "right")

           }

         }}

      }

    }

    case App(Const(str, _), t1) => "<mo>" + ST_isa(str) + "</mo>" + "<mfenced separators=\'\'>" + matml_of(t1, prior, "none") + "</mfenced>"

    case Free(str, _) => if (is_numeral(str)) "<mn>" + str + "</mn>" else "<mi>" + str + "</mi>"

    case Const(str, _) => str

    case _ => throw new IllegalArgumentException("matml_of WRONG arg: " + t)

  }

  def mathml_of(t: Term): String = "<math xmlns="+"\"&mathml;\""+"><mrow>" + matml_of(t, 0, "none") + "</mrow></math>"

}