1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/isac-java/src/java-tests/isac/bridge/TestTerm.scala	Fri Mar 26 10:45:05 2021 +0100
     1.3 @@ -0,0 +1,108 @@
     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 edu.tum.cs.isabelle._
    1.21 +import edu.tum.cs.isabelle.api._
    1.22 +import edu.tum.cs.isabelle.japi._
    1.23 +import edu.tum.cs.isabelle.pure._
    1.24 +import edu.tum.cs.isabelle.hol._
    1.25 +import edu.tum.cs.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 setup = Setup(Paths.get(IsabelleHome), JPlatform.guess(),
    1.69 +//  val setup = Setup(Paths.get(BridgeMainPaths.ISABELLE_HOME), JPlatform.guess(),
    1.70 +    val setup = Setup(Paths.get("/usr/local/isabisac/"), JPlatform.guess(),
    1.71 +          new Version("2015"), Setup.defaultPackageName)
    1.72 +    val env = JSetup.makeEnvironment(setup)
    1.73 +    val config = Configuration.fromBuiltin("libisabelle_Isac")
    1.74 +    val sys = Await.result(System.create(env, config), 10.seconds)
    1.75 +    val thy = Theory(sys, "Main")
    1.76 +    
    1.77 +    val expr = Await.result(Expr.ofString[scala.math.BigInt](thy, "3"), 10.seconds)
    1.78 +    println(expr)
    1.79 +    
    1.80 +    val expr2 = Await.result(sys.invoke(ReadTerm)(("3", Type("Int.int", Nil), "Main")), 10.seconds)
    1.81 +    println(expr2)
    1.82 +    
    1.83 +    val expr3 = Await.result(sys.invoke(MakeInt)(()), 10.seconds)
    1.84 +    println(expr3)
    1.85 +    //----- in Protocol.thy#operation_setup make_int: HOLogic.mk_number @{typ int} 3
    1.86 +    // HOLogic.mk_number @{typ int} 3
    1.87 +    //--- ouput in SML:
    1.88 +    //       Const ("Num.numeral_class.numeral", "num ⇒ int") $ (
    1.89 +    //         Const ("Num.num.Bit1", "num ⇒ num") $ 
    1.90 +    //         Const ("Num.num.One", "num"))
    1.91 +    //----- from ../TestTerm.scala:
    1.92 +    // result(sys.invoke(MakeInt)(())
    1.93 +    //--- ouput in scala:
    1.94 +    // Success(
    1.95 +    //   App(Const(Num.numeral_class.numeral,Type(fun,List(Type(Num.num,List()), Type(Int.int,List())))),
    1.96 +    //     App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),
    1.97 +    //         Const(Num.num.One,Type(Num.num,List())))))
    1.98 +    
    1.99 +    val t: Term = Const("HOL.True", Typ.dummyT)
   1.100 +    
   1.101 +    t match {
   1.102 +      case Const(_, _) =>
   1.103 +      case Free(_, _) =>
   1.104 +      case Abs(_, _, _) =>
   1.105 +      case App(_, _) =>
   1.106 +      case Var(_, _) =>
   1.107 +      case Bound(_) =>
   1.108 +    }
   1.109 +  }
   1.110 +
   1.111 +}
   1.112 \ No newline at end of file