Streamlined access to Slang runtime library type hierarchy.

sireum · Oct 1, 2024 · dedd712 · dedd712
1 parent af263f7
commit dedd712
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 7 deletions.
diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaRcTest.scala
@@ -85,7 +85,7 @@ class LogikaRcTest extends SireumRcSpec {
     val nameExePathMap = Smt2Invoke.nameExePathMap(sireumHome)
     Logika.checkScript(Some(f.string), content, c, nameExePathMap, Os.numOfProcessors,
       th => Smt2Impl.create(c, ISZ(), th, reporter),
-      NoTransitionSmt2Cache.create, reporter, T, Logika.defaultPlugins, _ => (tc.typeHierarchy, rep), line, ISZ(), ISZ())
+      NoTransitionSmt2Cache.create, reporter, T, Logika.defaultPlugins, line, ISZ(), ISZ())
     reporter.printMessages()
     val name = f.name.value
     if (name.startsWith(failPrefix)) {

diff --git a/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala b/jvm/src/test/scala/org/sireum/logika/LogikaTest.scala
@@ -32,7 +32,6 @@ import org.sireum.test._
 object LogikaTest {
 
   val sireumHome: Os.Path = Os.path(Os.env("SIREUM_HOME").get).canon
-  lazy val (tc, rep) = lang.FrontEnd.checkedLibraryReporterPar(Runtime.getRuntime.availableProcessors)
 
   val rlimit: Z = {
     var r: Z = 1000000
@@ -209,8 +208,7 @@ class LogikaTest extends TestSuite {
     Smt2Invoke.haltOnError = T
     val nameExePathMap = Smt2Invoke.nameExePathMap(sireumHome)
     Logika.checkScript(None(), input, config, nameExePathMap, Os.numOfProcessors, th => Smt2Impl.create(config, ISZ(),
-      th, reporter), NoTransitionSmt2Cache.create, reporter, T, Logika.defaultPlugins, _ => (tc.typeHierarchy, rep),
-      0, ISZ(), ISZ())
+      th, reporter), NoTransitionSmt2Cache.create, reporter, T, Logika.defaultPlugins, 0, ISZ(), ISZ())
     if (reporter.hasIssue) {
       msgOpt match {
         case Some(msg) =>

diff --git a/shared/src/main/scala/org/sireum/logika/Logika.scala b/shared/src/main/scala/org/sireum/logika/Logika.scala
@@ -427,7 +427,7 @@ object Logika {
 
   def checkScript(fileUriOpt: Option[String], input: String, config: Config, nameExePathMap: HashMap[String, String],
                   maxCores: Z, smt2f: lang.tipe.TypeHierarchy => Smt2, cache: Logika.Cache, reporter: Reporter,
-                  hasLogika: B, plugins: ISZ[Plugin], thInit: Z => (TypeHierarchy, message.Reporter), line: Z,
+                  hasLogika: B, plugins: ISZ[Plugin], line: Z,
                   skipMethods: ISZ[String], skipTypes: ISZ[String]): Unit = {
     val parsingStartTime = extension.Time.currentMillis
     val isWorksheet: B = fileUriOpt match {
@@ -449,12 +449,12 @@ object Logika {
           if (!isWorksheet) {
             return
           }
-          val (th, rep) = extension.Cancel.cancellable(() => thInit(maxCores))
+          val (tc, rep) = extension.Cancel.cancellable(() => lang.FrontEnd.checkedLibraryReporter)
           val typeCheckingStartTime = extension.Time.currentMillis
           reporter.timing(libraryDesc, typeCheckingStartTime - libraryStartTime)
           reporter.reports(rep.messages)
           val (th2, p) = extension.Cancel.cancellable(() =>
-            lang.FrontEnd.checkWorksheet(config.parCores, Some(th), program, reporter))
+            lang.FrontEnd.checkWorksheet(config.parCores, Some(tc.typeHierarchy), program, reporter))
           if (!reporter.hasError) {
             lang.tipe.PostTipeAttrChecker.checkProgram(p, reporter)
           }