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(_) =>

    }

  }

}