From 5a40de25e4ebc4980bc725ac45b0fd28f0096359 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Wed, 21 Aug 2024 10:39:20 +0200 Subject: [PATCH] Replaces scope-safe builder usage in Apalache internals with scop-unsafe builder usage (#2935) * separate unsafe builder * tests * Update tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala Co-authored-by: Igor Konnov * features --------- Co-authored-by: Igor Konnov --- .unreleased/features/unsafe.md | 1 + .../apalache/tla/bmcmt/LazyEquality.scala | 26 ++-- .../apalache/tla/bmcmt/SeqModelChecker.scala | 6 +- .../apalache/tla/bmcmt/SymbStateDecoder.scala | 31 +++-- .../apalache/tla/bmcmt/arena/PtrUtil.scala | 2 +- .../tla/bmcmt/arena/PureArenaAdapter.scala | 2 +- .../apalache/tla/bmcmt/caches/EqCache.scala | 2 +- .../tla/bmcmt/caches/IntRangeCache.scala | 2 +- .../tla/bmcmt/caches/IntValueCache.scala | 2 +- .../tla/bmcmt/caches/ModelValueCache.scala | 2 +- .../tla/bmcmt/caches/RecordDomainCache.scala | 2 +- .../bmcmt/rules/CardinalityConstRule.scala | 2 +- .../apalache/tla/bmcmt/rules/DomainRule.scala | 2 +- .../tla/bmcmt/rules/FoldSetRule.scala | 2 +- .../apalache/tla/bmcmt/rules/FunAppRule.scala | 2 +- .../bmcmt/rules/FunAppRuleWithArrays.scala | 2 +- .../tla/bmcmt/rules/FunCtorRule.scala | 2 +- .../bmcmt/rules/FunCtorRuleWithArrays.scala | 2 +- .../tla/bmcmt/rules/FunExceptRule.scala | 5 +- .../bmcmt/rules/FunExceptRuleWithArrays.scala | 5 +- .../tla/bmcmt/rules/IfThenElseRule.scala | 7 +- .../apalache/tla/bmcmt/rules/QuantRule.scala | 10 +- .../tla/bmcmt/rules/RecCtorRule.scala | 2 +- .../apalache/tla/bmcmt/rules/RepeatRule.scala | 2 +- .../apalache/tla/bmcmt/rules/SeqOpsRule.scala | 2 +- .../tla/bmcmt/rules/SetAsFunRule.scala | 5 +- .../tla/bmcmt/rules/SetCtorRule.scala | 2 +- .../apalache/tla/bmcmt/rules/SetCupRule.scala | 2 +- .../tla/bmcmt/rules/SetFilterRule.scala | 2 +- .../apalache/tla/bmcmt/rules/SetInRule.scala | 5 +- .../tla/bmcmt/rules/SetInRuleWithArrays.scala | 22 +-- .../bmcmt/rules/SetInRuleWithFunArrays.scala | 5 +- .../tla/bmcmt/rules/SetUnionRule.scala | 5 +- .../apalache/tla/bmcmt/rules/aux/AuxOps.scala | 11 +- .../tla/bmcmt/rules/aux/CherryPick.scala | 29 ++-- .../tla/bmcmt/rules/aux/IntOracle.scala | 9 +- .../tla/bmcmt/rules/aux/MockOracle.scala | 9 +- .../apalache/tla/bmcmt/rules/aux/Oracle.scala | 9 +- .../tla/bmcmt/rules/aux/OracleHelper.scala | 2 +- .../tla/bmcmt/rules/aux/PowSetCtor.scala | 2 +- .../bmcmt/rules/aux/PropositionalOracle.scala | 12 +- .../tla/bmcmt/rules/aux/ProtoSeqOps.scala | 2 +- .../bmcmt/rules/aux/RecordAndVariantOps.scala | 2 +- .../apalache/tla/bmcmt/rules/aux/SetOps.scala | 5 +- .../tla/bmcmt/rules/aux/SparseOracle.scala | 8 +- .../rules/aux/UninterpretedConstOracle.scala | 10 +- .../tla/bmcmt/rules/aux/ValueGenerator.scala | 2 +- .../tla/bmcmt/rules/aux/ZipOracle.scala | 5 +- .../tla/bmcmt/smt/Z3SolverContext.scala | 2 +- .../aux/caches/IntRangeCache.scala | 2 +- .../aux/caches/IntValueCache.scala | 2 +- .../aux/caches/RecordDomainCache.scala | 2 +- .../caches/UninterpretedLiteralCache.scala | 2 +- .../aux/oracles/IntOracle.scala | 5 +- .../aux/oracles/MockOracle.scala | 9 +- .../stratifiedRules/aux/oracles/Oracle.scala | 9 +- .../aux/oracles/SparseOracle.scala | 9 +- .../oracles/UninterpretedConstOracle.scala | 6 +- .../aux/oracles/ZipOracle.scala | 5 +- .../base/IntConstStratifiedRule.scala | 2 +- .../bool/AndStratifiedRule.scala | 16 +-- .../bool/OrStratifiedRule.scala | 14 +- .../set/SetCtorStratifiedRule.scala | 2 +- .../set/SetCupStratifiedRule.scala | 1 + .../set/SetFilterStratifiedRule.scala | 2 +- .../apalache/tla/bmcmt/RewriterBase.scala | 6 +- .../apalache/tla/bmcmt/TestCherryPick.scala | 9 +- .../tla/bmcmt/TestSymbStateDecoder.scala | 18 +-- .../bmcmt/TestSymbStateRewriterAction.scala | 3 +- .../TestSymbStateRewriterApalacheGen.scala | 3 +- .../TestSymbStateRewriterAssignment.scala | 34 ++--- .../TestSymbStateRewriterChooseOrGuess.scala | 2 +- .../bmcmt/TestSymbStateRewriterFunSet.scala | 6 +- .../bmcmt/TestSymbStateRewriterRecord.scala | 12 +- .../bmcmt/TestSymbStateRewriterRepeat.scala | 2 +- .../rules/aux/TestPropositionalOracle.scala | 3 +- .../bmcmt/rules/aux/TestSparseOracle.scala | 3 +- .../aux/TestUninterpretedConstOracle.scala | 3 +- .../smt/TestRecordingSolverContext.scala | 6 +- .../ApalacheRewriterTest.scala | 5 +- .../stratifiedRules/BoolRewriterTest.scala | 3 +- .../stratifiedRules/IntRewriterTest.scala | 3 +- .../stratifiedRules/SetRewriterTest.scala | 3 +- .../aux/IntRangeCacheTest.scala | 3 +- .../aux/IntValueCacheTest.scala | 3 +- .../aux/RecordDomainCacheTest.scala | 3 +- .../aux/UninterpretedLiteralCacheTest.scala | 3 +- .../aux/oracles/TestIntOracle.scala | 10 +- .../aux/oracles/TestMockOracle.scala | 10 +- .../aux/oracles/TestSparseOracle.scala | 6 +- .../TestUninterpretedConstOracle.scala | 10 +- .../trex/TestTransitionExecutorImpl.scala | 14 +- .../apalache/tla/pp/ConstSimplifierBase.scala | 7 +- .../apalache/tla/bmcmt/ArenaCell.scala | 6 +- .../forsyte/apalache/tla/bmcmt/ElemPtr.scala | 17 ++- .../apalache/tla/typecomp/ParamUtil.scala | 75 ++++++++++ .../tla/typecomp/ScopeUnsafeBuilder.scala | 128 ++++++++++++++++++ .../apalache/tla/typecomp/ScopedBuilder.scala | 65 +-------- .../apalache/tla/typecomp/package.scala | 5 + .../typecomp/subbuilder/ActionBuilder.scala | 2 +- .../typecomp/subbuilder/ApalacheBuilder.scala | 4 +- .../subbuilder/ApalacheInternalBuilder.scala | 2 +- .../subbuilder/ArithmeticBuilder.scala | 2 +- .../tla/typecomp/subbuilder/BaseBuilder.scala | 2 +- .../tla/typecomp/subbuilder/BoolBuilder.scala | 2 +- .../typecomp/subbuilder/ControlBuilder.scala | 2 +- .../subbuilder/FiniteSetBuilder.scala | 2 +- .../tla/typecomp/subbuilder/FunBuilder.scala | 2 +- .../subbuilder/LiteralAndNameBuilder.scala | 2 +- .../tla/typecomp/subbuilder/SeqBuilder.scala | 2 +- .../tla/typecomp/subbuilder/SetBuilder.scala | 2 +- .../typecomp/subbuilder/TemporalBuilder.scala | 2 +- .../typecomp/subbuilder/VariantBuilder.scala | 2 +- .../typecomp/unsafe/UnsafeActionBuilder.scala | 2 +- .../unsafe/UnsafeApalacheBuilder.scala | 14 +- .../UnsafeApalacheInternalBuilder.scala | 9 +- .../unsafe/UnsafeArithmeticBuilder.scala | 2 +- .../typecomp/unsafe/UnsafeBaseBuilder.scala | 9 +- .../typecomp/unsafe/UnsafeBoolBuilder.scala | 2 +- .../unsafe/UnsafeControlBuilder.scala | 2 +- .../unsafe/UnsafeFiniteSetBuilder.scala | 2 +- .../typecomp/unsafe/UnsafeFunBuilder.scala | 11 +- .../unsafe/UnsafeLiteralAndNameBuilder.scala | 2 +- .../typecomp/unsafe/UnsafeSeqBuilder.scala | 2 +- .../typecomp/unsafe/UnsafeSetBuilder.scala | 9 +- .../unsafe/UnsafeTemporalBuilder.scala | 2 +- .../unsafe/UnsafeVariantBuilder.scala | 15 +- .../forsyte/apalache/tla/types/package.scala | 6 + .../tla/typecomp/TestApalacheBuilder.scala | 2 +- .../apalache/tla/typecomp/TestHybrid.scala | 2 +- 130 files changed, 565 insertions(+), 427 deletions(-) create mode 100644 .unreleased/features/unsafe.md create mode 100644 tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala create mode 100644 tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala diff --git a/.unreleased/features/unsafe.md b/.unreleased/features/unsafe.md new file mode 100644 index 0000000000..99205f081a --- /dev/null +++ b/.unreleased/features/unsafe.md @@ -0,0 +1 @@ +Added scope-unsafe builder. \ No newline at end of file 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 index e50e21db89..b4d09c0825 100644 --- 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 index da36921b93..1d96cdf622 100644 --- 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 index 974aab97e7..ca4f5ba709 100644 --- 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 index c81c24f6ab..28f570c42b 100644 --- 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 index 72f43e98f8..01b7357a5e 100644 --- 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 index 21646402d3..984baef229 100644 --- 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 index 47ec20a096..5f92925f81 100644 --- 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 index 2bce3fcba9..284bf02d02 100644 --- 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 index 3318cc1d6e..fe25ac55d0 100644 --- 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 index 606c429769..fc68488903 100644 --- 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 index d424032ab2..5a083fdf83 100644 --- 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 index 7cf90cc6f9..02c19a730f 100644 --- 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 index f1a895676b..f3e87a8484 100644 --- 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 index c46e087842..3505ecee11 100644 --- 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 index 0f1e5531e6..6690fc4784 100644 --- 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 index c823cfb84b..767a4b2ee7 100644 --- 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 index 73b9c06aa9..e0393c441f 100644 --- 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 index 36ff58c28a..a29232d67a 100644 --- 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 <> 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 index 86c2b6174a..8bb0385770 100644 --- 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 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))) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala index 5753c1bc55..c27230be1d 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IfThenElseRule.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.CherryPick import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir.oper.TlaControlOper import at.forsyte.apalache.tla.lir.{BoolT1, ConstT1, IntT1, OperEx} -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 rule for IF A THEN B ELSE C. @@ -63,7 +62,7 @@ class IfThenElseRule(rewriter: SymbStateRewriter) extends RewritingRule { private def iteBasic( state: SymbState, commonType: CellT, - pred: TBuilderInstruction, + pred: BuilderT, thenCell: ArenaCell, elseCell: ArenaCell) = { val newArena = state.arena.appendCellOld(commonType) @@ -78,7 +77,7 @@ class IfThenElseRule(rewriter: SymbStateRewriter) extends RewritingRule { // The cool thing is that we do not have to compare the results anymore. It is all defined by the oracle. private def iteGeneral( state: SymbState, - pred: TBuilderInstruction, + pred: BuilderT, thenCell: ArenaCell, elseCell: ArenaCell) = { def solverAssert = rewriter.solverContext.assertGroundExpr _ diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala index d203be5da0..717325582e 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/QuantRule.scala @@ -4,10 +4,10 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, OracleHelper} 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, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import at.forsyte.apalache.tla.lir.oper._ import at.forsyte.apalache.tla.lir.values.{TlaIntSet, TlaNatSet} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction import com.typesafe.scalalogging.LazyLogging /** @@ -139,16 +139,16 @@ class QuantRule(rewriter: SymbStateRewriter) extends RewritingRule with LazyLogg val (predState: SymbState, predEsRaw: Seq[TlaEx]) = rewriter.rewriteBoundSeqUntilDone(setState, setCells.map(mkPair)) - val predEs: Seq[TBuilderInstruction] = predEsRaw.map(tla.unchecked) + val predEs: Seq[BuilderT] = predEsRaw.map(tla.unchecked) val nonEmpty = tla.or(setCells.map(c => tla.selectInSet(c.toBuilder, set.toBuilder)): _*) val empty = tla.and(setCells.map(c => tla.not(tla.selectInSet(c.toBuilder, set.toBuilder))): _*) - def elemWitnesses(elemAndPred: (ArenaCell, TBuilderInstruction)): TBuilderInstruction = { + def elemWitnesses(elemAndPred: (ArenaCell, BuilderT)): BuilderT = { tla.and(tla.selectInSet(elemAndPred._1.toBuilder, set.toBuilder), elemAndPred._2) } - def elemSatisfies(elemAndPred: (ArenaCell, TBuilderInstruction)): TBuilderInstruction = { + def elemSatisfies(elemAndPred: (ArenaCell, BuilderT)): BuilderT = { tla.or(tla.not(tla.selectInSet(elemAndPred._1.toBuilder, set.toBuilder)), elemAndPred._2) } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala index 327ceaf69a..a8b1835a96 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RecCtorRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.RecordAndVariantOps import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaFunOper import at.forsyte.apalache.tla.lir.values.TlaStr -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.immutable.{SortedMap, SortedSet} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala index 7bec841e0a..7dff798d78 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/RepeatRule.scala @@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming import at.forsyte.apalache.tla.lir.values.TlaInt 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 Repeat. This rule is similar to [[FoldSeqRule]]. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala index affd54df27..c089426668 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SeqOpsRule.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} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaSeqOper} /** diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala index a796dbbfdf..4f6396dd7b 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetAsFunRule.scala @@ -3,9 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules 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.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import at.forsyte.apalache.tla.lir.oper.ApalacheOper -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction /** * Implements a rule for Apalache!SetAsFun. @@ -118,7 +117,7 @@ class SetAsFunRule(rewriter: SymbStateRewriter) extends RewritingRule { val key1 = nextState.arena.getHas(pair1).head // ensure that a pair with the same key has not been included in the relation yet - def keysDifferOrNotIncluded(pair2Ptr: ElemPtr): TBuilderInstruction = { + def keysDifferOrNotIncluded(pair2Ptr: ElemPtr): BuilderT = { val pair2 = pair2Ptr.elem val key2 = nextState.arena.getHas(pair2).head // pair2 \notin funRel diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala index 765734621c..8ee6c25656 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCtorRule.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom} import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.{OperEx, SetT1, TlaEx, TypingException} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites the set constructor {e_1, ..., e_k}. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala index fad08ced10..4ee1c5f480 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaSetOper} import at.forsyte.apalache.tla.lir.{OperEx, TlaType1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites X \cup Y, that is, a union of two sets (not UNION). In the first encoding, we used a linear number of `in` diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala index d50920dd70..514dfad4e4 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetFilterRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir.oper.{TlaBoolOper, TlaSetOper} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites a set comprehension { x \in S: P }. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala index ea88a6558e..edb0153941 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRule.scala @@ -5,8 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaSetOper} 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} /** * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T]. @@ -114,7 +113,7 @@ class SetInRule(rewriter: SymbStateRewriter) extends RewritingRule { // In the new implementation, a function is a relation { <> : x \in U }. // Check that \A t \in f: t[1] \in S /\ t[2] \in T, and // `DOMAIN f = S`, since the above only implies `DOMAIN f \subseteq S` - def onPair(pair: ArenaCell): TBuilderInstruction = { + def onPair(pair: ArenaCell): BuilderT = { val tupleElems = nextState.arena.getHas(pair) val (arg, res) = (tupleElems.head, tupleElems.tail.head) nextState = rewriter.rewriteUntilDone(nextState.setRex(tla.selectInSet(arg.toBuilder, funsetDom.toBuilder))) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala index 3f0901d625..684b814e86 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, SymbState, SymbStateRewriter} 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} /** * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T]. @@ -33,16 +32,18 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite // TODO: Inlining this method is pointless. We should consider handling tuples and other structures natively in SMT. var newState = rewriter.lazyEq.cacheEqConstraints(state, setElems.cross(powsetDomainElems)) - def isInPowset(setElem: ArenaCell): TBuilderInstruction = { + def isInPowset(setElem: ArenaCell): BuilderT = { newState = newState.updateArena(_.appendCell(BoolT1)) val pred = newState.arena.topCell - def isInAndEqSetElem(powsetDomainElem: ArenaCell): TBuilderInstruction = { + def isInAndEqSetElem(powsetDomainElem: ArenaCell): BuilderT = { // powsetDomainElem \in powsetDomain /\ powsetDomainElem = setElem - tla - .and(tla.selectInSet(powsetDomainElem.toBuilder, powsetDomain.toBuilder), - tla.eql(powsetDomainElem.toBuilder, setElem.toBuilder)) - .map(simplifier.simplifyShallow) + simplifier.applySimplifyShallowToBuilderEx( + tla.and( + tla.selectInSet(powsetDomainElem.toBuilder, powsetDomain.toBuilder), + tla.eql(powsetDomainElem.toBuilder, setElem.toBuilder), + ) + ) } val elemsInAndEqSetElem = powsetDomainElems.map(isInAndEqSetElem) @@ -53,7 +54,8 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite pred.toBuilder } - val isSubset = tla.and(setElems.map(isInPowset): _*).map(simplifier.simplifyShallow) + val isSubset = + simplifier.applySimplifyShallowToBuilderEx(tla.and(setElems.map(isInPowset): _*)) newState = newState.updateArena(_.appendCell(BoolT1)) val pred = newState.arena.topCell.toBuilder rewriter.solverContext.assertGroundExpr(tla.eql(pred, isSubset)) @@ -88,7 +90,7 @@ class SetInRuleWithArrays(rewriter: SymbStateRewriter) extends SetInRule(rewrite // This method checks if f(x) \in T, for a given x // The goal is to ensure that \forall x \in DOMAIN f : f(x) \in T, by applying it to every arg \in DOMAIN f - def onFun(funsetDomElem: ArenaCell): TBuilderInstruction = { + def onFun(funsetDomElem: ArenaCell): BuilderT = { funsetCdm.cellType match { case _: PowSetT => nextState = rewriter diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala index 0b2aa208a7..0000d6f9f0 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetInRuleWithFunArrays.scala @@ -4,8 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.rules.aux.AuxOps._ import at.forsyte.apalache.tla.bmcmt.types._ import at.forsyte.apalache.tla.bmcmt.{ArenaCell, RewriterException, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir.{BoolT1, FunT1} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Rewrites set membership tests: x \in S, x \in SUBSET S, and x \in [S -> T]. @@ -38,7 +37,7 @@ class SetInRuleWithFunArrays(rewriter: SymbStateRewriter) extends SetInRule(rewr // This method checks if there is a pair (x,y) \in RELATION f s.t. x = arg \land arg \in DOMAIN f // The goal is to ensure that f's range is a subset of T, by applying it to every arg \in DOMAIN f - def onPair(arg: ArenaCell): TBuilderInstruction = { + def onPair(arg: ArenaCell): BuilderT = { val funApp = tla.app(funCell.toBuilder, arg.toBuilder) nextState = rewriter.rewriteUntilDone(nextState.setRex(funApp)) val funAppRes = nextState.asCell diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala index cbb3c19ae7..417e61b650 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala @@ -3,10 +3,9 @@ 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.types.CellTFrom -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.{OperEx, SetT1, TypingException} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction /** * Implements the rule for a union of all set elements, that is, UNION S for a set S that contains sets as elements. @@ -62,7 +61,7 @@ class SetUnionRule(rewriter: SymbStateRewriter) extends RewritingRule { // add all the elements to the arena nextState = nextState.updateArena(_.appendHas(newSetCell, unionElemPtrs: _*)) - def inPointingSet(elemCell: ArenaCell, set: ArenaCell): TBuilderInstruction = { + def inPointingSet(elemCell: ArenaCell, set: ArenaCell): BuilderT = { // this is sound, because we have generated element equalities // and thus can use congruence of in(...) for free tla.and(tla.selectInSet(set.toBuilder, topSetCell.toBuilder), diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala index 0e197f5ccc..e2aa2639ea 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/AuxOps.scala @@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Auxiliary methods for handling rewriting rules. @@ -46,13 +45,13 @@ object AuxOps { val domainElems = nextState.arena.getHas(domain) val relationElems = nextState.arena.getHas(relation) - def eqAndInDomain(domainElem: ArenaCell, checkedElem: ArenaCell): TBuilderInstruction = { + def eqAndInDomain(domainElem: ArenaCell, checkedElem: ArenaCell): BuilderT = { val eq = tla.unchecked(rewriter.lazyEq.safeEq(domainElem, checkedElem)) val selectInSet = tla.selectInSet(domainElem.toBuilder, domain.toBuilder) tla.and(eq, selectInSet) } - def isInDomain(elem: ArenaCell): TBuilderInstruction = { + def isInDomain(elem: ArenaCell): BuilderT = { if (domainElems.isEmpty) { tla.bool(false) } else { @@ -99,7 +98,7 @@ object AuxOps { checkedElem: ArenaCell, setElem: ArenaCell, setCell: ArenaCell, - lazyEq: Boolean): TBuilderInstruction = { + lazyEq: Boolean): BuilderT = { val conjunction = if (lazyEq) { tla.and( @@ -112,6 +111,6 @@ object AuxOps { tla.eql(checkedElem.toBuilder, setElem.toBuilder), ) } - conjunction.map(simplifier.simplifyShallow) + simplifier.applySimplifyShallowToBuilderEx(conjunction) } } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala index abf076190b..14076b0089 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PtrUtil 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.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types._ +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT, _} import scala.collection.immutable.SortedMap @@ -39,7 +38,7 @@ class CherryPick(rewriter: SymbStateRewriter) { * @return * a new symbolic state whose expression stores a fresh cell that corresponds to the picked element. */ - def pick(set: ArenaCell, state: SymbState, elseAssert: TBuilderInstruction): SymbState = { + def pick(set: ArenaCell, state: SymbState, elseAssert: BuilderT): SymbState = { set.cellType match { // all kinds of sets that should be kept unexpanded case PowSetT(t @ SetT1(_)) => @@ -110,7 +109,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, elems: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { assert(elems.nonEmpty) // this is an advanced operator -- you should know what you are doing val targetType = elems.head.cellType @@ -181,7 +180,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, elems: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(cellType, elems.map(_.toString).mkString(", "))) val arena = state.arena.appendCell(cellType) val resultCell = arena.topCell @@ -214,7 +213,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, tuples: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(cellType, tuples.map(_.toString).mkString(", "))) var newState = state @@ -262,7 +261,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, records: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { // the records do not always have the same type, but they do have compatible types val commonRecordT = findCommonRecordType(records) rewriter.solverContext @@ -353,7 +352,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, records: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { // new row records always have the same type val (fieldTypes, recordT) = records.head.cellType match { case CellTFrom(rt @ RecRowT1(RowT1(fieldTypes, None))) => (fieldTypes, rt) @@ -400,7 +399,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, variants: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { // variants should always have the same type val (optionTypes, variantT) = variants.head.cellType match { case CellTFrom(rt @ VariantT1(RowT1(opts, None))) => (opts, rt) @@ -580,7 +579,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, memberSets: Seq[ArenaCell], - elseAssert: TBuilderInstruction, + elseAssert: BuilderT, noSmt: Boolean = false): SymbState = { if (memberSets.isEmpty) { throw new RuntimeException("Picking from a statically empty set") @@ -602,7 +601,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, memberSets: Seq[ArenaCell], - elseAssert: TBuilderInstruction, + elseAssert: BuilderT, noSMT: Boolean): SymbState = { def solverAssert(e: TlaEx): Unit = rewriter.solverContext.assertGroundExpr(e) @@ -658,7 +657,7 @@ class CherryPick(rewriter: SymbStateRewriter) { // The awesome property of the oracle is that we do not have to compare the sets directly! // Instead, we compare the oracle values. // (chosen = 1 /\ in(z_i, R) <=> in(c_i, S_1)) \/ (chosen = 2 /\ in(z_i, R) <=> in(d_i, S_2)) \/ (chosen = N <=> elseAssert) - def nthIn(elemAndSet: (ArenaCell, ArenaCell), no: Int): (TBuilderInstruction, TBuilderInstruction) = { + def nthIn(elemAndSet: (ArenaCell, ArenaCell), no: Int): (BuilderT, BuilderT) = { if (elemsOfMemberSets(no).nonEmpty) { val inSet = tla.ite(tla.selectInSet(elemAndSet._1.toBuilder, elemAndSet._2.toBuilder), membershipEx, tla.storeNotInSet(picked.toBuilder, resultCell.toBuilder)) @@ -715,7 +714,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, memberSeqs: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { if (memberSeqs.isEmpty) { throw new RuntimeException("Picking a sequence from a statically empty set") } else if (memberSeqs.length == 1) { @@ -738,7 +737,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, memberSeqs: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { rewriter.solverContext .log("; CHERRY-PICK %s FROM [%s] {".format(seqType, memberSeqs.map(_.toString).mkString(", "))) @@ -829,7 +828,7 @@ class CherryPick(rewriter: SymbStateRewriter) { state: SymbState, oracle: Oracle, funs: Seq[ArenaCell], - elseAssert: TBuilderInstruction): SymbState = { + elseAssert: BuilderT): SymbState = { rewriter.solverContext.log("; CHERRY-PICK %s FROM [%s] {".format(funType, funs.map(_.toString).mkString(", "))) var nextState = state rewriter.solverContext.config.smtEncoding match { diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala index 6e0e31ecb4..46bfd4dce0 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/IntOracle.scala @@ -4,8 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState} import at.forsyte.apalache.tla.lir.{IntT1, ValEx} import at.forsyte.apalache.tla.lir.values.TlaInt -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle that uses an integer variable. Although using integers as an oracle is the most straightforward decision, @@ -23,13 +22,13 @@ class IntOracle(val intCell: ArenaCell, nvalues: Int) extends Oracle { override def size: Int = nvalues - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = + override def whenEqualTo(state: SymbState, position: Int): BuilderT = tla.eql(intCell.toBuilder, tla.int(position)) override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = { if (elseAssertions.nonEmpty && assertions.size != elseAssertions.size) { throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions") } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala index c36e6ffa24..1c10c3c6d6 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/MockOracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.SymbState import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle that always has the same value. This class specializes all methods to the case oracle == fixedValue. @@ -16,14 +15,14 @@ class MockOracle(fixedValue: Int) extends Oracle { override def size: Int = fixedValue + 1 - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = { + override def whenEqualTo(state: SymbState, position: Int): BuilderT = { tla.bool(position == fixedValue) } override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = assertions(fixedValue) override def evalPosition(solverContext: SolverContext, state: SymbState): Int = diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala index 8762c1f364..78a746876f 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/Oracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.SymbState import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An abstract version of an oracle that is used e.g. in CherryPick. @@ -30,7 +29,7 @@ trait Oracle extends Serializable { * @param position * a position the oracle should be equal to */ - def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction + def whenEqualTo(state: SymbState, position: Int): BuilderT /** * Produce a ground expression that contains assertions for the possible oracle values. @@ -46,8 +45,8 @@ trait Oracle extends Serializable { */ def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = { size match { // If the oracle has no candidate values, then caseAssertions should return a no-op for SMT, i.e. TRUE. case 0 => state.arena.cellTrue().toBuilder diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala index 0a619b9c13..35b63d5777 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/OracleHelper.scala @@ -1,7 +1,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * A helper class to create oracle values and compare them. In two previous solutions, we were using integers, then diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala index 270bccea4c..5d67003924 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.lir.SetT1 -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * This class constructs the power set of S, that is, SUBSET S. Sometimes, this is just unavoidable, e.g., consider { Q diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala index f1f7dde250..025869aed5 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PropositionalOracle.scala @@ -4,15 +4,15 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellTFrom import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir.BoolT1 -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._ class PropositionalOracle(bitCells: Seq[ArenaCell], nvalues: Int) extends Oracle { override def size: Int = nvalues - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = { - def mkLits(n: Int, cells: Seq[ArenaCell]): Seq[TBuilderInstruction] = { + override def whenEqualTo(state: SymbState, position: Int): BuilderT = { + def mkLits(n: Int, cells: Seq[ArenaCell]): Seq[BuilderT] = { cells match { case Nil => Nil @@ -35,8 +35,8 @@ class PropositionalOracle(bitCells: Seq[ArenaCell], nvalues: Int) extends Oracle override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = { if (elseAssertions.nonEmpty & assertions.size != elseAssertions.size) { throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions") } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala index dbcabd98e7..a776fea7e9 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ProtoSeqOps.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.types.{CellTFrom, UnknownT} import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.immutable.ArraySeq diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala index 2032574ae1..8e4dd60f82 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/RecordAndVariantOps.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.arena.{PtrUtil, PureArenaAdapter} import at.forsyte.apalache.tla.bmcmt.types.CellTFrom import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scala.collection.immutable.SortedMap diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala index 1911df2866..d347a62d66 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SetOps.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.{ArenaCell, SymbState, SymbStateRewriter} import at.forsyte.apalache.tla.lir.BoolT1 -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** *

A small collection of operations on sets that can be reused by rewriting rules.

@@ -57,7 +56,7 @@ class SetOps(rewriter: SymbStateRewriter) { // /\ c[i] \in S // /\ \A j \in 0..(i - 1): // ~b[j] \/ c[j] /= c[i] - def notSeen(j: Int): TBuilderInstruction = { + def notSeen(j: Int): BuilderT = { tla.or(tla.not(predicates(j).toBuilder), tla.not(tla.eql(c_i.toBuilder, elems(j).toBuilder))) } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala index 4112ea8563..b95064232b 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/SparseOracle.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.SymbState import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction +import at.forsyte.apalache.tla.types.{BuilderUT => BuilderT} /** * The oracle for sparse values, that is, a set S of naturals. This oracle is mapped on a smaller contiguous range @@ -23,15 +23,15 @@ class SparseOracle(oracle: Oracle, val values: Set[Int]) extends Oracle { override def size: Int = values.size - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = { + override def whenEqualTo(state: SymbState, position: Int): BuilderT = { assert(indexMap.contains(position)) oracle.whenEqualTo(state, indexMap(position)) } override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = oracle.caseAssertions(state, assertions, elseAssertions) override def evalPosition(solverContext: SolverContext, state: SymbState): Int = { diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala index 4a01eb73ef..1fac909c43 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/UninterpretedConstOracle.scala @@ -3,20 +3,20 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.lir.ConstT1 -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._ class UninterpretedConstOracle(valueCells: Seq[ArenaCell], oracleCell: ArenaCell, nvalues: Int) extends Oracle { override def size: Int = nvalues - override def whenEqualTo(state: SymbState, position: Int): TBuilderInstruction = + override def whenEqualTo(state: SymbState, position: Int): BuilderT = tla.eql(oracleCell.toBuilder, valueCells(position).toBuilder) override def caseAssertions( state: SymbState, - assertions: Seq[TBuilderInstruction], - elseAssertions: Seq[TBuilderInstruction] = Seq.empty): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertions: Seq[BuilderT] = Seq.empty): BuilderT = { if (elseAssertions.nonEmpty && assertions.size != elseAssertions.size) { throw new IllegalStateException(s"Invalid call to Oracle, malformed elseAssertions") } diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala index 23784c3d16..66bd88d113 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ValueGenerator.scala @@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom} import at.forsyte.apalache.tla.lir.TypedPredefs._ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.{tla => tlaLegacy} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} import scalaz.unused import scala.collection.immutable.{SortedMap, SortedSet} diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala index edba7f30dc..88b674f175 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.tla.bmcmt.SymbState import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * [[ZipOracle]] is an optimization of [[Oracle]]. It groups several values of the background oracle together, in order @@ -21,7 +20,7 @@ import at.forsyte.apalache.tla.types.tla class ZipOracle(backOracle: Oracle, groups: Seq[Seq[Int]]) extends Oracle { override def size: Int = groups.size - override def whenEqualTo(state: SymbState, index: Int): TBuilderInstruction = { + override def whenEqualTo(state: SymbState, index: Int): BuilderT = { assert(index < groups.size) val conds = groups(index).map(i => backOracle.whenEqualTo(state, i)) tla.or(conds: _*) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index 883ec6bc89..0303ab7091 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -7,7 +7,7 @@ import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.profiler.{IdleSmtListener, SmtListener} import at.forsyte.apalache.tla.bmcmt.rewriter.ConstSimplifierForSmt 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._ import at.forsyte.apalache.tla.lir.io.UTFPrinter import at.forsyte.apalache.tla.lir.oper._ diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala index db962c93a1..2f3cb6662c 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntRangeCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, PureArena} import at.forsyte.apalache.tla.lir.{IntT1, SetT1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Cache ranges a..b and, as a special case, tuple domains. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala index 76e96e78fe..9002f4d476 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/IntValueCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena} 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/stratifiedRules/aux/caches/RecordDomainCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala index 23bef5c036..0eb8efa5c6 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/RecordDomainCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt.{ArenaCell, FixedElemPtr, PureArena} 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/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala index 2d1a7b9dac..6a62339b86 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala @@ -4,7 +4,7 @@ import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.types.{CellT, CellTFrom} import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena} import at.forsyte.apalache.tla.lir.{ConstT1, StrT1, TlaType1} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * A cache for uninterpreted literals, that are translated to uninterpreted SMT constants, with a unique sort per diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala index fee661f0bb..38ad298eec 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/IntOracle.scala @@ -5,8 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.lir.{IntT1, ValEx} import at.forsyte.apalache.tla.lir.values.TlaInt -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle that uses an integer variable. Although using integers as an oracle is the most straightforward decision, @@ -27,7 +26,7 @@ class IntOracle(val intCell: ArenaCell, nvalues: Int) extends Oracle { * Produce an expression that states that the chosen value equals to the value `v_{index}`. The actual implementation * may be different from an integer comparison. */ - override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = tla.eql(intCell.toBuilder, tla.int(index)) override def getIndexOfChosenValueFromModel(solverContext: SolverContext): BigInt = diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala index 53b288b0ce..09bb698e29 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/MockOracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle that always has the same value. This class specializes all methods to the case oracle == fixedValue. @@ -17,13 +16,13 @@ class MockOracle(fixedValue: Int) extends Oracle { override def size: Int = fixedValue + 1 - override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = tla.bool(index == fixedValue) override def caseAssertions( scope: RewriterScope, - assertions: Seq[TBuilderInstruction], - elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT = { require(assertions.size == this.size && elseAssertionsOpt.forall { _.size == this.size }, s"Invalid call to Oracle, assertion sequences must have length $size.") assertions(fixedValue) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala index 26efc705ed..74238f4c78 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/Oracle.scala @@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An oracle provides a means of choosing a single value, out of a finite collection of candidate values. It can @@ -29,7 +28,7 @@ trait Oracle { * Produce an expression that states that the chosen value equals to the value `v_{index}`. The actual implementation * may be different from an integer comparison. */ - def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction + def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT /** * Produce a ground expression that contains assertions for the possible oracle values. @@ -45,8 +44,8 @@ trait Oracle { */ def caseAssertions( scope: RewriterScope, - assertions: Seq[TBuilderInstruction], - elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = { + assertions: Seq[BuilderT], + elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT = { require(assertions.size == this.size && elseAssertionsOpt.forall { _.size == this.size }, s"Invalid call to Oracle, assertion sequences must have length $size.") size match { diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala index 55c9255f41..e02c0ba337 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/SparseOracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Given a set `indices` of size `N`, sparse oracle is able to answer {{{chosenValueIsEqualToIndexedValue(_, i),}}} for @@ -30,7 +29,7 @@ class SparseOracle(mkOracle: Int => Oracle, val values: Set[Int]) extends Oracle override def size: Int = values.size - def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = indexMap .get(index.toInt) .map { @@ -40,8 +39,8 @@ class SparseOracle(mkOracle: Int => Oracle, val values: Set[Int]) extends Oracle override def caseAssertions( scope: RewriterScope, - assertions: Seq[TBuilderInstruction], - elseAssertionsOpt: Option[Seq[TBuilderInstruction]] = None): TBuilderInstruction = + assertions: Seq[BuilderT], + elseAssertionsOpt: Option[Seq[BuilderT]] = None): BuilderT = oracle.caseAssertions(scope, assertions, elseAssertionsOpt) override def getIndexOfChosenValueFromModel(solverContext: SolverContext): BigInt = { diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala index 92e5549c93..bf1016cd91 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/UninterpretedConstOracle.scala @@ -6,8 +6,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLit import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope} import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.lir.ConstT1 -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._ /** * An oracle that uses a fixed collection of potential cells. @@ -24,7 +24,7 @@ class UninterpretedConstOracle(val valueCells: Seq[ArenaCell], val oracleCell: A */ override def size: Int = valueCells.size - override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = if (valueCells.indices.contains(index)) tla.eql(oracleCell.toBuilder, valueCells(index.toInt).toBuilder) else tla.bool(false) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala index 054dac080a..240251b916 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/ZipOracle.scala @@ -2,8 +2,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.oracles import at.forsyte.apalache.tla.bmcmt.smt.SolverContext import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * [[ZipOracle]] is an optimization of [[Oracle]]. It groups several values of the background oracle together, in order @@ -21,7 +20,7 @@ import at.forsyte.apalache.tla.types.tla class ZipOracle(backOracle: Oracle, groups: Seq[Seq[Int]]) extends Oracle { override def size: Int = groups.size - override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): TBuilderInstruction = + override def chosenValueIsEqualToIndexedValue(scope: RewriterScope, index: BigInt): BuilderT = if (groups.indices.contains(index)) { val conds = groups(index.toInt).map(i => backOracle.chosenValueIsEqualToIndexedValue(scope, i)) tla.or(conds: _*) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala index f82de7f822..3737632188 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/IntConstStratifiedRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.IntValueCache import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, StratifiedRule} import at.forsyte.apalache.tla.lir.values.TlaInt import at.forsyte.apalache.tla.lir.{TlaEx, ValEx} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites integer constants. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala index 26ffcdf960..76bee4f8fc 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/AndStratifiedRule.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope} import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule} import at.forsyte.apalache.tla.lir.oper.TlaBoolOper import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, TlaEx} -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Implements the rule for conjunction. @@ -20,8 +19,7 @@ import at.forsyte.apalache.tla.types.tla * @author * Jure Kukovec */ -class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) - extends StratifiedRule[Option[TBuilderInstruction]] { +class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) extends StratifiedRule[Option[BuilderT]] { private val simplifier = new ConstSimplifierForSmt() override def isApplicable(ex: TlaEx, scope: RewriterScope): Boolean = ex match { @@ -32,7 +30,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) override def buildArena(ex: TlaEx)(startingScope: RewriterScope): ( RewriterScope, ArenaCell, - Option[TBuilderInstruction]) = simplifier.simplifyShallow(ex) match { + Option[BuilderT]) = simplifier.simplifyShallow(ex) match { case OperEx(TlaBoolOper.and, args @ _*) => if (args.isEmpty) { // empty conjunction is always true @@ -40,9 +38,9 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) } else { // use short-circuiting on state-level expressions (like in TLC) - def toIte(es: Seq[TlaEx]): TBuilderInstruction = { + def toIte(es: Seq[TlaEx]): BuilderT = { // assume es is nonempty - es.map(tla.unchecked).reduceRight[TBuilderInstruction] { case (elem, partial) => + es.map(tla.unchecked).reduceRight[BuilderT] { case (elem, partial) => tla.ite(elem, partial, PureArena.cellFalse(startingScope.arena).toBuilder) } } @@ -58,7 +56,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) val (newScope, rewrittenArgCells) = // With AND all blocks belong to the same scope, so we have to propagate it - args.foldLeft((startingScope.copy(arena = arenaWithAndCell), Seq.empty[TBuilderInstruction])) { + args.foldLeft((startingScope.copy(arena = arenaWithAndCell), Seq.empty[BuilderT])) { case ((scope, cellSeq), term) => val (newScope, termCell) = rewriter.rewrite(term)(scope) (newScope, cellSeq :+ termCell.toBuilder) @@ -74,7 +72,7 @@ class AndStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) (scope, cell, None) } - override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[TBuilderInstruction]): Unit = { + override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[BuilderT]): Unit = { // Only add constraints, if ITE rewriting didn't fire (in that case, the ITE rule does it for us) auxData.foreach { conjunction => rewriter.assert(tla.eql(cell.toBuilder, conjunction)) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala index 187803e49c..93233c86fa 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/bool/OrStratifiedRule.scala @@ -6,8 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule} import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope} import at.forsyte.apalache.tla.lir.{BoolT1, OperEx, TlaEx} import at.forsyte.apalache.tla.lir.oper.TlaBoolOper -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * Implements the rule for disjunction. @@ -20,8 +19,7 @@ import at.forsyte.apalache.tla.types.tla * @author * Jure Kukovec */ -class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) - extends StratifiedRule[Option[TBuilderInstruction]] { +class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) extends StratifiedRule[Option[BuilderT]] { private val simplifier = new ConstSimplifierForSmt() override def isApplicable(ex: TlaEx, scope: RewriterScope): Boolean = ex match { @@ -32,7 +30,7 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) override def buildArena(ex: TlaEx)(startingScope: RewriterScope): ( RewriterScope, ArenaCell, - Option[TBuilderInstruction]) = simplifier.simplifyShallow(ex) match { + Option[BuilderT]) = simplifier.simplifyShallow(ex) match { case OperEx(TlaBoolOper.or, args @ _*) => if (args.isEmpty) { // empty disjunction is always false @@ -40,9 +38,9 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) } else { // use short-circuiting on state-level expressions (like in TLC) - def toIte(es: Seq[TlaEx]): TBuilderInstruction = { + def toIte(es: Seq[TlaEx]): BuilderT = { // assume es is nonempty - es.map(tla.unchecked).reduceRight[TBuilderInstruction] { case (elem, partial) => + es.map(tla.unchecked).reduceRight[BuilderT] { case (elem, partial) => tla.ite(elem, PureArena.cellTrue(startingScope.arena).toBuilder, partial) } } @@ -71,7 +69,7 @@ class OrStratifiedRule(rewriter: Rewriter, shortCircuit: Boolean = false) (scope, cell, None) } - override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[TBuilderInstruction]): Unit = { + override def addConstraints(scope: RewriterScope, cell: ArenaCell, auxData: Option[BuilderT]): Unit = { // Only add constraints, if ITE rewriting didn't fire (in that case, the ITE rule does it for us) auxData.foreach { disjunction => rewriter.assert(tla.eql(cell.toBuilder, disjunction)) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala index f0fb928416..88572fa324 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCtorStratifiedRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope} import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, StratifiedRule} import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites the set constructor {e_1, ..., e_k}. diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala index ad4d437819..73d284806a 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetCupStratifiedRule.scala @@ -6,6 +6,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, S import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.{OperEx, TlaEx} +import at.forsyte.apalache.tla.typecomp._ /** * Rewrites X \cup Y, that is, a union of two sets (not UNION). diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala index 78156496c8..63b3520b1e 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/set/SetFilterStratifiedRule.scala @@ -5,7 +5,7 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{addCell, Rewriter, Rewrite import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaSetOper import at.forsyte.apalache.tla.lir.values.{TlaIntSet, TlaNatSet} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} /** * Rewrites a set comprehension { x \in S: P }. diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala index 911ede25ce..c540f12e9d 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/RewriterBase.scala @@ -3,10 +3,10 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.bmcmt.smt.SolverContext -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker import at.forsyte.apalache.tla.lir.transformations.standard.IncrementalRenaming -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction import org.scalatest.funsuite.FixtureAnyFunSuite import java.io.StringWriter @@ -19,7 +19,7 @@ trait RewriterBase extends FixtureAnyFunSuite { protected val renaming = new IncrementalRenaming(new IdleTracker) - protected def assertBuildEqual(a: TBuilderInstruction, b: TBuilderInstruction): Unit = + protected def assertBuildEqual(a: BuilderT, b: BuilderT): Unit = assert(a.build == b.build) protected def create(rewriterType: SMTEncoding): SymbStateRewriter = { diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala index cacf67134a..bef6f6dabc 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestCherryPick.scala @@ -3,10 +3,9 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, Oracle, OracleFactory} 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.parser.DefaultType1Parser -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.types.tlaU._ trait TestCherryPick extends RewriterBase { private val parser = DefaultType1Parser @@ -171,7 +170,7 @@ trait TestCherryPick extends RewriterBase { state = oracleState def mkRecord(i: Int, j: Int): ArenaCell = { - val rec = tla.rec("a" -> int(i), "b" -> int(j)).map(_.withTag(Typed(recordT))) + val rec = tla.rec("a" -> int(i), "b" -> int(j)).withTag(Typed(recordT)) state = rewriter.rewriteUntilDone(state.setRex(rec)) state.asCell } @@ -351,7 +350,7 @@ trait TestCherryPick extends RewriterBase { val (oracleState, oracle) = new OracleFactory(rewriter).newConstOracle(state, 2) state = oracleState - def mkFun(dom: TBuilderInstruction, map: TBuilderInstruction): ArenaCell = { + def mkFun(dom: BuilderT, map: BuilderT): ArenaCell = { val fun = funDef(map, name("x", IntT1) -> dom) state = rewriter.rewriteUntilDone(state.setRex(fun)) state.asCell diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala index b3de34187d..a83152a9d7 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateDecoder.scala @@ -3,19 +3,19 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaSetOper -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction import at.forsyte.apalache.tla.types.parser.DefaultType1Parser -import at.forsyte.apalache.tla.types.tla -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} +import at.forsyte.apalache.tla.typecomp._ +import at.forsyte.apalache.tla.types.tlaU._ trait TestSymbStateDecoder extends RewriterBase { private val parser = DefaultType1Parser private val int2 = parser("<>") - private def pair(i: Int, j: Int): TBuilderInstruction = tuple(int(i), int(j)) + private def pair(i: Int, j: Int): BuilderT = tuple(int(i), int(j)) test("decode bool") { rewriterType: SMTEncoding => - val originalEx: TBuilderInstruction = bool(true) + val originalEx: BuilderT = bool(true) val state = new SymbState(originalEx, arena, Binding()) val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) @@ -45,7 +45,7 @@ trait TestSymbStateDecoder extends RewriterBase { } test("decode str") { rewriterType: SMTEncoding => - val originalEx: TBuilderInstruction = str("hello") + val originalEx: BuilderT = str("hello") val state = new SymbState(originalEx, arena, Binding()) val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) @@ -141,7 +141,7 @@ trait TestSymbStateDecoder extends RewriterBase { val decoder = new SymbStateDecoder(solverContext, rewriter) val decodedEx = decoder.decodeCellToTlaEx(nextState.arena, cell) - val expectedOutcome: TBuilderInstruction = setAsFun(enumSet(pair(1, 2), pair(2, 3))) + val expectedOutcome: BuilderT = setAsFun(enumSet(pair(1, 2), pair(2, 3))) assertBuildEqual(expectedOutcome, decodedEx) } @@ -180,7 +180,7 @@ trait TestSymbStateDecoder extends RewriterBase { test("decode dynamically empty fun") { rewriterType: SMTEncoding => // this domain is not empty at the arena level, but it is in every SMT model - def dynEmpty(left: TBuilderInstruction): TBuilderInstruction = + def dynEmpty(left: BuilderT): BuilderT = filter(name("t", IntT1), left, bool(false)) val domEx = dynEmpty(enumSet(int(1))) @@ -246,7 +246,7 @@ trait TestSymbStateDecoder extends RewriterBase { val recEx = rec( "a" -> int(1), "b" -> bool(true), - ).map(_.withTag(Typed(parser("{ a: Int, b: Bool }")))) + ).withTag(Typed(parser("{ a: Int, b: Bool }"))) val state = new SymbState(recEx, arena, Binding()) val rewriter = create(rewriterType) val nextState = rewriter.rewriteUntilDone(state) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala index b741f7255f..cbd771fabb 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAction.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.SymbStateRewriter.Continue import at.forsyte.apalache.tla.lir.IntT1 -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ trait TestSymbStateRewriterAction extends RewriterBase { test("""x' is rewritten to the binding of x'""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala index 063e46ec2e..5d64a3a6be 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterApalacheGen.scala @@ -6,7 +6,8 @@ import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.convenience.{tla => tlaLegacy} import at.forsyte.apalache.tla.lir.oper.ApalacheOper import at.forsyte.apalache.tla.types.parser.DefaultType1Parser -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.tlaU._ +import at.forsyte.apalache.tla.typecomp._ trait TestSymbStateRewriterApalacheGen extends RewriterBase { private val parser = DefaultType1Parser diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala index 09dac17186..ede1eb8a8b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterAssignment.scala @@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding 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.{BuilderUT => BuilderT} +import at.forsyte.apalache.tla.types.tlaU._ /** * Tests for assignments. The assignments were at the core of Apalache 0.5.x. In Apalache 0.6.x, they are preprocessed @@ -12,19 +12,19 @@ import at.forsyte.apalache.tla.types.tla._ trait TestSymbStateRewriterAssignment extends RewriterBase { val ibI: TlaType1 = TupT1(IntT1, BoolT1, SetT1(IntT1)) - private val set12: TBuilderInstruction = enumSet(int(1), int(2)) - private val x_prime: TBuilderInstruction = prime(name("x", IntT1)) - private val x_primeS: TBuilderInstruction = prime(name("x", SetT1(IntT1))) - private val x_primeFbi: TBuilderInstruction = prime(name("x", FunT1(BoolT1, IntT1))) - private val x_primeFii: TBuilderInstruction = prime(name("x", FunT1(IntT1, IntT1))) - private val x_primeFib: TBuilderInstruction = prime(name("x", FunT1(IntT1, BoolT1))) - private val y_prime: TBuilderInstruction = prime(name("y", IntT1)) - private val boundName: TBuilderInstruction = name("t", IntT1) - private val boundNameS: TBuilderInstruction = name("t", SetT1(IntT1)) - private val boundNameFbi: TBuilderInstruction = name("t", FunT1(BoolT1, IntT1)) - private val boundNameFii: TBuilderInstruction = name("t", FunT1(IntT1, IntT1)) - private val boundNameFib: TBuilderInstruction = name("t", FunT1(IntT1, BoolT1)) - private val boolset: TBuilderInstruction = enumSet(bool(false), bool(true)) + private val set12: BuilderT = enumSet(int(1), int(2)) + private val x_prime: BuilderT = prime(name("x", IntT1)) + private val x_primeS: BuilderT = prime(name("x", SetT1(IntT1))) + private val x_primeFbi: BuilderT = prime(name("x", FunT1(BoolT1, IntT1))) + private val x_primeFii: BuilderT = prime(name("x", FunT1(IntT1, IntT1))) + private val x_primeFib: BuilderT = prime(name("x", FunT1(IntT1, BoolT1))) + private val y_prime: BuilderT = prime(name("y", IntT1)) + private val boundName: BuilderT = name("t", IntT1) + private val boundNameS: BuilderT = name("t", SetT1(IntT1)) + private val boundNameFbi: BuilderT = name("t", FunT1(BoolT1, IntT1)) + private val boundNameFii: BuilderT = name("t", FunT1(IntT1, IntT1)) + private val boundNameFib: BuilderT = name("t", FunT1(IntT1, BoolT1)) + private val boolset: BuilderT = enumSet(bool(false), bool(true)) test("""\E t \in {1, 2}: x' \in {t} ~~> TRUE and [x -> $C$k]""") { rewriterType: SMTEncoding => val asgn = skolem(exists(boundName, set12, assign(x_prime, boundName))) @@ -98,7 +98,7 @@ trait TestSymbStateRewriterAssignment extends RewriterBase { test("""\E t \in \in {t_2 \in {1}: FALSE}: x' \in {t} ~~> FALSE""") { rewriterType: SMTEncoding => // a regression test - def empty(set: TBuilderInstruction): TBuilderInstruction = { + def empty(set: BuilderT): BuilderT = { filter(name("t_2", IntT1), set, bool(false)) } @@ -181,7 +181,7 @@ trait TestSymbStateRewriterAssignment extends RewriterBase { test("""\E t \in {{1, 2}, {1+1, 2, 3}} \ {{2, 3}}: x' \in {t} ~~> TRUE and [x -> $C$k]""") { rewriterType: SMTEncoding => // equal elements in different sets mess up picking from a set - def setminus(left: TBuilderInstruction, right: TBuilderInstruction): TBuilderInstruction = { + def setminus(left: BuilderT, right: BuilderT): BuilderT = { // this is how Keramelizer translates setminus filter(name("t_2", SetT1(IntT1)), left, not(eql(name("t_2", SetT1(IntT1)), right))) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala index 8d60b6fdca..0181f58083 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterChooseOrGuess.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.lir.IntT1 -import at.forsyte.apalache.tla.types.tla._ +import at.forsyte.apalache.tla.types.tlaU._ trait TestSymbStateRewriterChooseOrGuess extends RewriterBase { test("""CHOOSE x \in { 1, 2, 3 }: x > 1""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala index 6a712f5161..57699ff2e0 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterFunSet.scala @@ -3,8 +3,8 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding 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.{BuilderUT => BuilderT} +import at.forsyte.apalache.tla.types.tlaU._ trait TestSymbStateRewriterFunSet extends RewriterBase { val i_to_B: TlaType1 = FunT1(IntT1, SetT1(BoolT1)) @@ -172,7 +172,7 @@ trait TestSymbStateRewriterFunSet extends RewriterBase { // this should be redundant in the presence of #91 test("""[x \in {0, 1, 2} \ {0} |-> 3] \in [{1, 2} -> {3, 4}]""") { rewriterType: SMTEncoding => // although 0 is in the function domain at the arena level, it does not belong to the set difference - def setminus(set: TBuilderInstruction, intVal: BigInt): TBuilderInstruction = { + def setminus(set: BuilderT, intVal: BigInt): BuilderT = { filter(name("t", IntT1), set, not(eql(name("t", IntT1), int(intVal)))) } diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala index fbe0d667d2..16e37f9ded 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRecord.scala @@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding 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._ import scala.collection.immutable.{SortedMap, SortedSet, TreeMap} @@ -82,7 +82,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { val record = rec( "a" -> int(1), "b" -> bool(false), - ).map { _.withTag(Typed(ribs)) } + ).withTag(Typed(ribs)) // We assume that record has the type RecT1("a" -> IntT1, "b" -> BoolT1, "c" -> StrT1). // This can happen due to type unification. The record access should still work, // though the access is expected to produce an arbitrary value (of proper type). @@ -130,7 +130,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { val record1 = rec( "a" -> int(1), "b" -> bool(false), - ).map { _.withTag(Typed(ribs)) } + ).withTag(Typed(ribs)) val record2 = rec( "a" -> int(2), "b" -> bool(true), @@ -165,7 +165,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { // and then -- when knowing the type of the filtered records -- map them somewhere. // Although, it is not easy to do in a symbolic encoding, we support this idiom. // We require though that all the records have type-compatible fields. - val record1 = rec("a" -> int(1)).map { _.withTag(Typed(rii)) } + val record1 = rec("a" -> int(1)).withTag(Typed(rii)) val record2 = rec("a" -> int(2), "c" -> int(3)) // Records in a set can have different sets of keys. This requires a type annotation. val setEx = enumSet(record1, record2) @@ -207,7 +207,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { "b" -> bool(false), "c" -> str("d"), ) - val record2 = rec("a" -> int(1)).map { _.withTag(Typed(ribs)) } + val record2 = rec("a" -> int(1)).withTag(Typed(ribs)) val eq = not(eql(record1, record2)) val state = new SymbState(eq, arena, Binding()) val rewriter = create(rewriterType) @@ -229,7 +229,7 @@ trait TestSymbStateRewriterRecord extends RewriterBase { } test("""DOMAIN [a |-> 1] = {"a"} under type annotations!""") { rewriterType: SMTEncoding => - val record = rec("a" -> int(1)).map(_.withTag(Typed(ribs))) + val record = rec("a" -> int(1)).withTag(Typed(ribs)) val domain = dom(record) val eq = eql(domain, enumSet(str("a"))) val state = new SymbState(eq, arena, Binding()) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala index aea018c7dd..29c525816b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestSymbStateRewriterRepeat.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} trait TestSymbStateRewriterRepeat extends RewriterBase { test("""Repeat(LET Op(a,i) == a + 1 IN Op, 5, 0) = 5""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala index 04a8b1f0f7..1302906eac 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestPropositionalOracle.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState} import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ trait TestPropositionalOracle extends RewriterBase with TestingPredefs { test("""Propositional Oracle.create""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala index 23715cdc85..2bfbe1256e 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestSparseOracle.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState} import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ trait TestSparseOracle extends RewriterBase with TestingPredefs { test("""Sparse Oracle.create""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala index 9c25fbee6c..8533863012 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/TestUninterpretedConstOracle.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux import at.forsyte.apalache.infra.passes.options.SMTEncoding import at.forsyte.apalache.tla.bmcmt.{Binding, RewriterBase, SymbState} import at.forsyte.apalache.tla.lir.{BoolT1, TestingPredefs} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ trait TestUninterpretedConstOracle extends RewriterBase with TestingPredefs { test("""UninterpretedConst Oracle.create""") { rewriterType: SMTEncoding => diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala index 56052ad099..4149cd7fa7 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/smt/TestRecordingSolverContext.scala @@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.smt import at.forsyte.apalache.tla.bmcmt.arena.PureArenaAdapter import at.forsyte.apalache.tla.lir.IntT1 -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 org.scalatest.funsuite.AnyFunSuite /** @@ -13,7 +13,7 @@ import org.scalatest.funsuite.AnyFunSuite trait TestRecordingSolverContext extends AnyFunSuite { protected var solverConfig: SolverConfig = _ - private val int42: TBuilderInstruction = tla.int(42) + private val int42: BuilderT = tla.int(42) test("operations proxied") { val solver = RecordingSolverContext.createZ3(None, solverConfig) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala index b7868f2683..dfeb025d37 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/ApalacheRewriterTest.scala @@ -3,8 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules import at.forsyte.apalache.tla.bmcmt.stratifiedRules.apalache.AssignmentStratifiedRule import at.forsyte.apalache.tla.bmcmt.{ArenaCell, Binding, PureArena} 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 org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite @@ -27,7 +26,7 @@ class ApalacheRewriterTest extends AnyFunSuite with BeforeAndAfterEach { val rule = new AssignmentStratifiedRule(rewriter) - def assignTo(lhs: TBuilderInstruction, rhs: TBuilderInstruction = tla.int(1)): TBuilderInstruction = + def assignTo(lhs: BuilderT, rhs: BuilderT = tla.int(1)): BuilderT = tla.assign(tla.prime(lhs), rhs) val startScope = RewriterScope.initial() diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala index 9736d3d815..04a12f6a2b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/BoolRewriterTest.scala @@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules import at.forsyte.apalache.tla.bmcmt.{ArenaCell, Binding, PureArena} import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala index 21e75e24cd..916f15299c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/IntRewriterTest.scala @@ -1,7 +1,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules import at.forsyte.apalache.tla.lir.{IntT1, NameEx, SetT1, Typed} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala index 562a148bf3..7332b32b19 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/SetRewriterTest.scala @@ -4,7 +4,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.set.SetFilterStratifiedRule import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt._ import at.forsyte.apalache.tla.lir._ -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala index 4b83e8acb8..6494248f02 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntRangeCacheTest.scala @@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.{IntRangeCache, IntValueCache} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala index 7895f465c8..2193bb49cb 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/IntValueCacheTest.scala @@ -2,7 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.IntValueCache -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala index 004243cf2a..f99923ad5b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/RecordDomainCacheTest.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.{RecordDomainCache, UninterpretedLiteralCache} import at.forsyte.apalache.tla.lir.{StrT1, TlaType1} -import at.forsyte.apalache.tla.types.{tla, ModelValueHandler} +import at.forsyte.apalache.tla.types.{tlaU => tla, ModelValueHandler} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala index 868cfa9e87..a9083a80d5 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala @@ -3,7 +3,8 @@ package at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux import at.forsyte.apalache.tla.bmcmt.PureArena import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLiteralCache import at.forsyte.apalache.tla.lir.{StrT1, TlaType1} -import at.forsyte.apalache.tla.types.{tla, ModelValueHandler} +import at.forsyte.apalache.tla.types.{tlaU => tla, ModelValueHandler} +import at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalatest.BeforeAndAfterEach import org.scalatest.funsuite.AnyFunSuite diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala index 8485c3f3e4..d24d073693 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestIntOracle.scala @@ -7,8 +7,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope import at.forsyte.apalache.tla.lir.{BoolT1, NameEx, OperEx, TlaEx, ValEx} import at.forsyte.apalache.tla.lir.oper.TlaOper import at.forsyte.apalache.tla.lir.values.TlaInt -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 org.junit.runner.RunWith import org.scalacheck.{Gen, Prop} import org.scalacheck.Prop.forAll @@ -62,7 +62,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { } - val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0 .to(10) .map { i => (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) @@ -70,7 +70,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { .unzip test("caseAssertions requires assertion sequences of equal length") { - val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for { i <- Gen.choose(0, assertionsA.size) j <- Gen.choose(0, assertionsB.size) opt <- Gen.option(Gen.const(assertionsB.take(j))) @@ -91,7 +91,7 @@ class TestIntOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { } test("caseAssertions constructs a collection of ITEs, or shorthands") { - val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for { size <- nonNegIntGen opt <- Gen.option(Gen.const(assertionsB.take(size))) } yield (size, assertionsA.take(size), opt) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala index 74afa816a8..a1c065d805 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestMockOracle.scala @@ -4,8 +4,8 @@ import at.forsyte.apalache.tla.bmcmt.smt.{SolverConfig, Z3SolverContext} import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.values.TlaBool -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 org.junit.runner.RunWith import org.scalacheck.Prop.forAll import org.scalacheck.{Gen, Prop} @@ -58,7 +58,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { check(prop, minSuccessful(1000), sizeRange(4)) } - val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0 .to(10) .map { i => (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) @@ -66,7 +66,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { .unzip test("caseAssertions requires assertion sequences of equal length") { - val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for { i <- Gen.choose(0, assertionsA.size) j <- Gen.choose(0, assertionsB.size) opt <- Gen.option(Gen.const(assertionsB.take(j))) @@ -86,7 +86,7 @@ class TestMockOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers { } test("caseAssertions always shorthands") { - val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for { fixed <- nonNegIntGen opt <- Gen.option(Gen.const(assertionsB.take(fixed + 1))) } yield (fixed, assertionsA.take(fixed + 1), opt) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala index c2c40e1007..a7b09be08c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestSparseOracle.scala @@ -6,8 +6,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.RewriterScope import at.forsyte.apalache.tla.bmcmt.types.CellT import at.forsyte.apalache.tla.bmcmt.{ArenaCell, PureArena} 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 at.forsyte.apalache.tla.typecomp._ import org.junit.runner.RunWith import org.scalacheck.Gen import org.scalacheck.Prop.forAll @@ -59,7 +59,7 @@ class TestSparseOracle extends AnyFunSuite with BeforeAndAfterEach with Checkers check(prop, minSuccessful(1000), sizeRange(4)) } - val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0 .to(10) .map { i => (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala index 6688fbc3df..4b047c464c 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/oracles/TestUninterpretedConstOracle.scala @@ -7,8 +7,8 @@ import at.forsyte.apalache.tla.bmcmt.stratifiedRules.aux.caches.UninterpretedLit import at.forsyte.apalache.tla.bmcmt.stratifiedRules.{Rewriter, RewriterScope, TestingRewriter} import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.TlaOper -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 org.junit.runner.RunWith import org.scalacheck.Prop.forAll import org.scalacheck.{Gen, Prop} @@ -69,7 +69,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w check(prop, minSuccessful(200), sizeRange(4)) } - val (assertionsA, assertionsB): (Seq[TBuilderInstruction], Seq[TBuilderInstruction]) = 0 + val (assertionsA, assertionsB): (Seq[BuilderT], Seq[BuilderT]) = 0 .to(10) .map { i => (tla.name(s"A$i", BoolT1), tla.name(s"B$i", BoolT1)) @@ -77,7 +77,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w .unzip test("caseAssertions requires assertion sequences of equal length") { - val assertionsGen: Gen[(Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val assertionsGen: Gen[(Seq[BuilderT], Option[Seq[BuilderT]])] = for { i <- Gen.choose(0, assertionsA.size) j <- Gen.choose(0, assertionsB.size) opt <- Gen.option(Gen.const(assertionsB.take(j))) @@ -97,7 +97,7 @@ class TestUninterpretedConstOracle extends AnyFunSuite with BeforeAndAfterEach w } test("caseAssertions constructs a collection of ITEs, or shorthands") { - val gen: Gen[(Int, Seq[TBuilderInstruction], Option[Seq[TBuilderInstruction]])] = for { + val gen: Gen[(Int, Seq[BuilderT], Option[Seq[BuilderT]])] = for { size <- nonNegIntGen opt <- Gen.option(Gen.const(assertionsB.take(size))) } yield (size, assertionsA.take(size), opt) diff --git a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala index 0b544e080a..ed9044555b 100644 --- a/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala +++ b/tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/trex/TestTransitionExecutorImpl.scala @@ -2,8 +2,8 @@ package at.forsyte.apalache.tla.bmcmt.trex import at.forsyte.apalache.tla.bmcmt.{Binding, StateInvariant} 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 at.forsyte.apalache.tla.typecomp._ /** * An abstract test suite that is parameterized by the snapshot type. @@ -16,8 +16,8 @@ import at.forsyte.apalache.tla.types.tla */ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] { - def nX: TBuilderInstruction = tla.name("x", IntT1) - def nY: TBuilderInstruction = tla.name("y", IntT1) + def nX: BuilderT = tla.name("x", IntT1) + def nY: BuilderT = tla.name("y", IntT1) test("constant initialization") { exeCtx: ExecutorContextT => // N' <- 1 @@ -129,7 +129,7 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] { // state 1 is produced by transition 1 assert(1 == decPath(1)._2) - def mapWithBuild(pairs: (String, TBuilderInstruction)*): Map[String, TlaEx] = + def mapWithBuild(pairs: (String, BuilderT)*): Map[String, TlaEx] = pairs.map { case (a, b) => a -> b.build }.toMap assert(mapWithBuild("x" -> tla.int(1), "y" -> tla.int(1)) == decPath(1)._1) @@ -225,9 +225,9 @@ trait TestTransitionExecutorImpl[SnapshotT] extends ExecutorBase[SnapshotT] { assert(!mayChange2) } - private def mkAssign(name: String, value: Int): TBuilderInstruction = + private def mkAssign(name: String, value: Int): BuilderT = tla.assign(tla.prime(tla.name(name, IntT1)), tla.int(value)) - private def mkAssignInt(name: String, rhs: TBuilderInstruction) = + private def mkAssignInt(name: String, rhs: BuilderT) = tla.assign(tla.prime(tla.name(name, IntT1)), rhs) } diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala index ad8a5209c2..23cbe6f36b 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ConstSimplifierBase.scala @@ -3,7 +3,7 @@ package at.forsyte.apalache.tla.pp import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper._ import at.forsyte.apalache.tla.lir.values.{TlaBool, TlaInt, TlaStr} -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderT, BuilderUT} /** *

A base class for constant simplification that is shared by more specialized simplifiers.

@@ -239,4 +239,9 @@ abstract class ConstSimplifierBase { case ex => ex } + + def applySimplifyShallowToBuilderEx(ex: BuilderUT): BuilderUT = + simplifyShallow(ex) // when using TlaEx + def applySimplifyShallowToBuilderEx(ex: BuilderT): BuilderT = + ex.map(simplifyShallow) // when using TBuilderInstruction } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala index 44f917e358..6e9e9a9d47 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ArenaCell.scala @@ -2,9 +2,9 @@ package at.forsyte.apalache.tla.bmcmt import at.forsyte.apalache.tla.bmcmt.PureArena.namePrefix import at.forsyte.apalache.tla.lir.{NameEx, TlaEx} -import at.forsyte.apalache.tla.typecomp -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} import at.forsyte.apalache.tla.bmcmt.types.CellT +import at.forsyte.apalache.tla.typecomp._ object ArenaCell { def isValidName(name: String): Boolean = { @@ -44,7 +44,7 @@ class ArenaCell(val id: Int, val cellType: CellT, val isUnconstrained: Boolean = * @return * a builder instruction that can be used with the typed builder */ - def toBuilder: typecomp.TBuilderInstruction = tla.name(toString, cellType.toTlaType1) + def toBuilder: BuilderT = tla.name(toString, cellType.toTlaType1) def mkTlaEq(rhs: ArenaCell): TlaEx = tla.eql(this.toBuilder, rhs.toBuilder) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala index c35692625e..6e97dce712 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/bmcmt/ElemPtr.scala @@ -1,7 +1,6 @@ package at.forsyte.apalache.tla.bmcmt -import at.forsyte.apalache.tla.typecomp.TBuilderInstruction -import at.forsyte.apalache.tla.types.tla +import at.forsyte.apalache.tla.types.{tlaU => tla, BuilderUT => BuilderT} /** * An abstract membership pointer. @@ -18,7 +17,7 @@ sealed trait ElemPtr { /** * Translate the membership test into an expression that can be understood by Z3SolverContext. */ - def toSmt: TBuilderInstruction + def toSmt: BuilderT /** * After certain set operations, every pointer must become a SmtExprElemPtr, because the operation invalidates the @@ -31,7 +30,7 @@ sealed trait ElemPtr { * filter). `ptr.restrict(x)` returns `ptr2`, such that `ptr2.toSmt` is logically equivalent (but not necessarily * syntactically equal) to `tla.and(ptr.toSmt, x)`, while `ptr.elem = ptr2.elem`. */ - def restrict(cond: TBuilderInstruction): SmtExprElemPtr + def restrict(cond: BuilderT): SmtExprElemPtr } /** @@ -42,9 +41,9 @@ sealed trait ElemPtr { * the element this pointer is pointing to. */ case class FixedElemPtr(elem: ArenaCell) extends ElemPtr { - override def toSmt: TBuilderInstruction = tla.bool(true) + override def toSmt: BuilderT = tla.bool(true) - override def restrict(cond: TBuilderInstruction): SmtExprElemPtr = SmtExprElemPtr(elem, cond) + override def restrict(cond: BuilderT): SmtExprElemPtr = SmtExprElemPtr(elem, cond) } /** @@ -56,7 +55,7 @@ case class FixedElemPtr(elem: ArenaCell) extends ElemPtr { * @param smtEx * the corresponding SMT expression. */ -case class SmtExprElemPtr(elem: ArenaCell, smtEx: TBuilderInstruction) extends ElemPtr { - override def toSmt: TBuilderInstruction = smtEx - def restrict(cond: TBuilderInstruction): SmtExprElemPtr = this.copy(smtEx = tla.and(smtEx, cond)) +case class SmtExprElemPtr(elem: ArenaCell, smtEx: BuilderT) extends ElemPtr { + override def toSmt: BuilderT = smtEx + def restrict(cond: BuilderT): SmtExprElemPtr = this.copy(smtEx = tla.and(smtEx, cond)) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala new file mode 100644 index 0000000000..a3dadd3420 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ParamUtil.scala @@ -0,0 +1,75 @@ +package at.forsyte.apalache.tla.typecomp + +import at.forsyte.apalache.tla.lir.{ + BoolT1, ConstT1, FunT1, IntT1, OperParam, OperT1, RealT1, RecRowT1, RecT1, RowT1, SeqT1, SetT1, SparseTupT1, StrT1, + TlaType1, TupT1, VarT1, VariantT1, +} + +object ParamUtil { + + type TypedParam = (OperParam, TlaType1) + + /** + * Evaluates whether a parameter type satisfies the type restrictions on operator parameters in TLA+. + * + * Parameters of TLA+ operators must: + * - have a non-operator type, unless they are (syntactically) marked higher-order (HO) + * - have a top-level operator type (OperT1) if they are marked HO + * - not contain `OperT1` in the type's syntax-tree in either case, except possibly at the root (if HO). In + * particular, a parameter to a HO operator with an `OperT1` type may not be HO itself. + */ + def isAcceptableParamType(canContainOper: Boolean): TlaType1 => Boolean = { + case FunT1(arg, res) => isAcceptableParamType(false)(arg) && isAcceptableParamType(false)(res) + case SetT1(elem) => isAcceptableParamType(false)(elem) + case SeqT1(elem) => isAcceptableParamType(false)(elem) + case TupT1(elems @ _*) => elems.forall(isAcceptableParamType(false)) + case SparseTupT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false)) + case RecT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false)) + case OperT1(args, res) => + if (canContainOper) + args.nonEmpty && + args.forall(isAcceptableParamType(false)) && + isAcceptableParamType(false)(res) + else false + case RowT1(fieldTypes, _) => fieldTypes.values.forall(isAcceptableParamType(false)) + case RecRowT1(row) => isAcceptableParamType(false)(row) + case VariantT1(row) => isAcceptableParamType(false)(row) + case IntT1 | StrT1 | BoolT1 | RealT1 | VarT1(_) | ConstT1(_) => true + } + + /** + * Throws if parameters don't satisfy [[isAcceptableParamType]]. Permits operator types iff the parameter arity is + * positive. + */ + def validateParamType(tp: TypedParam): Unit = { + val (OperParam(name, arity), tt) = tp + if (!isAcceptableParamType(canContainOper = arity > 0)(tt)) + throw new TBuilderTypeException( + s"Parameter $name type $tt and arity $arity are inconsistent. Parameters have operator types iff their arity is positive." + ) + } + + /** + * Determines the parameter arity, if the type is an operator type. We distinguish nullary operators from + * non-operators in this method. + */ + def typeAsOperArity(tt: TlaType1): Option[Int] = tt match { + case OperT1(args, _) => Some(args.size) + case _ => None + } + + /** + * Operator parameter with type information. Checks that parameters have permissible types. + */ + def param(name: String, tt: TlaType1): TypedParam = { + val arityOpt = typeAsOperArity(tt) + // operator parameters may not be nullary operators + if (arityOpt.contains(0)) + throw new TBuilderTypeException(s"Parameter $name may not have a nullary operator type $tt.") + val arity = arityOpt.getOrElse(0) // 0 here means not-an-operator + val ret = (OperParam(name, arity), tt) + validateParamType(ret) + ret + } + +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala new file mode 100644 index 0000000000..81438d1217 --- /dev/null +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopeUnsafeBuilder.scala @@ -0,0 +1,128 @@ +package at.forsyte.apalache.tla.typecomp + +import at.forsyte.apalache.tla.lir.TypedPredefs.TypeTagAsTlaType1 +import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.typecomp.unsafe.{ + UnsafeActionBuilder, UnsafeApalacheBuilder, UnsafeApalacheInternalBuilder, UnsafeArithmeticBuilder, UnsafeBaseBuilder, + UnsafeBoolBuilder, UnsafeControlBuilder, UnsafeFiniteSetBuilder, UnsafeFunBuilder, UnsafeLiteralAndNameBuilder, + UnsafeSeqBuilder, UnsafeSetBuilder, UnsafeTemporalBuilder, UnsafeVariantBuilder, +} + +/** + * Scope-unsafe Builder for TLA+ (Quint) IR expressions. + * + * The following guarantees hold for any IR tree successfully generated exclusively via ScopeUnsafeBuilder methods: + * - Typed-ness: All subexpressions will have a `Typed(_)` tag + * - Type correctness: + * - All literal expressions will have the correct type, as determined by their value ( `1: Int`, `"a" : Str`, etc.) + * - For each operator application expression `OperEx(oper, args:_*)(Typed(resultType))`, the following holds: + * - `oper(args:_*)` corresponds to some TNT operator with a signature `(T1,...,Tn) => T` + * - There exists some substitution `s`, such that: `s(T1) = typeof(args[1]), ..., s(Tn) = typeof(args[n])` and + * `s(T) = resultType`. Example: For `e @ OperEx(TlaSetOper.union, 1..4, {5})` the subexpressions `1..4, {5}` + * and `e` will all have types `Set(Int)`, since + * [[at.forsyte.apalache.tla.lir.oper.TlaSetOper.union TlaSetOper.union]] corresponds to `\union`, which has the + * signature `(Set(t), Set(t)) => Set(t)`, and the substitution required is `t -> Int`. + * + * If `strict` mode is enabled, the builder rejects inputs for ApalacheOper methods, which do not adhere to the method + * requirements ("... must be ..."), even if their types are correct. If `strict` mode is disabled, the builder should + * allow for the construction of any expression, which may be present in a freshly parsed specification (i.e. before + * preprocessing). + * + * @author + * Jure Kukovec + * @param strict + * If true, performs method requirement checks + */ +class ScopeUnsafeBuilder(val strict: Boolean = true) + extends UnsafeBaseBuilder with UnsafeBoolBuilder with UnsafeArithmeticBuilder with UnsafeSetBuilder + with UnsafeFiniteSetBuilder with UnsafeSeqBuilder with UnsafeActionBuilder with UnsafeFunBuilder + with UnsafeControlBuilder with UnsafeTemporalBuilder with UnsafeApalacheInternalBuilder with UnsafeApalacheBuilder + with UnsafeVariantBuilder with UnsafeLiteralAndNameBuilder { + + // The following two methods are included in the unsafe builder for interface compatibility with the + // scope-safe builder. They are both no-ops + def unchecked(ex: TlaEx): TlaEx = ex + def uncheckedDecl(decl: TlaOperDecl): TlaOperDecl = decl + + //////////////////// + // HYBRID METHODS // + //////////////////// + + /** x' = y */ + def primeEq(x: TlaEx, y: TlaEx): TlaEx = eql(prime(x), y) + + import ParamUtil._ + + def param(name: String, tt: TlaType1): TypedParam = ParamUtil.param(name, tt) + + /** opName(params[1],...,params[n]) == body */ + def decl(opName: String, body: TlaEx, params: TypedParam*): TlaOperDecl = { + params.foreach(validateParamType) + TlaOperDecl(opName, params.map(_._1).toList, body)( + Typed( + OperT1(params.map { _._2 }, body.typeTag.asTlaType1()) + ) + ) + } + + /** + * Creates an expression of the form + * + * {{{ + * LET uniqueName(p1,...,pn) == body IN uniqueName + * }}} + * + * Matching the representation of LAMBDAs produced by SANY. + * + * NOTE: It is left up to the caller to ensure `uniqueName` is unique. + * + * Failure to ensure uniqueness of names can lead to name collisions in case lambdas are nested. + */ + def lambda(uniqueName: String, body: TlaEx, params: TypedParam*): TlaEx = { + params.foreach(validateParamType) + val paramTypes = params.map(_._2) + val operType = OperT1(paramTypes, body.typeTag.asTlaType1()) + letIn(name(uniqueName, operType), decl(uniqueName, body, params: _*)) + } + + /** {{{LET decl(...) = ... IN body}}} */ + def letIn(body: TlaEx, decl: TlaOperDecl): TlaEx = + LetInEx(body, decl)(body.typeTag) + + /** + * {{{LET F_1(a_1^1,...,a_{n_1}^1) == X_1 F_2(a_1^2,...,b_{n_2}^2) == X_2 ... F_N(a_1^N,...,z_{n_N}^N) == X_N IN e}}} + * is equivalently translated to + * {{{ + * LET F_1(a_1^1,...,a_{n_1}^1) == X_1 IN + * LET F_2(a_1^2,...,b_{n_2}^2) == X_2 IN + * ... + * LET F_N(a_1^N,...,z_{n_N}^N) == X_N IN + * e + * }}} + */ + def letIn(body: TlaEx, decls: TlaOperDecl*): TlaEx = { + require(decls.nonEmpty, "decls must be nonempty.") + decls.foldRight(body) { case (decl, partial) => + letIn(partial, decl) + } + } + + /** + * [f EXCEPT ![a1] = e1, ![a2] = e2 ... ![an] = en] + * + * Is equivalent to {{{[[f EXCEPT ![a1] = e1] EXCEPT ![a2] = e2] EXCEPT ... ![an] = en]}}} + */ + def exceptMany( + f: TlaEx, + args: (TlaEx, TlaEx)*): TlaEx = { + require(args.nonEmpty, s"args must be nonempty.") + args.foldLeft(f) { case (fn, (ai, ei)) => + except(fn, ai, ei) + } + } + + /** + * A name expression referring to the TlaVarDecl + */ + def varDeclAsNameEx(decl: TlaVarDecl): TlaEx = name(decl.name, decl.typeTag.asTlaType1()) +} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala index 0a407d5319..6bfa4845cf 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/ScopedBuilder.scala @@ -168,70 +168,9 @@ class ScopedBuilder(val strict: Boolean = true) /** x' = y */ def primeEq(x: TBuilderInstruction, y: TBuilderInstruction): TBuilderInstruction = eql(prime(x), y) - type TypedParam = (OperParam, TlaType1) + import ParamUtil._ - /** - * Evaluates whether a parameter type satisfies the type restrictions on operator parameters in TLA+. - * - * Parameters of TLA+ operators must: - * - have a non-operator type, unless they are (syntactically) marked higher-order (HO) - * - have a top-level operator type (OperT1) if they are marked HO - * - not contain `OperT1` in the type's syntax-tree in either case, except possibly at the root (if HO). In - * particular, a parameter to a HO operator with an `OperT1` type may not be HO itself. - */ - private def isAcceptableParamType(canContainOper: Boolean): TlaType1 => Boolean = { - case FunT1(arg, res) => isAcceptableParamType(false)(arg) && isAcceptableParamType(false)(res) - case SetT1(elem) => isAcceptableParamType(false)(elem) - case SeqT1(elem) => isAcceptableParamType(false)(elem) - case TupT1(elems @ _*) => elems.forall(isAcceptableParamType(false)) - case SparseTupT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false)) - case RecT1(fieldTypes) => fieldTypes.values.forall(isAcceptableParamType(false)) - case OperT1(args, res) => - if (canContainOper) - args.nonEmpty && - args.forall(isAcceptableParamType(false)) && - isAcceptableParamType(false)(res) - else false - case RowT1(fieldTypes, _) => fieldTypes.values.forall(isAcceptableParamType(false)) - case RecRowT1(row) => isAcceptableParamType(false)(row) - case VariantT1(row) => isAcceptableParamType(false)(row) - case IntT1 | StrT1 | BoolT1 | RealT1 | VarT1(_) | ConstT1(_) => true - } - - /** - * Throws if parameters don't satisfy [[isAcceptableParamType]]. Permits operator types iff the parameter arity is - * positive. - */ - private def validateParamType(tp: TypedParam): Unit = { - val (OperParam(name, arity), tt) = tp - if (!isAcceptableParamType(canContainOper = arity > 0)(tt)) - throw new TBuilderTypeException( - s"Parameter $name type $tt and arity $arity are inconsistent. Parameters have operator types iff their arity is positive." - ) - } - - /** - * Determines the parameter arity, if the type is an operator type. We distinguish nullary operators from - * non-operators in this method. - */ - private def typeAsOperArity(tt: TlaType1): Option[Int] = tt match { - case OperT1(args, _) => Some(args.size) - case _ => None - } - - /** - * Operator parameter with type information. Checks that parameters have permissible types. - */ - def param(name: String, tt: TlaType1): TypedParam = { - val arityOpt = typeAsOperArity(tt) - // operator parameters may not be nullary operators - if (arityOpt.contains(0)) - throw new TBuilderTypeException(s"Parameter $name may not have a nullary operator type $tt.") - val arity = arityOpt.getOrElse(0) // 0 here means not-an-operator - val ret = (OperParam(name, arity), tt) - validateParamType(ret) - ret - } + def param(name: String, tt: TlaType1): TypedParam = ParamUtil.param(name, tt) /** opName(params[1],...,params[n]) == body */ def decl(opName: String, body: TBuilderInstruction, params: TypedParam*): TBuilderOperDeclInstruction = { diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala index 151101aa3a..ebe867a369 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/package.scala @@ -263,6 +263,11 @@ package object typecomp { def build: T = builderState } + // Included to facilitate seamless swapping between the scope-safe and unsafe builders + implicit class NoOpBuild(ex: TlaEx) { + def build: TlaEx = ex + } + /** * Apply the `build` method to a sequence. * diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala index 7201859d98..d9738e4e6f 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ActionBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil.binaryFromUnsafe * Jure Kukovec */ trait ActionBuilder { - private val unsafeBuilder = new UnsafeActionBuilder + private val unsafeBuilder = new UnsafeActionBuilder {} /** {{{e'}}} */ def prime(e: TBuilderInstruction): TBuilderInstruction = e.map(unsafeBuilder.prime) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala index 086eec7375..3397a0a982 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheBuilder.scala @@ -15,7 +15,9 @@ import scalaz._ */ trait ApalacheBuilder { val strict: Boolean - private val unsafeBuilder = new UnsafeApalacheBuilder(strict) + // UnsafeApalacheBuilder is a trait with a parameter `strict`, so we create a class here to instantiate it + private case class ApalacheBuilderU(strict: Boolean) extends UnsafeApalacheBuilder + private val unsafeBuilder = ApalacheBuilderU(strict) /** * {{{lhs := rhs}}} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala index c8f96a10b9..78e6997869 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ApalacheInternalBuilder.scala @@ -15,7 +15,7 @@ import scalaz.Scalaz._ * Jure Kukovec */ trait ApalacheInternalBuilder { - private val unsafeBuilder = new UnsafeApalacheInternalBuilder + private val unsafeBuilder = new UnsafeApalacheInternalBuilder {} /** * {{{__NotSupportedByModelChecker(msg): t}}} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala index 8b4d52a135..a10fcf9621 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ArithmeticBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil.binaryFromUnsafe * Jure Kukovec */ trait ArithmeticBuilder { - private val unsafeBuilder = new UnsafeArithmeticBuilder + private val unsafeBuilder = new UnsafeArithmeticBuilder {} /** {{{x + y}}} */ def plus(x: TBuilderInstruction, y: TBuilderInstruction): TBuilderInstruction = diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala index 3297271cb7..2f9b55d0cf 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BaseBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeBaseBuilder * Jure Kukovec */ trait BaseBuilder { - private val unsafeBuilder = new UnsafeBaseBuilder + private val unsafeBuilder = new UnsafeBaseBuilder {} /** {{{lhs = rhs}}} */ def eql(lhs: TBuilderInstruction, rhs: TBuilderInstruction): TBuilderInstruction = diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala index e00c3c3b3a..7c55539a0d 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/BoolBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil._ * Jure Kukovec */ trait BoolBuilder { - private val unsafeBuilder = new UnsafeBoolBuilder + private val unsafeBuilder = new UnsafeBoolBuilder {} /** {{{args[0] /\ ... /\ args[n]}}} */ def and(args: TBuilderInstruction*): TBuilderInstruction = buildSeq(args).map(unsafeBuilder.and(_: _*)) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala index 0e156acac8..0fdbd539d8 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/ControlBuilder.scala @@ -12,7 +12,7 @@ import scalaz._ * Jure Kukovec */ trait ControlBuilder { - private val unsafeBuilder = new UnsafeControlBuilder + private val unsafeBuilder = new UnsafeControlBuilder {} /** {{{IF p THEN A ELSE B}}} */ def ite(p: TBuilderInstruction, A: TBuilderInstruction, B: TBuilderInstruction): TBuilderInstruction = diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala index eb3e9ecd3d..a975845573 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FiniteSetBuilder.scala @@ -10,7 +10,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeFiniteSetBuilder * Jure Kukovec */ trait FiniteSetBuilder { - private val unsafeBuilder = new UnsafeFiniteSetBuilder + private val unsafeBuilder = new UnsafeFiniteSetBuilder {} /** {{{IsFiniteSet(set)}}} */ def isFiniteSet(set: TBuilderInstruction): TBuilderInstruction = set.map(unsafeBuilder.isFiniteSet) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala index a4570d6c2f..846563253d 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/FunBuilder.scala @@ -15,7 +15,7 @@ import at.forsyte.apalache.tla.lir.VarT1 * Jure Kukovec */ trait FunBuilder { - private val unsafeBuilder = new UnsafeFunBuilder + private val unsafeBuilder = new UnsafeFunBuilder {} /** * {{{[ args[0]._1 |-> args[0]._2, ..., args[n]._1 |-> args[n]._2 ]}}} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala index a4204a890a..5fd4178efe 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/LiteralAndNameBuilder.scala @@ -14,7 +14,7 @@ import scalaz._ * Jure Kukovec */ trait LiteralAndNameBuilder { - private val unsafeBuilder = new UnsafeLiteralAndNameBuilder + private val unsafeBuilder = new UnsafeLiteralAndNameBuilder {} /** {{{i : Int}}} */ def int(i: BigInt): TBuilderInstruction = unsafeBuilder.int(i).point[TBuilderInternalState] diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala index c3ec3d5eb4..4375f677ec 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SeqBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeSeqBuilder * Jure Kukovec */ trait SeqBuilder { - private val unsafeBuilder = new UnsafeSeqBuilder + private val unsafeBuilder = new UnsafeSeqBuilder {} /** {{{Append(seq,elem)}}} */ def append(seq: TBuilderInstruction, elem: TBuilderInstruction): TBuilderInstruction = diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala index 293748f3ff..c1e9b6c3e1 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/SetBuilder.scala @@ -14,7 +14,7 @@ import scalaz.Scalaz._ * Jure Kukovec */ trait SetBuilder { - private val unsafeBuilder = new UnsafeSetBuilder + private val unsafeBuilder = new UnsafeSetBuilder {} /** * {{{ diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala index 1d6de793ad..9be47382c7 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/TemporalBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeTemporalBuilder * Jure Kukovec */ trait TemporalBuilder { - private val unsafeBuilder = new UnsafeTemporalBuilder + private val unsafeBuilder = new UnsafeTemporalBuilder {} /** {{{[]P}}} */ def box(P: TBuilderInstruction): TBuilderInstruction = P.map(unsafeBuilder.box) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala index 80914ec431..7295ace16c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/subbuilder/VariantBuilder.scala @@ -12,7 +12,7 @@ import at.forsyte.apalache.tla.typecomp.unsafe.UnsafeVariantBuilder * Jure Kukovec */ trait VariantBuilder { - private val unsafeBuilder = new UnsafeVariantBuilder + private val unsafeBuilder = new UnsafeVariantBuilder {} /** * {{{Variant(tagName, value): targetVariantType}}} diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala index 00fc856656..b968f16b1c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeActionBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaActionOper * @author * Jure Kukovec */ -class UnsafeActionBuilder extends ProtoBuilder { +trait UnsafeActionBuilder extends ProtoBuilder { /** {{{e'}}} */ def prime(e: TlaEx): TlaEx = buildBySignatureLookup(TlaActionOper.prime, e) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala index 42c63bce5a..0808c85ea3 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheBuilder.scala @@ -10,11 +10,9 @@ import at.forsyte.apalache.tla.lir.values.TlaInt * @author * Jure Kukovec */ -class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA integers from Scala ints - private val intBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaInt: BigInt => TlaEx = intBuilder.int +trait UnsafeApalacheBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + val strict: Boolean + // We extend LiteralBuilder to make TLA integers from Scala ints /** * {{{lhs := rhs}}} @@ -40,7 +38,7 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui */ def gen(n: BigInt, t: TlaType1): TlaEx = { if (strict) require(n > 0, s"Expected n to be positive, found $n.") - OperEx(ApalacheOper.gen, mkTlaInt(n))(Typed(t)) + OperEx(ApalacheOper.gen, int(n))(Typed(t)) } /** @@ -53,7 +51,7 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui def repeat(F: TlaEx, n: BigInt, x: TlaEx): TlaEx = { if (strict) require(n > 0, s"Expected n to be positive, found $n.") if (strict) require(isNaryPassByName(n = 2)(F), s"Expected F to be a binary operator passed by name, found $F.") - buildBySignatureLookup(ApalacheOper.repeat, F, mkTlaInt(n), x) + buildBySignatureLookup(ApalacheOper.repeat, F, int(n), x) } /** @@ -116,7 +114,7 @@ class UnsafeApalacheBuilder(private val strict: Boolean = true) extends ProtoBui require(n >= 0, s"Expected n to be nonnegative, found $n.") require(isNaryPassByName(n = 1)(F), s"Expected F to be a unary operator passed by name, found $F.") } - buildBySignatureLookup(ApalacheOper.mkSeq, mkTlaInt(n), F) + buildBySignatureLookup(ApalacheOper.mkSeq, int(n), F) } /** diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala index 68fdcf22d7..6b12d9000c 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeApalacheInternalBuilder.scala @@ -9,11 +9,8 @@ import at.forsyte.apalache.tla.lir.oper.{ApalacheInternalOper, TlaOper} * @author * Jure Kukovec */ -class UnsafeApalacheInternalBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from Scala strings - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeApalacheInternalBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend LiteralBuilder to make TLA strings from Scala strings /** * {{{__NotSupportedByModelChecker(msg): t}}} @@ -22,7 +19,7 @@ class UnsafeApalacheInternalBuilder extends ProtoBuilder { * argument. */ def notSupportedByModelChecker(msg: String, tt: TlaType1): TlaEx = - OperEx(ApalacheInternalOper.notSupportedByModelChecker, mkTlaStr(msg))(Typed(tt)) + OperEx(ApalacheInternalOper.notSupportedByModelChecker, str(msg))(Typed(tt)) /** * distinct diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala index 7a6e1dcdba..cd4fc08636 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeArithmeticBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaArithOper * @author * Jure Kukovec */ -class UnsafeArithmeticBuilder extends ProtoBuilder { +trait UnsafeArithmeticBuilder extends ProtoBuilder { /** {{{x + y}}} */ def plus(x: TlaEx, y: TlaEx): TlaEx = buildBySignatureLookup(TlaArithOper.plus, x, y) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala index 24ed493673..8da8399d03 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBaseBuilder.scala @@ -11,11 +11,8 @@ import at.forsyte.apalache.tla.types.{Substitution, TypeUnifier, TypeVarPool} * @author * Jure Kukovec */ -class UnsafeBaseBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from Scala strings - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeBaseBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend the LiteralBuilder to make TLA strings from Scala strings /** {{{lhs = rhs}}} */ def eql(lhs: TlaEx, rhs: TlaEx): TlaEx = buildBySignatureLookup(TlaOper.eq, lhs, rhs) @@ -84,7 +81,7 @@ class UnsafeBaseBuilder extends ProtoBuilder { */ def label(ex: TlaEx, args: String*): TlaEx = { require(args.nonEmpty, s"args must be nonempty.") - val argsAsStringExs = args.map { mkTlaStr } + val argsAsStringExs = args.map { str } buildBySignatureLookup(TlaOper.label, ex +: argsAsStringExs: _*) } } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala index 48dfcb446d..5ff07224d4 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeBoolBuilder.scala @@ -10,7 +10,7 @@ import at.forsyte.apalache.tla.typecomp.BuilderUtil * @author * Jure Kukovec */ -class UnsafeBoolBuilder extends ProtoBuilder { +trait UnsafeBoolBuilder extends ProtoBuilder { /** {{{args[0] /\ ... /\ args[n]}}} */ def and(args: TlaEx*): TlaEx = buildBySignatureLookup(TlaBoolOper.and, args: _*) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala index 6b016cced2..5d55941202 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeControlBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaControlOper * @author * Jure Kukovec */ -class UnsafeControlBuilder extends ProtoBuilder { +trait UnsafeControlBuilder extends ProtoBuilder { /** {{{IF p THEN A ELSE B}}} */ def ite(p: TlaEx, A: TlaEx, B: TlaEx): TlaEx = buildBySignatureLookup(TlaControlOper.ifThenElse, p, A, B) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala index 2e26ca8a59..6d7e258d18 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFiniteSetBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaFiniteSetOper * @author * Jure Kukovec */ -class UnsafeFiniteSetBuilder extends ProtoBuilder { +trait UnsafeFiniteSetBuilder extends ProtoBuilder { /** {{{IsFiniteSet(set)}}} */ def isFiniteSet(set: TlaEx): TlaEx = buildBySignatureLookup(TlaFiniteSetOper.isFiniteSet, set) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala index f2b4bfa763..e596000136 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeFunBuilder.scala @@ -16,11 +16,8 @@ import scala.collection.immutable.SortedMap * @author * Jure Kukovec */ -class UnsafeFunBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from Scala strings - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeFunBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend the LiteralBuilder to make TLA strings from Scala strings private def formRecordFieldTypes(args: Seq[TlaEx]): SortedMap[String, TlaType1] = { require(TlaFunOper.rec.arity.cond(args.size), s"Expected record args to have even arity, found $args.") @@ -57,7 +54,7 @@ class UnsafeFunBuilder extends ProtoBuilder { def rowRec(rowVar: Option[VarT1], args: (String, TlaEx)*): TlaEx = { // _recMixed does all the require checks val flatArgs = args.flatMap { case (k, v) => - Seq(mkTlaStr(k), v) + Seq(str(k), v) } rowRecMixed(rowVar, flatArgs: _*) } @@ -82,7 +79,7 @@ class UnsafeFunBuilder extends ProtoBuilder { def rec(args: (String, TlaEx)*): TlaEx = { // _recMixed does all the require checks val flatArgs = args.flatMap { case (k, v) => - Seq(mkTlaStr(k), v) + Seq(str(k), v) } recMixed(flatArgs: _*) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala index 058d0dff38..cef4cedcad 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeLiteralAndNameBuilder.scala @@ -11,7 +11,7 @@ import at.forsyte.apalache.tla.types.ModelValueHandler * @author * Jure Kukovec */ -class UnsafeLiteralAndNameBuilder { +trait UnsafeLiteralAndNameBuilder { /** {{{i : Int}}} */ def int(i: BigInt): TlaEx = ValEx(TlaInt(i))(Typed(IntT1)) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala index 8dee27c310..55ccf2c1b0 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSeqBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.oper.TlaSeqOper * @author * Jure Kukovec */ -class UnsafeSeqBuilder extends ProtoBuilder { +trait UnsafeSeqBuilder extends ProtoBuilder { /** {{{Append(seq,elem)}}} */ def append(seq: TlaEx, elem: TlaEx): TlaEx = buildBySignatureLookup(TlaSeqOper.append, seq, elem) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala index 8c852397f1..f422985fdc 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeSetBuilder.scala @@ -14,11 +14,8 @@ import scala.collection.immutable.SortedMap * @author * Jure Kukovec */ -class UnsafeSetBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from Scala strings - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeSetBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend the LiteralBuilder to make TLA strings from Scala strings /** * {{{ @@ -109,7 +106,7 @@ class UnsafeSetBuilder extends ProtoBuilder { def recSet(kvs: (String, TlaEx)*): TlaEx = { // _recSetMixed does all the require checks val args = kvs.flatMap { case (k, v) => - Seq(mkTlaStr(k), v) + Seq(str(k), v) } recSetMixed(args: _*) } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala index 38e1139f26..fb5aa72f73 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeTemporalBuilder.scala @@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir.{NameEx, TlaEx} * @author * Jure Kukovec */ -class UnsafeTemporalBuilder extends ProtoBuilder { +trait UnsafeTemporalBuilder extends ProtoBuilder { /** {{{[]P}}} */ def box(P: TlaEx): TlaEx = buildBySignatureLookup(TlaTempOper.box, P) diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala index 2d8d2a3a5e..a344cd8cc6 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/typecomp/unsafe/UnsafeVariantBuilder.scala @@ -12,11 +12,8 @@ import at.forsyte.apalache.tla.typecomp.{BuilderUtil, PartialSignature} * @author * Jure Kukovec */ -class UnsafeVariantBuilder extends ProtoBuilder { - - // We borrow the LiteralBuilder to make TLA strings from name tags (Scala strings) - private val strBuilder = new UnsafeLiteralAndNameBuilder - private def mkTlaStr: String => TlaEx = strBuilder.str +trait UnsafeVariantBuilder extends ProtoBuilder with UnsafeLiteralAndNameBuilder { + // We extend the LiteralBuilder to make TLA strings from name tags (Scala strings) /** * {{{Variant(tagName, value): targetVariantType}}} @@ -35,7 +32,7 @@ class UnsafeVariantBuilder extends ProtoBuilder { } val sig = completePartial(VariantOper.variant.name, partialSig) - BuilderUtil.composeAndValidateTypes(VariantOper.variant, sig, mkTlaStr(tagName), value) + BuilderUtil.composeAndValidateTypes(VariantOper.variant, sig, str(tagName), value) } /** {{{VariantFilter(tagName, set)}}} */ @@ -46,7 +43,7 @@ class UnsafeVariantBuilder extends ProtoBuilder { } val sig = completePartial(VariantOper.variantFilter.name, partialSig) - BuilderUtil.composeAndValidateTypes(VariantOper.variantFilter, sig, mkTlaStr(tagName), set) + BuilderUtil.composeAndValidateTypes(VariantOper.variantFilter, sig, str(tagName), set) } /** {{{VariantTag(variant)}}} */ @@ -59,7 +56,7 @@ class UnsafeVariantBuilder extends ProtoBuilder { case Seq(StrT1, VariantT1(RowT1(fields, _)), a) if fields.get(tagName).contains(a) => a } val sig = completePartial(VariantOper.variantGetOrElse.name, partialSig) - BuilderUtil.composeAndValidateTypes(VariantOper.variantGetOrElse, sig, mkTlaStr(tagName), variant, defaultValue) + BuilderUtil.composeAndValidateTypes(VariantOper.variantGetOrElse, sig, str(tagName), variant, defaultValue) } /** {{{VariantGetUnsafe(tagName, variant)}}} */ @@ -69,6 +66,6 @@ class UnsafeVariantBuilder extends ProtoBuilder { case Seq(StrT1, VariantT1(RowT1(fields, _))) if fields.contains(tagName) => fields(tagName) } val sig = completePartial(VariantOper.variantGetUnsafe.name, partialSig) - BuilderUtil.composeAndValidateTypes(VariantOper.variantGetUnsafe, sig, mkTlaStr(tagName), variant) + BuilderUtil.composeAndValidateTypes(VariantOper.variantGetUnsafe, sig, str(tagName), variant) } } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala index bbd898b721..d39d3a411e 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/types/package.scala @@ -1,5 +1,7 @@ package at.forsyte.apalache.tla +import at.forsyte.apalache.tla.lir.TlaEx + /** * Defines a premade instance of [[at.forsyte.apalache.tla.typecomp.ScopedBuilder ScopedBuilder]], named [[tla]]. * @@ -132,6 +134,9 @@ package object types { import at.forsyte.apalache.tla.typecomp._ + type BuilderT = TBuilderInstruction + type BuilderUT = TlaEx + /** * A short-hand to the instance of the typed builder, so one can easily construct expressions. * @@ -150,4 +155,5 @@ package object types { * [[at.forsyte.apalache.tla.typecomp.ScopedBuilder ScopedBuilder]] for implementation details. */ val tla: ScopedBuilder = new ScopedBuilder(strict = true) + val tlaU: ScopeUnsafeBuilder = new ScopeUnsafeBuilder(strict = true) } diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala index f8e4cf684a..c61d3035ea 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestApalacheBuilder.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.typecomp import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.ApalacheOper -import at.forsyte.apalache.tla.types.tla.TypedParam +import at.forsyte.apalache.tla.typecomp.ParamUtil.TypedParam import org.junit.runner.RunWith import org.scalatestplus.junit.JUnitRunner import scalaz.unused diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala index 0b6400fd95..809da08b76 100644 --- a/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala +++ b/tlair/src/test/scala/at/forsyte/apalache/tla/typecomp/TestHybrid.scala @@ -2,7 +2,7 @@ package at.forsyte.apalache.tla.typecomp import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper.{TlaActionOper, TlaBoolOper, TlaOper} -import at.forsyte.apalache.tla.types.tla.TypedParam +import at.forsyte.apalache.tla.typecomp.ParamUtil.TypedParam import org.junit.runner.RunWith import org.scalacheck.Prop.forAll import org.scalatestplus.junit.JUnitRunner