package isac.gui.mawen.syntax

import isac.gui.mawen.scalaterm.TestsDATA

import isac.gui.mawen.TestDATA

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

import isac.gui.mawen.syntax.isabelle.XLibrary

import isac.gui.mawen.editor.TestDATAeditor

import junit.framework.TestCase

import org.junit.Assert._

class TestAst extends TestCase {

   // x / y

  def a1 = Appl(List(Constant("Fields.inverse_class.divide"), Variable ("x"), Variable ("y")))

  // a * b / c

  def a2 = Appl(List(Constant("Groups.times_class.times"), Variable ("a"), Appl(List(Constant("Fields.inverse_class.divide"), Variable("b"), Variable("c")))))

  // sin(a + b) / c

  def a3 = Appl(List

      (Constant("Fields.inverse_class.divide"), 

          Appl(List(Constant("sin"), 

              Appl(List(Constant("Groups.plus_class.plus"), 

                  Variable("a"), 

                  Variable("b")

              ))

          ))

          ,Variable ("c")

      ))

  def a4 = Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Groups.plus_class.plus"), Variable("a"), Variable("b"))), Variable("c")))

  def a5 = Appl(List(Constant("Groups.plus_class.plus"), Variable("a"), Appl(List(Constant("Groups.plus_class.plus"), Variable("b"), Variable("c")))))

  def test_prefix_string_of() {

    println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_prefix_string_of");

    assertEquals(Ast.prefix_string_of(a1), "/ x y")

    assertEquals(Ast.prefix_string_of(a2), "* a / b c")

    assertEquals(Ast.prefix_string_of(a3), "/ sin + a b c")

    println("\\--END isac.gui.mawen.asttrans.TestAst#test_prefix_string_of");

  }

    def test_math_string_of() {

    println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_math_string_of");

    assertEquals(Ast.math_string_of(a1), "x / y")

    assertEquals(Ast.math_string_of(a2), "a * (b / c)")

    assertEquals(Ast.math_string_of(a3), "sin (a + b) / c")

    assertEquals(Ast.math_string_of(a4), "a + b + c")

    assertEquals(Ast.math_string_of(a5), "a + (b + c)")

    println("\\--END isac.gui.mawen.asttrans.TestAst#test_math_string_of");

  }

  /* 

   * The examples for reference of Natalie Karl initially took terms,

   * @see isac.gui.mawen.scalaterm.TestUtil.

   * Here we check, whether term_to_ast + Ast.string_of give the same result.

   */

  def test_examples_for_NK() {

    println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_examples_for_NK");

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t1)),

        "aaa + bbb = processed_by_Isabelle_Isac ")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t2)), 

        "a + 2 * b + 3 * (c + d)")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t31)), 

        "aaa + bbb + ccc")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t32)), 

        "aaa + (bbb + ccc)")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t41)), 

        "Diff (x + sin (x ^ 2), x)")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t42)), 

        "d_d x (x + sin (x ^ 2))")

    // MAWEN example for reference No.1

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt1())), 

        "Simplify (1 + 2 * x * (y + 3) / (4 * z * (y + 3)) + 5)")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt3())), 

        "1 + 2 * x * (y + 3) / (4 * z * (y + 3)) + 5")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt4())), 

        "1 + 2 * x / (4 * z) + 5")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt5())), 

        "1 + x / (2 * z) + 5")

    assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt6())), 

        "6 + x / (2 * z)")

    println("\\--END isac.gui.mawen.asttrans.TestAst#test_examples_for_NK");

  }

  //test additional examples with BOX, CURSOR, GAP

  def test_BOX_CURSOR_GAP() {

    println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_BOX_CURSOR_GAP");

    assertEquals("aaa + bbb", Ast.math_string_of(TestDATAeditor.nest_BOX_1))   

    assertEquals("aaa + bbb", Ast.math_string_of(TestDATAeditor.nest_BOX_2))   

    assertEquals("aaa + bbb", Ast.math_string_of(TestDATAeditor.nest_BOX_3))

    assertEquals("aaa + bbb", Ast.math_string_of(TestDATAeditor.nest_BOX_1_CURSOR))   

    assertEquals(  "# + bbb", Ast.math_string_of(TestDATAeditor.nest_BOX_1_CURSOR_GAP))

    assertEquals("aaa + bbb", Ast.math_string_of(TestDATAeditor.nest_BOX_1_CURSOR_b))

    assertEquals("aaa + bbb", Ast.math_string_of(TestDATAeditor.nest_CURSOR_BOX_3A))   

    assertEquals("aaa + bbb", Ast.math_string_of(TestDATAeditor.nest_CURSOR_BOX_3B))

    assertEquals("d_d x x + d_d x (sin (x ^ 2))", Ast.math_string_of(TestDATAeditor.box_05))   

    assertEquals("d_d bdv (sin (u)) = cos (u) * d_d bdv u", Ast.math_string_of(TestDATAeditor.box_06))   

    assertEquals("d_d x x + cos (x ^ 2) * d_d x #", Ast.math_string_of(TestDATAeditor.box_07_with_cursor))   

    assertEquals("a + (# + c)", Ast.math_string_of(TestDATAeditor.box_gap_cursor))   

    assertEquals("#", Ast.math_string_of(TestDATAeditor.box_with_cursor_on_gap))   

    assertEquals("# + #", Ast.math_string_of(TestDATAeditor.in_1a))   

    assertEquals("a + # / #", Ast.math_string_of(TestDATAeditor.in_1b))   

    assertEquals("a + b / #", Ast.math_string_of(TestDATAeditor.in_1c))   

    println("\\--END isac.gui.mawen.asttrans.TestAst#test_BOX_CURSOR_GAP");

  }

    /* from Isabelle2016-1-MAWEN ast.ML: 

     * fun try_rules ((lhs, rhs) :: pats) ast = (*WN*)

     * 

     * lemma "[aaa,bbb] = ddd" --- term_to_ast ---

     * with types dropped in ast and rule.

     * 

     * assert was too expensive at this moment.

     */

  def test_list_normal() {

    println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_list_normal");

    //======= 1.successful application 

    //###try_rules ast: Appl[Constant("List.list.Cons"), Appl[Constant("_constrain"), Appl[Constant("_free"), Variable("bbb"]), Appl[Constant("_ofsort"), Appl[Constant("_tfree"), Variable("'a"]), Constant("\ <^class>HOL.type"]]), Constant("List.list.Nil"]) 

    //###try_rules lhs: Appl[Constant("List.list.Cons"), Variable("x"), Constant("List.list.Nil"]) 

    //###try_rules rhs: Appl[Constant("_list"), Variable("x"]) 

    //------- ast in try_rules (from additional output):

    var ast =

      Ast.Appl(List(

        Ast.Constant("List.list.Cons"),

        Ast.Variable("bbb"),

        Ast.Constant("List.list.Nil")))

    var lhs =

      Appl(List(

        Constant("List.list.Cons"),

        Variable("x"),

        Constant("List.list.Nil")))

    var rhs =

      Appl(List(

        Constant("_list"),

        Variable("x")))

    assertEquals(Ast.matches(ast, lhs), Some((Map("x" -> Variable("bbb")),List())))

    // //--------------- tests BEFORE made local to normalize ---------------\\

    //assertEquals(Ast.xtry(ast, "List.list.Cons"), Some(Appl(List(Constant("_list"), Variable("bbb")))))

    //assertEquals(Ast.try_rules(XSyntax.print_rules("List.list.Cons"), ast), Some(Appl(List(Constant("_list"), Variable("bbb")))))

    //assertEquals(Ast.try_rules(List((lhs, rhs)), ast), Some(Appl(List(Constant("_list"), Variable("bbb")))))

    //assertEquals(Ast.rewrite(ast), Some(Appl(List(Constant("_list"), Variable("bbb")))))

    //assertEquals(Ast.norm_root(ast), Appl(List(Constant("_list"), Variable("bbb"))))

    //assertEquals(Ast.norm(ast),      Appl(List(Constant("_list"), Variable("bbb"))))

    //assertEquals(Ast.normal(ast),    Appl(List(Constant("_list"), Variable("bbb"))))

    // \\--------------- tests BEFORE made local to normalize ---------------//

    assertEquals(Ast.normalize(XSyntax.print_rules, ast), Appl(List(Constant("_list"), Variable("bbb"))))

    //------- whole ast calling try_rules:

    ast =

      Ast.Appl(List(

        Ast.Constant("List.list.Cons"),

        Ast.Variable("aaa"),

        Ast.Appl(List(

          Ast.Constant("List.list.Cons"),

          Ast.Variable("bbb"),

          Ast.Appl(List(

            Ast.Constant("List.list.Cons"),

            Ast.Variable("ccc"),

            Ast.Constant("List.list.Nil")))))))            

    assertEquals(Ast.matches(ast, lhs), None) //--> None: the rewriter calls try_rules!

    // //--------------- tests BEFORE made local to normalize ---------------\\

    //assertEquals(Ast.xtry(ast, "List.list.Cons"), None)

    //assertEquals(Ast.try_rules(XSyntax.print_rules("List.list.Cons"), ast), None)

    //assertEquals(Ast.try_rules(List((lhs, rhs)), ast), None)

    //assertEquals(Ast.rewrite(ast), None)

    //assertEquals(Ast.norm_root(ast), Appl(List(Constant("List.list.Cons"), Variable("aaa"), Appl(List(Constant("List.list.Cons"), Variable("bbb"), Appl(List(Constant("List.list.Cons"), Variable("ccc"), Constant("List.list.Nil"))))))))

    //assertEquals(Ast.normal(ast),    Appl(List(Constant("_list"), Appl(List(Constant("_args"), Variable("aaa"), Appl(List(Constant("_args"), Variable("bbb"), Variable("ccc"))))))))

    //assertEquals(Ast.normal(ast),    Appl(List(Constant("_list"), Appl(List(Constant("_args"), Variable("aaa"), Appl(List(Constant("_args"), Variable("bbb"), Variable("ccc"))))))))

    // \\--------------- tests BEFORE made local to normalize ---------------//

    assertEquals(Ast.normalize(XSyntax.print_rules, ast),

      Appl(List(

        Constant("_list"), Appl(List(

          Constant("_args"), Variable("aaa"), Appl(List(

            Constant("_args"), Variable("bbb"), Variable("ccc"))))))))

    /* output from Isabelle_Isac adds types to above structure:

       Appl(List(

/*_list*/Constant("_list"), Appl(List(

/*_args*/  Constant("_args"), Appl(List(

             Constant("_constrain"), Appl(List(

/* aaa */      Constant("_free"), Variable("aaa"))), Appl(List(

                 Constant("_ofsort"), Appl(List(

                   Constant("_tfree"), Variable("'a"))), Constant("\\<^class>HOL.type"))))), Appl(List(

/*_args*/            Constant("_args"), Appl(List(

                       Constant("_constrain"), Appl(List(

/* bbb */                Constant("_free"), Variable("bbb"))), Appl(List(

                           Constant("_ofsort"), Appl(List(

                             Constant("_tfree"), Variable("'a"))), Constant("\\<^class>HOL.type"))))), Appl(List(

                               Constant("_constrain"), Appl(List(

/* ccc */                        Constant("_free"), Variable("ccc"))), Appl(List(

                                   Constant("_ofsort"), Appl(List(

                                     Constant("_tfree"), Variable("'a"))), Constant("\\<^class>HOL.type")))))))))))

     */

    ast =

      Appl(List(

        Constant("_list"), Appl(List(

          Constant("_args"), Variable("aaa"), Appl(List(

            Constant("_args"), Variable("bbb"), Variable("ccc")))))))    

    assertEquals("[aaa, bbb, ccc]", Ast.math_string_of(ast))

    println("\\--END isac.gui.mawen.asttrans.TestAst#test_list_normal");

  }

  val ast =

/*List()*/    Appl(List(

/*List(1)*/     Constant("Groups.plus_class.plus"),

/*List(2)*/     Appl(List(

/*List(2,1)*/     Constant("Groups.plus_class.plus"),

/*List(2,2)*/     Variable("a"),

/*List(2,3)*/     Appl(List(

/*List(2,3,1)*/     Constant("Groups.plus_class.plus"),

/*List(2,3,2)*/     Variable("b"),

/*List(2,3,3)*/     Variable("c"))) )),

/*List(3)*/     Variable("d")))

  def test_update() {

    println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_update");

    assertEquals("a + (b + c) + d", math_string_of(ast))

    assertEquals("X  + d", math_string_of(add(List(2), Constant("X"), ast)))

    assertEquals("X  + (b + c) + d", math_string_of(add(List(2,2), Constant("X"), ast)))

    assertEquals("a + (X  + c) + d", math_string_of(add(List(2,3,2), Constant("X"), ast)))

    assertEquals("a + (b + X ) + d", math_string_of(add(List(2,3,3), Constant("X"), ast)))

    assertEquals("a + (b + c) + X ", math_string_of(add(List(3), Constant("X"), ast)))

    assertEquals("X + Y + d", math_string_of(add(List(2),

        Appl(List(

         Constant("Groups.plus_class.plus"),

         Variable("X"),

         Variable("Y"))), ast)))

    println("\\--END isac.gui.mawen.asttrans.TestAst#test_update");

  }

  def test_math_string_of_arbitrary() {

    println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_math_string_of_arbitrary");

    val arbitrary = Appl(List(Variable("a"), Constant("b"),

      Appl(List(Constant("Groups.plus_class.plus"), Variable("c"),Variable("d"))),

      Appl(List(Variable("y"),Variable("x"))) ))

    assertEquals("a b  (c + d) (y (x))", math_string_of(arbitrary))

    println("\\--END isac.gui.mawen.asttrans.TestAst#test_math_string_of_arbitrary");

  }

}