Java-like annotations in comments (#503)

* add annotation parser

* saving source info for the declarations

* processing annotations for all declarations

* integrated AnnotationStore in the guice modules

* add ADR004 on in-comment annotations

* added the specialized syntax for one-arguments annotations

* added the inline annotation arguments

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

@@ -63,3 +63,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,143 @@
+# ADR-004: Syntax for Java-like annotations in TLA+ comments
+
+| author      | revision |
+| ----------- | --------:|
+| Igor Konnov |        2 | 
+
+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. Operator declarations, including:
+   1. Top-level operator declarations, e.g., `Foo(x) == e`.
+   1. Operators defined via LET-IN, e.g., `Foo(x) == LET Inner(y) == e IN f`.
+   1. Recursive operators, e.g., `RECURSIVE Fact(_) Fact(n) == ...`
+ 1. Recursive and non-recursive functions including:
+   1. Top-level functions, e.g., `foo[i \in Int] == e`.
+   2. Functions defined via LET-IN, e.g.,`Foo == LET foo[i \in Int] == e IN f`
+
+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? ')' | ':' inlineArg ';' )?
+ArgList     ::= (Arg) ( ',' Arg )*
+Arg         ::= (string | integer | boolean)
+inlineArg   ::= <char sequence excluding ';'>
+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:
+
+ 1. `@tailrec`
+ 1. `@type("(Int, Int) => Int")`
+ 1. `@type: (Int, Int) => Int ;`
+ 1. `@random(true)`
+ 1. `@deprecated("Use operator Foo instead")`
+ 1. `@range(0, 100)`
+
+The above examples are just syntactically correct. Their meaning, if there is
+any, is defined by the tool that is reading these annotations. Note that the
+example 3 is not following the syntax of Java annotations. We have introduced
+this format for one-argument annotations, especially, for type annotations.
+Its purpose is to reduce the visual clutter in annotations that accept a string
+as their only argument.
+
+## 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
+  \* the single-argument annotation
+  \* @type: Set(Int);
+  set
+
+\* @pure
+\* using the Java annotations, a bit verbose:
+\* @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.
+
+We also support the concise syntax for the annotations that accept a string as
+a simple argument. For these annotations, we had to add the end marker ';'.
+This is done because the SANY parser is pruning the linefeed character `\n`,
+so it would be otherwise impossible to find the end of an annotation.
+
+
+[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,6 +2,8 @@ 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._
@@ -15,11 +17,11 @@ import com.google.inject.name.Names
 import com.google.inject.{AbstractModule, TypeLiteral}
 
 /**
-  * A configuration that binds all the passes from the parser to the checker.
-  * If you are not sure how the binding works, check the tutorial on Google Guice.
-  *
-  * @author Igor Konnov
-  */
+ * A configuration that binds all the passes from the parser to the checker.
+ * If you are not sure how the binding works, check the tutorial on Google Guice.
+ *
+ * @author Igor Konnov
+ */
 class CheckerModule extends AbstractModule {
   override def configure(): Unit = {
     // the options singleton
@@ -30,20 +32,24 @@ 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])
       .to(classOf[ExprGradeStoreImpl])
     bind(new TypeLiteral[TypeFinder[CellT]] {})
-      .to(classOf[TrivialTypeFinder])   // using a trivial type finder
+      .to(classOf[TrivialTypeFinder]) // using a trivial type finder
 
     // transformation tracking
     // TODO: the binding of TransformationListener should disappear in the future
     bind(classOf[TransformationListener])
       .to(classOf[ChangeListener])
     // check TransformationTrackerProvider to find out which listeners the tracker is using
     bind(classOf[TransformationTracker])
-        .toProvider(classOf[TransformationTrackerProvider])
+      .toProvider(classOf[TransformationTrackerProvider])
 
     // SanyParserPassImpl is the default implementation of SanyParserPass
     bind(classOf[SanyParserPass])