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

}