Move ArchiveParser.parser to GlobalState

LS-Lab · Sep 12, 2024 · 28cdfd5 · 28cdfd5
1 parent a7eff96
commit 28cdfd5
Show file tree

Hide file tree

Showing 18 changed files with 106 additions and 106 deletions.
diff --git a/keymaerax-core/src/main/scala/org/keymaerax/GlobalState.scala b/keymaerax-core/src/main/scala/org/keymaerax/GlobalState.scala
@@ -5,7 +5,10 @@
 
 package org.keymaerax
 
-import org.keymaerax.parser.DLParser
+import org.keymaerax.bellerophon.ReflectiveExpressionBuilder
+import org.keymaerax.bellerophon.parser.{BellePrettyPrinter, DLBelleParser}
+import org.keymaerax.btactics.TactixInit
+import org.keymaerax.parser.{ArchiveParser, DLArchiveParser, DLParser}
 
 /**
  * This object aims to centralize as much global state as possible, with the ultimate goal of eliminating global state.
@@ -19,11 +22,14 @@ import org.keymaerax.parser.DLParser
  *   - [[org.keymaerax.btactics.TactixInit]]
  *   - [[org.keymaerax.btactics.ToolProvider]]
  *   - [[org.keymaerax.core.PrettyPrinter]]
- *   - [[org.keymaerax.parser.ArchiveParser]]
  *
  * If you stumble across any other global state, add it to the list!
  */
 
 object GlobalState {
   val parser = new DLParser
+
+  val archiveParser: ArchiveParser = new DLArchiveParser(
+    new DLBelleParser(BellePrettyPrinter, ReflectiveExpressionBuilder(_, _, Some(TactixInit.invGenerator), _))
+  )
 }
diff --git a/keymaerax-core/src/main/scala/org/keymaerax/btactics/TactixLibrary.scala b/keymaerax-core/src/main/scala/org/keymaerax/btactics/TactixLibrary.scala
@@ -5,6 +5,7 @@
 
 package org.keymaerax.btactics
 
+import org.keymaerax.GlobalState
 import org.keymaerax.bellerophon._
 import org.keymaerax.bellerophon.parser.BelleParser
 import org.keymaerax.btactics.ArithmeticSimplification.smartHide
@@ -17,8 +18,8 @@ import org.keymaerax.core._
 import org.keymaerax.infrastruct.Augmentors._
 import org.keymaerax.infrastruct.{AntePosition, FormulaTools, PosInExpr, Position, RestrictedBiDiUnificationMatch}
 import org.keymaerax.lemma.{Lemma, LemmaDBFactory}
+import org.keymaerax.parser.Declaration
 import org.keymaerax.parser.StringConverter.StringToStringConverter
-import org.keymaerax.parser.{ArchiveParser, Declaration}
 import org.keymaerax.pt.ProvableSig
 import org.keymaerax.tools.ToolEvidence
 import org.keymaerax.tools.ext.{AllOf, Atom, Mathematica, OneOf}
@@ -1611,7 +1612,7 @@ object TactixLibrary
           val model = info.find(_._1 == "model")
           (model, tactic) match {
             case (Some(model), Some(tactic)) =>
-              val defs = ArchiveParser.parser(model._2).head.defs
+              val defs = GlobalState.archiveParser(model._2).head.defs
               if (tactic.contains("expandAllDefs")) { defs.substs }
               else {
                 val subst1 =

diff --git a/keymaerax-core/src/main/scala/org/keymaerax/parser/ArchiveParser.scala b/keymaerax-core/src/main/scala/org/keymaerax/parser/ArchiveParser.scala
@@ -6,9 +6,8 @@
 package org.keymaerax.parser
 
 import org.keymaerax.GlobalState
-import org.keymaerax.bellerophon.parser.{BellePrettyPrinter, DLBelleParser, TacticParser}
-import org.keymaerax.bellerophon.{BelleExpr, ReflectiveExpressionBuilder}
-import org.keymaerax.btactics.TactixInit
+import org.keymaerax.bellerophon.BelleExpr
+import org.keymaerax.bellerophon.parser.TacticParser
 import org.keymaerax.core._
 import org.keymaerax.infrastruct.Augmentors._
 import org.keymaerax.infrastruct.ExpressionTraversal.{ExpressionTraversalFunction, StopTraversal}
@@ -612,25 +611,17 @@ trait ArchiveParser extends (String => List[ParsedArchiveEntry]) {
 }
 
 object ArchiveParser extends ArchiveParser {
-  val parser: ArchiveParser = new DLArchiveParser(
-    new DLBelleParser(BellePrettyPrinter, ReflectiveExpressionBuilder(_, _, Some(TactixInit.invGenerator), _))
-  )
-
-  /** @inheritdoc */
-  override protected def doParse(input: String, parseTactics: Boolean): List[ParsedArchiveEntry] = parser
+  override protected def doParse(input: String, parseTactics: Boolean): List[ParsedArchiveEntry] = GlobalState
+    .archiveParser
     .doParse(input, parseTactics)
 
-  /** @inheritdoc */
-  override def parseFromFile(file: String): List[ParsedArchiveEntry] = parser.parseFromFile(file)
+  override def parseFromFile(file: String): List[ParsedArchiveEntry] = GlobalState.archiveParser.parseFromFile(file)
 
-  /** @inheritdoc */
-  override def exprParser: Parser = parser.exprParser
+  override def exprParser: Parser = GlobalState.archiveParser.exprParser
 
-  /** @inheritdoc */
-  override def tacticParser: TacticParser = parser.tacticParser
+  override def tacticParser: TacticParser = GlobalState.archiveParser.tacticParser
 
-  /** @inheritdoc */
-  override def definitionsPackageParser: String => Declaration = parser.definitionsPackageParser
+  override def definitionsPackageParser: String => Declaration = GlobalState.archiveParser.definitionsPackageParser
 
   private[parser] object BuiltinAnnotationDefinitions {
     val defs: Declaration = Declaration(Map(

diff --git a/keymaerax-core/src/main/scala/org/keymaerax/parser/KeYmaeraXArchivePrinter.scala b/keymaerax-core/src/main/scala/org/keymaerax/parser/KeYmaeraXArchivePrinter.scala
@@ -5,6 +5,7 @@
 
 package org.keymaerax.parser
 
+import org.keymaerax.GlobalState
 import org.keymaerax.core._
 import org.keymaerax.info.Version
 import org.keymaerax.infrastruct.Augmentors.ExpressionAugmentor
@@ -414,7 +415,8 @@ class KeYmaeraXLegacyArchivePrinter(withComments: Boolean = false) extends (Pars
 
       if (withComments) {
         assert(
-          ArchiveParser.parser(printed).map(_.model) == ArchiveParser.parser(entry.problemContent).map(_.model),
+          GlobalState.archiveParser(printed).map(_.model) ==
+            GlobalState.archiveParser(entry.problemContent).map(_.model),
           "Expected printed entry and stored problem content to reparse to same model",
         )
 

diff --git a/keymaerax-webui/src/main/scala/org/keymaerax/hydra/ArchiveEntryPrinter.scala b/keymaerax-webui/src/main/scala/org/keymaerax/hydra/ArchiveEntryPrinter.scala
@@ -5,14 +5,9 @@
 
 package org.keymaerax.hydra
 
+import org.keymaerax.GlobalState
 import org.keymaerax.btactics.TactixLibrary
-import org.keymaerax.parser.{
-  ArchiveParser,
-  KeYmaeraXArchivePrinter,
-  ParseException,
-  ParsedArchiveEntry,
-  PrettierPrintFormatProvider,
-}
+import org.keymaerax.parser.{KeYmaeraXArchivePrinter, ParseException, ParsedArchiveEntry, PrettierPrintFormatProvider}
 
 import scala.annotation.nowarn
 import scala.collection.immutable.{::, List, Nil}
@@ -21,7 +16,7 @@ object ArchiveEntryPrinter {
   @nowarn("msg=match may not be exhaustive")
   def archiveEntry(modelInfo: ModelPOJO, tactics: List[(String, String)], withComments: Boolean): String =
     try {
-      ArchiveParser.parser(modelInfo.keyFile) match {
+      GlobalState.archiveParser(modelInfo.keyFile) match {
         case (entry @ ParsedArchiveEntry(name, _, _, _, _, _, _, _, _)) :: Nil if name == "<undefined>" =>
           new KeYmaeraXArchivePrinter(PrettierPrintFormatProvider(_, 80), withComments)(
             replaceInfo(entry, modelInfo.name, tactics)

diff --git a/...erax-webui/src/main/scala/org/keymaerax/hydra/requests/proofs/GetProofLemmasRequest.scala b/...erax-webui/src/main/scala/org/keymaerax/hydra/requests/proofs/GetProofLemmasRequest.scala
@@ -5,11 +5,11 @@
 
 package org.keymaerax.hydra.requests.proofs
 
+import org.keymaerax.GlobalState
 import org.keymaerax.core.{Formula, Sequent}
 import org.keymaerax.hydra.responses.proofs.ProofLemmasResponse
 import org.keymaerax.hydra.{DBAbstraction, ModelPOJO, ProofPOJO, ReadRequest, Response, UserProofRequest}
 import org.keymaerax.lemma.LemmaDBFactory
-import org.keymaerax.parser.ArchiveParser
 
 import java.io.File
 import scala.collection.immutable.{IndexedSeq, List, Nil}
@@ -42,9 +42,10 @@ class GetProofLemmasRequest(db: DBAbstraction, userId: String, proofId: String)
             val modelConc = e
               ._1
               .defs
-              .exhaustiveSubst(
-                Sequent(IndexedSeq(), IndexedSeq(ArchiveParser.parser(e._1.keyFile).head.model.asInstanceOf[Formula]))
-              )
+              .exhaustiveSubst(Sequent(
+                IndexedSeq(),
+                IndexedSeq(GlobalState.archiveParser(e._1.keyFile).head.model.asInstanceOf[Formula]),
+              ))
             lemmaConc != modelConc // outdated or unexpected if different conclusion
           case None => true
         }

diff --git a/keymaerax-webui/src/main/scala/org/keymaerax/hydra/responses/models/GetModelResponse.scala b/keymaerax-webui/src/main/scala/org/keymaerax/hydra/responses/models/GetModelResponse.scala
@@ -5,14 +5,15 @@
 
 package org.keymaerax.hydra.responses.models
 
+import org.keymaerax.GlobalState
 import org.keymaerax.hydra.{ModelPOJO, Response}
 import org.keymaerax.parser.{ArchiveParser, ParseException}
 import spray.json.{JsArray, JsBoolean, JsNumber, JsObject, JsString, JsValue}
 
 class GetModelResponse(model: ModelPOJO) extends Response {
 
   private def illustrationLinks(): List[String] =
-    try { ArchiveParser.parser(model.keyFile).flatMap(_.info.get("Illustration")) }
+    try { GlobalState.archiveParser(model.keyFile).flatMap(_.info.get("Illustration")) }
     catch { case _: ParseException => Nil }
 
   def getJson: JsValue = JsObject(

diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/bellerophon/SpoonFeedingInterpreterTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/bellerophon/SpoonFeedingInterpreterTests.scala
@@ -5,6 +5,7 @@
 
 package org.keymaerax.bellerophon
 
+import org.keymaerax.GlobalState
 import org.keymaerax.bellerophon.parser.BellePrettyPrinter
 import org.keymaerax.btactics.TactixLibrary._
 import org.keymaerax.btactics.{
@@ -3107,8 +3108,8 @@ class SpoonFeedingInterpreterTests extends TacticTestBase {
   "Delayed substitution" should "support introducing variables for function symbols of closed provables" in withMathematica {
     _ =>
       withDatabase { db =>
-        val entry = ArchiveParser
-          .parser(
+        val entry = GlobalState
+          .archiveParser(
             """ArchiveEntry "Delayed Substitution from dIRule"
               |ProgramVariables Real x, y, r; End.
               |Problem x^2+y^2=r -> [{x'=r*y,y'=-r*x}]x^2+y^2=r End.
@@ -3142,8 +3143,8 @@ class SpoonFeedingInterpreterTests extends TacticTestBase {
 
   it should "work if steps modify the subgoal and dIRule constifies after" in withMathematica { _ =>
     withDatabase { db =>
-      val entry = ArchiveParser
-        .parser(
+      val entry = GlobalState
+        .archiveParser(
           """ArchiveEntry "Delayed Substitution from dIRule"
             |ProgramVariables Real x, y, r; End.
             |Problem x^2+y^2=r -> [{x'=r*y,y'=-r*x}]x^2+y^2=r End.
@@ -3178,8 +3179,8 @@ class SpoonFeedingInterpreterTests extends TacticTestBase {
 
   it should "support unfinished dIRule if sole open goal" in withMathematica { _ =>
     withDatabase { db =>
-      val entry = ArchiveParser
-        .parser(
+      val entry = GlobalState
+        .archiveParser(
           """ArchiveEntry "Delayed Substitution from dIRule"
             |ProgramVariables Real x, y, r; End.
             |Problem x^2+y^2=r -> [{x'=r*y,y'=-r*x}]x^2+y^2=r End.
@@ -3205,8 +3206,8 @@ class SpoonFeedingInterpreterTests extends TacticTestBase {
   it should "FEATURE_REQUEST: expand definitions after applying backsubstitutions from constification" taggedAs TodoTest in withMathematica {
     _ =>
       withDatabase { db =>
-        val entry = ArchiveParser
-          .parser(
+        val entry = GlobalState
+          .archiveParser(
             """ArchiveEntry "Delayed Substitution from dIRule"
               |Definitions Real sqsum(Real x, Real y) = x^2+y^2; End.
               |ProgramVariables Real x, y, r; End.
@@ -3255,8 +3256,8 @@ class SpoonFeedingInterpreterTests extends TacticTestBase {
   it should "FEATURE_REQUEST: expand definitions exhaustively after applying backsubstitutions from constification" taggedAs TodoTest in withMathematica {
     _ =>
       withDatabase { db =>
-        val entry = ArchiveParser
-          .parser(
+        val entry = GlobalState
+          .archiveParser(
             """ArchiveEntry "Delayed Substitution from dIRule"
               |Definitions Real dosqsum(Real x, Real y) = x^2+y^2; Real sqsum(Real x, Real y) = dosqsum(x,y); End.
               |ProgramVariables Real x, y, r; End.
@@ -3304,8 +3305,8 @@ class SpoonFeedingInterpreterTests extends TacticTestBase {
 
   it should "support nested constifications" in withMathematica { _ =>
     withDatabase { db =>
-      val entry = ArchiveParser
-        .parser(
+      val entry = GlobalState
+        .archiveParser(
           """ArchiveEntry "Delayed Substitution from dIRule"
             |ProgramVariables Real x, y, r, s; End.
             |Problem x^2+y^2+s=r -> [{x'=r*y,y'=-r*x}]x^2+y^2+s=r End.
@@ -3438,8 +3439,8 @@ class SpoonFeedingInterpreterTests extends TacticTestBase {
   it should "FEATURE_REQUEST: return delayed substitution on unfinished dIRule when mixed with unconstified branches" taggedAs TodoTest in withMathematica {
     _ =>
       withDatabase { db =>
-        val entry = ArchiveParser
-          .parser(
+        val entry = GlobalState
+          .archiveParser(
             """ArchiveEntry "Delayed Substitution from dIRule"
               |ProgramVariables Real x, y, r; End.
               |Problem x^2+y^2=r -> [{x'=r*y,y'=-r*x}]x^2+y^2=r End.

diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/btactics/BenchmarkTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/btactics/BenchmarkTests.scala
@@ -514,7 +514,7 @@ class BenchmarkTester(val benchmarkName: String, val url: String, val timeout: I
       .setAnnotationListener((p: Program, inv: Formula) =>
         generator.products += (p -> (generator.products.getOrElse(p, Nil) :+ Invariant(inv)))
       )
-    val entry = ArchiveParser.parser(modelContent).head
+    val entry = GlobalState.archiveParser(modelContent).head
     TactixInit.invSupplier = generator
     TactixInit.differentialInvGenerator = FixedGenerator(Nil)
     TactixInit.loopInvGenerator = FixedGenerator(Nil)
@@ -530,7 +530,7 @@ class BenchmarkTester(val benchmarkName: String, val url: String, val timeout: I
     TactixInit.differentialInvGenerator = InvariantGenerator.cached(InvariantGenerator.differentialInvariantGenerator)
     TactixInit.loopInvGenerator = InvariantGenerator.cached(InvariantGenerator.loopInvariantGenerator)
     GlobalState.parser.setAnnotationListener((_: Program, _: Formula) => {})
-    val entry = ArchiveParser.parser(modelContent).head
+    val entry = GlobalState.archiveParser(modelContent).head
     (entry.model.asInstanceOf[Formula], entry.defs)
   }
 

diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/btactics/InvariantGeneratorTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/btactics/InvariantGeneratorTests.scala
@@ -11,8 +11,8 @@ import org.keymaerax.btactics.TactixLibrary._
 import org.keymaerax.core._
 import org.keymaerax.hydra.DatabasePopulator
 import org.keymaerax.infrastruct.{FormulaTools, SuccPosition}
+import org.keymaerax.parser.Declaration
 import org.keymaerax.parser.StringConverter._
-import org.keymaerax.parser.{ArchiveParser, Declaration}
 import org.keymaerax.tagobjects.{IgnoreInBuildTest, TodoTest}
 import org.keymaerax.tags.{ExtremeTest, UsualTest}
 import org.keymaerax.tools.ext.{MathematicaInvGenTool, PlotConverter}
@@ -997,7 +997,7 @@ class NonlinearExamplesTester(
     TactixInit.invSupplier = FixedGenerator(Nil)
     TactixInit.differentialInvGenerator = FixedGenerator(Nil)
     GlobalState.parser.setAnnotationListener((_: Program, _: Formula) => {})
-    val entry = ArchiveParser.parser(modelContent).head
+    val entry = GlobalState.archiveParser(modelContent).head
     (entry.model.asInstanceOf[Formula], entry.defs)
   }
 

diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/btactics/SequentialInterpreterTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/btactics/SequentialInterpreterTests.scala
@@ -5,6 +5,7 @@
 
 package org.keymaerax.btactics
 
+import org.keymaerax.GlobalState
 import org.keymaerax.bellerophon._
 import org.keymaerax.btactics.DebuggingTactics.error
 import org.keymaerax.btactics.TacticFactory.anon
@@ -755,8 +756,8 @@ class SequentialInterpreterTests extends TacticTestBase {
   }
 
   "Tactics with delayed substitution" should "replay expandAll" in withMathematica { _ =>
-    val entry = ArchiveParser
-      .parser(
+    val entry = GlobalState
+      .archiveParser(
         """ArchiveEntry "Delayed Substitution"
           |Definitions Bool p(Real x) <-> x>0; Bool q(Real y) <-> y>0; End.
           |ProgramVariables Real x; Real y; End.
@@ -785,8 +786,8 @@ class SequentialInterpreterTests extends TacticTestBase {
   }
 
   it should "replay when expanded on branches" in withMathematica { _ =>
-    val entry = ArchiveParser
-      .parser(
+    val entry = GlobalState
+      .archiveParser(
         """ArchiveEntry "Delayed Substitution"
           |Definitions Bool p(Real x) <-> x>0; Bool q(Real y) <-> y>0; End.
           |ProgramVariables Real x; Real y; End.
@@ -822,8 +823,8 @@ class SequentialInterpreterTests extends TacticTestBase {
   }
 
   it should "replay when expanded only on some branches" in withMathematica { _ =>
-    val entry = ArchiveParser
-      .parser(
+    val entry = GlobalState
+      .archiveParser(
         """ArchiveEntry "Delayed Substitution"
           |Definitions Bool p(Real x) <-> x>0; Bool q(Real y) <-> y>0; End.
           |ProgramVariables Real x; Real y; End.
@@ -861,8 +862,8 @@ class SequentialInterpreterTests extends TacticTestBase {
   }
 
   it should "support introducing variables for function symbols of closed provables" in withMathematica { _ =>
-    val entry = ArchiveParser
-      .parser(
+    val entry = GlobalState
+      .archiveParser(
         """ArchiveEntry "Delayed Substitution from dIRule"
           |ProgramVariables Real x, y, r; End.
           |Problem x^2+y^2=r -> [{x'=r*y,y'=-r*x}]x^2+y^2=r End.

diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/btactics/TactixLibraryTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/btactics/TactixLibraryTests.scala
@@ -725,8 +725,8 @@ class TactixLibraryTests extends TacticTestBase {
   )
 
   it should "apply ODE duration heuristic to multiple ODEs" in withZ3 { _ =>
-    val problem = ArchiveParser
-      .parser(
+    val problem = GlobalState
+      .archiveParser(
         """Theorem ""
           |Problem
           |x < -4

diff --git a/keymaerax-webui/src/test/scala/org/keymaerax/launcher/LauncherTests.scala b/keymaerax-webui/src/test/scala/org/keymaerax/launcher/LauncherTests.scala
@@ -5,6 +5,7 @@
 
 package org.keymaerax.launcher
 
+import org.keymaerax.GlobalState
 import org.keymaerax.btactics.TacticTestBase
 import org.keymaerax.core.{Formula, Sequent}
 import org.keymaerax.parser.{
@@ -75,7 +76,7 @@ class LauncherTests extends TacticTestBase {
       .loneElement
       .asInstanceOf[ToolEvidence]
       .info
-    ArchiveParser.parser(model).loneElement.expandedModel shouldBe conjecture.expandedModel
+    GlobalState.archiveParser(model).loneElement.expandedModel shouldBe conjecture.expandedModel
     tactic shouldBe "master"
     proof shouldBe empty // proof term not exported
   }
@@ -145,7 +146,7 @@ class LauncherTests extends TacticTestBase {
           Sequent(IndexedSeq(), IndexedSeq(conjecture.expandedModel.asInstanceOf[Formula]))
         val ("tool", "KeYmaera X") :: ("model", model) :: ("tactic", tactic) :: ("proof", proof) :: Nil =
           exported._3.loneElement.asInstanceOf[ToolEvidence].info
-        val entry = ArchiveParser.parser(model).loneElement
+        val entry = GlobalState.archiveParser(model).loneElement
         entry.name shouldBe conjecture.name
         entry.expandedModel shouldBe conjecture.expandedModel
         tactic shouldBe "master()"