Replaces scope-safe builder usage in Apalache internals with scop-uns…

…afe builder usage (#2935) * separate unsafe builder * tests * Update tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala Co-authored-by: Igor Konnov <[email protected]> * features --------- Co-authored-by: Igor Konnov <[email protected]>
apalache-mc · Aug 21, 2024 · 5a40de2 · 5a40de2
1 parent b287556
commit 5a40de2
Show file tree

Hide file tree

Showing 130 changed files with 565 additions and 427 deletions.
diff --git a/.unreleased/features/unsafe.md b/.unreleased/features/unsafe.md
@@ -0,0 +1 @@
+Added scope-unsafe builder.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala
@@ -8,8 +8,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps}
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import scalaz.unused
 
 import scala.collection.immutable.SortedMap
@@ -41,7 +40,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
    * @return
    *   tla.eql(left, right), provided that left and right can be compared
    */
-  def safeEq(left: ArenaCell, right: ArenaCell): TBuilderInstruction = {
+  def safeEq(left: ArenaCell, right: ArenaCell): BuilderT = {
     if (left == right) {
       tla.bool(true) // this is just true
     } else {
@@ -319,14 +318,14 @@ class LazyEquality(rewriter: SymbStateRewriter)
         // inAndEq checks if lelem is in right
         val inAndEqList = rightElems.map(inAndEq(rewriter, _, lelem, right, lazyEq = true))
         // There are plenty of valid subformulas. Simplify!
-        tla.or(inAndEqList: _*).map(simplifier.simplifyShallow)
+        simplifier.applySimplifyShallowToBuilderEx(tla.or(inAndEqList: _*))
       }
 
       def notInOrExists(lelem: ArenaCell) = {
         val notInOrExists =
-          tla
-            .or(tla.not(tla.selectInSet(lelem.toBuilder, left.toBuilder)), exists(lelem))
-            .map(simplifier.simplifyShallow)
+          simplifier.applySimplifyShallowToBuilderEx(
+              tla.or(tla.not(tla.selectInSet(lelem.toBuilder, left.toBuilder)), exists(lelem))
+          )
 
         if (simplifier.isBoolConst(notInOrExists)) {
           notInOrExists // just return the constant
@@ -340,7 +339,8 @@ class LazyEquality(rewriter: SymbStateRewriter)
         }
       }
 
-      val forEachNotInOrExists = tla.and(leftElems.map(notInOrExists): _*).map(simplifier.simplifyShallow)
+      val forEachNotInOrExists =
+        simplifier.applySimplifyShallowToBuilderEx(tla.and(leftElems.map(notInOrExists): _*))
       newState = newState.updateArena(_.appendCell(BoolT1))
       val pred = newState.arena.topCell
       rewriter.solverContext.assertGroundExpr(tla.eql(pred.toBuilder, forEachNotInOrExists))
@@ -471,7 +471,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
     val commonKeys = leftType.fieldTypes.keySet.intersect(rightType.fieldTypes.keySet)
     var newState = state
 
-    def keyEq(key: String): TBuilderInstruction = {
+    def keyEq(key: String): BuilderT = {
       val leftIndex = leftType.fieldTypes.keySet.toList.indexOf(key)
       val rightIndex = rightType.fieldTypes.keySet.toList.indexOf(key)
 
@@ -522,7 +522,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
       leftRec: ArenaCell,
       rightRec: ArenaCell): SymbState = {
     var nextState = state
-    def fieldsEq(name: String): TBuilderInstruction = {
+    def fieldsEq(name: String): BuilderT = {
       val leftField = recordOps.getField(nextState.arena, leftRec, name)
       val rightField = recordOps.getField(nextState.arena, rightRec, name)
       // The field values may be non-basic expressions. Use lazy equality over them too.
@@ -545,7 +545,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
     val leftTag = recordOps.getVariantTag(nextState.arena, leftVar)
     val rightTag = recordOps.getVariantTag(nextState.arena, rightVar)
 
-    def valuesEq(tagName: String): TBuilderInstruction = {
+    def valuesEq(tagName: String): BuilderT = {
       val leftValue = recordOps.getUnsafeVariantValue(nextState.arena, leftVar, tagName)
       val rightValue = recordOps.getUnsafeVariantValue(nextState.arena, rightVar, tagName)
       // The field values may be non-basic expressions. Use lazy equality over them too.
@@ -569,7 +569,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
   private def mkTupleEq(state: SymbState, left: ArenaCell, right: ArenaCell): SymbState = {
     var newState = state
 
-    def elemEq(lelem: ArenaCell, relem: ArenaCell): TBuilderInstruction = {
+    def elemEq(lelem: ArenaCell, relem: ArenaCell): BuilderT = {
       newState = cacheOneEqConstraint(newState, lelem, relem)
       safeEq(lelem, relem)
     }
@@ -602,7 +602,7 @@ class LazyEquality(rewriter: SymbStateRewriter)
     val len1Ex = len1.toBuilder
     val len2Ex = len2.toBuilder
 
-    def eqPairwise(indexBase1: Int, cells: (ArenaCell, ArenaCell)): TBuilderInstruction = {
+    def eqPairwise(indexBase1: Int, cells: (ArenaCell, ArenaCell)): BuilderT = {
       nextState = cacheOneEqConstraint(nextState, cells._1, cells._2)
       // Either (1) one of the lengths is below the index, or (2) the elements are equal.
       // The case (1) is compensated with the constraint sizesEq below.

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SeqModelChecker.scala
@@ -10,8 +10,8 @@ import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaOper}
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.transformations.standard.ReplaceFixed
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.typecomp._
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import com.typesafe.scalalogging.LazyLogging
 
 import scala.util.Random
@@ -442,7 +442,7 @@ class SeqModelChecker[ExecutorContextT](
     val stateType = RecT1(checkerInput.rootModule.varDeclarations.map(d => d.name -> d.typeTag.asTlaType1()): _*)
 
     // convert a variable binding to a record
-    def mkRecord(b: Binding): TBuilderInstruction = {
+    def mkRecord(b: Binding): BuilderT = {
       val ctorArgs = b.toMap.map { case (key, value) =>
         (key, tla.name(value.toString, stateType.fieldTypes(key)))
       }

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala
@@ -8,8 +8,8 @@ import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir.values._
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
+import at.forsyte.apalache.tla.typecomp._
 import com.typesafe.scalalogging.LazyLogging
 
 import scala.collection.immutable.SortedMap
@@ -24,16 +24,21 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
   private val protoSeqOps = new ProtoSeqOps(rewriter)
   private val recordOps = new RecordAndVariantOps(rewriter)
 
+  def evalGroundExprForBuilderEx(ex: TBuilderInstruction): TBuilderInstruction =
+    ex.map(solverContext.evalGroundExpr) // when using TBuilderInstruction
+  def evalGroundExprForBuilderEx(ex: TlaEx): TlaEx =
+    solverContext.evalGroundExpr(ex) // when using TlaEx
+
   def decodeStateVariables(state: SymbState): Map[String, TlaEx] = {
     state.binding.toMap.map(p => (p._1, reverseMapVar(decodeCellToTlaEx(state.arena, p._2), p._1, p._2)))
   }
 
-  def decodeCellToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): TBuilderInstruction = cell.cellType match {
+  def decodeCellToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): BuilderT = cell.cellType match {
     case CellTFrom(BoolT1) =>
-      cell.toBuilder.map(solverContext.evalGroundExpr)
+      evalGroundExprForBuilderEx(cell.toBuilder)
 
     case CellTFrom(IntT1) =>
-      cell.toBuilder.map(solverContext.evalGroundExpr)
+      evalGroundExprForBuilderEx(cell.toBuilder)
 
     case ct @ CellTFrom(StrT1 | ConstT1(_)) =>
       // First, attempt to check the cache
@@ -128,7 +133,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
       throw new RewriterException("Don't know how to decode the cell %s of type %s".format(cell, cell.cellType), NullEx)
   }
 
-  private def decodeOldRecordToTlaEx(arena: PureArenaAdapter, cell: ArenaCell, recordT: RecT1): TBuilderInstruction = {
+  private def decodeOldRecordToTlaEx(arena: PureArenaAdapter, cell: ArenaCell, recordT: RecT1): BuilderT = {
     def exToStr(ex: TlaEx): TlaStr = ex match {
       case ValEx(s @ TlaStr(_)) => s
       case _                    => throw new RewriterException("Expected a string, found: " + ex, ex)
@@ -141,7 +146,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     val fieldValues = arena.getHas(cell)
     val keyList = recordT.fieldTypes.keySet.toList
 
-    def eachField(es: List[TBuilderInstruction], key: String): List[TBuilderInstruction] = {
+    def eachField(es: List[BuilderT], key: String): List[BuilderT] = {
       if (!dom.contains(TlaStr(key))) {
         es // skip
       } else {
@@ -151,7 +156,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
       }
     }
 
-    val keysAndValues = keyList.reverse.foldLeft(List.empty[TBuilderInstruction])(eachField)
+    val keysAndValues = keyList.reverse.foldLeft(List.empty[BuilderT])(eachField)
     if (keysAndValues.nonEmpty) {
       tla.recMixed(keysAndValues: _*)
     } else {
@@ -165,7 +170,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
   private def decodeRecordToTlaEx(
       arena: PureArenaAdapter,
       cell: ArenaCell,
-      fieldTypes: SortedMap[String, TlaType1]): TBuilderInstruction =
+      fieldTypes: SortedMap[String, TlaType1]): BuilderT =
     tla.rowRec(None,
         fieldTypes.keySet.toList.map { k =>
           k -> decodeCellToTlaEx(arena, recordOps.getField(arena, cell, k))
@@ -174,7 +179,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
   private def decodeVariantToTlaEx(
       arena: PureArenaAdapter,
       cell: ArenaCell,
-      options: SortedMap[String, TlaType1]): TBuilderInstruction = {
+      options: SortedMap[String, TlaType1]): BuilderT = {
     val tagName = decodeCellToTlaEx(arena, recordOps.getVariantTag(arena, cell)).build match {
       case ValEx(TlaStr(name)) => name
 
@@ -184,7 +189,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     tla.variant(tagName, value, VariantT1(RowT1(options, None)))
   }
 
-  private def decodeFunToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): TBuilderInstruction = {
+  private def decodeFunToTlaEx(arena: PureArenaAdapter, cell: ArenaCell): BuilderT = {
     // a function is represented with the relation {(x, f[x]) : x \in S}
     val relation = arena.getCdm(cell)
 
@@ -195,7 +200,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
           // given this, we query the solver about the function's domain instead
           val domain = arena.getDom(cell)
 
-          def inDom(elem: ArenaCell): TBuilderInstruction = {
+          def inDom(elem: ArenaCell): BuilderT = {
             val elemEx = elem.toBuilder
             val domEx = domain.toBuilder
             tla.selectInSet(elemEx, domEx)
@@ -257,7 +262,7 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     }
   }
 
-  private def findCellInSet(cells: Seq[ArenaCell], ex: TBuilderInstruction): Option[ArenaCell] = {
+  private def findCellInSet(cells: Seq[ArenaCell], ex: BuilderT): Option[ArenaCell] = {
     def isEq(c: ArenaCell): Boolean = {
       val query = tla.and(tla.eql(c.toBuilder, ex))
       tla.bool(true).build == solverContext.evalGroundExpr(query)

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PtrUtil.scala
@@ -1,7 +1,7 @@
 package at.forsyte.apalache.tla.bmcmt.arena
 
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr, SmtExprElemPtr}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Contains miscellaneous methods related to [[ElemPtr]]s.

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/arena/PureArenaAdapter.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr, PureAren
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Declares the same interface as [[Arena]]s (with the exception of [[ElemPtr]] usage).

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/EqCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.caches.EqCache._
 import at.forsyte.apalache.tla.bmcmt.rewriter.Recoverable
 import at.forsyte.apalache.tla.bmcmt.{ArenaCell, StackableContext}
 import at.forsyte.apalache.tla.lir.TlaEx
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 import scala.collection.mutable
 

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntRangeCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, FixedElemPtr}
 import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir.{IntT1, SetT1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Cache tuple domains as well as ranges a..b.

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/IntValueCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.ArenaCell
 import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir.IntT1
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * A cache for integer constants that maps an integer to an integer constant in SMT.

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala
@@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.bmcmt.types.CellTFrom
 import at.forsyte.apalache.tla.lir.{ConstT1, StrT1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * A cache for model values that are translated as uninterpreted constants, with a unique sort per uniterpreted type.

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/RecordDomainCache.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, ElemPtr, SmtExprElemPtr}
 import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter
 import at.forsyte.apalache.tla.bmcmt.smt.SolverContext
 import at.forsyte.apalache.tla.lir.{SetT1, StrT1}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 import scala.collection.immutable.SortedSet
 

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/CardinalityConstRule.scala
@@ -6,7 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick
 import at.forsyte.apalache.tla.lir.oper.{ApalacheOper, TlaArithOper, TlaFiniteSetOper}
 import at.forsyte.apalache.tla.lir.values.TlaInt
 import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, ValEx}
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Optimization for Cardinality(S) >= k, where k is constant. See [docs/smt/Cardinality.md].

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala
@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewriting DOMAIN f, that is, translating the domain of a function, record, tuple, or sequence.

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FoldSetRule.scala
@@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.lir.oper.ApalacheOper
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming
 import at.forsyte.apalache.tla.pp.Inliner
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Rewriting rule for FoldSet. Similar to Cardinality, we need to consider element set presence and multiplicity.

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRule.scala
@@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, ProtoSeqOps, RecordAndVariantOps}
 import at.forsyte.apalache.tla.bmcmt.types._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
 import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr}
 import at.forsyte.apalache.tla.lir._

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.types._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 import at.forsyte.apalache.tla.lir.{BoolT1, FunT1, RecT1, SetT1, TlaEx}
 
 /**

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRule.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.infra.passes.options.SMTEncoding
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * The new implementation of a function constructor that encodes a function f = [x \in S |-> e] the classical way: f =

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunCtorRuleWithArrays.scala
@@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._
 import at.forsyte.apalache.tla.bmcmt.types._
 import at.forsyte.apalache.tla.lir._
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla}
 
 /**
  * Encodes the construction of a function f = [x \in S |-> e]. We carry the domain set in a separate set cell. The

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRule.scala
@@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.{ProtoSeqOps, RecordAndVariantOps
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaFunOper
 import at.forsyte.apalache.tla.lir.values.{TlaInt, TlaStr}
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 import scalaz.unused
 
 /**
@@ -66,7 +65,7 @@ class FunExceptRule(rewriter: SymbStateRewriter) extends RewritingRule {
       indexCell: ArenaCell,
       valueCell: ArenaCell): SymbState = {
     // rewrite tuples <<j_i, e_i>> to cells
-    def mkPair(indexCell: ArenaCell, resCell: ArenaCell): TBuilderInstruction =
+    def mkPair(indexCell: ArenaCell, resCell: ArenaCell): BuilderT =
       tla.tuple(indexCell.toBuilder, resCell.toBuilder)
 
     var nextState = rewriter.rewriteUntilDone(state.setRex(mkPair(indexCell, valueCell)))

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunExceptRuleWithArrays.scala
@@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules
 import at.forsyte.apalache.tla.bmcmt._
 import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil
 import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps.constrainRelationArgs
-import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.tla
+import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT}
 
 /**
  * Rewriting EXCEPT for functions, tuples, and records.
@@ -31,7 +30,7 @@ class FunExceptRuleWithArrays(rewriter: SymbStateRewriter) extends FunExceptRule
     nextState = nextState.updateArena(_.setDom(resultFunCell, domainCell))
 
     // Make pair <arg,res> to propagate metadata
-    def mkPair(indexCell: ArenaCell, resCell: ArenaCell): TBuilderInstruction =
+    def mkPair(indexCell: ArenaCell, resCell: ArenaCell): BuilderT =
       tla.tuple(indexCell.toBuilder, resCell.toBuilder)
 
     nextState = rewriter.rewriteUntilDone(nextState.setRex(mkPair(indexCell, valueCell)))