wneuper/isac: isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala@b4e3883d7b66

     1 /**

     2  * @author Walther Neuper

     3  * Created on May 18, 2017

     4  * (c) due to copyright terms

     5  */

     7 package isac.gui.mawen

     9 import isac.bridge.Isabelle_Isac

    10 import isac.bridge.xml.DataTypes

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

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

    15 import junit.framework.TestCase

    16 import org.junit.Assert._

    18 /**

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

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

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

    22  * References use labels in mmahringer-master.tex.

    23  */

    24 class TestUseCases extends TestCase {

    26   var sys_ : JSystem = null

    27   override def setUp() {

    28     sys_ = Isabelle_Isac.connect();

    29   }

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

    32   def testUC_userguide() {

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

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

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

    37     var form = DataTypes.xml_to_Formula_NEW(tree)

    38     var ast = form.getTerm

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

    40     assertEquals(ast,

    41       Appl(List(

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

    43         Appl(List(

    44           Constant("Diff.d_d"),

    45           Variable("x"),

    46           Variable("x"))),

    47         Appl(List(

    48           Constant("Diff.d_d"),

    49           Variable("x"),

    50           Appl(List(

    51             Constant("Transcendental.sin"),

    52             Appl(List(

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

    54               Variable("x"),

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

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

    57     assertEquals(math_string_of(ast), term_str)

    58     val ast_05 =  // copied to TestData.scala

    59       Appl(List(

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

    61         Appl(List(

    62           Constant("Diff.d_d"),

    63           Variable("x"),

    64           Variable("x"))),

    65         Appl(List(

    66           Constant("Diff.d_d"),

    67           Variable("x"),

    68           Appl(List(                 //added to above

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

    70             Appl(List(

    71               Constant("Transcendental.sin"),

    72               Appl(List(             //added to above

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

    74                 Appl(List(

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

    76                   Variable("x"),

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

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

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

    81     form = DataTypes.xml_to_Formula_NEW(tree)

    82     ast = form.getTerm

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

    84     assertEquals(ast,

    85       Appl(List(

    86         Constant("HOL.eq"),

    87         Appl(List(

    88           Constant("Diff.d_d"),

    89           Variable("bdv"),

    90           Appl(List(

    91             Constant("Transcendental.sin"),

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

    93         Appl(List(

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

    95           Appl(List(

    96             Constant("Transcendental.cos"),

    97             Variable("u"))),

    98           Appl(List(

    99             Constant("Diff.d_d"),

   100             Variable("bdv"),

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

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

   103     assertEquals(math_string_of(ast), term_str)

   104     val ast_06 = // copied to TestData.scala

   105       Appl(List(

   106         Constant("HOL.eq"),

   107         Appl(List(

   108           Constant("Diff.d_d"),

   109           Variable("bdv"),

   110           Appl(List(                 //added to above

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

   112             Appl(List(

   113               Constant("Transcendental.sin"),

   114               Appl(List(             //added to above

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

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

   117         Appl(List(

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

   119           Appl(List(                 //added to above

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

   121             Appl(List(

   122               Constant("Transcendental.cos"),

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

   124           Appl(List(

   125             Constant("Diff.d_d"),

   126             Variable("bdv"),

   127             Appl(List(               //added to above

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

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

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

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

   133     form = DataTypes.xml_to_Formula_NEW(tree)

   134     ast = form.getTerm

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

   136     assertEquals(ast,

   137       Appl(List(

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

   139         Appl(List(

   140           Constant("Diff.d_d"),

   141           Variable("x"),

   142           Variable("x"))),

   143         Appl(List(

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

   145           Appl(List(

   146             Constant("Transcendental.cos"),

   147             Appl(List(

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

   149               Variable("x"),

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

   151           Appl(List(

   152             Constant("Diff.d_d"),

   153             Variable("x"),

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

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

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

   157     val ast_07 = // copied to TestData.scala

   158       Appl(List(

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

   160         Appl(List(

   161           Constant("Diff.d_d"),

   162           Variable("x"),

   163           Variable("x"))),

   164         Appl(List(

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

   166           Appl(List(                 //added to above

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

   168             Appl(List(

   169               Constant("Transcendental.cos"),

   170               Appl(List(

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

   172                 Variable("x"),

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

   174           Appl(List(

   175             Constant("Diff.d_d"),

   176             Variable("x"),

   177             Appl(List(               //added to above

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

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

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

   182   }

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

   185   def testUC_multfrac() {

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

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

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

   190     var form = DataTypes.xml_to_Formula_NEW(tree)

   191     var ast = form.getTerm

   192     assertEquals(ast,

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

   194     assertEquals(term_str, math_string_of(ast))

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

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

   198     form = DataTypes.xml_to_Formula_NEW(tree)

   199     ast = form.getTerm

   200     assertEquals(ast,

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

   202     assertEquals(term_str, math_string_of(ast))

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

   205   }

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

   208   /*

   209 	TODO in cooperation with mmahringer

   210    */

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

   213   def testUC_engmath() {

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

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

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

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

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

   220     var form = DataTypes.xml_to_Formula_NEW(tree)

   221     var ast = form.getTerm

   222     assertEquals(ast,

   223       Appl(List(

   224         Constant("HOL.eq"),

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

   226         Appl(List(

   227           Constant("Integrate.Integral"),

   228           Appl(List(

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

   230             Variable("c_3"),

   231             Appl(List(

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

   233               Appl(List(

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

   235                 Variable("1"),

   236                 Appl(List(

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

   238                   Variable("-1"),

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

   240                   Appl(List(

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

   242                     Appl(List(

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

   244                       Appl(List(

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

   246                       Appl(List(

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

   248                           Appl(List(

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

   250                           Appl(List(

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

   252                     Appl(List(

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

   254                       Appl(List(

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

   256                         Appl(List(

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

   258                         Variable("6"))),

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

   260           Variable("x")))))

   261     )

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

   263       math_string_of(ast))

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

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

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

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

   270     form = DataTypes.xml_to_Formula_NEW(tree)

   271     ast = form.getTerm

   272     //println(math_string_of(ast))

   273     assertEquals(term_str, math_string_of(ast))

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

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

   277     form = DataTypes.xml_to_Formula_NEW(tree)

   278     ast = form.getTerm

   279     //println(raw_string_of(ast))

   280     assertEquals(ast,

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

   282     )

   283     assertEquals(term_str, math_string_of(ast))

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

   286   }

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

   289   def testUC_ifthenelse() {

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

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

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

   294       //  Coercion inference failed:

   295       //  no supremum

   296       //

   297       //  Cannot fulfil subtype constraints:

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

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

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

   302     var term_str =

   303       "Program Simplify t_t =" +

   304       "  Repeat (" +

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

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

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

   308       "    Try (Rewrite_Set verschoenere False)) t_t"

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

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

   311     var form = DataTypes.xml_to_Formula_NEW(tree)

   312     var ast = form.getTerm

   313     assertEquals(ast,

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

   315     )

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

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

   319   }

   321   override def tearDown() {

   322     sys_.dispose()

   323     super.tearDown()

   324   }

   325 }

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 26 Mar 2021 10:45:05 +0100
changeset 5239	b4e3883d7b66
parent 5229	6bf0e95981e3
permissions	-rw-r--r--