|
1 package isac.bridge |
|
2 |
|
3 import junit.framework.TestCase |
|
4 |
|
5 import isac.util.BridgeMainPaths |
|
6 |
|
7 import java.nio.file.Paths |
|
8 import java.io.InputStream |
|
9 import junit.framework.Assert._ |
|
10 |
|
11 import scala.concurrent._ |
|
12 import scala.concurrent.ExecutionContext.Implicits.global |
|
13 import scala.concurrent.duration._ |
|
14 //import org.scalatest.junit.JUnit3Suite |
|
15 //import org.scalatest.junit.AssertionsForJUnit |
|
16 |
|
17 import edu.tum.cs.isabelle._ |
|
18 import edu.tum.cs.isabelle.api._ |
|
19 import edu.tum.cs.isabelle.japi._ |
|
20 import edu.tum.cs.isabelle.pure._ |
|
21 import edu.tum.cs.isabelle.hol._ |
|
22 import edu.tum.cs.isabelle.setup.Setup |
|
23 |
|
24 class TestTerm extends TestCase { |
|
25 |
|
26 val ReadTerm = Operation.implicitly[(String, Typ, String), Option[Term]]("read_term") |
|
27 |
|
28 val MakeInt = Operation.implicitly[Unit, Term]("make_int") |
|
29 |
|
30 var IsabelleHome: String = _ |
|
31 |
|
32 // get ISABELLE_HOME from BridgeMain.properties, compare isac.bridge.TestPIDE in java |
|
33 // override def setUp() { |
|
34 // var inputStream: InputStream = null |
|
35 // try { |
|
36 // val prop = new Properties() |
|
37 // GOON |
|
38 // } |
|
39 // catch { case e: Exception => |
|
40 // e.printStackTrace() |
|
41 // sys.exit(1) |
|
42 // } |
|
43 // |
|
44 // IsabelleHome = new StringBuilder("TODO") |
|
45 // } |
|
46 |
|
47 // another temmplate: http://stackoverflow.com/questions/15658310/scala-load-java-properties |
|
48 // override def setUp() { |
|
49 // val IsabelleHome = |
|
50 // try { |
|
51 // //val prop = new Properties(List[String]) |
|
52 // val prop = new Properties() |
|
53 // prop.load(new FileInputStream("TODO")) |
|
54 // ( |
|
55 // new String(prop.getProperty("ISABELLE_HOME")) |
|
56 // ) |
|
57 // } catch { case e: Exception => |
|
58 // e.printStackTrace() |
|
59 // sys.exit(1) |
|
60 // } |
|
61 // } |
|
62 |
|
63 |
|
64 def testTerm() { |
|
65 //val setup = Setup(Paths.get(IsabelleHome), JPlatform.guess(), |
|
66 // val setup = Setup(Paths.get(BridgeMainPaths.ISABELLE_HOME), JPlatform.guess(), |
|
67 val setup = Setup(Paths.get("/usr/local/isabisac/"), JPlatform.guess(), |
|
68 new Version("2015"), Setup.defaultPackageName) |
|
69 val env = JSetup.makeEnvironment(setup) |
|
70 val config = Configuration.fromBuiltin("libisabelle_Isac") |
|
71 val sys = Await.result(System.create(env, config), 10.seconds) |
|
72 val thy = Theory(sys, "Main") |
|
73 |
|
74 val expr = Await.result(Expr.ofString[scala.math.BigInt](thy, "3"), 10.seconds) |
|
75 println(expr) |
|
76 |
|
77 val expr2 = Await.result(sys.invoke(ReadTerm)(("3", Type("Int.int", Nil), "Main")), 10.seconds) |
|
78 println(expr2) |
|
79 |
|
80 val expr3 = Await.result(sys.invoke(MakeInt)(()), 10.seconds) |
|
81 println(expr3) |
|
82 //----- in Protocol.thy#operation_setup make_int: HOLogic.mk_number @{typ int} 3 |
|
83 // HOLogic.mk_number @{typ int} 3 |
|
84 //--- ouput in SML: |
|
85 // Const ("Num.numeral_class.numeral", "num ⇒ int") $ ( |
|
86 // Const ("Num.num.Bit1", "num ⇒ num") $ |
|
87 // Const ("Num.num.One", "num")) |
|
88 //----- from ../TestTerm.scala: |
|
89 // result(sys.invoke(MakeInt)(()) |
|
90 //--- ouput in scala: |
|
91 // Success( |
|
92 // App(Const(Num.numeral_class.numeral,Type(fun,List(Type(Num.num,List()), Type(Int.int,List())))), |
|
93 // App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))), |
|
94 // Const(Num.num.One,Type(Num.num,List()))))) |
|
95 |
|
96 val t: Term = Const("HOL.True", Typ.dummyT) |
|
97 |
|
98 t match { |
|
99 case Const(_, _) => |
|
100 case Free(_, _) => |
|
101 case Abs(_, _, _) => |
|
102 case App(_, _) => |
|
103 case Var(_, _) => |
|
104 case Bound(_) => |
|
105 } |
|
106 } |
|
107 |
|
108 } |