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/TestUseCases.scala
author Walther Neuper <wneuper@ist.tugraz.at>
Thu, 18 May 2017 10:16:13 +0200
changeset 5107 7d1e524480b8
child 5114 ed20ab7dbb48
permissions -rw-r--r--
collect test data from User Requirements 
     1 /**

     2  * @author Walther Neuper

     3  * Created on May 18, 2017

     4  * (c) due to copyright terms

     5  */

     6 

     7 package isac.gui.mawen

     8 

     9 import isac.bridge.Isabelle_Isac

    10 import isac.bridge.xml.DataTypes

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

    12 

    13 import junit.framework.TestCase

    14 import org.junit.Assert._

    15 

    16 /**

    17  * Use Cases from Marco Mahringer's master thesis.

    18  * References labels from mmahringer-master.tex.

    19  */

    20 class TestUseCases extends TestCase {

    21   

    22   val sys_ = Isabelle_Isac.connect();

    23   

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

    25   def testUC_userguide() {

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

    27     

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

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

    30     var form = DataTypes.xml_to_Formula_NEW(tree)

    31     var ast = form.getTerm

    32     //println(Ast.raw_string_of(ast))

    33     assertEquals(ast, 

    34       Appl(List(

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

    36         Appl(List(

    37           Constant("Diff.d_d"),

    38           Variable("x"),

    39           Variable("x"))),

    40         Appl(List(

    41           Constant("Diff.d_d"),

    42           Variable("x"),

    43           Appl(List(

    44             Constant("Transcendental.sin"),

    45             Appl(List(

    46               Constant("Power.power_class.power"),

    47               Variable("x"),

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

    49     //println(Ast.math_string_of(ast))

    50     assertEquals(math_string_of(ast), term_str)

    51 

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

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

    54     form = DataTypes.xml_to_Formula_NEW(tree)

    55     ast = form.getTerm

    56     //println(Ast.raw_string_of(ast))

    57     assertEquals(ast, 

    58       Appl(List(

    59         Constant("HOL.eq"),

    60         Appl(List(

    61           Constant("Diff.d_d"),

    62           Variable("bdv"),

    63           Appl(List(

    64             Constant("Transcendental.sin"),

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

    66         Appl(List(

    67           Constant("Groups.times_class.times"),

    68           Appl(List(

    69             Constant("Transcendental.cos"),

    70             Variable("u"))),

    71           Appl(List(

    72             Constant("Diff.d_d"),

    73             Variable("bdv"),

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

    75     //println(Ast.math_string_of(ast))

    76     assertEquals(math_string_of(ast), term_str)

    77     

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

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

    80     form = DataTypes.xml_to_Formula_NEW(tree)

    81     ast = form.getTerm

    82     //println(Ast.raw_string_of(ast))

    83     assertEquals(ast, 

    84       Appl(List(

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

    86         Appl(List(

    87           Constant("Diff.d_d"),

    88           Variable("x"),

    89           Variable("x"))),

    90         Appl(List(

    91           Constant("Groups.times_class.times"),

    92           Appl(List(

    93             Constant("Transcendental.cos"),

    94             Appl(List(

    95               Constant("Power.power_class.power"),

    96               Variable("x"),

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

    98           Appl(List(

    99             Constant("Diff.d_d"),

   100             Variable("x"),

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

   102     //println(Ast.math_string_of(ast))

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

   104      

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

   106   }

   107   

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

   109   def testUC_multfrac() {

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

   111     

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

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

   114     var form = DataTypes.xml_to_Formula_NEW(tree)

   115     var ast = form.getTerm

   116     assertEquals(ast,

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

   118     assertEquals(term_str, math_string_of(ast))

   119 

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

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

   122     form = DataTypes.xml_to_Formula_NEW(tree)

   123     ast = form.getTerm

   124     assertEquals(ast,

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

   126     assertEquals(term_str, math_string_of(ast))

   127     

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

   129   }

   130 

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

   132   /*

   133 	TODO in cooperation with mmahringer

   134    */

   135 

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

   137   def testUC_engmath() {

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

   139     

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

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

   142     var form = DataTypes.xml_to_Formula_NEW(tree)

   143     var ast = form.getTerm

   144     assertEquals(ast,    

   145       Appl(List(

   146         Constant("HOL.eq"),

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

   148         Appl(List(

   149           Constant("Integrate.Integral"),

   150           Appl(List(

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

   152             Variable("c_3"),

   153             Appl(List(

   154               Constant("Groups.times_class.times"),

   155               Appl(List(

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

   157                 Variable("1"),

   158                 Appl(List(

   159                   Constant("Groups.times_class.times"),

   160                   Variable("-1"),

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

   162                   Appl(List(

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

   164                     Appl(List(

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

   166                       Appl(List(

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

   168                       Appl(List(

   169                         Constant("Groups.times_class.times"),

   170                           Appl(List(

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

   172                           Appl(List(

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

   174                     Appl(List(

   175                       Constant("Groups.times_class.times"),

   176                       Appl(List(

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

   178                         Appl(List(

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

   180                         Variable("6"))),

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

   182           Variable("x")))))

   183     )

   184 //    assertEquals(term_str, math_string_of(ast)) ------ TODO math_string_of UNCOVERED CASE 

   185 

   186     

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

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

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

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

   191     form = DataTypes.xml_to_Formula_NEW(tree)

   192     ast = form.getTerm

   193 //TODO fun + pair + list

   194 //    assertEquals(ast,    

   195 //      Appl(List(Variable("Probl"), Appl(List(Constant("Product_Type.Pair"), Constant("Biegelinie.Biegelinie"), Appl(List(Constant("List.list.Cons"), Variable("setzeRandbedingungen"), Appl(List(Constant("List.list.Cons"), Variable("Biegelinien"), Constant("List.list.Nil")))))))))

   196 //    )    

   197 //    assertEquals(term_str, math_string_of(ast)) ------ math_string_of UNCOVERED CASE 

   198     

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

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

   201     form = DataTypes.xml_to_Formula_NEW(tree)

   202     ast = form.getTerm

   203 //TODO fun + list

   204 //    assertEquals(ast,    

   205 //      Appl(List(Constant("List.list.Cons"), Appl(List(Constant("HOL.eq"), Appl(List(Constant("Groups.times_class.times"), Variable("L"), Variable("q_0"))), Variable("c"))), Appl(List(Constant("List.list.Cons"), 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("List.list.Cons"), Appl(List(Constant("HOL.eq"), Variable("0"), Variable("c_4"))), Appl(List(Constant("List.list.Cons"), Appl(List(Constant("HOL.eq"), Variable("0"), Variable("c_3"))), Constant("List.list.Nil")))))))))

   206 //    )    

   207 //    println(math_string_of(ast))    //TODO scala.MatchError:Appl...

   208 

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

   210   }

   211 

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

   213   def testUC_ifthenelse() {

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

   215     

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

   217       //NOTE:  Isabelle error messages indicates problems with termination

   218       //  Coercion inference failed:

   219       //  no supremum

   220       //  

   221       //  Cannot fulfil subtype constraints:

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

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

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

   225 

   226     var term_str = 

   227       "Program Simplify t_t =" +

   228       "  Repeat (" +

   229       "    Try (Rewrite_Set klammern_aufloesen False) @@" +

   230       "    Try (Rewrite_Set ordne_alphabetisch False) @@" +

   231       "    Try (Rewrite_Set fasse_zusammen False) @@" +

   232       "    Try (Rewrite_Set verschoenere False)) t_t"

   233     //NOTE: pretty blocks have not yet been considered

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

   235     var form = DataTypes.xml_to_Formula_NEW(tree)

   236     var ast = form.getTerm

   237     assertEquals(ast,

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

   239     )

   240 //    assertEquals(term_str, math_string_of(ast)) ------ TODO math_string_of UNCOVERED CASE 

   241    

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

   243   }

   244 

   245 }
wneuper/isac