closes #41, closes #112

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

@@ -21,23 +21,40 @@ class SubstTranslator(sourceStore: SourceStore, context: Context) extends LazyLo
   }
 
   private def subExpr(renaming: Map[String, TlaEx], ex: TlaEx): TlaEx = {
-    def subRec(ex: TlaEx): TlaEx = ex match {
-      case NameEx(name) =>
-        renaming.getOrElse(name, NameEx(name))
+    def subRec(ex: TlaEx): TlaEx = {
+      val newEx =
+        ex match {
+          case NameEx(name) =>
+            renaming.getOrElse(name, NameEx(name))
 
-      case LetInEx( body, defs@_* ) =>
-        def subDecl( d : TlaOperDecl ) = d.copy( body = subRec( d.body ) )
-        LetInEx( subRec(body), defs map subDecl :_*)
+          case LetInEx(body, defs@_*) =>
+            def subDecl(d: TlaOperDecl) = {
+              d.copy(body = subRec(d.body))
+            }
 
-      case OperEx(op, args@_*) =>
-        if (renaming.nonEmpty
-          && Seq(TlaActionOper.enabled, TlaActionOper.composition, TlaTempOper.leadsTo).exists(_.name == op.name)) {
-          // TODO: find out how to deal with ENABLED and other tricky operators
-          logger.warn("Substitution of %s needs care. The current implementation may fail to work.".format(op.name))
+            LetInEx(subRec(body), defs map subDecl: _*)
+
+          case OperEx(op, args@_*) =>
+            if (renaming.nonEmpty
+              && Seq(TlaActionOper.enabled, TlaActionOper.composition, TlaTempOper.leadsTo).exists(_.name == op.name)) {
+              // TODO: find out how to deal with ENABLED and other tricky operators
+              logger.warn("Substitution of %s needs care. The current implementation may fail to work.".format(op.name))
+            }
+            OperEx(op, args map subRec: _*)
+
+          case d => d
         }
-        OperEx(op, args map subRec: _*)
 
-      case d => d
+      // copy the source info
+      sourceStore.find(ex.ID) match {
+        case Some(loc) =>
+          sourceStore.add(newEx.ID, loc)
+
+        case None =>
+          logger.warn("No source for expr@" + ex.ID)
+      }
+      // return
+      newEx
     }
 
     subRec(ex)
@@ -63,7 +80,7 @@ class SubstTranslator(sourceStore: SourceStore, context: Context) extends LazyLo
 }
 
 object SubstTranslator {
-  def apply(sourceStore: SourceStore, context: Context) : SubstTranslator = {
+  def apply(sourceStore: SourceStore, context: Context): SubstTranslator = {
     new SubstTranslator(sourceStore, context)
   }
 }

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

@@ -1,14 +1,14 @@
 package at.forsyte.apalache.tla.imp.passes
 
-import java.io.{File, FileWriter, PrintWriter}
+import java.io.File
 import java.nio.file.Path
 
 import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin}
 import at.forsyte.apalache.tla.imp.SanyImporter
 import at.forsyte.apalache.tla.imp.src.SourceStore
 import at.forsyte.apalache.tla.lir.TlaModule
-import at.forsyte.apalache.tla.lir.io.PrettyWriter
-import at.forsyte.apalache.tla.lir.io.JsonWriter
+import at.forsyte.apalache.tla.lir.io.{JsonWriter, PrettyWriter}
+import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
 import com.google.inject.Inject
 import com.google.inject.name.Named
 import com.typesafe.scalalogging.LazyLogging
@@ -48,6 +48,11 @@ class SanyParserPassImpl @Inject()(val options: PassOptions,
       val outdir = options.getOrError("io", "outdir").asInstanceOf[Path]
       PrettyWriter.write(rootModule.get, new File(outdir.toFile, "out-parser.tla"))
       JsonWriter.write(rootModule.get, new File(outdir.toFile, "out-parser.json"))
+
+      if (options.getOrElse("general", "debug", false)) {
+        val sourceLocator = SourceLocator(sourceStore.makeSourceMap, new ChangeListener())
+        rootModule.get.operDeclarations foreach sourceLocator.checkConsistency
+      }
     }
     rootModule.isDefined
   }

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

@@ -1093,6 +1093,7 @@ class TestSanyImporter extends FunSuite {
       _.name == "A"
     }.collect {
       case TlaOperDecl(_, _, LetInEx(body, defs@_*)) =>
+        assert(locationStore.contains(body.ID))
         assert(3 == defs.length)
         val xDecl = defs.head
         assert("X" == xDecl.name)
@@ -1462,6 +1463,40 @@ class TestSanyImporter extends FunSuite {
     assert(expected == bOfM.asInstanceOf[TlaOperDecl].body)
   }
 
+  // regression for #112
+  test("LET-IN inside INSTANCE") {
+    val text =
+      """---- MODULE letInInstance ----
+        |---- MODULE M ----
+        |VARIABLE x
+        |a ==
+        |  LET b == {} IN
+        |  b
+        |================================
+        |VARIABLE x
+        |INSTANCE M
+        |================================
+        |""".stripMargin
+
+    val sourceStore = new SourceStore
+    val (rootName, modules) = new SanyImporter(sourceStore)
+      .loadFromSource("letInInstance", Source.fromString(text))
+    assert(1 == modules.size)
+    // the root module and naturals
+    val root = modules(rootName)
+    // we strip away the operator declarations by Naturals
+    assert(2 == root.declarations.size)
+    val aOfM = root.declarations(1)
+    aOfM.asInstanceOf[TlaOperDecl].body match {
+      case LetInEx(body, bDecl) =>
+        assert(sourceStore.contains(body.ID))
+        assert(sourceStore.contains(bDecl.body.ID))
+
+      case _ =>
+        fail("expected declaration of b")
+    }
+  }
+
   // this test fails for the moment
   ignore("RECURSIVE operator inside INSTANCE") {
     val text =

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/AbstractTransformer.scala

@@ -22,8 +22,17 @@ abstract class AbstractTransformer(tracker: TransformationTracker) extends TlaEx
     * @return a new expression
     */
   def transform: TlaExTransformation = tracker.track {
-    case OperEx(op, args @ _*) =>
-      transformOneLevel(OperEx(op, args map transform :_*))
+    case oper @ OperEx(op, args @ _*) =>
+      val newArgs = args map transform
+      val newOper =
+        if (newArgs.map(_.ID) != args.map(_.ID)) {
+          // Introduce a new operator only if the arguments have changed.
+          // Otherwise, we would introduce lots of redundant chains in ChangeListener.
+          tracker.hold(oper, OperEx(op, newArgs: _*)) // fixes #41
+        } else {
+          oper
+        }
+      transformOneLevel(newOper)
 
     case LetInEx(body, defs @ _*) =>
       def mapDecl(d: TlaOperDecl): TlaOperDecl = {

tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/passes/PreproPassImpl.scala

@@ -4,8 +4,10 @@ import java.io.File
 import java.nio.file.Path
 
 import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin}
+import at.forsyte.apalache.tla.imp.src.SourceStore
 import at.forsyte.apalache.tla.lir.TlaModule
 import at.forsyte.apalache.tla.lir.io.PrettyWriter
+import at.forsyte.apalache.tla.lir.storage.{ChangeListener, SourceLocator}
 import at.forsyte.apalache.tla.lir.transformations.{TlaModuleTransformation, TransformationTracker}
 import at.forsyte.apalache.tla.lir.transformations.standard._
 import at.forsyte.apalache.tla.pp.{Desugarer, Keramelizer, Normalizer, UniqueNameGenerator}
@@ -24,6 +26,8 @@ class PreproPassImpl @Inject()( val options: PassOptions,
                                 gen: UniqueNameGenerator,
                                 renaming: IncrementalRenaming,
                                 tracker: TransformationTracker,
+                                sourceStore: SourceStore,
+                                changeListener: ChangeListener,
                                 @Named("AfterPrepro") nextPass: Pass with TlaModuleMixin)
     extends PreproPass with LazyLogging {
 
@@ -67,8 +71,13 @@ class PreproPassImpl @Inject()( val options: PassOptions,
     // dump the result of preprocessing
     val outdir = options.getOrError("io", "outdir").asInstanceOf[Path]
     PrettyWriter.write(afterModule, new File(outdir.toFile, "out-prepro.tla"))
-
     outputTlaModule = Some(afterModule)
+
+    if (options.getOrElse("general", "debug", false)) {
+      val sourceLocator = SourceLocator(sourceStore.makeSourceMap, changeListener)
+      outputTlaModule.get.operDeclarations foreach sourceLocator.checkConsistency
+    }
+
     true
   }
 

tlair/pom.xml

@@ -31,6 +31,12 @@
             <artifactId>scalatest_${scalaBinaryVersion}</artifactId>
             <scope>test</scope>
         </dependency>
+
+        <dependency>
+            <groupId>com.typesafe.scala-logging</groupId>
+            <artifactId>scala-logging_2.12</artifactId>
+        </dependency>
+
         <!-- https://mvnrepository.com/artifact/org.scalaz/scalaz-core -->
         <dependency>
             <groupId>org.scalaz</groupId>

tlair/src/main/scala/at/forsyte/apalache/tla/lir/storage/SourceLocator.scala

@@ -1,19 +1,53 @@
 package at.forsyte.apalache.tla.lir.storage
 
-import at.forsyte.apalache.tla.lir.{TlaEx, UID}
+import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.src.SourceLocation
+import com.typesafe.scalalogging.LazyLogging
 
 /**
   * SourceLocator is used to identify locations in the original .tla specification,
   * from which a given expression, possibly derived from a transformation, originates.
   */
-sealed case class SourceLocator(
-                                 sourceMap : SourceMap,
-                                 changeListener : ChangeListener
-                               ) {
+sealed case class SourceLocator(sourceMap : SourceMap,
+                                changeListener : ChangeListener) extends LazyLogging {
   def sourceOf( id : UID ) : Option[SourceLocation] =
     sourceMap.get( changeListener.traceBack( id ) )
 
   def sourceOf( ex : TlaEx ) : Option[SourceLocation] =
     sourceOf( ex.ID )
+
+
+  /**
+    * A debugging method that recursively checks whether all subexpressions of the operator body have source information.
+    * When this is not the case, the function prints ids of the topmost problematic expressions.
+    * This method may be quite slow, so it should be used in the debugging mode only.
+    */
+  def checkConsistency(decl: TlaOperDecl): Unit = {
+    checkConsistency(decl.body)
+  }
+
+  /**
+    * A debugging method that recursively checks whether all subexpressions of an expression have source information.
+    * When this is not the case, the function prints ids of the topmost problematic expressions.
+    * This method may be quite slow, so it should be used in the debugging mode only.
+    */
+  def checkConsistency(ex: TlaEx): Unit = {
+    if (sourceOf(ex).isEmpty) {
+      var str = ex.toString
+      str = if (str.length > 70) str.substring(0, 69) + "..." else str
+      logger.error("No source for expr@%s: %s".format(ex.ID, str))
+    } else {
+      ex match {
+        case OperEx(_, args @ _*) =>
+          args foreach checkConsistency
+
+        case LetInEx(body, decls @ _*) =>
+          checkConsistency(body)
+          decls.foreach(d => checkConsistency(d.body))
+
+        case _ => // do nothing
+      }
+    }
+  }
+
 }

tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/TransformationTracker.scala

@@ -1,11 +1,33 @@
 package at.forsyte.apalache.tla.lir.transformations
 
+import at.forsyte.apalache.tla.lir.TlaEx
+
 /**
   * An implementation of this trait wraps an expression transformer with the code that somehow tracks the transformation.
   * For instance, it can wrap a transformation with calls to transformation listeners.
   *
   * @author Igor Konnov
   */
 trait TransformationTracker {
-  def track(t: TlaExTransformation): TlaExTransformation
+  /**
+    * Decorate a transformation with a tracker.
+    * @param tr an expression transformation
+    * @return a new transformation that applies tr and tracks the changes
+    */
+  def track(tr: TlaExTransformation): TlaExTransformation
+
+  /**
+    * Sometimes, one has to track a change in a temporary expression that will get transformed into something else
+    * before it gets a chance to get tracked with `track`, which only works with end-to-end transformations.
+    * In this case, we have to record the change as a side effect and return the new expression.
+    * Avoid using this method by default. This is a second-chance method.
+    *
+    * @param from the original expression
+    * @param to the new expression
+    * @return the new expression
+    */
+  def hold(from: TlaEx, to: TlaEx): TlaEx = {
+    def tr(f : TlaEx): TlaEx = to
+    track(tr)(from)
+  }
 }

tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/IncrementalRenaming.scala

@@ -149,17 +149,12 @@ class IncrementalRenaming @Inject()(tracker : TransformationTracker) extends Tla
     */
   private def getNextUniqueFromBase( name: String ) = getNextUnique( getBase( name ) )
 
-  /**
-    * Returns y, but establishes tracking between x and y. Needed for better granularity of tracking.
-    */
-  private def trackedSubstitution( x : TlaEx, y : TlaEx ) = tracker.track( _ => y )( x )
-
   private def rename( alreadyRenamed: Map[String,String] ): TlaExTransformation = tracker.track {
     case ex @ NameEx(name) =>
       // If a name has been marked for replacement (i.e. is an entry in alreadyRenamed)
       // we simply substitute in the pre-computed new name
       if ( alreadyRenamed.contains( name ) )
-        trackedSubstitution( ex, NameEx( alreadyRenamed( name ) ) )
+        tracker.hold( ex, NameEx( alreadyRenamed( name ) ) )
       else
         ex
 
@@ -175,7 +170,8 @@ class IncrementalRenaming @Inject()(tracker : TransformationTracker) extends Tla
       val newName = getNextUniqueFromBase( name )
       val newRenamed = alreadyRenamed + ( name -> newName )
       val newArgs = otherArgs.map( rename( newRenamed ) )
-      OperEx( op, trackedSubstitution( nex, NameEx( newName ) ) +: newArgs : _* )
+      val trackedName = tracker.hold(nex, NameEx(newName))
+      OperEx( op, trackedName +: newArgs : _* )
 
     // Certain operators introduce several bound variables at once
     case OperEx( op, result, varsAndSets@_* )