Upgrade dependencies to Guice 7 (#2781)

* Upgrade to guice 6

* Upgrade to guice 7

Guice 7 dropped support for `javax.inject.*`
in favor of `jakarta.inject.*`:
https://github.com/google/guice/wiki/Guice700#jee-jakarta-transition

Since we do not want to pull in Java EE, we're
switching to the properietary `com.google` package.

mod-infra/src/main/scala/at/forsyte/apalache/infra/DefaultExceptionAdapter.scala

@@ -1,6 +1,6 @@
 package at.forsyte.apalache.infra
 
-import javax.inject.Singleton
+import com.google.inject.Singleton
 
 /**
  * The default adapter does nothing.

project/Dependencies.scala

@@ -22,7 +22,7 @@ object Dependencies {
       "commons-beanutils" % "commons-beanutils" % "1.9.4" // Apparently an untracked dependency of commonsConfiguration2
     val commonsConfiguration2 = "org.apache.commons" % "commons-configuration2" % "2.9.0"
     val commonsIo = "commons-io" % "commons-io" % "2.15.0"
-    val guice = "com.google.inject" % "guice" % "5.1.0"
+    val guice = "com.google.inject" % "guice" % "7.0.0"
     val kiama = "org.bitbucket.inkytonik.kiama" %% "kiama" % "2.5.1"
     val logbackClassic = "ch.qos.logback" % "logback-classic" % logbackVersion
     val logbackCore = "ch.qos.logback" % "logback-core" % logbackVersion

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala

@@ -14,10 +14,9 @@ import at.forsyte.apalache.tla.lir.{
 }
 import at.forsyte.apalache.tla.pp.{IrrecoverablePreprocessingError, NotInKeraError, OverridingError, TlaInputError}
 import at.forsyte.apalache.tla.typecheck.TypingInputException
+import com.google.inject.{Inject, Singleton}
 import com.typesafe.scalalogging.LazyLogging
 
-import javax.inject.{Inject, Singleton}
-
 /**
  * The adapter for all exceptions that can be produced when running the model checker.
  *

tla-io/src/main/scala/at/forsyte/apalache/tla/imp/ParserExceptionAdapter.scala

@@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.imp
 import at.forsyte.apalache.infra.ExceptionAdapter
 import com.typesafe.scalalogging.LazyLogging
 
-import javax.inject.{Inject, Singleton}
+import com.google.inject.{Inject, Singleton}
 
 // TODO: This can be removed in theory, but our current architecture requires executable passes
 // include a injectable instance of `ExceptionAdapater`

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Desugarer.scala

@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.lir.oper._
 import at.forsyte.apalache.tla.lir.transformations.{TlaExTransformation, TransformationTracker}
 import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr}
 
-import javax.inject.Singleton
+import com.google.inject.Singleton
 import at.forsyte.apalache.tla.typecomp.ScopedBuilder
 
 /**

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala

@@ -8,8 +8,7 @@ import at.forsyte.apalache.tla.lir.transformations.{LanguageWatchdog, TlaExTrans
 import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr}
 import TypedPredefs._
 
-import javax.inject.Singleton
-import scala.math.BigInt
+import com.google.inject.Singleton
 
 /**
  * <p>An optimizer of KerA+ expressions.</p>

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Keramelizer.scala

@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.lir.oper._
 import at.forsyte.apalache.tla.lir.transformations.standard.FlatLanguagePred
 import at.forsyte.apalache.tla.lir.transformations.{LanguageWatchdog, TlaExTransformation, TransformationTracker}
 
-import javax.inject.Singleton
+import com.google.inject.Singleton
 
 /**
  * <p>A simplifier from TLA+ to KerA+. This transformation assumes that all operator definitions and internal

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/Normalizer.scala

@@ -8,7 +8,7 @@ import at.forsyte.apalache.tla.lir.transformations.{LanguageWatchdog, TlaExTrans
 import at.forsyte.apalache.tla.lir.values.TlaBool
 import at.forsyte.apalache.tla.lir._
 
-import javax.inject.Singleton
+import com.google.inject.Singleton
 
 /**
  * This transformation turns subexpressions of a TLA+ expression into negated normal form.

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/TypeSubstitutor.scala

@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.transformations.{TlaExTransformation, TransformationTracker}
 import at.forsyte.apalache.tla.types.Substitution
 
-import javax.inject.Singleton
+import com.google.inject.Singleton
 
 /**
  * <p>Apply a type substitution to the types of a subexpression.</p>

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/temporal/LoopEncoder.scala

@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.pp.temporal
 
 import at.forsyte.apalache.tla.lir._
 
-import javax.inject.Singleton
+import com.google.inject.Singleton
 import com.typesafe.scalalogging.LazyLogging
 import at.forsyte.apalache.tla.typecomp._
 import at.forsyte.apalache.tla.pp.temporal.DeclUtils._

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/temporal/TableauEncoder.scala

@@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.pp.temporal
 
 import at.forsyte.apalache.tla.lir._
 
-import javax.inject.Singleton
+import com.google.inject.Singleton
 import com.typesafe.scalalogging.LazyLogging
 import scalaz.Scalaz.{init => _}
 import at.forsyte.apalache.tla.pp.UniqueNameGenerator

tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/IncrementalRenaming.scala

@@ -6,7 +6,7 @@ import at.forsyte.apalache.tla.lir.transformations.{
   TlaDeclTransformation, TlaExTransformation, TlaModuleTransformation, TransformationTracker,
 }
 
-import javax.inject.{Inject, Singleton}
+import com.google.inject.{Inject, Singleton}
 import scala.collection.immutable.HashMap
 
 // Igor @ 07.11.2019: refactoring needed