package isac.bridge

 import junit.framework.TestCase

 import scala.concurrent._

 import scala.concurrent.ExecutionContext.Implicits.global

 import scala.concurrent.duration._

 import java.nio.file.Paths

 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._

 class TestTerm extends TestCase {

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

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

   def testTerm() {

     val env = JSetup.makeEnvironment(

                 Paths.get("/usr/local/isabisac"), JPlatform.guess(), new Version("2015"))

     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)

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

     t match {

       case Const(_, _) =>

       case Free(_, _) =>

     }

   }

 }