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;
@@ -101,7 +103,7 @@ public Expression(IToken tok) {
   }
 
   protected Expression(Cloner cloner, Expression original) {
-
+    Attributes = cloner.CloneAttributes(original.Attributes);
     tok = cloner.Tok(original.tok);
     RangeToken = cloner.Range(original.RangeToken);
 

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

@@ -9,7 +9,6 @@
 namespace Microsoft.Dafny;
 
 public partial class Parser {
-
   public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, CancellationToken cancellationToken)
     : this(scanner, errors, cancellationToken)  // the real work
   {
@@ -25,6 +24,14 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca
     theModule = new FileModuleDefinition(scanner.FirstToken);
   }
 
+  public void MergeInto(ref Attributes attrsStack, ref Attributes attrsTarget) {
+    Attributes.MergeInto(ref attrsStack, ref attrsTarget);
+  }
+
+  public Attributes Consume(ref Attributes attrs) {
+    return Attributes.Consume(ref attrs);
+  }
+
   bool IsReveal(IToken nextToken) => la.kind == _reveal || (la.kind == _hide && nextToken.kind is _star or _ident);
 
   bool IsIdentifier(int kind) {
@@ -458,6 +465,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 +652,7 @@ class DeclModifierData {
     public bool IsOpaque;
     public IToken OpaqueToken;
     public IToken FirstToken;
+    public Attributes Attributes = null;
   }
 
   private ModuleKindEnum GetModuleKind(DeclModifierData mods) {
@@ -644,6 +670,16 @@ private ModuleKindEnum GetModuleKind(DeclModifierData mods) {
     return ModuleKindEnum.Concrete;
   }
 
+  /// <summary>
+  /// Before literals that end a block, we usually add CheckNoAttributes to avoid any non-attached attributes
+  /// </summary>
+  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) {