fix 295: support for LOCAL INSTANCE Sequences

CHANGES.md

@@ -1,5 +1,7 @@
 ## Unreleased #unstable
-
+
+ * support for standard modules that are instantiated with LOCAL INSTANCE, see #295
+ * support for LAMBDAs, see #285 and #289
  * no theories in the model checker due to types, see #22
  * operators and checker caches made Serializable
  * better diagnostics for the recursive operators, see #272 

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

@@ -41,12 +41,15 @@ class OpApplTranslator(sourceStore: SourceStore, val context: Context, val recSt
       val oper = node.getOperator
       // non-constant operators
       oper.getKind match {
+          // an operator that is at the core of TLA+, e.g., { 1 }, \A x \in S: e
         case ASTConstants.BuiltInKind =>
           translateBuiltin(node)
 
+          // an operator parameter that must be an operator itself
         case ASTConstants.FormalParamKind =>
           translateFormalParam(node)
 
+          // either a user-defined operator or an operator from the standard library, e.g., Sequences
         case ASTConstants.UserDefinedOpKind =>
           translateUserOperator(node)
 
@@ -58,15 +61,68 @@ class OpApplTranslator(sourceStore: SourceStore, val context: Context, val recSt
 
   /////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
 
-  // call to a user-defined operator, either a LOCAL one, or not
-  private def translateUserOperator(node: OpApplNode) = {
-    if (node.getOperator.isLocal) {
-      translateLocalOperator(node)
+  // call to a user-defined operator (may come from the standard library), either a LOCAL one, or not
+  private def translateUserOperator(applyNode: OpApplNode) = {
+    if (!applyNode.getOperator.isLocal) {
+      translateNonLocalUserOperator(applyNode)
     } else {
-      translateNonLocalUserOperator(node)
+      // issue 295: https://github.com/informalsystems/apalache/issues/295
+      // LOCAL operators may originate from the standard library :face_palm
+      // For instance, if the user writes LOCAL INSTANCE Sequences
+      applyNode.getOperator match {
+        case opdef: OpDefNode =>
+            // translate as an application of a standard library operator
+          translateLocalLibraryOperatorOrValue(opdef, applyNode)
+            .getOrElse {
+              // or as an application of a local user-defined operator
+              translateLocalOperator(opdef, applyNode)
+            }
+
+        case _ =>
+          val msg = "Expected a LOCAL operator defined with OpDefNode, found: " + applyNode.getOperator.getClass
+          throw new SanyImporterException(msg)
+      }
+    }
+  }
+
+  // call an operator or a value (e.g., Sequences!Append or Integers!Int) from a standard module
+  // that is instantiated with LOCAL INSTANCE
+  private def translateLocalLibraryOperatorOrValue(opdef: OpDefNode, applyNode: OpApplNode): Option[TlaEx] = {
+    val source = opdef.getSource
+    if (source == null || source.getOriginallyDefinedInModuleNode == null) {
+      None
+    } else {
+      val operatorName = source.getName.toString
+      // the original module, in which the operator is defined
+      val modName = source.getOriginallyDefinedInModuleNode.getName.toString
+      StandardLibrary.libraryOperators.get((modName, operatorName)).map {
+            // a library operator
+        tlaOper =>
+          val exTran = ExprOrOpArgNodeTranslator(sourceStore, context, recStatus)
+          val args = applyNode.getArgs.toList.map { p => exTran.translate(p) }
+          OperEx(tlaOper, args: _*)
+      }.orElse {
+            // a library value
+        StandardLibrary.libraryValues.get((modName, operatorName)).map(ValEx)
+      }
     }
   }
 
+  // call a user-defined operator that is defined locally
+  private def translateLocalOperator(opdef: OpDefNode, node: OpApplNode): TlaEx = {
+    /* Since we do not know the original location of the local operator,
+       we can only re-define it with a LET-IN expression */
+    // translate the declaration of the LOCAL operator
+    val decl = OpDefTranslator(sourceStore, context).translate(opdef)
+    // translate its arguments
+    val exTran = ExprOrOpArgNodeTranslator(sourceStore, context, recStatus)
+    val args = node.getArgs.toList.map { p => exTran.translate(p) }
+    // apply the operator by its name
+    val app = OperEx(TlaOper.apply, NameEx(decl.name) +: args: _*)
+    // return the expression LET F(..) = .. IN F(args)
+    LetInEx(app, decl)
+  }
+
   // call a user-defined operator that is not defined with LOCAL
   private def translateNonLocalUserOperator(node: OpApplNode) = {
     val opcode = node.getOperator.getName.toString
@@ -109,28 +165,6 @@ class OpApplTranslator(sourceStore: SourceStore, val context: Context, val recSt
     }
   }
 
-  // call a user-defined operator that is defined locally
-  private def translateLocalOperator(node: OpApplNode): TlaEx = {
-    /* Since we do not know the original location of the local operator,
-       we can only re-define it with a LET-IN expression */
-    node.getOperator match {
-      case opdef: OpDefNode =>
-        // translate the declaration of the LOCAL operator
-        val decl = OpDefTranslator(sourceStore, context).translate(opdef)
-        // translate its arguments
-        val exTran = ExprOrOpArgNodeTranslator(sourceStore, context, recStatus)
-        val args = node.getArgs.toList.map { p => exTran.translate(p) }
-        // apply the operator by its name
-        val app = OperEx(TlaOper.apply, NameEx(decl.name) +: args: _*)
-        // return the expression LET F(..) = .. IN F(args)
-        LetInEx(app, decl)
-
-      case _ =>
-        val msg = "Expected a LOCAL operator defined with OpDefNode, found: " + node.getOperator.getClass
-        throw new SanyImporterException(msg)
-    }
-  }
-
   // translate an operator application that uses a parameter operator, i.e.,
   // in A(B(_)) == B(1), translate the application B(1)
   private def translateFormalParam(node: OpApplNode): TlaEx = {

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

@@ -2147,6 +2147,61 @@ class TestSanyImporter extends FunSuite {
     }
   }
 
+  test("operators of local instances of the standard modules") {
+    // Issue #295: the built-in operators are not eliminated when using LOCAL INSTANCE
+    val text =
+      """---- MODULE issue295 ----
+        |---- MODULE A ----
+        |LOCAL INSTANCE Sequences
+        |A == Append(<<>>, {})
+        |==================
+        |INSTANCE A
+        |================================
+        |""".stripMargin
+
+    val locationStore = new SourceStore
+    val (rootName, modules) = new SanyImporter(locationStore)
+      .loadFromSource("issue295", Source.fromString(text))
+    // the root module and naturals
+    val root = modules(rootName)
+    // the definitions of the standard operators are filtered out
+    assert(1 == root.declarations.size)
+    root.declarations(0) match {
+      case TlaOperDecl("A", _, body) =>
+        assert(append(tuple(), enumSet()) == body)
+
+      case d => fail("unexpected declaration: " + d)
+    }
+  }
+
+  test("values of local instances of the standard modules") {
+    // Issue #295: the built-in operators are not eliminated when using LOCAL INSTANCE
+    val text =
+      """---- MODULE issue295 ----
+        |---- MODULE A ----
+        |LOCAL INSTANCE Integers
+        |A == Int
+        |==================
+        |INSTANCE A
+        |================================
+        |""".stripMargin
+
+    val locationStore = new SourceStore
+    val (rootName, modules) = new SanyImporter(locationStore)
+      .loadFromSource("issue295", Source.fromString(text))
+    // the root module and naturals
+    val root = modules(rootName)
+    // the definitions of the standard operators are filtered out
+    assert(1 == root.declarations.size)
+    root.declarations(0) match {
+      case TlaOperDecl("A", _, body) =>
+        assert(ValEx(TlaIntSet) == body)
+
+      case d => fail("unexpected declaration: " + d)
+    }
+  }
+
+
   test("ignore theorems") {
     // this proof is a garbage, just to check, whether the translator works
     val text =