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/scalaterm/ScalaTermFromString.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 package isac.gui.mawen.scalaterm;

     2 

     3 import isac.bridge.Isabelle_Isac

     4 import isac.bridge.xml.DataTypes

     5 import edu.tum.cs.isabelle.pure._  // for Term

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

     7 import edu.tum.cs.isabelle.japi._  // for JSystem

     8 

     9 import junit.framework.TestCase

    10 import org.junit.Assert._

    11 

    12 /**

    13  * Create libisabelle's Scala Term from String for tests.

    14  * Compare ScalaAstFromString.

    15  */

    16 class ScalaTermFromString extends TestCase {

    17   

    18   var sys_ : JSystem = null

    19   override def setUp() {

    20     sys_ = Isabelle_Isac.connect();

    21   }

    22   

    23   /**

    24    * test output from ~~/src/Tools/isac/ProgLang/termC.sml: scala_of_term

    25    */

    26   def test_scala_of_term() {

    27     println("/--BEGIN isac.gui.mawen.TestUseCases#test_scala_of_term");

    28 

    29     var term_str = "aaa"

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

    31     var term = DataTypes.xml_to_Term(tree)

    32     assertEquals(term,

    33       // copied output from ~~/src/Tools/isac/ProgLang/termC.sml: scala_of_term

    34       Free("aaa", TFree("'a", List())) 

    35     )

    36      

    37     term_str = "let aaa = bbb in aaa"

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

    39     term = DataTypes.xml_to_Term(tree)

    40     assertEquals(term,

    41       // copied output from ~~/src/Tools/isac/ProgLang/termC.sml: scala_of_term

    42       App(App(Const("HOL.Let", Type("fun", List(TFree("'a", List("HOL.type")),Type("fun", List(Type("fun", List(TFree("'a", List("HOL.type")),TFree("'a", List("HOL.type")))),TFree("'a", List("HOL.type"))))))), Free("bbb", TFree("'a", List("HOL.type")))), Abs("aaa", TFree("'a", List("HOL.type")), Bound(0))) 

    43     )

    44 

    45     // ATTENTION: numerals are different due to specific Isac code: 

    46     // ~~/src/Tools/isac/ProgLang/termC.sml: numbers_to_string

    47     term_str = "0"

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

    49     term = DataTypes.xml_to_Term(tree)

    50     assertEquals(term,

    51       // NOT copied:

    52       Free("0", TFree("'a", List("Groups.zero")))

    53     )

    54     // copied output from ~~/src/Tools/isac/ProgLang/termC.sml: scala_of_term (without parse*)

    55     Const("Groups.zero_class.zero", TFree("'a", List("Groups.zero"))) 

    56     

    57     println("\\--END isac.gui.mawen.TestUseCases#test_scala_of_term");

    58   }

    59 

    60   def test_etc() {

    61     println("/--BEGIN isac.gui.mawen.syntax.ScalaAstFromString#test_etc");

    62     

    63     //dummy

    64     var term_str = "dummy"

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

    66     var term = DataTypes.xml_to_Term(tree)

    67 

    68     term_str = "(aaa, bbb, ccc, ddd)"

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

    70     term = DataTypes.xml_to_Term(tree)

    71     assertEquals(term,

    72       // copied output from SML: writeln(scala_of_term(@{term "(aaa, bbb, ccc)"}))

    73     App(

    74       App(

    75         Const("Product_Type.Pair", Type("fun", List(TFree("'a", List("HOL.type")),Type("fun", List(Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type")))))),Type("Product_Type.prod", List(TFree("'a", List("HOL.type")),Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))))))),

    76         Free("aaa", TFree("'a", List("HOL.type")))),

    77       App(

    78         App(

    79           Const("Product_Type.Pair", Type("fun", List(TFree("'b", List("HOL.type")),Type("fun", List(Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type")))),Type("Product_Type.prod", List(TFree("'b", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))))),

    80           Free("bbb", TFree("'b", List("HOL.type")))),

    81         App(

    82           App(

    83             Const("Product_Type.Pair", Type("fun", List(TFree("'c", List("HOL.type")),Type("fun", List(TFree("'d", List("HOL.type")),Type("Product_Type.prod", List(TFree("'c", List("HOL.type")),TFree("'d", List("HOL.type"))))))))),

    84             Free("ccc", TFree("'c", List("HOL.type")))),

    85           Free("ddd", TFree("'d", List("HOL.type"))

    86         ))

    87       ))

    88     )

    89     println("\\--END isac.gui.mawen.syntax.ScalaAstFromString#test_etc");

    90   }

    91 

    92   override def tearDown() {

    93     sys_.dispose()

    94     super.tearDown()

    95   }

    96 }
wneuper/isac