fix #143: proper translation of chained substitutions in INSTANCE

tla-import/src/main/scala/at/forsyte/apalache/tla/imp/Context.scala

@@ -80,6 +80,12 @@ trait Context {
     */
   def setLookupPrefix(prefix: List[String]): Context
 
+  /**
+    * Get the lookup prefix that represents the instantiation path from the root module down to the instances
+    * @return the sequence of instance names
+    */
+  val lookupPrefix: List[String]
+
   /**
     * Add all definitions from the other context. We assume that the keys in the both contexts do not intersect.
     * If the keys intersect, an implementation is free to throw an IllegalStateException at some point...

tla-import/src/main/scala/at/forsyte/apalache/tla/imp/SubstTranslator.scala

@@ -10,8 +10,6 @@ import tla2sany.semantic._
   * Translate a module instance. This class needs extensive testing,
   * as the module instantiation rules are quite sophisticated (Ch. 17).
   *
-  * TODO: is this class actually used? If not, remove.
-  *
   * @author konnov
   */
 class SubstTranslator(sourceStore: SourceStore, context: Context) extends LazyLogging {
@@ -61,11 +59,32 @@ class SubstTranslator(sourceStore: SourceStore, context: Context) extends LazyLo
   }
 
   private def mkRenaming(substInNode: SubstInNode): Map[String, TlaEx] = {
-    val exprTranslator = ExprOrOpArgNodeTranslator(sourceStore, context, OutsideRecursion())
+    // In the substitution INSTANCE ... WITH x <- e, the expression e should be evaluated in the context one level up.
+    // Consider the following example:
+    //    ------------------- MODULE A ----------------------
+    //    ------------------- MODULE B ----------------------
+    //    ------------------- MODULE C -------------------
+    //    VARIABLE x
+    //    magic == x /= 2
+    //    ===================================================
+    //    VARIABLE y
+    //    C1 == INSTANCE C WITH x <- y
+    //    ===================================================
+    //    VARIABLE z
+    //    B1 == INSTANCE B WITH y <- z
+    //    ===================================================
+    //
+    // SANY gives us the operator B1!C1!magic == (x /= 2)[x <- y][y <- z]
+    // Note that y should be translated in the context of B1, whereas z should be translated in the root context.
+    //
+    // See issue #143: https://github.com/informalsystems/apalache/issues/143
+    val upperLookupPrefix = context.lookupPrefix.dropRight(1)
+    val upperContext = context.setLookupPrefix(upperLookupPrefix)
+    val exprTranslator = ExprOrOpArgNodeTranslator(sourceStore, upperContext, OutsideRecursion())
 
     def eachSubst(s: Subst): (String, TlaEx) = {
       val replacement = exprTranslator.translate(s.getExpr)
-      // TODO: what if a constant happens to be an operator?
+      // only constants and variables are allowed in the left-hand side of operator substitutions
       if (s.getOp.getKind != ASTConstants.ConstantDeclKind && s.getOp.getKind != ASTConstants.VariableDeclKind) {
         throw new SanyImporterException("Expected a substituted name %s to be a CONSTANT or a VARIABLE, found kind %d"
           .format(s.getOp.getName, s.getOp.getKind))

tla-import/src/test/scala/at/forsyte/apalache/tla/imp/TestSanyImporter.scala

@@ -1523,6 +1523,82 @@ class TestSanyImporter extends FunSuite {
     }
   }
 
+  // regression for #143
+  test("Lookup inside substitutions") {
+    val text =
+      """------------------- MODULE P ----------------------
+        |------------------- MODULE Vot ----------------------
+        |------------------- MODULE Cons -------------------
+        |VARIABLE chosen
+        |Init == chosen = {}
+        |Next == chosen = {2}
+        |===================================================
+        |chosen == {2}
+        |C == INSTANCE Cons
+        |===================================================
+        |V == INSTANCE Vot
+        |===================================================""".stripMargin
+
+    val sourceStore = new SourceStore
+    val (rootName, modules) = new SanyImporter(sourceStore)
+      .loadFromSource("P", Source.fromString(text))
+    assert(1 == modules.size)
+    // the root module and naturals
+    val root = modules(rootName)
+    // expect V!chosen, V!C!Init and V!C!Next
+    assert(3 == root.declarations.size)
+    val next = root.declarations.find(_.name == "V!C!Next")
+      .getOrElse(fail("V!C!Next not found"))
+    assert("V!C!Next" == next.name)
+    next.asInstanceOf[TlaOperDecl].body match {
+      case body @ OperEx(TlaOper.eq,
+                         OperEx(TlaOper.apply, NameEx("V!chosen")),
+                         OperEx(TlaSetOper.enumSet, ValEx(TlaInt(i)))) =>
+        assert(i == 2)
+        assert(sourceStore.contains(body.ID))
+
+      case _ =>
+        fail("expected V!C!Next == V!chosen = {2}")
+    }
+  }
+
+  // regression for #143
+  test("Series of substitutions") {
+    val text =
+      """------------------- MODULE A ----------------------
+        |------------------- MODULE B ----------------------
+        |------------------- MODULE C -------------------
+        |VARIABLE x
+        |magic == x /= 2
+        |===================================================
+        |VARIABLE y
+        |C1 == INSTANCE C WITH x <- y
+        |===================================================
+        |VARIABLE z
+        |B1 == INSTANCE B WITH y <- z
+        |===================================================""".stripMargin
+
+    val sourceStore = new SourceStore
+    val (rootName, modules) = new SanyImporter(sourceStore)
+      .loadFromSource("A", Source.fromString(text))
+    assert(1 == modules.size)
+    // the root module and naturals
+    val root = modules(rootName)
+    // expect B1!C1!magic and z
+    assert(2 == root.declarations.size)
+    val magic = root.declarations.find(_.name == "B1!C1!magic")
+      .getOrElse(fail("B1!C1!magic not found"))
+    assert("B1!C1!magic" == magic.name)
+    magic.asInstanceOf[TlaOperDecl].body match {
+      case body @ OperEx(TlaOper.ne, NameEx("z"), ValEx(TlaInt(i))) =>
+        assert(i == 2)
+        assert(sourceStore.contains(body.ID))
+
+      case _ =>
+        fail("expected B1!C1!magic == z /= 2")
+    }
+  }
+
   // this test fails for the moment
   ignore("RECURSIVE operator inside INSTANCE") {
     val text =