package isac.bridge

 import junit.framework.TestCase

 import isac.util.BridgeMainPaths

 import java.nio.file.Paths

 import java.io.InputStream

 import junit.framework.Assert._

 import scala.concurrent._

 import scala.concurrent.ExecutionContext.Implicits.global

 import scala.concurrent.duration._

 //import org.scalatest.junit.JUnit3Suite

 //import org.scalatest.junit.AssertionsForJUnit

 import edu.tum.cs.isabelle._

 import edu.tum.cs.isabelle.api._

 import edu.tum.cs.isabelle.japi._

 import edu.tum.cs.isabelle.pure._

 import edu.tum.cs.isabelle.hol._

 import edu.tum.cs.isabelle.setup.Setup

 class TestTerm extends TestCase {

   val ReadTerm = Operation.implicitly[(String, Typ, String), Option[Term]]("read_term")

   val MakeInt = Operation.implicitly[Unit, Term]("make_int")

   var IsabelleHome: String = _

   // get ISABELLE_HOME from BridgeMain.properties, compare isac.bridge.TestPIDE in java

 //  override def setUp() {

 //    var inputStream: InputStream = null

 //    try {

 //      val prop = new Properties()

 //      GOON

 //    }

 //    catch { case e: Exception =>

 //      e.printStackTrace()

 //      sys.exit(1)

 //    }

 //    

 //    IsabelleHome = new StringBuilder("TODO")

 //  }

   // another temmplate: http://stackoverflow.com/questions/15658310/scala-load-java-properties

 //  override def setUp() {

 //    val IsabelleHome = 

 //      try {

 //        //val prop = new Properties(List[String])

 //        val prop = new Properties()

 //        prop.load(new FileInputStream("TODO"))

 //        (

 //          new String(prop.getProperty("ISABELLE_HOME"))

 //        ) 

 //        } catch { case e: Exception => 

 //          e.printStackTrace()

 //          sys.exit(1)

 //        }

 //    }

   def testTerm() {

     //val setup = Setup(Paths.get(IsabelleHome), JPlatform.guess(),

 //  val setup = Setup(Paths.get(BridgeMainPaths.ISABELLE_HOME), JPlatform.guess(),

     val setup = Setup(Paths.get("/usr/local/isabisac/"), JPlatform.guess(),

           new Version("2015"), Setup.defaultPackageName)

     val env = JSetup.makeEnvironment(setup)

     val config = Configuration.fromBuiltin("libisabelle_Isac")

     val sys = Await.result(System.create(env, config), 10.seconds)

     val thy = Theory(sys, "Main")

     val expr = Await.result(Expr.ofString[scala.math.BigInt](thy, "3"), 10.seconds)

     println(expr)

     val expr2 = Await.result(sys.invoke(ReadTerm)(("3", Type("Int.int", Nil), "Main")), 10.seconds)

     println(expr2)

     val expr3 = Await.result(sys.invoke(MakeInt)(()), 10.seconds)

     println(expr3)

     //----- in Protocol.thy#operation_setup make_int: HOLogic.mk_number @{typ int} 3

     // HOLogic.mk_number @{typ int} 3

     //--- ouput in SML:

     //       Const ("Num.numeral_class.numeral", "num ⇒ int") $ (

     //         Const ("Num.num.Bit1", "num ⇒ num") $ 

     //         Const ("Num.num.One", "num"))

     //----- from ../TestTerm.scala:

     // result(sys.invoke(MakeInt)(())

     //--- ouput in scala:

     // Success(

     //   App(Const(Num.numeral_class.numeral,Type(fun,List(Type(Num.num,List()), Type(Int.int,List())))),

     //     App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),

     //         Const(Num.num.One,Type(Num.num,List())))))

     val t: Term = Const("HOL.True", Typ.dummyT)

     t match {

       case Const(_, _) =>

       case Free(_, _) =>

       case Abs(_, _, _) =>

       case App(_, _) =>

       case Var(_, _) =>

       case Bound(_) =>

     }

   }

 }