1.1 --- a/isac-java/src/java-tests/isac/bridge/TestTerm.scala	Wed Sep 12 16:24:42 2018 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,110 +0,0 @@
     1.4 -package isac.bridge
     1.5 -
     1.6 -import junit.framework.TestCase
     1.7 -
     1.8 -import isac.util.BridgeMainPaths
     1.9 -
    1.10 -import java.nio.file.Paths
    1.11 -import java.io.InputStream
    1.12 -import junit.framework.Assert._
    1.13 -
    1.14 -import scala.concurrent._
    1.15 -import scala.concurrent.ExecutionContext.Implicits.global
    1.16 -import scala.concurrent.duration._
    1.17 -//import org.scalatest.junit.JUnit3Suite
    1.18 -//import org.scalatest.junit.AssertionsForJUnit
    1.19 -
    1.20 -import info.hupel.isabelle._
    1.21 -import info.hupel.isabelle.api._
    1.22 -import info.hupel.isabelle.japi._
    1.23 -import info.hupel.isabelle.pure._
    1.24 -import info.hupel.isabelle.hol._
    1.25 -import info.hupel.isabelle.setup.Setup
    1.26 -
    1.27 -class TestTerm extends TestCase {
    1.28 -
    1.29 -  val ReadTerm = Operation.implicitly[(String, Typ, String), Option[Term]]("read_term")
    1.30 -  
    1.31 -  val MakeInt = Operation.implicitly[Unit, Term]("make_int")
    1.32 -  
    1.33 -  var IsabelleHome: String = _
    1.34 -  
    1.35 -  // get ISABELLE_HOME from BridgeMain.properties, compare isac.bridge.TestPIDE in java
    1.36 -//  override def setUp() {
    1.37 -//    var inputStream: InputStream = null
    1.38 -//    try {
    1.39 -//      val prop = new Properties()
    1.40 -//      GOON
    1.41 -//    }
    1.42 -//    catch { case e: Exception =>
    1.43 -//      e.printStackTrace()
    1.44 -//      sys.exit(1)
    1.45 -//    }
    1.46 -//    
    1.47 -//    IsabelleHome = new StringBuilder("TODO")
    1.48 -//  }
    1.49 -
    1.50 -  // another temmplate: http://stackoverflow.com/questions/15658310/scala-load-java-properties
    1.51 -//  override def setUp() {
    1.52 -//    val IsabelleHome = 
    1.53 -//      try {
    1.54 -//        //val prop = new Properties(List[String])
    1.55 -//        val prop = new Properties()
    1.56 -//        prop.load(new FileInputStream("TODO"))
    1.57 -//        (
    1.58 -//          new String(prop.getProperty("ISABELLE_HOME"))
    1.59 -//        ) 
    1.60 -//        } catch { case e: Exception => 
    1.61 -//          e.printStackTrace()
    1.62 -//          sys.exit(1)
    1.63 -//        }
    1.64 -//    }
    1.65 - 
    1.66 -  
    1.67 -  def testTerm() {
    1.68 -    val res = JResources.dumpIsabelleResources()
    1.69 -    val config = Configuration.fromBuiltin("libisabelle_Isac")
    1.70 -    val env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res)
    1.71 -    val sys = JSystem.create(env, config)
    1.72 -//    val setup = Setup(Paths.get("/usr/local/isabisac/"), JPlatform.guess(),
    1.73 -//          new Version("2015"), Setup.defaultPackageName)
    1.74 -//    val env = JSetup.makeEnvironment(setup)
    1.75 -//    val config = Configuration.fromBuiltin("libisabelle_Isac")
    1.76 -//    val sys = Await.result(System.create(env, config), 10.seconds)
    1.77 -    val thy = Theory(sys, "Main")
    1.78 -    
    1.79 -    val expr = Await.result(Expr.ofString[scala.math.BigInt](thy, "3"), 10.seconds)
    1.80 -    println(expr)
    1.81 -    
    1.82 -    val expr2 = Await.result(sys.invoke(ReadTerm)(("3", Type("Int.int", Nil), "Main")), 10.seconds)
    1.83 -    println(expr2)
    1.84 -    
    1.85 -    val expr3 = Await.result(sys.invoke(MakeInt)(()), 10.seconds)
    1.86 -    println(expr3)
    1.87 -    //----- in Protocol.thy#operation_setup make_int: HOLogic.mk_number @{typ int} 3
    1.88 -    // HOLogic.mk_number @{typ int} 3
    1.89 -    //--- ouput in SML:
    1.90 -    //       Const ("Num.numeral_class.numeral", "num ⇒ int") $ (
    1.91 -    //         Const ("Num.num.Bit1", "num ⇒ num") $ 
    1.92 -    //         Const ("Num.num.One", "num"))
    1.93 -    //----- from ../TestTerm.scala:
    1.94 -    // result(sys.invoke(MakeInt)(())
    1.95 -    //--- ouput in scala:
    1.96 -    // Success(
    1.97 -    //   App(Const(Num.numeral_class.numeral,Type(fun,List(Type(Num.num,List()), Type(Int.int,List())))),
    1.98 -    //     App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),
    1.99 -    //         Const(Num.num.One,Type(Num.num,List())))))
   1.100 -    
   1.101 -    val t: Term = Const("HOL.True", Typ.dummyT)
   1.102 -    
   1.103 -    t match {
   1.104 -      case Const(_, _) =>
   1.105 -      case Free(_, _) =>
   1.106 -      case Abs(_, _, _) =>
   1.107 -      case App(_, _) =>
   1.108 -      case Var(_, _) =>
   1.109 -      case Bound(_) =>
   1.110 -    }
   1.111 -  }
   1.112 -
   1.113 -}
   1.114 \ No newline at end of file