wneuper/isac: isac-java/src/java-tests/isac/bridge/xml/TestDataTypesDATA.scala@b4e3883d7b66

     1 /*

     2  * @author Walther Neuper

     3  * Copyright (c) due to license terms

     4  * Created on Jul 14, 2015

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

     6  */

     7 package isac.bridge.xml

     9 import isac.util.formulae.ModelItem

    10 import isac.gui.mawen.scalaterm.Util

    12 import edu.tum.cs.isabelle._      // for Codec

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

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

    16 import java.util.Vector

    17 import scala.collection.JavaConverters._

    18 import scala.collection.JavaConversions._

    20 /*

    21  * Compile test data for TestDataTypes.java.

    22  *

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

    24  * made working with standard examples neither from within Eclipse

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

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

    27  * nor with ScalaTest

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

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

    30  */

    31 object TestDataTypesDATA {

    33   //---------------------------------- for TestDataTypes.java#testCalcHead

    34   def create_REF_FORMULA_out (): XML.Tree = {

    35     val REF_FORMULA_out =

    36       XML.Elem(("REFFORMULA", Nil), List(

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

    38         XML.Elem(("CALCHEAD", List(("status", "incorrect"))), List(

    39           XML.Elem(("POSITION", Nil), List(

    40             XML.Elem(("INTLIST", Nil), Nil),

    41             XML.Elem(("POS", Nil), List(XML.Text("Pbl"))))),

    42           XML.Elem(("HEAD", Nil), List(

    43             XML.Elem(("FORMULA", Nil), List(

    44               XML.Elem(("ISA", Nil), List(XML.Text("solve (x + 1 = 2, x)"))),

    45               XML.Elem(("TERM", Nil), List(Codec[Term].encode(TestsDATA.term_mini_subpbl_1())) ))) )),

    46           XML.Elem(("MODEL", Nil), List(

    47             XML.Elem(("GIVEN", Nil), Nil),

    48             XML.Elem(("WHERE", Nil), List(

    49               XML.Elem(("ITEM", List(("status", "false"))), List(

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

    51                   XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),

    52             XML.Elem(("FIND", Nil), Nil),

    53             XML.Elem(("RELATE", Nil),  Nil))),

    54           XML.Elem(("BELONGSTO", Nil), List(XML.Text("Pbl"))),

    55           XML.Elem(("SPECIFICATION", Nil), List(

    56             XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),

    57             XML.Elem(("PROBLEMID", Nil), List(

    58               XML.Elem(("STRINGLIST", Nil), List(

    59                   XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),

    60             XML.Elem(("METHODID", Nil), List(

    61               XML.Elem(("STRINGLIST", Nil), List(

    62                   XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))))));

    63     REF_FORMULA_out

    64   }

    65   def create_xml_model (REF_FORMULA_out: XML.Tree): XML.Tree = REF_FORMULA_out match {

    66     case

    67       XML.Elem(("REFFORMULA", Nil), List(

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

    69         XML.Elem(("CALCHEAD", List(("status", "incorrect"))), List(

    70           XML.Elem(("POSITION", Nil), List(

    71             XML.Elem(("INTLIST", Nil), Nil),

    72             XML.Elem(("POS", Nil), List(XML.Text("Pbl"))))),

    73           XML.Elem(("HEAD", Nil), List(

    74             XML.Elem(("FORMULA", Nil), List(

    75               XML.Elem(("ISA", Nil), List(XML.Text("solve (x + 1 = 2, x)"))),

    76               XML.Elem(("TERM", Nil), _ ))) )),

    77           xml_model,

    78           XML.Elem(("BELONGSTO", Nil), List(XML.Text("Pbl"))),

    79           XML.Elem(("SPECIFICATION", Nil), List(

    80             XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),

    81             XML.Elem(("PROBLEMID", Nil), List(

    82               XML.Elem(("STRINGLIST", Nil), List(

    83                   XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),

    84             XML.Elem(("METHODID", Nil), List(

    85               XML.Elem(("STRINGLIST", Nil), List(

    86                   XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))))))

    87        => xml_model

    88     case _ => throw new IllegalArgumentException("create_xml_model exn")

    89   }

    90   def create_xml_given (xml_model: XML.Tree): XML.Tree = xml_model match {

    91     case

    92       XML.Elem(("MODEL", Nil), List(

    93         xml_given,

    94         XML.Elem(("WHERE", Nil), List(

    95           XML.Elem(("ITEM", List(("status", "false"))), List(

    96             XML.Elem(("MATHML", Nil), List(

    97               XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),

    98         XML.Elem(("FIND", Nil), Nil),

    99         XML.Elem(("RELATE", Nil),  Nil)))

   100       => xml_given

   101     case _ => throw new IllegalArgumentException("create_xml_given exn")

   102   }

   103   def create_xml_where (xml_model: XML.Tree): XML.Tree = xml_model match {

   104     case

   105       XML.Elem(("MODEL", Nil), List(

   106         XML.Elem(("GIVEN", Nil), Nil),

   107         xml_where,

   108         XML.Elem(("FIND", Nil), Nil),

   109         XML.Elem(("RELATE", Nil),  Nil)))

   110       => xml_where

   111     case _ => throw new IllegalArgumentException("create_xml_where exn")

   112   }

   113   def create_xml_find (xml_model: XML.Tree): XML.Tree = xml_model match {

   114     case

   115       XML.Elem(("MODEL", Nil), List(

   116         XML.Elem(("GIVEN", Nil), Nil),

   117         XML.Elem(("WHERE", Nil), List(

   118           XML.Elem(("ITEM", List(("status", "false"))), List(

   119             XML.Elem(("MATHML", Nil), List(

   120               XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),

   121         xml_find,

   122         XML.Elem(("RELATE", Nil),  Nil)))

   123       => xml_find

   124     case _ => throw new IllegalArgumentException("create_xml_find exn")

   125   }

   126   def create_xml_relate (xml_model: XML.Tree): XML.Tree = xml_model match {

   127     case

   128       XML.Elem(("MODEL", Nil), List(

   129         XML.Elem(("GIVEN", Nil), Nil),

   130         XML.Elem(("WHERE", Nil), List(

   131           XML.Elem(("ITEM", List(("status", "false"))), List(

   132             XML.Elem(("MATHML", Nil), List(

   133               XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),

   134         XML.Elem(("FIND", Nil), Nil),

   135         xml_relate))

   136       => xml_relate

   137     case _ => throw new IllegalArgumentException("create_xml_relate exn")

   138   }

   139   def create_xml_item (): XML.Tree = {

   140     XML.Elem(("ITEM", List(("status", "false"))), List(

   141       XML.Elem(("MATHML", Nil), List(

   142         XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v")))))))

   143   }

   144   def jVector2sList(ivect: Vector[ModelItem]): List[ModelItem] = {

   145     ivect.asScala.toList

   146   }

   147   def create_xml_calchead (REF_FORMULA_out: XML.Tree): XML.Tree = REF_FORMULA_out match {

   148     case

   149       XML.Elem(("REFFORMULA", Nil), List(

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

   151         xml_calchead)) => xml_calchead

   152     case _ => throw new IllegalArgumentException("create_xml_calchead exn")

   153   }

   154   def create_xml_spec (REF_FORMULA_out: XML.Tree): XML.Tree = REF_FORMULA_out match {

   155     case

   156       XML.Elem(("REFFORMULA", Nil), List(

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

   158         XML.Elem(("CALCHEAD", List(("status", "incorrect"))), List(

   159           XML.Elem(("POSITION", Nil), List(

   160             XML.Elem(("INTLIST", Nil), Nil),

   161             XML.Elem(("POS", Nil), List(XML.Text("Pbl"))))),

   162           XML.Elem(("HEAD", Nil), List(

   163             XML.Elem(("FORMULA", Nil), List(

   164               XML.Elem(("ISA", Nil), List(XML.Text("solve (x + 1 = 2, x)"))),

   165               XML.Elem(("TERM", Nil), _ ))) )),

   166           XML.Elem(("MODEL", Nil), List(

   167             XML.Elem(("GIVEN", Nil), Nil),

   168             XML.Elem(("WHERE", Nil), List(

   169               XML.Elem(("ITEM", List(("status", "false"))), List(

   170                 XML.Elem(("MATHML", Nil), List(

   171                   XML.Elem(("ISA", Nil), List(XML.Text("precond_rootpbl v_v"))))))))),

   172             XML.Elem(("FIND", Nil), Nil),

   173             XML.Elem(("RELATE", Nil),  Nil))),

   174           XML.Elem(("BELONGSTO", Nil), List(XML.Text("Pbl"))),

   175           xml_spec ))))

   176       => xml_spec

   177     case _ => throw new IllegalArgumentException("create_xml_spec exn")

   178   }

   179   def create_xml_thy (xml_spec: XML.Tree): XML.Tree = xml_spec match {

   180     case

   181       XML.Elem(("SPECIFICATION", Nil), List(

   182         XML.Elem(("THEORYID", Nil), List(xml_thy)),

   183         XML.Elem(("PROBLEMID", Nil), List(

   184           XML.Elem(("STRINGLIST", Nil), List(

   185               XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),

   186         XML.Elem(("METHODID", Nil), List(

   187           XML.Elem(("STRINGLIST", Nil), List(

   188               XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))

   189       => xml_thy

   190     case _ => throw new IllegalArgumentException("create_xml_thy exn")

   191   }

   192   def create_xml_pbl (xml_spec: XML.Tree): XML.Tree = xml_spec match {

   193     case

   194       XML.Elem(("SPECIFICATION", Nil), List(

   195         XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),

   196         XML.Elem(("PROBLEMID", Nil), List(xml_pbl)),

   197         XML.Elem(("METHODID", Nil), List(

   198           XML.Elem(("STRINGLIST", Nil), List(

   199               XML.Elem(("STRING", Nil), List(XML.Text("e_metID")))))))))

   200       => xml_pbl

   201     case _ => throw new IllegalArgumentException("create_xml_pbl exn")

   202   }

   203   def create_xml_met (xml_spec: XML.Tree): XML.Tree = xml_spec match {

   204     case

   205       XML.Elem(("SPECIFICATION", Nil), List(

   206         XML.Elem(("THEORYID", Nil), List(XML.Text("e_domID"))),

   207         XML.Elem(("PROBLEMID", Nil), List(

   208           XML.Elem(("STRINGLIST", Nil), List(

   209               XML.Elem(("STRING", Nil), List(XML.Text("e_pblID"))))))),

   210         XML.Elem(("METHODID", Nil), List(xml_met))))

   211       => xml_met

   212     case _ => throw new IllegalArgumentException("create_xml_met exn")

   213   }

   214   //TODO: vvvvvvvvvvvvvv should exist with another identifier

   215   def create_Formula_NEW (term: Term): XML.Tree = {

   216     XML.Elem(("FORMULA", Nil), List(

   217       XML.Elem(("ISA", Nil), List(XML.Text(Util.string_of(term)))),

   218       XML.Elem(("TERM", Nil), List(Codec[Term].encode(term)))))

   219   }

   221 }

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