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 edu.tum.cs.isabelle.pure._   // for Term

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

  var post_ast : Ast.Ast = //copied from Isabelle2016-1-MAWEN, types dropped

    Appl(List(

      Constant("_tuple"),  

      Variable("aaa"),

      Appl(List(

        Constant("_tuple_args"),  

        Variable("bbb"),

        Appl(List(

          Constant("_tuple_args"),

          Variable("ccc"),

          Appl(List(

            Constant("_tuple_arg"),  

            Variable("ddd")))))))))

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

    assertEquals(Ast.math_string_of(post_ast), "(aaa, bbb, ccc, ddd)")

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

  }

  def test_tuple_normal() = {

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

    // cp from ScalaTermFromString#test_etc, term_str = "(aaa, bbb, ccc, ddd)"

    var term_from_Isabelle_Isac =

      App(

        App(

          Const("Product_Type.Pair", Type("fun", List(TFree("'a", List("HOL.type")),Type("fun", List(Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type")))))),Type("Product_Type.prod", List(TFree("'a", List("HOL.type")),Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))))))),

          Free("aaa", TFree("'a", List("HOL.type")))),

        App(

          App(

            Const("Product_Type.Pair", Type("fun", List(TFree("'b", List("HOL.type")),Type("fun", List(Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type")))),Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))))),

            Free("bbb", TFree("'b", List("HOL.type")))),

          App(

            App(

              Const("Product_Type.Pair", Type("fun", List(TFree("'c", List("HOL.type")),Type("fun", List(TFree("'d", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))),

              Free("ccc", TFree("'c", List("HOL.type")))),

            Free("ddd", TFree("'d", List("HOL.type"))

          ))

        ))

    var simple_ast = Syntax_Phases.simple_ast_of(term_from_Isabelle_Isac)

    assertEquals(simple_ast,

      Appl(List(  //println(raw_string_of(simple_ast))

        Constant("Product_Type.Pair"),

        Variable("aaa"),

        Appl(List(

          Constant("Product_Type.Pair"),

          Variable("bbb"),

          Appl(List(

            Constant("Product_Type.Pair"), //???vvvvvvvvvvvvv

            Variable("ccc"),

            Variable("ddd")))

          ))

        ))

      )

    var pre_ast : Ast.Ast = simple_ast

//    pre_ast : Ast.Ast =  //copied from Isabelle2016-1-MAWEN, types dropped MAY

//      Appl(List(

//        Constant("Product_Type.Pair"),

//        Variable("aaa"),

//        Appl(List(

//          Constant("Product_Type.Pair"),

//          Variable("bbb"),

//          Appl(List(

//            Constant("Product_Type.Pair"),

//            Appl(List(                     //???^^^^^^^^^^^

//               Variable("ccc"))),

//               Variable("ddd")))))))

    var post_ast : Ast.Ast = //copied from Isabelle2016-1-MAWEN, types dropped

      Appl(List(

        Constant("_tuple"),  

        Variable("aaa"),

        Appl(List(

          Constant("_tuple_args"),  

          Variable("bbb"),

          Appl(List(

            Constant("_tuple_args"),

            Variable("ccc"),

            Appl(List(

              Constant("_tuple_arg"),  

              Variable("ddd")))))))))

    val ast = normalize(XSyntax.print_rules, pre_ast)

    assertEquals(ast, post_ast)        // LETZTES "_tuple_args" <> "_tuple_args"

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

  }

  def test_matches() = {

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

    // at this ast rule 2 should match

    val ML4_2old_ast = //AFTER rewrite 3, rule 2, from ###ML old_ast

      Appl(List(

        Constant("_tuple"),  

        Variable("bbb"),

        Appl(List(

          Constant("_tuple_arg"),   //<---vv

          Appl(List(

            Constant("_tuple"),     //<---^^

              Variable("ccc"),

              Appl(List(

                Constant("_tuple_arg"),  

                Variable("ddd")))  ))))))   //->

    val ML4_2lhs = //AFTER rewrite 3, rule 2, from ###ML try_rules lhs:

      Appl(List(

        Constant("_tuple"),

        Variable("x"),

        Appl(List(

          Constant("_tuple_arg"),

          Appl(List(

            Constant("_tuple"),

            Variable("y"),

            Variable("z"))))))) 

    var ast_pat = (ML4_2old_ast, ML4_2lhs)

    // println("matches(ast_pat): " + matches(ast_pat))

    // matches(ast_pat): Some((Map(x -> Variable(bbb), y -> Variable(ccc), z -> Appl(List(Constant(_tuple_arg), Variable(ddd)))),List()))

    assertTrue((!(matches(ast_pat)).isEmpty))

    val scala4_2old_ast = //AFTER rewrite 3, NO rule 1, from ###post.scala:

      Appl(List(

        Constant("_tuple"),

        Variable("aaa"),

        Appl(List(

          Constant("_tuple_arg"),   //<---vv pattern from ###ML 4. rule 2 NOT RECOGNISED

          Appl(List(

            Constant("_tuple"),     //<---^^ pattern from ###ML 4. rule 2 NOT RECOGNISED

            Variable("bbb"),

            Appl(List(

              Constant("_tuple_arg"),     //<---vv pattern from ###ML 4. rule 2 NOT RECOGNISED

              Appl(List(

                Constant("_tuple"),       //<---^^ pattern from ###ML 4. rule 2 NOT RECOGNISED

                Variable("ccc"),

                Appl(List(

                  Constant("_tuple_arg"),

                  Variable("ddd")))))))))))))

    ast_pat = (scala4_2old_ast, ML4_2lhs)

    // println("matches(ast_pat): " + matches(ast_pat))

    // matches(ast_pat): Some((Map(x -> Variable(aaa), y -> Variable(bbb), z -> Appl(List(Constant(_tuple_arg), Appl(List(Constant(_tuple), Variable(ccc), Appl(List(Constant(_tuple_arg), Variable(ddd)))))))),List()))

    assertTrue((!(matches(ast_pat)).isEmpty))

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

  }

  def test_update() {

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

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

    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_get_value() {

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

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

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

    assertEquals("a", math_string_of(get_value (List(2,2), ast)))

    assertEquals("b + c", math_string_of(get_value (List(2,3), ast)))

    assertEquals("b", math_string_of(get_value (List(2,3,2), ast)))

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

  }

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

  }

}