Annotations

[AZWN]

Short description

The possibility to add annotations to (e.g.) rules and constraints.

Problem description.

Alternative uses of a specification can require manipulation of/search through a specification. Currently, there are no ways to annotate (e.g.) rules and constraints properly.

Describe the solution you'd like

Syntax to annotation rules/constraints; e.g.

@[Fallback()]
subtype(_, _) :- @[AlwaysFail()] false.

These annotations should be preserved at specification loading time:

Rule rule = StatixTerms.rule().match(ruleTerm /* <- from compiled spec */);
List<ITerm> ruleAnnotations = rule.getAnnotations();
Map<IConstraint, ITem> bodyAnnotations = rule.body().getAllAnnotations(); /* <- get all annotations of sub-constraints */

Open Questions
More careful analysis of what members can require annotations must be made:

• sorts
• constructors
• constructor arguments
• particular terms
• labels
• ...

Additional context

Would have been useful for reference synthesis.

[Virtlink]

Annotations should not impact the semantics of the language, and annotations that are unrecognized should be ignored by tools dealing with annotations. This would allow, e.g., reference retention to use one set of annotations, and rename refactoring another, without interfering or even having to know about each other. As a result, multiple annotations should be allowed.

@[RefSyn(), Rename]
typeOfExpr : scope * Expr -> TYPE

@[RefSyn()]
@[Rename]
declOk : scope * Decl

---

An annotation, at the very least, should consist of an identifier and a number of fields (like a record). This allows one to specify, for example, reference retention search precedence or whether to exclude a rule.

@[RefSyn(isReference: true, cost: 10)]

---

For reference synthesis it would be great to be able to annotate both individual rules definitions and predicate types. The semantics of applying an annotation to a rule or predicate would be determined by the annotation interpreter. In the case of reference synthesis, an annotation on a predicate would apply on each rule defined for that predicate, but an annotation on a rule would override the annotation on the predicate.

---

Additionally, annotations on the whole file would also be very useful. Such annotations can apply to all rules defined in the file, or some other aspect of the file, depending on the annotation interpreter. For example with reference synthesis this can be used to exclude all rules in a file by default, and include only those that are relevant.

@[RefSyn(isReference: false)]
module java/names/ExpressionNames

rules
  @[RefSyn(isReference: true)]
  resolveExprName : scope * QID -> VAR_DECL

---

Annotations could also be used in more standardized ways. For example, to indicate the predicate types to use for single-file analysis, multi-file analysis, repl, and tests.

@[SingleFileAnalysis]
programOk : Start

@[MultiFileAnalysisProject]
projectOk : scope

@[MultiFileAnalysisFile]
fileOk : scope * Start

@[TestAnalysis]
testUnitOk : scope * Start

@[ReplAnalysis]
replOk : scope