package isac.gui.mawen.scalaterm

 import isac.gui.mawen.syntax.XSyntax

 import isac.gui.mawen.syntax.Ast

 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)

   /* 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 = XSyntax.isa_prior(str)

       if (prior > pri) {

          XSyntax.isa_fix(str) match {

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

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

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

       }else{

          XSyntax.isa_fix(str) match {

          case "infixl" => {

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

              "(" + str_of(t1, pri, "left") + XSyntax.isa_math(str) + str_of(t2, pri, "right") + ")"

            }else{

              str_of(t1, pri, "left") + XSyntax.isa_math(str) + str_of(t2, pri, "right")

            }

          }

          case "infixr" => {

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

              "(" + str_of(t1, pri, "left") + XSyntax.isa_math(str) + str_of(t2, pri, "right") + ")"

            }else{

              str_of(t1, pri, "left") + XSyntax.isa_math(str) + str_of(t2, pri, "right")

            }

          }

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

       }}

     case App(Const(str, _), t1) => XSyntax.isa_math(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 insert_nodes(t: Ast.Ast, n: DefaultMutableTreeNode): DefaultMutableTreeNode = t match {

     case Ast.Appl(List(Ast.Appl(List(Ast.Constant("Product_Type.Pair"), t1)), t2))

     => n //TODO

     case Ast.Appl(List(Ast.Appl(List(Ast.Constant(str), t1)), t2))

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

          n.setUserObject(new TreeNodeContent(XSyntax.ast_math(str),

              Ast.math_string_of(Ast.Appl(List(Ast.Appl(List(Ast.Constant(str), t1)), t2)))))

          n.add(insert_nodes(t1, tmp1))

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

          n.add(insert_nodes(t2, tmp2))

          n 

       }

     case Ast.Appl(List(Ast.Constant(str), t1))

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

          n.setUserObject(new TreeNodeContent(XSyntax.ast_math(str),

              Ast.math_string_of(Ast.Appl(List(Ast.Constant(str), t1)))))

          n.add(insert_nodes(t1, tmp))

          n 

       }

     case Ast.Variable(str) => { n.setUserObject(str); n }

     case Ast.Constant(str) => { n.setUserObject(str); n }

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

   }

   def jtree_of(t: Ast.Ast): DefaultMutableTreeNode = insert_nodes(t, new DefaultMutableTreeNode)

  /*

   * Code not adapted to migration from Term to Ast.

   * 

   structure beeped in java class SoundUtils - necessary to beep other components?

   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.termtree.SoundUtils.tone(261, 500)

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

     => { isac.gui.mawen.termtree.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.termtree.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.termtree.SoundUtils.repeatTone(1000+(10*line), 500,indent)

       }

     case Const(str, _) => { 

        isac.gui.mawen.termtree.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 = XSyntax.isa_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 = XSyntax.isa_prior(str)

       if (prior > pri) {

          XSyntax.isa_fix(str) match {

          case "prefix" => "<mfenced separators=\'\'>" + "<mo>" + XSyntax.isa_math(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>" + 

            XSyntax.isa_math(str) + "</mo>" + matml_of(t2, pri, "right") + "</mfenced>"

          }

       }else{

          XSyntax.isa_fix(str) match {

          case "prefix" => "<mo>" + XSyntax.isa_math(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>" + XSyntax.isa_math(str) + "</mo>" + matml_of(t2, pri, "right")

            }else{

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

            }

          }}

       }

     }

     case App(Const(str, _), t1) => "<mo>" + XSyntax.isa_math(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>"

 }