Java-like annotations in comments

[konnov]

This PR addresses two related issues: #262 and #226. Instead of developing a special solution for type annotations, we produce a simple and general syntax of annotations, like in Java. To make use of the annotations, this PR also extends SanyImporter to parse annotations in the comments that are written in front of declarations. The annotation syntax and examples are given in ADR004 (this PR).

On top of that, TestAnnotationParser is the first property-based test in Apalache :-)

• Tests added for any new code
• Documentation added for any new functionality
• Entry added to UNRELEASED.md for any new functionality

[konnov]

@shonfeder the formatting check fails on a markdown file. What shall we do?

[shonfeder]

I left some comments, but I'm hoping the size of this PR will be very reduced once the formatting is fixed (as per the failing CI job) so I'll hold of on reviewing more until then.

[shonfeder]

Would we have the same problem with @type(Int => Int)?

[konnov]

yes, the types may contain parentheses, that will confuse the annotation parser a lot. These are two separate parsers: one of java-like annotations, and one for types.

[konnov]

The problem is that we don't have an end marker, which is usually \n. How about adding the infamous semicolon in the end of a quote-free annotation:

\* @type: (Int, Int) => Int ;

[konnov]

I have added this special form to the annotations. It definitely has less clutter when writing type annotations.

[shonfeder]

@konnov did you already try make fmt-fix?

[konnov]

interesting. I forgot to do it. Can we add it to a PR template.

[konnov]

There are plenty of small replacements in files, basically adding one more parameter annotationStore: AnnotationStore.

[shonfeder]

LGTM

[konnov]

I have resolved the conflicts. The last commit is massive, as it merges the formatting reversal from unstable