diff --git a/UNRELEASED.md b/UNRELEASED.md index bbd5ce1fa8..faa559879f 100644 --- a/UNRELEASED.md +++ b/UNRELEASED.md @@ -23,3 +23,4 @@ ### Bug fixes * Fix potential non-determinism when picking from `[S -> T]`, see #1753 + * Fix the bug in uninterpreted types, see #1792 diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/ModelValueHandler.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/ModelValueHandler.scala index e369b94485..4361bd12ba 100644 --- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/ModelValueHandler.scala +++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/ModelValueHandler.scala @@ -25,6 +25,18 @@ object ModelValueHandler { */ private val matchRegex: Regex = raw"([a-zA-Z0-9_]+)_OF_([A-Z_][A-Z0-9_]*)".r + /** + * Is the supplied string encoding a model value. + * + * @param text + * a string to test + * @return + * true, if the string encodes a model value + */ + def isModelValue(text: String): Boolean = { + typeAndIndex(text).isDefined + } + /** * Returns the type of `s`. If `s` follows the pattern for model values, its type is `ConstT1(_)`, otherwise is is a * regular string. diff --git a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala index 526d24840d..9aee3467c2 100644 --- a/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala +++ b/tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala @@ -3,9 +3,9 @@ package at.forsyte.apalache.tla.typecheck.etc import at.forsyte.apalache.io.annotations.store.{findAnnotation, AnnotationStore} import at.forsyte.apalache.io.annotations.{Annotation, AnnotationStr, StandardAnnotations} import at.forsyte.apalache.io.typecheck.parser.{DefaultType1Parser, Type1ParseError} +import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.lir.oper._ import at.forsyte.apalache.tla.lir.values._ -import at.forsyte.apalache.tla.lir._ import at.forsyte.apalache.tla.typecheck._ import com.typesafe.scalalogging.LazyLogging @@ -968,6 +968,12 @@ class ToEtcExpr( (SparseTupT1(fieldNo.toInt -> a), IntT1, a), ) + case ValEx(TlaStr(fieldName)) if ModelValueHandler.isModelValue(fieldName) => + // fieldName encodes a constant of an uninterpreted sort + val a = varPool.fresh + val uninterpretedType = ModelValueHandler.modelValueOrString(fieldName) + Seq((FunT1(uninterpretedType, a), uninterpretedType, a)) + case ValEx(TlaStr(fieldName)) => // f[s] or [f EXCEPT ![s] = ...], where s is a string literal val a = varPool.fresh diff --git a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala index bc99dd4cef..e84d27ed08 100644 --- a/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala +++ b/tla-types/src/test/scala/at/forsyte/apalache/tla/typecheck/etc/TestToEtcExpr.scala @@ -400,6 +400,17 @@ class TestToEtcExpr extends AnyFunSuite with BeforeAndAfterEach with ToEtcExprBa assert(gen(access).explain(List(), List()).isDefined) } + test("""f["1_OF_A"]""") { + // it should always be a function, because A is an uninterpreted type + val fun = Seq(parser("((A -> a), A) => a")) + val expected = mkUniqApp(fun, mkUniqName("f"), mkUniqConst(ConstT1("A"))) + val access = tla.appFun(tla.name("f"), tla.str("1_OF_A")) + assert(expected == gen(access)) + + // Has custom type error message + assert(gen(access).explain(List(), List()).isDefined) + } + test("DOMAIN f") { // DOMAIN is applied to one of the four objects: a function, a sequence, a record, or a sparse tuple val types = Seq(parser("(a -> b) => Set(a)"), parser("Seq(c) => Set(Int)"), parser("[] => Set(Str)"),