Mercurial Mercurial > wneuper > isac / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala
author Walther Neuper <wneuper@ist.tugraz.at>
Sun, 18 Jun 2017 15:10:05 +0200
changeset 5137 dd797d56d238
parent 5123 b9dbd51ae5cf
child 5138 8a471d24281c
permissions -rw-r--r--
ast-translation for tuple

Notes:
* syntax.scala: symtab : TreeMap requires specific entry for Ast.try_headless_rules
* the tracing code will be removed in the next changeset 
     1 package isac.gui.mawen.syntax

     2 

     3 import isac.gui.mawen.scalaterm.TestsDATA

     4 import isac.gui.mawen.TestDATA

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

     6 import edu.tum.cs.isabelle.pure._   // for Term

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

     8 import isac.gui.mawen.editor.TestDATAeditor

     9 

    10 import junit.framework.TestCase

    11 import org.junit.Assert._

    12 

    13 

    14 class TestAst extends TestCase {

    15 

    16    // x / y

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

    18   

    19   // a * b / c

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

    21   

    22   // sin(a + b) / c

    23   def a3 = Appl(List

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

    25           Appl(List(Constant("sin"), 

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

    27                   Variable("a"), 

    28                   Variable("b")

    29               ))

    30           ))

    31           ,Variable ("c")

    32       ))

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

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

    35   

    36   def test_prefix_string_of() {

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

    38     

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

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

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

    42     

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

    44   }

    45   

    46     def test_math_string_of() {

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

    48     

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

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

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

    52 

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

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

    55     

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

    57   }

    58   

    59   /* 

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

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

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

    63    */

    64   def test_examples_for_NK() {

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

    66 

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

    68         "aaa + bbb = processed_by_Isabelle_Isac ")

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

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

    71 

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

    73         "aaa + bbb + ccc")

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

    75         "aaa + (bbb + ccc)")

    76 

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

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

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

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

    81     

    82     // MAWEN example for reference No.1

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

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

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

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

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

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

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

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

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

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

    93 

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

    95   }

    96 

    97   //test additional examples with BOX, CURSOR, GAP

    98   def test_BOX_CURSOR_GAP() {

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

   100     

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

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

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

   104 

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

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

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

   108 

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

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

   111 

   112 

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

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

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

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

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

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

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

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

   121 

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

   123   }

   124 

   125 

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

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

   128      * 

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

   130      * with types dropped in ast and rule.

   131      * 

   132      * assert was too expensive at this moment.

   133      */

   134   def test_list_normal() {

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

   136     

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

   138     //###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"]) 

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

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

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

   142     var ast =

   143       Ast.Appl(List(

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

   145         Ast.Variable("bbb"),

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

   147     var lhs =

   148       Appl(List(

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

   150         Variable("x"),

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

   152     var rhs =

   153       Appl(List(

   154         Constant("_list"),

   155         Variable("x")))

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

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

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

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

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

   161 

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

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

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

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

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

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

   168 

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

   170     ast =

   171       Ast.Appl(List(

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

   173         Ast.Variable("aaa"),

   174         Ast.Appl(List(

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

   176           Ast.Variable("bbb"),

   177           Ast.Appl(List(

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

   179             Ast.Variable("ccc"),

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

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

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

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

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

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

   186 

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

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

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

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

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

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

   193       Appl(List(

   194         Constant("_list"), Appl(List(

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

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

   197             

   198     /* output from Isabelle_Isac adds types to above structure:

   199        Appl(List(

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

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

   202              Constant("_constrain"), Appl(List(

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

   204                  Constant("_ofsort"), Appl(List(

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

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

   207                        Constant("_constrain"), Appl(List(

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

   209                            Constant("_ofsort"), Appl(List(

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

   211                                Constant("_constrain"), Appl(List(

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

   213                                    Constant("_ofsort"), Appl(List(

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

   215      */

   216 

   217     ast =

   218       Appl(List(

   219         Constant("_list"), Appl(List(

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

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

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

   223     

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

   225   }

   226 

   227   def test_tuple_normal() = {

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

   229     

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

   231     var term_from_Isabelle_Isac =

   232       App(

   233         App(

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

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

   236         App(

   237           App(

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

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

   240           App(

   241             App(

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

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

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

   245           ))

   246         ))

   247     var simple_ast = Syntax_Phases.simple_ast_of(term_from_Isabelle_Isac)

   248     assertEquals(simple_ast,

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

   250         Constant("Product_Type.Pair"),

   251         Variable("aaa"),

   252         Appl(List(

   253           Constant("Product_Type.Pair"),

   254           Variable("bbb"),

   255           Appl(List(

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

   257             Variable("ccc"),

   258             Variable("ddd")))

   259           ))

   260         ))

   261       )

   262     var pre_ast : Ast.Ast = simple_ast

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

   264 //      Appl(List(

   265 //        Constant("Product_Type.Pair"),

   266 //        Variable("aaa"),

   267 //        Appl(List(

   268 //          Constant("Product_Type.Pair"),

   269 //          Variable("bbb"),

   270 //          Appl(List(

   271 //            Constant("Product_Type.Pair"),

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

   273 //               Variable("ccc"))),

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

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

   276       Appl(List(

   277         Constant("_tuple"),  

   278         Variable("aaa"),

   279         Appl(List(

   280           Constant("_tuple_args"),  

   281           Variable("bbb"),

   282           Appl(List(

   283             Constant("_tuple_args"),

   284             Variable("ccc"),

   285             Appl(List(

   286               Constant("_tuple_arg"),  

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

   288     val ast = normalize(XSyntax.print_rules, pre_ast)

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

   290                   

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

   292   }

   293   

   294     

   295   val ast =

   296 /*List()*/    Appl(List(

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

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

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

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

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

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

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

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

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

   306             

   307   def test_update() {

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

   309 

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

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

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

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

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

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

   316     

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

   318         Appl(List(

   319          Constant("Groups.plus_class.plus"),

   320          Variable("X"),

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

   322     

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

   324   }

   325 

   326   def test_math_string_of_arbitrary() {

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

   328     

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

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

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

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

   333     

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

   335   }

   336 }
wneuper/isac