UL support

apalache-mc · Oct 12, 2023 · 72aaea0 · 72aaea0
1 parent c7417b8
commit 72aaea0
Show file tree

Hide file tree

Showing 5 changed files with 78 additions and 39 deletions.
diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/config/TlcConfig.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/config/TlcConfig.scala
@@ -1,9 +1,9 @@
 package at.forsyte.apalache.infra.tlc.config
 
 import at.forsyte.apalache.infra.tlc.config.ConfigModelValue.STR_PREFIX
-import at.forsyte.apalache.tla.lir.convenience.tla
-import at.forsyte.apalache.tla.lir.{BoolT1, IntT1, SetT1, StrT1, TlaEx, Typed, VarT1}
-import at.forsyte.apalache.tla.lir.TypedPredefs._
+import at.forsyte.apalache.tla.lir.{TlaType1, Typed, VarT1}
+import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
+import at.forsyte.apalache.tla.types.{tla, ModelValueHandler}
 
 import scala.util.parsing.input.NoPosition
 
@@ -46,7 +46,7 @@ sealed abstract class ConfigConstExpr {
    * @return
    *   the TLA IR expression that represents the parsed constant expression
    */
-  def toTlaEx: TlaEx
+  def toTla: TBuilderInstruction
 }
 
 object ConfigModelValue {
@@ -64,11 +64,11 @@ object ConfigModelValue {
  *   the name of a model value
  */
 case class ConfigModelValue(name: String) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = {
+  override def toTla: TBuilderInstruction = {
     // currently, we use the type Str for all model values.
     // In the future, we might want to distinguish between different uninterpreted types.
     // See https://github.com/informalsystems/apalache/issues/570
-    tla.str(STR_PREFIX + name).typed(StrT1)
+    tla.str(STR_PREFIX + name)
   }
 }
 
@@ -79,7 +79,7 @@ case class ConfigModelValue(name: String) extends ConfigConstExpr {
  *   an integer as BigInt
  */
 case class ConfigIntValue(num: BigInt) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.bigInt(num).typed(IntT1)
+  override def toTla: TBuilderInstruction = tla.int(num)
 }
 
 /**
@@ -89,7 +89,7 @@ case class ConfigIntValue(num: BigInt) extends ConfigConstExpr {
  *   a boolean
  */
 case class ConfigBoolValue(b: Boolean) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.bool(b).typed(BoolT1)
+  override def toTla: TBuilderInstruction = tla.bool(b)
 }
 
 /**
@@ -99,7 +99,13 @@ case class ConfigBoolValue(b: Boolean) extends ConfigConstExpr {
  *   a string
  */
 case class ConfigStrValue(str: String) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = tla.str(str).typed(StrT1)
+  override def toTla: TBuilderInstruction = {
+    ModelValueHandler.typeAndIndex(str) match {
+      case None                => tla.str(str)
+      case Some((constT, idx)) => tla.const(idx, constT)
+    }
+
+  }
 }
 
 /**
@@ -109,18 +115,18 @@ case class ConfigStrValue(str: String) extends ConfigConstExpr {
  *   the set elements, which are constant expression themselves.
  */
 case class ConfigSetValue(elems: ConfigConstExpr*) extends ConfigConstExpr {
-  override def toTlaEx: TlaEx = {
-    val setElems = elems.map(_.toTlaEx)
+  override def toTla: TBuilderInstruction = {
+    val setElems = elems.map(_.toTla)
     if (setElems.isEmpty) {
       // the element type is uknown, introduce a polymorphic type Set(a)
-      tla.enumSet().typed(SetT1(VarT1(0)))
+      tla.emptySet(VarT1(0))
     } else {
       // the element type should be unique
-      val headType = setElems.head.typeTag.asTlaType1()
+      val headType = TlaType1.fromTypeTag(setElems.head.typeTag)
       if (setElems.tail.exists(_.typeTag != Typed(headType))) {
         throw new TlcConfigParseError("Set elements have different types: " + setElems.mkString(", "), NoPosition)
       } else {
-        tla.enumSet(setElems: _*).typed(SetT1(headType))
+        tla.enumSet(setElems: _*)
       }
     }
   }

diff --git a/test/tla/Test2750.cfg b/test/tla/Test2750.cfg
@@ -0,0 +1,8 @@
+INIT
+Init
+NEXT
+Next
+INVARIANT
+Inv
+CONSTANT
+C = "1_OF_A"
diff --git a/test/tla/Test2750.tla b/test/tla/Test2750.tla
@@ -0,0 +1,19 @@
+----------------------- MODULE Test2750 -----------------------------
+VARIABLES
+    \* @type: A;
+    x
+
+CONSTANT
+    \* @type: A;
+    C
+
+
+Init ==
+    /\ x = C
+
+Next ==
+    UNCHANGED x
+
+Inv == TRUE
+
+===============================================================================
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
@@ -2324,6 +2324,13 @@ $ apalache-mc check --config=Bug2750.cfg Bug2750.tla | sed 's/[IEW]@.*//'
 EXITCODE: ERROR (255)
 ```
 
+### check Test2750.tla
+
+```sh
+$ apalache-mc check --config=Test2750.cfg Test2750.tla | sed 's/[IEW]@.*//'
+...
+EXITCODE: OK
+```
 
 ### check profiling
 

diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/TlcConfigImporter.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/TlcConfigImporter.scala
@@ -1,10 +1,10 @@
 package at.forsyte.apalache.tla.pp
 
 import at.forsyte.apalache.infra.tlc.config._
-import at.forsyte.apalache.tla.lir.TypedPredefs._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.lir.convenience._
 import at.forsyte.apalache.tla.lir.transformations.TlaModuleTransformation
+import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
+import at.forsyte.apalache.tla.types.tla
 import com.typesafe.scalalogging.LazyLogging
 
 /**
@@ -17,28 +17,26 @@ import com.typesafe.scalalogging.LazyLogging
  *   Andrey Kuprianov
  */
 class TlcConfigImporter(config: TlcConfig) extends TlaModuleTransformation with LazyLogging {
-  private val boolOperT = OperT1(Seq(), BoolT1)
+  OperT1(Seq(), BoolT1)
 
-  private def mkBoolName(name: String): TlaEx = {
-    tla.name(name).typed(BoolT1)
+  private def mkBoolName(name: String): TBuilderInstruction = {
+    tla.name(name, BoolT1)
   }
 
   override def apply(mod: TlaModule): TlaModule = {
 
     val assignments = config.constAssignments.map { case (param, value) =>
-      val valueEx = value.toTlaEx
-      val operT = OperT1(Seq(), valueEx.typeTag.asTlaType1())
-      tla.declOp(ConstAndDefRewriter.OVERRIDE_PREFIX + param, value.toTlaEx).as(operT)
+      val valueEx = value.toTla
+      tla.decl(ConstAndDefRewriter.OVERRIDE_PREFIX + param, valueEx)
     }
     val replacements = config.constReplacements.map { case (param, value) =>
       mod.declarations.find(_.name == value) match {
         case Some(d: TlaOperDecl) =>
           if (d.formalParams.isEmpty) {
-            val tt = d.typeTag.asTlaType1()
+            val tt = TlaType1.fromTypeTag(d.typeTag)
             assert(tt.isInstanceOf[OperT1])
-            val operT = tt.asInstanceOf[OperT1]
-            val application = tla.appOp(tla.name(value).typed(operT)).typed(operT.res)
-            tla.declOp(ConstAndDefRewriter.OVERRIDE_PREFIX + param, application).as(operT)
+            val application = tla.appOp(tla.name(value, tt))
+            tla.decl(ConstAndDefRewriter.OVERRIDE_PREFIX + param, application)
           } else {
             val nparams = d.formalParams.size
             throw new TLCConfigurationError(
@@ -47,42 +45,43 @@ class TlcConfigImporter(config: TlcConfig) extends TlaModuleTransformation with
 
         case Some(d) =>
           // This is a branch from the old untyped encoding. Does it make sense in the type encoding?
-          val tt = d.typeTag.asTlaType1()
-          tla.declOp(ConstAndDefRewriter.OVERRIDE_PREFIX + param, tla.name(value).typed(tt)).as(OperT1(Seq(), tt))
+          val tt = TlaType1.fromTypeTag(d.typeTag)
+          tla.decl(ConstAndDefRewriter.OVERRIDE_PREFIX + param, tla.name(value, tt))
 
         case None =>
           throw new TLCConfigurationError(s"Met a replacement $param <- $value, but $value is not found")
       }
     }
     val stateConstraints = config.stateConstraints.zipWithIndex.map { case (value, index) =>
-      tla.declOp(TlcConfigImporter.STATE_PREFIX + index, mkBoolName(value)).as(boolOperT)
+      tla.decl(TlcConfigImporter.STATE_PREFIX + index, mkBoolName(value))
     }
     val actionConstraints = config.actionConstraints.zipWithIndex.map { case (value, index) =>
-      tla.declOp(TlcConfigImporter.ACTION_PREFIX + index, mkBoolName(value)).as(boolOperT)
+      tla.decl(TlcConfigImporter.ACTION_PREFIX + index, mkBoolName(value))
     }
     val invariants = config.invariants.zipWithIndex.map { case (value, index) =>
-      tla.declOp(TlcConfigImporter.INVARIANT_PREFIX + index, mkBoolName(value)).as(boolOperT)
+      tla.decl(TlcConfigImporter.INVARIANT_PREFIX + index, mkBoolName(value))
     }
     val temporalProps = config.temporalProps.zipWithIndex.map { case (value, index) =>
-      tla.declOp(TlcConfigImporter.TEMPORAL_PREFIX + index, mkBoolName(value)).as(boolOperT)
+      tla.decl(TlcConfigImporter.TEMPORAL_PREFIX + index, mkBoolName(value))
     }
     val behaviorSpec = config.behaviorSpec match {
       case InitNextSpec(init, next) =>
         List(
-            tla.declOp(TlcConfigImporter.INIT, mkBoolName(init)).as(boolOperT),
-            tla.declOp(TlcConfigImporter.NEXT, mkBoolName(next)).as(boolOperT),
+            tla.decl(TlcConfigImporter.INIT, mkBoolName(init)),
+            tla.decl(TlcConfigImporter.NEXT, mkBoolName(next)),
         )
 
       case TemporalSpec(name) =>
-        List(tla.declOp(TlcConfigImporter.SPEC, mkBoolName(name)).as(boolOperT))
+        List(tla.decl(TlcConfigImporter.SPEC, mkBoolName(name)))
 
       case NullSpec() =>
         throw new TLCConfigurationError("Neither INIT and NEXT, nor SPECIFICATION found in the TLC configuration file")
     }
-    new TlaModule(mod.name,
-        mod.declarations
-          ++ assignments ++ replacements ++ stateConstraints ++ actionConstraints
-          ++ invariants ++ temporalProps ++ behaviorSpec)
+
+    val extendedDecls: Iterable[TlaDecl] =
+      (assignments ++ replacements ++ stateConstraints ++ actionConstraints ++ invariants ++ temporalProps ++ behaviorSpec)
+        .map(_.build)
+    TlaModule(mod.name, mod.declarations ++ extendedDecls)
   }
 }