Feat at attributes

Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs

@@ -39,7 +39,6 @@ void ObjectInvariant() {
  Contract.Invariant(Term != null);
  }
 
- public Attributes Attributes;
  Attributes IAttributeBearingDeclaration.Attributes => Attributes;
 
  [FilledInDuringResolution] public List<BoundedPool> Bounds;

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchExpr.cs

@@ -19,7 +19,6 @@ public class NestedMatchExpr : Expression, ICloneable<NestedMatchExpr>, ICanForm
  IReadOnlyList<NestedMatchCase> INestedMatch.Cases => Cases;
 
  public readonly bool UsesOptionalBraces;
- public Attributes Attributes;
 
  [FilledInDuringResolution]
  public Expression Flattened { get; set; }

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -40,6 +40,8 @@ public Expression Resolved {
 
  public PreType PreType;
 
+ public Attributes Attributes; // @-attributes
+
  public virtual IEnumerable<Expression> TerminalExpressions {
  get {
  yield return this;

Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs

@@ -9,7 +9,7 @@ public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBeari
  public readonly List<Expression> RHSs;
  public readonly Expression Body;
  public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression
- public Attributes Attributes { get; set; }
+ Attributes IAttributeBearingDeclaration.Attributes => Attributes;
  [FilledInDuringResolution] public List<BoundedPool> Constraint_Bounds; // null for Exact=true and for when expression is in a ghost context
  // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count;
  private Expression translationDesugaring; // filled in during translation, lazily; to be accessed only via Translation.LetDesugaring; always null when Exact==true

Source/DafnyCore/AST/Grammar/ParseErrors.cs

@@ -11,6 +11,7 @@ public class ParseErrors {
  public enum ErrorId {
  // ReSharper disable once InconsistentNaming
  none,
+ p_extra_attributes,
  p_duplicate_modifier,
  p_abstract_not_allowed,
  p_no_ghost_for_by_method,
@@ -144,7 +145,9 @@ public enum ErrorId {
  }
 
  static ParseErrors() {
-
+ Add(ErrorId.p_extra_attributes,
+ @"
+@-attributes cannot be placed here".TrimStart(), Remove(true, "Remove this at-attribute"));
  Add(ErrorId.p_duplicate_modifier,
  @"
 No Dafny modifier, such as [`abstract`, `static`, `ghost`](https://dafny.org/latest/DafnyRef/DafnyRef#sec-declaration-modifiers) may be repeated

Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs

@@ -458,6 +458,24 @@ bool IsGenericInstantiation(bool inExpressionContext) {
  return false;
  }
  }
+ /* The following is the largest lookahead there is. It needs to check if what follows
+ * can be nothing but "<" Type { "," Type } ">".
+ * If inExpressionContext == true, it also checks the token immediately after
+ * the ">" to help disambiguate some cases (see implementation comment). 
+ */
+ bool IsAtCall() {
+ IToken pt = la;
+ if (pt.val != "@") {
+ return false;
+ }
+ // Beginning of the file, on a different line or separated by a space: Not an At-call. Must be an attribute
+ if (pt.Prev == null || pt.Prev.line != pt.line || pt.Prev.col + pt.Prev.val.Length + pt.TrailingTrivia.Trim().Length < pt.col - pt.LeadingTrivia.Trim().Length) {
+ return false;
+ }
+
+ return true;
+ }
+
  /* Returns true if the next thing is of the form:
  * "<" Type { "," Type } ">"
  */
@@ -627,6 +645,7 @@ class DeclModifierData {
  public bool IsOpaque;
  public IToken OpaqueToken;
  public IToken FirstToken;
+ public Attributes Attributes = null;
  }
 
  private ModuleKindEnum GetModuleKind(DeclModifierData mods) {
@@ -644,6 +663,13 @@ private ModuleKindEnum GetModuleKind(DeclModifierData mods) {
  return ModuleKindEnum.Concrete;
  }
 
+ public void CheckNoAttributes(ref Attributes attrs) {
+ if (attrs != null) {
+ SemErr(ErrorId.p_extra_attributes, attrs.RangeToken, "Attribute not expected here");
+ attrs = null;
+ }
+ }
+
  // Check that token has not been set, then set it.
  public void CheckAndSetToken(ref IToken token) {
  if (token != null) {

Source/DafnyCore/AST/Types/Types.cs

@@ -17,6 +17,10 @@ public abstract class Type : TokenNode {
  public override IEnumerable<INode> PreResolveChildren => TypeArgs.OfType<Node>();
  public static Type Nat() { return new UserDefinedType(Token.NoToken, "nat", null); } // note, this returns an unresolved type
  public static Type String() { return new UserDefinedType(Token.NoToken, "string", null); } // note, this returns an unresolved type
+
+ public static Type ResolvedString() {
+ return new SeqType(new CharType()); }
+
  public static readonly BigOrdinalType BigOrdinal = new BigOrdinalType();
 
  private static ThreadLocal<List<VisibilityScope>> _scopes = new();

Source/DafnyCore/Backends/BoogieExtractor.cs

@@ -186,7 +186,7 @@ public override void VisitMethod(Method method) {
  return triggers;
  }
 
- private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) {
+ private QKeyValue? GetKeyValues(IToken tok, Attributes? attributes) {
  QKeyValue? kv = null;
  var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute);
  if (extractAttributes == null) {