Java-like annotations in comments

UNRELEASED.md

@@ -10,3 +10,11 @@
          * Another change description, see #124
 
      DO NOT LEAVE A BLANK LINE BELOW THIS PREAMBLE -->
+### SANY importer
+
+  * parsing in-comment Java-like annotations, see #226
+  * tracking the source of variable/constant declarations and operator definitions, see #262
+
+### Documentation
+
+  * ADR004: In-comment annotations for declarations (of constants, variables, operators)

docs/src/SUMMARY.md

@@ -62,3 +62,4 @@
 # Design Documents
 
 - [ADR-002: types and type annotations](./adr/002adr-types.md)
+- [ADR-004: code annotations](./adr/004adr-annotations.md)

docs/src/adr/004adr-annotations.md

@@ -0,0 +1,136 @@
+# ADR-004: Syntax for Java-like annotations in comments
+
+**author:** Igor Konnov
+
+This ADR documents our decision on using Java-like annotations in comments.
+Our main motivation to have annotations is to simplify type annotations, as
+presented in [ADR-002][]. Hence, in the following text, we are using
+examples for type annotations. However, the annotations framework is not
+restricted to types. Similar to Java and Scala, we can use annotations
+to decorate operators with hints, which may aid the model checker.
+
+## 1. What can be annotated
+
+Annotations should be written in comments that are written in front of a
+declaration. The following declarations are supported:
+
+ 1. Constant declarations, e.g., `CONSTANT N`.
+ 1. Variable declarations, e.g., `VARIABLE x`.
+ 1. Top-level operator declarations, e.g., `Foo(x) == e`.
+ 1. LET-IN operator declarations, e.g., `Foo(x) == LET Inner(y) == e IN f`.
+ 1. Recursive functions, e.g., `foo[i \in Int] == e`.
+ 1. Recursive operators, that are declared either at the top-level or by using
+    LET-IN.
+
+For an example, see Section 3.
+
+
+## 2. Annotations syntax
+
+An annotation is a string that follows the grammar (question mark denotes
+optional rules):
+
+```
+Annotation  ::= '@' javaIdentifier ( '(' ArgList? ')' )?
+ArgList     ::= (Arg) ( ',' Arg )*
+Arg         ::= (string | integer | boolean)
+string      ::= '"' <char sequence> '"'
+integer     ::= '-'? [0-9]+
+boolean     ::= ('false' | 'true')
+```
+
+Java Language Specification defines how a [Java identifier] looks like.
+The sequence `<char sequence>` is a sequence admitted by [JavaTokenParsers]:
+
+  - Any character except double quotes, control characters or backslash `\`
+  - A backslash followed by another backslash, a single or double quote,
+    or one of the letters `b`, `f`, `n`, `r` or `t`
+  - `\` followed by u followed by four hexadecimal digits
+
+**Examples.** The following strings are examples of syntactically correct
+annotations:
+
+ - `@tailrec`
+ - `@type("(Int, Int) => Int")`
+ - `@random(true)`
+ - `@deprecated("Use operator Foo instead")`
+ - `@range(0, 100)`
+
+The above examples are just syntactically correct. They meaning, if there is
+any, is defined by the tool that is reading these annotations.
+
+## 3. An annotated specification
+
+The following specification shows how to write annotations, so they can be
+correctly parsed by the SANY parser and Apalache. Note the location of comments
+in front of: local operators, LET-definitions, and recursive operators.
+Although these locations may seem to be suboptimal, this is how the SANY
+parser locates comments that precede declarations.
+
+```tla
+-------- MODULE Annotations ----------
+EXTENDS Integers
+
+CONSTANT
+  \* @type(" Int ")
+  N
+
+VARIABLE
+  \* @type(" Set(Int) ")
+  set
+
+\* @pure
+\* @type(" Int => Int ")
+Inc(n) == n + 1
+
+\* @type(" Int => Int ")
+LOCAL LocalInc(x) == x + 1
+
+A(n) ==
+  LET \* @pure
+      \* @type(" Int => Int ")
+      Dec(x) == x + 1
+  IN
+  Dec(n)
+
+RECURSIVE Fact(_)
+\* @tailrec
+\* @type(" Int => Int ")
+Fact(n) ==
+  IF n <= 1 THEN 1 ELSE n * Fact(n - 1)
+
+\* @tailrec
+\* @type(" Int -> Int ")
+FactFun[n \in Int] ==
+  IF n <= 1 THEN 1 ELSE n * FactFun[n - 1]
+
+======================================
+```
+
+## 4. Implementation
+
+The implementation of the annotation parser can be found in the class
+`at.forsyte.apalache.io.annotations.AnnotationParser` of the module
+`tla-import`. (TODO: place a link when the PR is merged).
+
+## 5. Discussion
+
+Most likely, this topic does not deserve much discussion, as we are using
+the pretty standard syntax of Java annotations. So we are following the
+principle of the least surprise.
+
+A more concise syntax for type annotations could be as follows:
+
+```tla
+\* @type: Int => Int
+Inc(n) == n + 1
+```
+
+However, this concise syntax is technically harder to parse (SANY is prunning
+`'\n'`). Moreover, it would require additional syntax for multiline annotations.
+
+
+[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[JavaTokenParsers]: https://www.scala-lang.org/api/2.12.2/scala-parser-combinators/scala/util/parsing/combinator/JavaTokenParsers.html
+[Java identifier]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8
+

pom.xml

@@ -111,6 +111,12 @@
                 <version>3.0.1</version>
                 <scope>test</scope>
             </dependency>
+            <dependency>
+                <groupId>org.scalacheck</groupId>
+                <artifactId>scalacheck_${scalaBinaryVersion}</artifactId>
+                <version>1.14.1</version>
+                <scope>test</scope>
+            </dependency>
             <!--
              check this page: http://www.scalatest.org/user_guide/testing_with_mock_objects#jMock
             -->

test/tla/Annotations.tla

@@ -0,0 +1,37 @@
+-------- MODULE Annotations ----------
+EXTENDS Integers
+
+CONSTANT
+  \* @type("Int")
+  N
+
+VARIABLE
+  \* @type("Set(Int)")
+  set
+
+\* @pure
+\* @type("Int => Int")
+Inc(n) == n + 1
+
+\* @type("Int => Int")
+LOCAL LocalInc(x) == x + 1
+
+A(n) ==
+  LET \* @pure
+      \* @type("Int => Int")
+      Dec(x) == x + 1
+  IN
+  Dec(n)
+
+RECURSIVE Fact(_)
+\* @tailrec
+\* @type("Int => Int")
+Fact(n) ==
+  IF n <= 1 THEN 1 ELSE n * Fact(n - 1)
+
+\* @tailrec
+\* @type("Int -> Int")
+FactFun[n \in Int] ==
+  IF n <= 1 THEN 1 ELSE n * FactFun[n - 1]
+
+======================================

test/tla/cli-integration-tests.md

@@ -107,6 +107,15 @@ EXITCODE: OK
 ...
 ```
 
+### parse Annotations succeeds
+
+```sh
+$ apalache-mc parse Annotations.tla | sed 's/I@.*//'
+...
+EXITCODE: OK
+...
+```
+
 ## running the check command
 
 

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerModule.scala

@@ -2,17 +2,16 @@ package at.forsyte.apalache.tla.bmcmt.config
 
 import at.forsyte.apalache.infra.{DefaultExceptionAdapter, ExceptionAdapter}
 import at.forsyte.apalache.infra.passes._
+import at.forsyte.apalache.io.annotations.AnnotationStoreProvider
+import at.forsyte.apalache.io.annotations.store.AnnotationStore
 import at.forsyte.apalache.tla.assignments.passes._
 import at.forsyte.apalache.tla.bmcmt.analyses._
 import at.forsyte.apalache.tla.bmcmt.passes._
 import at.forsyte.apalache.tla.bmcmt.types.eager.TrivialTypeFinder
 import at.forsyte.apalache.tla.bmcmt.types.{CellT, TypeFinder}
 import at.forsyte.apalache.tla.imp.passes.{SanyParserPass, SanyParserPassImpl}
 import at.forsyte.apalache.tla.lir.storage.ChangeListener
-import at.forsyte.apalache.tla.lir.transformations.{
-  TransformationListener,
-  TransformationTracker
-}
+import at.forsyte.apalache.tla.lir.transformations.{TransformationListener, TransformationTracker}
 import at.forsyte.apalache.tla.pp.passes._
 import com.google.inject.name.Names
 import com.google.inject.{AbstractModule, TypeLiteral}
@@ -33,6 +32,10 @@ class CheckerModule extends AbstractModule {
       .to(classOf[CheckerExceptionAdapter])
 
     // stores
+    // Create an annotation store with the custom provider.
+    // We have to use TypeLiteral, as otherwise Guice is getting confused by type erasure.
+    bind(new TypeLiteral[AnnotationStore]() {} )
+      .toProvider(classOf[AnnotationStoreProvider])
     bind(classOf[FormulaHintsStore])
       .to(classOf[FormulaHintsStoreImpl])
     bind(classOf[ExprGradeStore])

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestModelChecker.scala

@@ -9,6 +9,7 @@ import at.forsyte.apalache.tla.lir.convenience.tla
 import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.BmcOper
 import at.forsyte.apalache.tla.lir.storage.ChangeListener
+
 import org.junit.runner.RunWith
 import org.scalatest.junit.JUnitRunner
 import org.scalatest.{BeforeAndAfter, FunSuite}
@@ -20,8 +21,8 @@ class TestModelChecker extends FunSuite with BeforeAndAfter {
   private var typeFinder: TrivialTypeFinder = new TrivialTypeFinder()
   private var exprGradeStore: ExprGradeStore = new ExprGradeStoreImpl()
   private var hintsStore: FormulaHintsStoreImpl = new FormulaHintsStoreImpl()
-  private var sourceStore: SourceStore = new SourceStore()
   private var changeListener: ChangeListener = new ChangeListener()
+  private var sourceStore: SourceStore = _
 
   before {
     // initialize the model checker
@@ -794,49 +795,6 @@ class TestModelChecker extends FunSuite with BeforeAndAfter {
     assert(Checker.Outcome.NoError == outcome)
   }
 
-  ////////////////////////////////////////////////////////////////////
-  private def importTla(name: String, text: String) = {
-    val (rootName, modules) = new SanyImporter(new SourceStore)
-      .loadFromSource(name, Source.fromString(text))
-    val mod = expectSingleModule(name, rootName, modules)
-    val init = mod.declarations.find(_.name == "Init").get
-    val next = mod.declarations.find(_.name == "Next").get
-    (mod, init, next)
-  }
-
-  private def expectOperatorDeclaration(
-      expectedName: String,
-      idx: Int,
-      mod: TlaModule
-  ): TlaOperDecl = {
-    mod.declarations(idx) match {
-      case decl: TlaOperDecl =>
-        assert(expectedName == decl.name)
-        decl
-
-      case _ =>
-        fail("Expected operator " + expectedName + " at position " + idx)
-    }
-  }
-
-  // copied from TestSanyImporter
-  private def expectSingleModule(
-      expectedRootName: String,
-      rootName: String,
-      modules: Map[String, TlaModule]
-  ): TlaModule = {
-    assert(expectedRootName == rootName)
-    assert(1 <= modules.size)
-    val root = modules.get(rootName)
-    root match {
-      case Some(mod) =>
-        mod
-
-      case None =>
-        fail("Module " + rootName + " not found")
-    }
-  }
-
   private def mkAssign(name: String, value: Int) =
     tla.assignPrime(tla.name(name), tla.int(value))
 

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestVCGenerator.scala

@@ -4,6 +4,8 @@ import at.forsyte.apalache.tla.imp.SanyImporter
 import at.forsyte.apalache.tla.imp.src.SourceStore
 import at.forsyte.apalache.tla.lir.transformations.impl.IdleTracker
 import at.forsyte.apalache.tla.lir.{TlaModule, TlaOperDecl}
+import at.forsyte.apalache.io.annotations.store._
+
 import org.junit.runner.RunWith
 import org.scalatest.FunSuite
 import org.scalatest.junit.JUnitRunner
@@ -66,9 +68,7 @@ class TestVCGenerator extends FunSuite {
   }
 
   private def assertDecl(
-      mod: TlaModule,
-      name: String,
-      expectedBodyText: String
+      mod: TlaModule, name: String, expectedBodyText: String
   ): Unit = {
     val vc = mod.declarations.find(_.name == name)
     assert(vc.nonEmpty, s"(VC $name not found)")
@@ -78,7 +78,7 @@ class TestVCGenerator extends FunSuite {
 
   private def loadFromText(moduleName: String, text: String): TlaModule = {
     val locationStore = new SourceStore
-    val (rootName, modules) = new SanyImporter(locationStore)
+    val (rootName, modules) = new SanyImporter(locationStore, createAnnotationStore())
       .loadFromSource(moduleName, Source.fromString(text))
     modules(moduleName)
   }

tla-import/pom.xml

@@ -60,6 +60,11 @@
             <artifactId>scalatest_${scalaBinaryVersion}</artifactId>
             <scope>test</scope>
         </dependency>
+        <dependency>
+            <groupId>org.scalacheck</groupId>
+            <artifactId>scalacheck_${scalaBinaryVersion}</artifactId>
+            <scope>test</scope>
+        </dependency>
     </dependencies>