Move Parser.parser to GlobalState

keymaerax-core/src/main/scala/org/keymaerax/GlobalState.scala

@@ -20,7 +20,6 @@ import org.keymaerax.parser.DLParser
  *   - [[org.keymaerax.btactics.ToolProvider]]
  *   - [[org.keymaerax.core.PrettyPrinter]]
  *   - [[org.keymaerax.parser.ArchiveParser]]
- *   - [[org.keymaerax.parser.Parser]]
  *
  * If you stumble across any other global state, add it to the list!
  */

keymaerax-core/src/main/scala/org/keymaerax/bellerophon/parser/BelleParser.scala

@@ -13,7 +13,7 @@ import org.keymaerax.core._
 import org.keymaerax.infrastruct.{AntePosition, PosInExpr, Position}
 import org.keymaerax.parser.StringConverter._
 import org.keymaerax.parser.{COLON => _, COMMA => _, Declaration, EOF => _, IDENT => _, _}
-import org.keymaerax.{Configuration, Logging}
+import org.keymaerax.{Configuration, GlobalState, Logging}
 
 import scala.annotation.{nowarn, tailrec}
 import scala.util.matching.Regex
@@ -55,7 +55,7 @@ object BelleParser extends TacticParser with Logging {
   }
 
   override val tacticParser: String => BelleExpr = this
-  override val expressionParser: Parser = Parser.parser
+  override val expressionParser: Parser = GlobalState.parser
   override val printer: BelleExpr => String = BellePrettyPrinter
 
   /** @inheritdoc */
@@ -467,8 +467,8 @@ object BelleParser extends TacticParser with Logging {
               .map(_.trim)
               .toList match {
               case LIST_END :: Nil => Nil // explicit empty list
-              case head :: Nil => Parser.parser.formulaParser(head) :: Nil // single-element lists without :: nil
-              case scala.collection.:+(args, LIST_END) => args.map(Parser.parser.formulaParser) // all other lists
+              case head :: Nil => GlobalState.parser.formulaParser(head) :: Nil // single-element lists without :: nil
+              case scala.collection.:+(args, LIST_END) => args.map(GlobalState.parser.formulaParser) // all other lists
               case l => throw ParseException(
                   "Formula list in " + USING.img + SPACE + DOUBLE_QUOTE + l.mkString(DOUBLE_COLON) + DOUBLE_QUOTE +
                     " must end in " + DOUBLE_COLON + SPACE + LIST_END,

keymaerax-core/src/main/scala/org/keymaerax/bellerophon/parser/BelleTerminal.scala

@@ -5,8 +5,9 @@
 
 package org.keymaerax.bellerophon.parser
 
+import org.keymaerax.GlobalState
 import org.keymaerax.bellerophon.PositionLocator
-import org.keymaerax.core.{Expression, Formula, Program, SubstitutionPair, Term}
+import org.keymaerax.core.{Expression, SubstitutionPair}
 import org.keymaerax.infrastruct.{FormulaTools, PosInExpr}
 import org.keymaerax.parser.{LexException, Parser, UnknownLocation}
 
@@ -194,7 +195,7 @@ private case class EXPRESSION(override val exprString: String, override val deli
       exprString.startsWith(delimiters._1) && exprString.endsWith(delimiters._2),
       s"EXPRESSION.regexp should ensure delimited expression begin and end with $delimiters, but an EXPRESSION was constructed with argument: $exprString",
     )
-    Parser.parser(undelimitedExprString)
+    GlobalState.parser(undelimitedExprString)
   }
 }
 

keymaerax-core/src/main/scala/org/keymaerax/btactics/InvariantProvers.scala

@@ -5,13 +5,14 @@
 
 package org.keymaerax.btactics
 
+import org.keymaerax.GlobalState
 import org.keymaerax.bellerophon._
 import org.keymaerax.btactics.Idioms.?
 import org.keymaerax.btactics.TacticFactory._
 import org.keymaerax.core._
 import org.keymaerax.infrastruct.Augmentors.{SequentAugmentor, _}
 import org.keymaerax.infrastruct.{Augmentors, DependencyAnalysis, PosInExpr, Position}
-import org.keymaerax.parser.{Declaration, Parser}
+import org.keymaerax.parser.Declaration
 import org.keymaerax.pt.ProvableSig
 import org.slf4j.LoggerFactory
 
@@ -53,7 +54,7 @@ object InvariantProvers {
           val subst: USubst =
             if (bounds.length == 1) USubst(Seq(SubstitutionPair(DotTerm(), bounds.head)))
             else USubst(bounds.map(xi => { i = i + 1; SubstitutionPair(DotTerm(Real, Some(i)), xi) }))
-          val jj: Formula = Parser
+          val jj: Formula = GlobalState
             .parser
             .formulaParser("jjl(" + subst.subsDefsInput.map(sp => sp.what.prettyString).mkString(",") + ")")
           SearchAndRescueAgain(

keymaerax-core/src/main/scala/org/keymaerax/cli/KeYmaeraXProofChecker.scala

@@ -5,6 +5,7 @@
 
 package org.keymaerax.cli
 
+import org.keymaerax.GlobalState
 import org.keymaerax.bellerophon.IOListeners.PrintProgressListener
 import org.keymaerax.bellerophon.parser.BelleParser
 import org.keymaerax.bellerophon.{
@@ -19,7 +20,7 @@ import org.keymaerax.btactics.{TactixLibrary, ToolProvider}
 import org.keymaerax.core.{insist, False, Formula, PrettyPrinter, Sequent, USubst}
 import org.keymaerax.infrastruct.Augmentors._
 import org.keymaerax.lemma.{Lemma, LemmaDBFactory}
-import org.keymaerax.parser.{ArchiveParser, Declaration, KeYmaeraXExtendedLemmaParser, ParsedArchiveEntry, Parser}
+import org.keymaerax.parser.{ArchiveParser, Declaration, KeYmaeraXExtendedLemmaParser, ParsedArchiveEntry}
 import org.keymaerax.pt.{IsabelleConverter, ProvableSig, TermProvable}
 import org.keymaerax.tools.ToolEvidence
 import org.slf4j.{LoggerFactory, MarkerFactory}
@@ -101,7 +102,7 @@ object KeYmaeraXProofChecker {
           assert(witness.subgoals.isEmpty)
           val expected = inputSequent.exhaustiveSubst(USubst(defs.substs))
           // @note pretty-printing the result of parse ensures that the lemma states what's actually been proved.
-          insist(Parser.parser.formulaParser(PrettyPrinter.printer(input)) == input, "parse of print is identity")
+          insist(GlobalState.parser.formulaParser(PrettyPrinter.printer(input)) == input, "parse of print is identity")
           // @note assert(witness.isProved, "Successful proof certificate") already checked in line above
           insist(
             witness.proved == expected,

keymaerax-core/src/main/scala/org/keymaerax/cli/grade/AssessmentProver.scala

@@ -5,6 +5,7 @@
 
 package org.keymaerax.cli.grade
 
+import org.keymaerax.GlobalState
 import org.keymaerax.bellerophon.parser.BelleParser
 import org.keymaerax.bellerophon.{
   BelleExpr,
@@ -46,7 +47,6 @@ import org.keymaerax.parser.{
   KeYmaeraXArchivePrinter,
   ParseException,
   ParsedArchiveEntry,
-  Parser,
   PrettierPrintFormatProvider,
 }
 import org.keymaerax.pt.ProvableSig
@@ -478,7 +478,7 @@ object AssessmentProver {
             case Some(q) =>
               def runQE(question: String, answers: List[String]) = {
                 run(() => {
-                  val m = expand(question, answers, Parser.parser).asInstanceOf[Formula]
+                  val m = expand(question, answers, GlobalState.parser).asInstanceOf[Formula]
                   KeYmaeraXProofChecker(5.seconds, Declaration(Map.empty))(QE)(Sequent(IndexedSeq.empty, IndexedSeq(m)))
                 })
               }
@@ -541,7 +541,7 @@ object AssessmentProver {
             case _ => Right("Answer must be a KeYmaera X formula, but got " + have.longHintString)
           }
         case Modes.DI => args.get("question") match {
-            case Some(q) => Parser.parser.programParser(q) match {
+            case Some(q) => GlobalState.parser.programParser(q) match {
                 case ode: ODESystem => have match {
                     case h: ExpressionArtifact => h.expr match {
                         case hf: Formula => run(() => dICheck(ode, hf))
@@ -584,31 +584,31 @@ object AssessmentProver {
               }
           }
         case Modes.LOOP =>
-          val invArg = args.get("inv").map(Parser.parser.formulaParser)
+          val invArg = args.get("inv").map(GlobalState.parser.formulaParser)
           args.get("question") match {
             case Some(q) => have match {
                 case h: ExpressionArtifact => h.expr match {
                     case hf: Formula =>
                       var inv: Option[Formula] = None
-                      Parser
+                      GlobalState
                         .parser
                         .setAnnotationListener({
                           case (_: Loop, f) => inv = Some(f)
                           case _ =>
                         })
-                      val m = expand(q, hf.prettyString :: Nil, Parser.parser.formulaParser)
+                      val m = expand(q, hf.prettyString :: Nil, GlobalState.parser.formulaParser)
                       run(() => loopCheck(m, invArg.getOrElse(inv.getOrElse(hf))))
                     case _ => Right("Answer must be a KeYmaera X formula, but got " + have.longHintString)
                   }
                 case ListExpressionArtifact(h) =>
                   var inv: Option[Formula] = None
-                  Parser
+                  GlobalState
                     .parser
                     .setAnnotationListener({
                       case (_: Loop, f) => inv = Some(f)
                       case _ =>
                     })
-                  val m = expand(q, h.map(_.prettyString), Parser.parser.formulaParser)
+                  val m = expand(q, h.map(_.prettyString), GlobalState.parser.formulaParser)
                   run(() =>
                     loopCheck(
                       m,
@@ -750,7 +750,7 @@ object AssessmentProver {
           def runBelleProof(question: String, answers: List[String]): Either[ProvableSig, String] = {
             run(() => {
               val generator = new ConfigurableGenerator()
-              Parser
+              GlobalState
                 .parser
                 .setAnnotationListener((p: Program, inv: Formula) =>
                   generator.products +=
@@ -759,7 +759,7 @@ object AssessmentProver {
                         Invariant(inv, Some(InvariantHint.Annotation(tryHard = true)))).distinct)
                 )
               TactixInit.invSupplier = generator
-              val m = expand(question, answers, Parser.parser).asInstanceOf[Formula]
+              val m = expand(question, answers, GlobalState.parser).asInstanceOf[Formula]
               val t = expand(args("tactic"), answers, BelleParser)
               val p = prove(Sequent(IndexedSeq(), IndexedSeq(m)), t)
               // tactics that end in assert are checking whether or not the proof ends in a certain state; all others

keymaerax-core/src/main/scala/org/keymaerax/core/Proof.scala

@@ -39,7 +39,7 @@
  */
 package org.keymaerax.core
 
-import org.keymaerax.parser.Parser
+import org.keymaerax.GlobalState
 
 import java.security.MessageDigest
 import scala.annotation.nowarn
@@ -1025,7 +1025,7 @@ object Provable {
     if (separator < 0) throw new ProvableStorageException("syntactically ill-formed format", storedProvable)
     val storedChecksum = storedProvable.substring(separator + 2)
     val remainder = storedProvable.substring(0, separator)
-    (try { Parser.parser.storedInferenceParser(remainder) }
+    (try { GlobalState.parser.storedInferenceParser(remainder) }
     catch {
       case ex: Exception =>
         throw new ProvableStorageException("cannot be parsed: " + ex.toString, storedProvable).initCause(ex)

keymaerax-core/src/main/scala/org/keymaerax/parser/ArchiveParser.scala

@@ -5,6 +5,7 @@
 
 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
@@ -552,7 +553,8 @@ trait ArchiveParser extends (String => List[ParsedArchiveEntry]) {
       if (e.defs.decls.isEmpty) ArchiveParser.elaborate(e.copy(defs = ArchiveParser.declarationsOf(e.model)))
       else ArchiveParser.elaborate(e)
     )
-    result.foreach(_.annotations.foreach({ case (p: Program, f: Formula) => Parser.parser.annotationListener(p, f) }))
+    result
+      .foreach(_.annotations.foreach({ case (p: Program, f: Formula) => GlobalState.parser.annotationListener(p, f) }))
     result
   }
   protected def doParse(input: String, parseTactics: Boolean): List[ParsedArchiveEntry]

keymaerax-core/src/main/scala/org/keymaerax/parser/DLArchiveParser.scala

@@ -122,9 +122,9 @@ class DLArchiveParser(tacticParser: DLTacticParser) extends ArchiveParser {
 
   /** Parse a single archive entry without source. */
   def archiveEntryNoSource[$: P](shared: Option[Declaration]): P[ParsedArchiveEntry] = {
-    val al = Parser.parser.annotationListener
+    val al = expParser.annotationListener
     val annotations = ListBuffer.empty[(Program, Formula)]
-    Parser.parser.setAnnotationListener((p: Program, f: Formula) => annotations.append((p, f)))
+    expParser.setAnnotationListener((p: Program, f: Formula) => annotations.append((p, f)))
     try {
       (archiveStart ~~/ blank ~ (label ~ ":").? ~ string ~ metaInfo ~
         (for {
@@ -134,11 +134,9 @@ class DLArchiveParser(tacticParser: DLTacticParser) extends ArchiveParser {
               tacticProof(shared.map(_ ++ archiveDecls).getOrElse(archiveDecls)).rep
         } yield (archiveDecls, rest)) ~ metaInfo ~ ("End" ~ label.? ~ ".")).flatMapX({
         case (kind, label, name, meta, (decl, (prob, probString, tacs)), moremeta, endlabel) =>
-          Parser
-            .parser
-            .setAnnotationListener(
-              al
-            ) // @note done parsing annotations; reset annotation listeners because elaborate may access them
+          expParser.setAnnotationListener(
+            al
+          ) // @note done parsing annotations; reset annotation listeners because elaborate may access them
           if (endlabel.isDefined && endlabel != label)
             Fail.opaque("end label: " + endlabel + " is optional but should be the same as the start label: " + label)
           else {
@@ -165,7 +163,7 @@ class DLArchiveParser(tacticParser: DLTacticParser) extends ArchiveParser {
             Pass(result)
           }
       })
-    } finally { Parser.parser.setAnnotationListener(al) }
+    } finally { expParser.setAnnotationListener(al) }
   }
 
   /** Parses a single archive entry */

keymaerax-core/src/main/scala/org/keymaerax/parser/KeYmaeraXPrettyPrinter.scala

@@ -15,10 +15,11 @@
  */
 package org.keymaerax.parser
 
+import org.keymaerax.GlobalState
 import org.keymaerax.core._
-import org.keymaerax.parser.OpSpec.op
 import org.keymaerax.infrastruct.PosInExpr
 import org.keymaerax.infrastruct.PosInExpr.HereP
+import org.keymaerax.parser.OpSpec.op
 
 import scala.annotation.tailrec
 import scala.collection.immutable._
@@ -130,10 +131,9 @@ trait BasePrettyPrinter extends PrettyPrinter {
  */
 object FullPrettyPrinter extends BasePrettyPrinter {
 
-  import OpSpec.op
-  import OpSpec.statementSemicolon
+  import OpSpec.{op, statementSemicolon}
 
-  val parser: Parser = Parser.parser
+  val parser: Parser = GlobalState.parser
   val fullPrinter: (Expression => String) = this
 
   /** Pretty-print term to a string but without contract checking! */
@@ -258,10 +258,9 @@ object FullPrettyPrinter extends BasePrettyPrinter {
  */
 class KeYmaeraXPrinter extends BasePrettyPrinter {
 
-  import OpSpec.op
-  import OpSpec.statementSemicolon
+  import OpSpec.{op, statementSemicolon}
 
-  lazy val parser: Parser = Parser.parser
+  lazy val parser: Parser = GlobalState.parser
   val fullPrinter: (Expression => String) = FullPrettyPrinter
 
   /** Pretty-print term to a string but without contract checking! */

keymaerax-core/src/main/scala/org/keymaerax/parser/Parser.scala

@@ -14,8 +14,8 @@
  */
 package org.keymaerax.parser
 
-import org.keymaerax.Configuration
 import org.keymaerax.core._
+import org.keymaerax.{Configuration, GlobalState}
 
 import scala.util.Try
 
@@ -116,7 +116,6 @@ trait Parser extends (String => Expression) {
 }
 
 object Parser extends (String => Expression) {
-  val parser: Parser = new DLParser
 
   /**
    * `true` has unary negation `-` bind weakly like binary subtraction. `false` has unary negation `-` bind strong just
@@ -131,7 +130,7 @@ object Parser extends (String => Expression) {
   val numNeg: Boolean = OpSpec.negativeNumber
 
   /** Parses `input`. */
-  override def apply(input: String): Expression = parser(input)
+  override def apply(input: String): Expression = GlobalState.parser(input)
 
   /** Parses a comma-separated list of expressions. */
   def parseExpressionList(s: String): List[Expression] = {

keymaerax-core/src/main/scala/org/keymaerax/parser/SequentParser.scala

@@ -5,6 +5,7 @@
 
 package org.keymaerax.parser
 
+import org.keymaerax.GlobalState
 import org.keymaerax.core.{Formula, Sequent}
 
 /** Parses sequents of the form ```ante_1, ante_2, ..., ante_n ==> succ_1, ..., succ_n```. */
@@ -19,10 +20,10 @@ object SequentParser {
       .split(FML_SPLITTER)
       .foldLeft[(List[Formula], String)](List.empty, "")({ case ((fmls, acc), next) =>
         val fmlCandidate = acc + (if (acc.nonEmpty) "," else "") + next
-        try { (fmls :+ Parser.parser.formulaParser(fmlCandidate), "") }
+        try { (fmls :+ GlobalState.parser.formulaParser(fmlCandidate), "") }
         catch { case _: ParseException => (fmls, fmlCandidate) }
       })
-    if (unparseable.nonEmpty) List(Parser.parser.formulaParser(unparseable)) // @note will throw ParseException
+    if (unparseable.nonEmpty) List(GlobalState.parser.formulaParser(unparseable)) // @note will throw ParseException
     else fmls
   }