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/bridge/xml/TestsDATA.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  * Copyright (c) due to license terms

     4  * Created on Aug 28, 2015

     5  * Institute for Softwaretechnology, Graz University of Technology, Austria.

     6  */

     7 package isac.bridge.xml

     8 

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

    10 import edu.tum.cs.isabelle.pure._ // DEFINES type Term

    11 

    12 /*

    13  * Compile test data for TestDataTypes.java.

    14  * 

    15  * This setup has been chosen after <Run As> <Scala JUnit Test> could not

    16  * made working with standard examples neither from within Eclipse

    17  * * http://scala-ide.org/docs/2.0.x/testingframeworks.html

    18  * * http://scala-ide.org/docs/current-user-doc/features/test-finder/index.html

    19  * nor with ScalaTest

    20  * * http://www.scalatest.org/download

    21  * * http://www.scalatest.org/user_guide/using_scalatest_with_eclipse

    22  */

    23 object TestsDATA {

    24 

    25   //---------------------------------- for TestXMLout.java#test_match

    26   def create_AAA (): XML.Tree =

    27     XML.Elem(("AAA", Nil), Nil)

    28   def create_BBB (): XML.Tree =

    29     XML.Elem(("BBB", Nil), Nil)

    30   def create_CCCddd (): XML.Tree =

    31     XML.Elem(("CCC", Nil), List(

    32       XML.Elem(("ddd", Nil), Nil)))

    33   def create_DDDeeeFFF (): XML.Tree =

    34     XML.Elem(("DDD", Nil), List(

    35       XML.Elem(("eee", Nil), List(XML.Text("FFF")))))

    36   def create_EEEfffGGGhhhIII (): XML.Tree =

    37     XML.Elem(("EEE", Nil), List(

    38       XML.Elem(("fff", Nil), List(XML.Text("GGG"))),

    39       XML.Elem(("hhh", Nil), List(XML.Text("III")))))

    40 

    41   def match_ABC(t: XML.Tree): java.lang.String = t match {

    42     case

    43       XML.Elem(("AAA", Nil), Nil) => "AAA"

    44     case

    45       XML.Elem(("BBB", Nil), Nil) => "BBB"

    46     case

    47       XML.Elem(("CCC", Nil), List(

    48         XML.Elem(("ddd", Nil), Nil))) => "CCCddd"

    49     case

    50       XML.Elem(("DDD", Nil), List(

    51         XML.Elem(("eee", Nil), List(XML.Text("FFF")))))

    52       => "DDDeeeFFF"

    53     case

    54       XML.Elem(("EEE", Nil), List(

    55         XML.Elem(("fff", Nil), List(XML.Text("GGG"))),

    56         XML.Elem(("hhh", Nil), List(XML.Text("III")))))

    57       => "EEEfffGGGhhhIII"

    58     case

    59       XML.Elem(("SYSERROR", Nil), List(

    60         XML.Elem(("CALCID", Nil), List(XML.Text(_))),

    61         XML.Elem(("ERROR", Nil), List(XML.Text(_)))))

    62       => "SYSERROR"

    63     case _ => "no match"

    64   }

    65 

    66   //---------------------------------- for TestXMLout.java#test_is_message

    67   def create_SYSERROR (): XML.Tree =

    68       XML.Elem(("SYSERROR", Nil), List(

    69         XML.Elem(("CALCID", Nil), List(XML.Text("1"))),

    70         XML.Elem(("ERROR", Nil), List(XML.Text("no Rewrite_Set...")))))

    71   /*

    72    * intermediateSteps xml_out = <SYSERROR><CALCID>1</CALCID><ERROR>no Rewrite_Set...</ERROR></SYSERROR>

    73    */

    74 

    75         

    76   //---------------------------------- for ../TestPIDE.java#testTermTransfer

    77   //----- see Isabelle_Isac/test/../mathml.sml--- create testdata for TestPIDE.java#testTermTransfer ---

    78   //      https://intra.ist.tugraz.at/hg/isa/rev/5ce72a592f7f

    79   // val t = @{term "aaa + bbb::real"}

    80   // ... gives in SML:

    81   //  ( ( Const ("Groups.plus_class.plus", "real ⇒ real ⇒ real") $ Free ("aaa", "real") ) $ Free ("bbb", "real") )

    82   // ... gives in SML with left-associativity:

    83   // val

    84   //  (*App*) (

    85   //    (*App*) ( 

    86   //      Const ("Groups.plus_class.plus", _) $ 

    87   //      Free ("aaa", _) ) $ 

    88   //    Free ("bbb", _)   ) = t

    89   // ... gives in SML with explicit typ:

    90   //  (*App*) (

    91   //    (*App*) (

    92   //        Const ("Groups.plus_class.plus", Type ("fun", [

    93   //                                           Type ("Real.real", []), 

    94   //                                           Type ("fun", [

    95   //                                             Type ("Real.real", []), 

    96   //                                             Type ("Real.real", [])])])) $ 

    97   //          Free ("aaa", Type ("Real.real", [])) ) $ 

    98   //          Free ("bbb", Type ("Real.real", [])) )

    99   def test_term (): Term = 

   100         App(

   101           App(

   102             Const ("Groups.plus_class.plus", Type("fun", List(

   103                                                Type("Real.real", List()), 

   104                                                Type("fun", List(

   105                                                  Type("Real.real", List()), 

   106                                                  Type("Real.real", List())))))),

   107               Free ("aaa", Type ("Real.real", List()))),

   108               Free ("bbb", Type ("Real.real", List())))

   109 

   110   /*

   111    * "solve (x + 1 = (2::real), (x::real))" parsed via <code>ScalaTermFromString</code> to

   112    * App(Const("Equation.solve",Type("fun",List(Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List()))), Type(List.list,List(Type("HOL.bool",List())))))),App(App(Const("Product_Type.Pair",Type("fun",List(Type("HOL.bool",List()), Type("fun",List(Type("Real.real",List()), Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List())))))))),App(App(Const("HOL.eq",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("HOL.bool",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),Free("1",Type("Real.real",List())))),Free("2",Type(Real.real,List())))),Free("x",Type("Real.real",List()))))

   113    */

   114   def term_mini_subpbl_1 (): Term = {

   115     App(Const("Equation.solve",Type("fun",List(Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List()))), Type("List.list",List(Type("HOL.bool",List())))))),App(App(Const("Product_Type.Pair",Type("fun",List(Type("HOL.bool",List()), Type("fun",List(Type("Real.real",List()), Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List())))))))),App(App(Const("HOL.eq",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("HOL.bool",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),Free("1",Type("Real.real",List())))),Free("2",Type("Real.real",List())))),Free("x",Type("Real.real",List()))))

   116   }

   117 }
wneuper/isac