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/TestDATA.scala
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--
reset mathematics-engine to Isabelle2015

note: for this version libisabelle was available,
which connects front-end (Java) and back-end (Isabelle/ML) 
     1 /**

     2  * @author Walther Neuper

     3  * Created on Sep 25, 2015

     4  * (c) copyright due to license terms

     5  */

     6 

     7 package isac.gui.mawen

     8 

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

    10 import edu.tum.cs.isabelle.api.XML

    11 

    12   /*

    13    * terms for tests

    14    */

    15 object TestDATA {

    16   

    17   //---------------------------- for <code>TestXml</code>

    18   // the priorities of the operators are from ~~/src/HOL/Groups.thy, Fields.thy, Power.thy, ...

    19   

    20   // "1 + (2 * x * (y + 3)) / (4 * z * (y + 3)) + 5" ... Isabelle's + is left-associative:

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

    22   def term_1(): XML.Tree = {

    23     XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

    24       XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

    25         XML.Elem(("NUM", Nil), List(XML.Text ("1"))),              

    26         XML.Elem(("OP", List(("id", "/"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

    27           XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

    28             XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

    29               XML.Elem(("NUM", Nil), List(XML.Text ("2"))),              

    30               XML.Elem(("VAR", Nil), List(XML.Text ("x")))

    31               ) ),              

    32             XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

    33               XML.Elem(("VAR", Nil), List(XML.Text ("y"))),              

    34               XML.Elem(("NUM", Nil), List(XML.Text ("3")))

    35               ) )

    36             ) ),              

    37           XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

    38             XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

    39               XML.Elem(("NUM", Nil), List(XML.Text ("4"))),              

    40               XML.Elem(("VAR", Nil), List(XML.Text ("y")))

    41               ) ),              

    42             XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

    43               XML.Elem(("VAR", Nil), List(XML.Text ("y"))),              

    44               XML.Elem(("NUM", Nil), List(XML.Text ("3")))

    45               ) )

    46             ) )

    47           ) )

    48         ) ),              

    49       XML.Elem(("NUM", Nil), List(XML.Text ("5")))

    50       ) )

    51   }

    52   // the above term cancelled

    53   // "1 + (2 * x) / (4 * z) + 5" ... Isabelle's + is left-associative, thus () omitted:

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

    55   def term_2(): XML.Tree = {

    56     XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

    57       XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

    58         XML.Elem(("NUM", Nil), List(XML.Text ("1"))),              

    59         XML.Elem(("OP", List(("id", "/"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

    60           XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

    61             XML.Elem(("NUM", Nil), List(XML.Text ("2"))),              

    62             XML.Elem(("VAR", Nil), List(XML.Text ("x")))

    63             ) ),              

    64           XML.Elem(("OP", List(("id", "*"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

    65             XML.Elem(("NUM", Nil), List(XML.Text ("4"))),              

    66             XML.Elem(("VAR", Nil), List(XML.Text ("y")))

    67             ) )

    68           ) )

    69         ) ),              

    70       XML.Elem(("NUM", Nil), List(XML.Text ("5")))

    71       ) )

    72   }

    73   

    74   //---------------------------- for <code>TestWorksheetForMawen</code>

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

    76   def term_Nil_Frm(): XML.Tree = {

    77     XML.Elem(("CASCMD", List(("id", "Diff"), ("args", "2"))), List(

    78       XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

    79         XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

    80         XML.Elem(("OP", List(("id", "sin"), ("args", "1"), ("prior", "99"), ("fix", "pre"))), List(

    81           XML.Elem(("OP", List(("id", "^"), ("args", "2"), ("prior", "80"), ("fix", "in"))), List(

    82             XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

    83             XML.Elem(("NUM", Nil), List(XML.Text ("2"))))))))),

    84       XML.Elem(("VAR", Nil), List(XML.Text ("x")))))

    85   }

    86   

    87   // "d_d x (x + sin (x ^ 2))" as it comes from Isabelle (as SMLString)

    88   def term_1_Frm_from_ISA(): XML.Tree = {                   // vvvvvvvvvvv--- enforces (term)

    89     XML.Elem(("OP", List(("id", "d_d"), ("args", "2"), ("prior", "99"), ("fix", "pre"))), List(

    90       XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

    91       XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

    92         XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

    93         XML.Elem(("OP", List(("id", "sin"), ("args", "1"), ("prior", "99"), ("fix", "pre"))), List(

    94           XML.Elem(("OP", List(("id", "^"), ("args", "2"), ("prior", "80"), ("fix", "in"))), List(

    95             XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

    96             XML.Elem(("NUM", Nil), List(XML.Text ("2")))))))))))

    97   }

    98   // "d_d x (x + sin (x ^ 2))" as presented to the gui ??????????????????????????????????????????????????

    99   // version a: involves not-clarified mixfix notation

   100   def term_1_Frm(): XML.Tree = {

   101     // ambiguous..: no division -------v             vvv             vvv--- like "=" in HOL.thy ?????????

   102     XML.Elem(("OP", List(("id", "/"), ("args", "3"), ("prior", "50"), ("fix", "mixfix"))), List(

   103       XML.Elem(("CONST", Nil), List(XML.Text ("d"))),  // CONST or OP or VAR ??????????????????????

   104       XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

   105       XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

   106         XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

   107         XML.Elem(("OP", List(("id", "sin"), ("args", "1"), ("prior", "99"), ("fix", "pre"))), List(

   108             XML.Elem(("OP", List(("id", "^"), ("args", "2"), ("prior", "80"), ("fix", "in"))), List(

   109               XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

   110               XML.Elem(("NUM", Nil), List(XML.Text ("2")))))))))))

   111   } // if ("args", "2") then we have no root for "/ d x" and "(x + sin (x ^ 2))" ????????????????????????

   112   // but we could treat this as fraction --------^^^^^^^ and ^^^^^^^^^^^^^^^^^^^ is dangling without root

   113 

   114   // "d_d x (x + sin (x ^ 2))" as presented to the gui ??????????????????????????????????????????????????

   115   // version b: allows to represent "d_d x" as a normal fraction, but introduces additional TERM

   116   def term_1_Frmb(): XML.Tree = {

   117     XML.Elem(("TERM", List(("args", "2"))), List(

   118       XML.Elem(("OP", List(("id", "/"), ("args", "2"), ("prior", "70"), ("fix", "in"))), List(

   119         XML.Elem(("CONST", Nil), List(XML.Text ("d"))),  // CONST or OP or VAR ????????????????????

   120         XML.Elem(("TERM", List(("args", "2"))), List(   // "d x" in the denominator have no root otherwise !!!!!!!!

   121           XML.Elem(("CONST", Nil), List(XML.Text ("d"))),

   122           XML.Elem(("VAR", Nil), List(XML.Text ("x"))))))),

   123       XML.Elem(("OP", List(("id", "+"), ("args", "2"), ("prior", "65"), ("fix", "in"))), List(

   124         XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

   125         XML.Elem(("OP", List(("id", "sin"), ("args", "1"), ("prior", "99"), ("fix", "pre"))), List(

   126             XML.Elem(("OP", List(("id", "^"), ("args", "2"), ("prior", "80"), ("fix", "in"))), List(

   127               XML.Elem(("VAR", Nil), List(XML.Text ("x"))),

   128               XML.Elem(("NUM", Nil), List(XML.Text ("2")))))))))))

   129   }

   130   // CONCLUSION: either d_d as mixfix (with fraction?), or introduce TERM as root, or ???????????????????

   131   

   132   // TestData from TestUseCases.testUC_userguide()

   133   def ast_05() : Ast =

   134       Appl(List(

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

   136         Appl(List(

   137           Constant("Diff.d_d"),

   138           Variable("x"),

   139           Variable("x"))),

   140         Appl(List(

   141           Constant("Diff.d_d"),

   142           Variable("x"),

   143           Appl(List(                 //added to above

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

   145             Appl(List(

   146               Constant("Transcendental.sin"),

   147               Appl(List(             //added to above

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

   149                 Appl(List(

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

   151                   Variable("x"),

   152                   Variable("2")))))))))))))

   153                   

   154     def ast_06() : Ast =

   155       Appl(List(

   156         Constant("HOL.eq"),

   157         Appl(List(

   158           Constant("Diff.d_d"),

   159           Variable("bdv"),

   160           Appl(List(                 //added to above

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

   162             Appl(List(

   163               Constant("Transcendental.sin"),

   164               Appl(List(             //added to above

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

   166                 Variable("u"))))))))),

   167         Appl(List(

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

   169           Appl(List(                 //added to above

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

   171             Appl(List(

   172               Constant("Transcendental.cos"),

   173               Variable("u"))))),

   174           Appl(List(

   175             Constant("Diff.d_d"),

   176             Variable("bdv"),

   177             Appl(List(               //added to above

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

   179               Variable("u")))))))))

   180               

   181     def ast_07() : Ast =

   182       Appl(List(

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

   184         Appl(List(

   185           Constant("Diff.d_d"),

   186           Variable("x"),

   187           Variable("x"))),

   188         Appl(List(

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

   190           Appl(List(                 //added to above

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

   192             Appl(List(

   193               Constant("Transcendental.cos"),

   194               Appl(List(

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

   196                 Variable("x"),

   197                 Variable("2"))))))),

   198           Appl(List(

   199             Constant("Diff.d_d"),

   200             Variable("x"),

   201             Appl(List(               //added to above

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

   203               Variable("GAP")))))))))

   204 

   205 }
wneuper/isac