From e99605217fffaa86207cafa0ec6829c35b39e777 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@informal.systems>
Date: Fri, 20 May 2022 17:27:16 +0200
Subject: [PATCH 1/2] fix the bug in type checking uninterpreted types

---
 .../apalache/tla/typecheck/ModelValueHandler.scala   | 12 ++++++++++++
 .../apalache/tla/typecheck/etc/ToEtcExpr.scala       |  8 +++++++-
 .../apalache/tla/typecheck/etc/TestToEtcExpr.scala   | 11 +++++++++++
 3 files changed, 30 insertions(+), 1 deletion(-)

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 63ce6b1f08..e060216e1b 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 1c043b8023..bcfad4a72b 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 75f7d83c50..62a0f44281 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)"),

From 8b3b2a762d194578851d838dd2464422e4c66b50 Mon Sep 17 00:00:00 2001
From: Igor Konnov <igor@informal.systems>
Date: Fri, 20 May 2022 17:30:58 +0200
Subject: [PATCH 2/2] add release notes

---
 UNRELEASED.md | 1 +
 1 file changed, 1 insertion(+)

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