/**

 * @author Walther Neuper

 * Created on May 18, 2017

 * (c) due to copyright terms

 */

package isac.gui.mawen

import isac.bridge.Isabelle_Isac

import isac.bridge.xml.DataTypes

import isac.gui.mawen.syntax.Ast._   //"._" simplifies "Ast.Ast" to "Ast"

import edu.tum.cs.isabelle.japi._

import junit.framework.TestCase

import org.junit.Assert._

/**

 * Use Cases from Marco Mahringer's master thesis.

 * We assert <code>Ast.math_string_of</code>, because <code>Formula.math_text_</code>'s String

 * is used for transfer of formulas for front-end --> Isabelle_Isac.

 * References use labels in mmahringer-master.tex.

 */

class TestUseCases extends TestCase {

  var sys_ : JSystem = null

  override def setUp() {

    sys_ = Isabelle_Isac.connect();

  }

  /* mmahringer-master.tex \label{UC:user-guide} */

  def testUC_userguide() {

    println("/--BEGIN isac.gui.mawen.TestUseCases#testUC_userguide");

    var term_str = "d_d x x + d_d x (sin (x ^ 2))"

    var tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    var form = DataTypes.xml_to_Formula_NEW(tree)

    var ast = form.getTerm

    //println(Ast.raw_string_of(ast))

    assertEquals(ast, 

      Appl(List(

        Constant("Groups.plus_class.plus"),

        Appl(List(

          Constant("Diff.d_d"),

          Variable("x"),

          Variable("x"))),

        Appl(List(

          Constant("Diff.d_d"),

          Variable("x"),

          Appl(List(

            Constant("Transcendental.sin"),

            Appl(List(

              Constant("Power.power_class.power"),

              Variable("x"),

              Variable("2"))))))))))

    //println(Ast.math_string_of(ast))

    assertEquals(math_string_of(ast), term_str)

    val ast_05 =  // copied to TestData.scala

      Appl(List(

        Constant("Groups.plus_class.plus"),

        Appl(List(

          Constant("Diff.d_d"),

          Variable("x"),

          Variable("x"))),

        Appl(List(

          Constant("Diff.d_d"),

          Variable("x"),

          Appl(List(                 //added to above

            Constant("BOX.1"),       //added to above

            Appl(List(

              Constant("Transcendental.sin"),

              Appl(List(             //added to above

                Constant("BOX.2"),   //added to above

                Appl(List(

                  Constant("Power.power_class.power"),

                  Variable("x"),

                  Variable("2")))))))))))))

    term_str = "d_d bdv (sin (u)) = cos (u) * d_d bdv u"

    tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    form = DataTypes.xml_to_Formula_NEW(tree)

    ast = form.getTerm

    //println(Ast.raw_string_of(ast))

    assertEquals(ast, 

      Appl(List(

        Constant("HOL.eq"),

        Appl(List(

          Constant("Diff.d_d"),

          Variable("bdv"),

          Appl(List(

            Constant("Transcendental.sin"),

            Variable("u"))))),

        Appl(List(

          Constant("Groups.times_class.times"),

          Appl(List(

            Constant("Transcendental.cos"),

            Variable("u"))),

          Appl(List(

            Constant("Diff.d_d"),

            Variable("bdv"),

            Variable("u"))))))))

    //println(Ast.math_string_of(ast))

    assertEquals(math_string_of(ast), term_str)

    val ast_06 = // copied to TestData.scala

      Appl(List(

        Constant("HOL.eq"),

        Appl(List(

          Constant("Diff.d_d"),

          Variable("bdv"),

          Appl(List(                 //added to above

            Constant("BOX.1"),       //added to above

            Appl(List(

              Constant("Transcendental.sin"),

              Appl(List(             //added to above

                Constant("BOX.2"),   //added to above

                Variable("u"))))))))),

        Appl(List(

          Constant("Groups.times_class.times"),

          Appl(List(                 //added to above

            Constant("BOX.3"),       //added to above

            Appl(List(

              Constant("Transcendental.cos"),

              Variable("u"))))),

          Appl(List(

            Constant("Diff.d_d"),

            Variable("bdv"),

            Appl(List(               //added to above

              Constant("BOX.4"),     //added to above

              Variable("u")))))))))

    term_str = "d_d x x + cos (x ^ 2) * d_d x GAP"

    tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    form = DataTypes.xml_to_Formula_NEW(tree)

    ast = form.getTerm

    //println(Ast.raw_string_of(ast))

    assertEquals(ast, 

      Appl(List(

        Constant("Groups.plus_class.plus"),

        Appl(List(

          Constant("Diff.d_d"),

          Variable("x"),

          Variable("x"))),

        Appl(List(

          Constant("Groups.times_class.times"),

          Appl(List(

            Constant("Transcendental.cos"),

            Appl(List(

              Constant("Power.power_class.power"),

              Variable("x"),

              Variable("2"))))),

          Appl(List(

            Constant("Diff.d_d"),

            Variable("x"),

            Variable("GAP")))))))) //NOT Constant("#"), because comes from Isabelle_Isac

    //println(Ast.math_string_of(ast))

    assertEquals(math_string_of(ast), term_str) //Isabelle requires (sin (x ^ 2)

    val ast_07 = // copied to TestData.scala

      Appl(List(

        Constant("Groups.plus_class.plus"),

        Appl(List(

          Constant("Diff.d_d"),

          Variable("x"),

          Variable("x"))),

        Appl(List(

          Constant("Groups.times_class.times"),

          Appl(List(                 //added to above

            Constant("BOX.3"),       //added to above

            Appl(List(

              Constant("Transcendental.cos"),

              Appl(List(

                Constant("Power.power_class.power"),

                Variable("x"),

                Variable("2"))))))),

          Appl(List(

            Constant("Diff.d_d"),

            Variable("x"),

            Appl(List(               //added to above

              Constant("BOX.4"),     //added to above

              Variable("GAP")))))))))

    println("\\--END isac.gui.mawen.TestUseCases#testUC_userguide");

  }

  /* mmahringer-master.tex \label{UC:mult-frac} */

  def testUC_multfrac() {

    println("/--BEGIN isac.gui.mawen.TestUseCases#testUC_multfrac");

    var term_str = "Simplify (1 + 1 / 2 + (2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^ 2 - 9)))"

    var tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    var form = DataTypes.xml_to_Formula_NEW(tree)

    var ast = form.getTerm

    assertEquals(ast,

      Appl(List(Constant("Simplify.Simplify"), Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Groups.plus_class.plus"), Variable("1"), Appl(List(Constant("Fields.inverse_class.divide"), Variable("1"), Variable("2"))))), Appl(List(Constant("Fields.inverse_class.divide"), Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Fields.inverse_class.divide"), Variable("2"), Appl(List(Constant("Groups.plus_class.plus"), Variable("x"), Variable("3"))))), Appl(List(Constant("Fields.inverse_class.divide"), Variable("2"), Appl(List(Constant("Groups.minus_class.minus"), Variable("x"), Variable("3"))))))), Appl(List(Constant("Fields.inverse_class.divide"), Appl(List(Constant("Groups.times_class.times"), Variable("8"), Variable("x"))), Appl(List(Constant("Groups.minus_class.minus"), Appl(List(Constant("Power.power_class.power"), Variable("x"), Variable("2"))), Variable("9"))))))))))))

    assertEquals(term_str, math_string_of(ast))

    term_str = "1 + 1 / 2 + (2 / (x + 3) + 2 / (x - 3)) / (8 * x / (x ^ 2 - 9))"

    tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    form = DataTypes.xml_to_Formula_NEW(tree)

    ast = form.getTerm

    assertEquals(ast,

      Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Groups.plus_class.plus"), Variable("1"), Appl(List(Constant("Fields.inverse_class.divide"), Variable("1"), Variable("2"))))), Appl(List(Constant("Fields.inverse_class.divide"), Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Fields.inverse_class.divide"), Variable("2"), Appl(List(Constant("Groups.plus_class.plus"), Variable("x"), Variable("3"))))), Appl(List(Constant("Fields.inverse_class.divide"), Variable("2"), Appl(List(Constant("Groups.minus_class.minus"), Variable("x"), Variable("3"))))))), Appl(List(Constant("Fields.inverse_class.divide"), Appl(List(Constant("Groups.times_class.times"), Variable("8"), Variable("x"))), Appl(List(Constant("Groups.minus_class.minus"), Appl(List(Constant("Power.power_class.power"), Variable("x"), Variable("2"))), Variable("9"))))))))))

    assertEquals(term_str, math_string_of(ast))

    println("\\--END isac.gui.mawen.TestUseCases#testUC_multfrac");

  }

  //\label{UC:gaps} --------------------------------------------------------------------

  /*

	TODO in cooperation with mmahringer

   */

  /* mmahringer-master.pdf \label{UC:eng-math} */

  def testUC_engmath() {

    println("/--BEGIN isac.gui.mawen.TestUseCases#testUC_engmath");

    // the integral's "D x" is only input, NOT output                                            -------------vvv

    //assertEquals("y (x) = Integral (c_3 + 1 / (-1 * EI ) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3)) x"

    var term_str = "y (x) = Integral (c_3 + 1 / (-1 * EI ) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3)) D x"

    var tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    var form = DataTypes.xml_to_Formula_NEW(tree)

    var ast = form.getTerm

    assertEquals(ast,    

      Appl(List(

        Constant("HOL.eq"),

        Appl(List(Variable/*NOT Constant*/("y"), Variable("x"))),

        Appl(List(

          Constant("Integrate.Integral"),

          Appl(List(

            Constant("Groups.plus_class.plus"),

            Variable("c_3"),

            Appl(List(

              Constant("Groups.times_class.times"),

              Appl(List(

                Constant("Fields.inverse_class.divide"),

                Variable("1"),

                Appl(List(

                  Constant("Groups.times_class.times"),

                  Variable("-1"),

                  Constant("Biegelinie.EI"))))),

                  Appl(List(

                    Constant("Groups.plus_class.plus"),

                    Appl(List(

                      Constant("Groups.plus_class.plus"),

                      Appl(List(

                        Constant("Groups.times_class.times"), Variable("c_2"), Variable("x"))),

                      Appl(List(

                        Constant("Groups.times_class.times"),

                          Appl(List(

                            Constant("Fields.inverse_class.divide"), Variable("c"), Variable("2"))),

                          Appl(List(

                            Constant("Power.power_class.power"), Variable("x"), Variable("2"))))))),

                    Appl(List(

                      Constant("Groups.times_class.times"),

                      Appl(List(

                        Constant("Fields.inverse_class.divide"),

                        Appl(List(

                          Constant("Groups.times_class.times"), Variable("-1"), Variable("q_0"))),

                        Variable("6"))),

                      Appl(List(Constant("Power.power_class.power"), Variable("x"), Variable("3"))))))))))),

          Variable("x")))))

    )

    assertEquals("y (x) = Integral (c_3 + 1 / (-1 * EI ) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3)) x", 

      math_string_of(ast))

    //NOTE: -----------vv (reason unclear):

    //term_str = "Problem (Biegelinie, [setzeRandbedingungen, Biegelinien])"  //NOT ok

    term_str =    "Probl (Biegelinie , [setzeRandbedingungen, Biegelinien])"  //OK

    tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    form = DataTypes.xml_to_Formula_NEW(tree)

    ast = form.getTerm

    //println(math_string_of(ast))

    assertEquals(term_str, math_string_of(ast))

    term_str = "[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]"

    tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    form = DataTypes.xml_to_Formula_NEW(tree)

    ast = form.getTerm

    //println(raw_string_of(ast))

    assertEquals(ast,    

      Appl(List(Constant("_list"), Appl(List(Constant("_args"), Appl(List(Constant("HOL.eq"), Appl(List(Constant("Groups.times_class.times"), Variable("L"), Variable("q_0"))), Variable("c"))), Appl(List(Constant("_args"), Appl(List(Constant("HOL.eq"), Variable("0"), Appl(List(Constant("Fields.inverse_class.divide"), Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Groups.times_class.times"), Variable("2"), Variable("c_2"))), Appl(List(Constant("Groups.times_class.times"), Appl(List(Constant("Groups.times_class.times"), Variable("2"), Variable("L"))), Variable("c"))))), Appl(List(Constant("Groups.times_class.times"), Appl(List(Constant("Groups.times_class.times"), Variable("-1"), Appl(List(Constant("Power.power_class.power"), Variable("L"), Variable("2"))))), Variable("q_0"))))), Variable("2"))))), Appl(List(Constant("_args"), Appl(List(Constant("HOL.eq"), Variable("0"), Variable("c_4"))), Appl(List(Constant("HOL.eq"), Variable("0"), Variable("c_3")))))))))))

    )    

    assertEquals(term_str, math_string_of(ast))

    println("\\--END isac.gui.mawen.TestUseCases#testUC_engmath");

  }

  /* mmahringer-master.pdf \label{UC:if-then-else} */

  def testUC_ifthenelse() {

    println("/--BEGIN isac.gui.mawen.TestUseCases#testUC_ifthenelse");

    //if 0 < n then fac n = n * fac (n - 1) else 1

      //NOTE:  Isabelle error messages indicates problems with termination

      //  Coercion inference failed:

      //  no supremum

      //  

      //  Cannot fulfil subtype constraints:

      //    bool  <:  ??'a   from function Application  If (0 < n) (fac n = n * fac (n - 1))

      //    ??'a  <:  ??'b   from function Ast.Application

      //      if 0 < n then fac n = n * fac (n - 1) else 1

    var term_str = 

      "Program Simplify t_t =" +

      "  Repeat (" +

      "    Try (Rewrite_Set klammern_aufloesen False) @@" +

      "    Try (Rewrite_Set ordne_alphabetisch False) @@" +

      "    Try (Rewrite_Set fasse_zusammen False) @@" +

      "    Try (Rewrite_Set verschoenere False)) t_t"

    //NOTE: pretty blocks have not yet been considered

    var tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)

    var form = DataTypes.xml_to_Formula_NEW(tree)

    var ast = form.getTerm

    assertEquals(ast,

      Appl(List(Constant("HOL.eq"), Appl(List(Variable("Program"), Constant("Simplify.Simplify"), Variable("t_t"))), Appl(List(Constant("Script.Repeat"), Appl(List(Constant("Script.Seq"), Appl(List(Constant("Script.Try"), Appl(List(Constant("Script.Rewrite'_Set"), Variable("klammern_aufloesen"), Constant("HOL.False"))))), Appl(List(Constant("Script.Seq"), Appl(List(Constant("Script.Try"), Appl(List(Constant("Script.Rewrite'_Set"), Variable("ordne_alphabetisch"), Constant("HOL.False"))))), Appl(List(Constant("Script.Seq"), Appl(List(Constant("Script.Try"), Appl(List(Constant("Script.Rewrite'_Set"), Variable("fasse_zusammen"), Constant("HOL.False"))))), Appl(List(Constant("Script.Try"), Appl(List(Constant("Script.Rewrite'_Set"), Variable("verschoenere"), Constant("HOL.False"))))))))))), Variable("t_t")))))

    )

    assertEquals(math_string_of(ast), "Program Simplify  t_t = Repeat (Seq (Try (Rewrite'_Set klammern_aufloesen False )) (Seq (Try (Rewrite'_Set ordne_alphabetisch False )) (Seq (Try (Rewrite'_Set fasse_zusammen False )) (Try (Rewrite'_Set verschoenere False ))))) t_t")

    println("\\--END isac.gui.mawen.TestUseCases#testUC_ifthenelse");

  }

  override def tearDown() {

    sys_.dispose()

    super.tearDown()

  }

}