Feat: @-attributes on top-level declarations

Makefile

@@ -11,7 +11,8 @@ exe:
 	(cd "${DIR}" ; dotnet build Source/Dafny.sln ) ## includes parser
 
 format-dfy:
-	(cd "${DIR}"/Source/DafnyCore ; ../../Binaries/Dafny.exe format .)
+	(cd "${DIR}"/Source/DafnyCore ; make format)
+	(cd "${DIR}"/Source/DafnyStandardLibraries ; make format)
 
 dfy-to-cs: 
 	(cd "${DIR}"/Source/DafnyCore ; bash DafnyGeneratedFromDafny.sh)

Source/DafnyCore/AST/Attributes.cs

@@ -15,7 +15,37 @@ public static bool IsExplicitAxiom(this IAttributeBearingDeclaration me) =>
     Attributes.Contains(me.Attributes, "axiom");
 }
 
-public class Attributes : TokenNode {
+// Syntax of a formal of a built-in @-attribute
+// To create one, prefer using the chaining BuiltInAtAttributeSyntax.WithArg()
+public record BuiltInAtAttributeArgSyntax(
+  String ArgName,
+  Type ArgType, // If null, it means it's not resolved (@Induction and @Trigger)
+  Expression DefaultValue) {
+  public Formal ToFormal() {
+    Contract.Assert(ArgType != null);
+    return new Formal(Token.NoToken, ArgName, ArgType, true, false,
+      DefaultValue);
+  }
+}
+
+// Syntax for a built-in @-attribute.
+// To create such an attribute, use the Attributes.B() helper
+public record BuiltInAtAttributeSyntax(
+  string Name,
+  List<BuiltInAtAttributeArgSyntax> Args,
+  Func<IAttributeBearingDeclaration, bool> CanBeApplied) {
+  public BuiltInAtAttributeSyntax WithArg(String argName, Type argType, Expression defaultValue = null) {
+    var c = new List<BuiltInAtAttributeArgSyntax>(Args) {
+      new(argName, argType, defaultValue) };
+    return this with { Args = c };
+  }
+
+  public BuiltInAtAttributeSyntax Filter(Func<IAttributeBearingDeclaration, bool> canBeApplied) {
+    return this with { CanBeApplied = canBeApplied };
+  }
+}
+
+public class Attributes : TokenNode, ICanFormat {
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Name != null);
@@ -37,6 +67,7 @@ void ObjectInvariant() {
   public Attributes(string name, [Captured] List<Expression> args, Attributes prev) {
     Contract.Requires(name != null);
     Contract.Requires(cce.NonNullElements(args));
+    Contract.Requires(name != UserSuppliedAtAttribute.AtName || this is UserSuppliedAtAttribute);
     Name = name;
     Args = args;
     Prev = prev;
@@ -207,6 +238,241 @@ public static bool ContainsMatchingValue(Attributes attrs, string nm, ref object
       : new List<Node> { Prev });
 
   public override IEnumerable<INode> PreResolveChildren => Children;
+  public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
+    foreach (var token in OwnedTokens) {
+      switch (token.val) {
+        case "}": {
+            formatter.SetClosingIndentedRegion(token, indentBefore);
+            break;
+          }
+        case "@": {
+            formatter.SetIndentations(token, indentBefore, indentBefore, indentBefore);
+            break;
+          }
+        case ",": {
+            formatter.SetDelimiterInsideIndentedRegions(token, indentBefore);
+            break;
+          }
+        case "{" or "{:": {
+            formatter.SetOpeningIndentedRegion(token, indentBefore);
+            break;
+          }
+      }
+    }
+    foreach (var arg in Args) {
+      formatter.SetExpressionIndentation(arg);
+    }
+    formatter.SetClosingIndentedRegion(EndToken, indentBefore);
+    return false; // Don't do inner attributes, they should be performed independently
+  }
+
+  // Typically, {:} are indented when @-attributes are not
+  public static void SetIndents(Attributes attrs, int indentBefore, TokenNewIndentCollector formatter) {
+    foreach (var attribute in attrs.AsEnumerable()) {
+      if (attribute.StartToken.val == UserSuppliedAtAttribute.AtName) {
+        attribute.SetIndent(indentBefore, formatter);
+      } else {
+        attribute.SetIndent(indentBefore + formatter.SpaceTab, formatter);
+      }
+    }
+  }
+  private static string TupleItem0Name => "0";
+  // Helper to create a built-in @-attribute
+  static BuiltInAtAttributeSyntax BuiltIn(string name) {
+    return new BuiltInAtAttributeSyntax(
+      name, new List<BuiltInAtAttributeArgSyntax>(), _ => true);
+  }
+
+  // Helper to create an old-style attribute
+  private static Attributes A(string name, params Expression[] args) {
+    return new Attributes(name, args.ToList(), null);
+  }
+
+  // Helper to create an old-style attribute with only one argument
+  private static Attributes A1(string name, ActualBindings bindings) {
+    if (Get(bindings, 0, out var expr) && expr != null) {
+      return A(name, expr);
+    }
+
+    return A(name);
+  }
+
+  // Given a user-supplied @-attribute, expand it if recognized as builtin to an old-style attribute
+  // or mark it as not built-in for later resolution
+  public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttribute atAttribute, IAttributeBearingDeclaration attributeHost) {
+    var toMatch = atAttribute.Arg;
+    var name = atAttribute.UserSuppliedName;
+    var bindings = atAttribute.UserSuppliedPreResolveBindings;
+
+    if (name == null) {
+      program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, "Attribute not recognized: " + atAttribute.ToString());
+      return null;
+    }
+
+    if (!TryGetBuiltinAtAttribute(name, out var builtinSyntax) || builtinSyntax == null) {
+      atAttribute.Builtin = false; // Will be resolved after
+      return null;
+    }
+
+    if (!builtinSyntax.CanBeApplied(attributeHost)) {
+      program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind);
+    }
+
+    var formals = builtinSyntax.Args.Select(arg => arg.ToFormal()).ToArray();
+    ResolveLikeDatatypeConstructor(program, formals, name, atAttribute, bindings);
+
+    atAttribute.Builtin = true;
+    atAttribute.Arg.Type = Type.Int; // Dummy type to avoid crashes
+
+    switch (name) {
+      case "Compile": {
+          return A1("compile", bindings);
+        }
+      case "Fuel": {
+          if (Get(bindings, 0, out var lowFuel) && lowFuel != null) {
+            if (Get(bindings, 1, out var highFuel) && highFuel != null) {
+              if (Get(bindings, 2, out var functionName) && IsStringNotEmpty(functionName)) {
+                return A("fuel", functionName, lowFuel, highFuel);
+              }
+
+              return A("fuel", lowFuel, highFuel);
+            }
+
+            return A("fuel", lowFuel);
+          }
+
+          return A("fuel");
+        }
+      case "IsolateAssertions": {
+          return A("isolate_assertions");
+        }
+      case "Options": {
+          return A1("options", bindings);
+        }
+      default: {
+          throw new Exception("@-Attribute added to Attributes.BuiltinAtAttributes needs to be handled here");
+        }
+    }
+  }
+
+  // List of built-in @-attributes with their definitions.
+  // This list could be obtained from parsing and resolving a .Dfy file
+  // but for now it's good enough.
+  public static readonly List<BuiltInAtAttributeSyntax> BuiltinAtAttributes = new() {
+    BuiltIn("Compile")
+      .WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
+      .Filter(attributeHost =>
+          attributeHost is TopLevelDecl and not TypeParameter or MemberDecl or ModuleDefinition),
+    BuiltIn("Fuel")
+      .WithArg("low", Type.Int, DefaultInt(1))
+      .WithArg("high", Type.Int, DefaultInt(2))
+      .WithArg("functionName", Type.ResolvedString(), DefaultString(""))
+      .Filter(attributeHost => attributeHost is Function or AssertStmt),
+    BuiltIn("IsolateAssertions")
+      .Filter(attributeHost => attributeHost is ICanVerify),
+    BuiltIn("Options")
+      .WithArg(TupleItem0Name, Type.ResolvedString())
+      .Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition),
+  };
+
+  ////// Helpers to create default values for the @-attribute definitions above //////
+
+  public static LiteralExpr DefaultString(string value) {
+    return Expression.CreateStringLiteral(Token.NoToken, value);
+  }
+
+  public static LiteralExpr DefaultBool(bool value) {
+    return Expression.CreateBoolLiteral(Token.NoToken, value);
+  }
+
+  public static LiteralExpr DefaultInt(int value) {
+    return Expression.CreateIntLiteralNonnegative(Token.NoToken, value);
+  }
+
+  private static bool IsStringNotEmpty(Expression value) {
+    return value is StringLiteralExpr { Value: string and not "" };
+  }
+
+  // Given resolved bindings, gets the i-th argument according to the
+  // declaration formals order
+  private static bool Get(ActualBindings bindings, int i, out Expression expr) {
+    if (bindings.Arguments.Count < i + 1) {
+      expr = null;
+      return false;
+    }
+
+    expr = bindings.Arguments[i];
+    return true;
+  }
+
+  // Resolves bindings given a list of datatype constructor-like formals,
+  // obtained from built-in @-attribute definitions
+  private static void ResolveLikeDatatypeConstructor(
+    Program program, Formal[] formals, string attrName,
+    UserSuppliedAtAttribute attrs, ActualBindings bindings) {
+    var resolutionContext = new ResolutionContext(new NoContext(program.DefaultModuleDef), false); ;
+    var typeMap = new Dictionary<TypeParameter, Type>();
+    var resolver = new ModuleResolver(new ProgramResolver(program), program.Options);
+    resolver.reporter = program.Reporter;
+    resolver.moduleInfo = resolver.ProgramResolver.SystemModuleManager.systemNameInfo;
+    resolver.ResolveActualParameters(bindings, formals.ToList(), attrs.tok,
+      attrs, resolutionContext, typeMap, null);
+    resolver.FillInDefaultValueExpressions();
+    resolver.SolveAllTypeConstraints();
+    // Verify that arguments are given literally
+    foreach (var binding in bindings.ArgumentBindings) {
+      if (binding.Actual is not LiteralExpr) {
+        program.Reporter.Error(MessageSource.Resolver, binding.Actual.RangeToken, $"Argument to attribute {attrName} must be a literal");
+      }
+    }
+  }
+
+  // Recovers a built-in @-Attribute if it exists
+  public static bool TryGetBuiltinAtAttribute(string name, out BuiltInAtAttributeSyntax builtinAtAttribute) {
+    return BuiltInAtAttributeDictionary.TryGetValue(name, out builtinAtAttribute);
+  }
+
+  // Builtin @-attributes dictionary based on the sequence of definitions of @-attributes
+  public static Dictionary<string, BuiltInAtAttributeSyntax> BuiltInAtAttributeDictionary =
+    BuiltinAtAttributes.ToDictionary(b => {
+      if (b.Name.Contains("_") || b.Name.Contains("-") || Char.IsLower(b.Name[0])) {
+        throw new Exception("Builtin @-attributes are PascalCase for consistency");
+      }
+      return b.Name;
+    }, b => b);
+
+  // Overridable method to clone the attribute as if the new attribute was placed after "prev" in the source code
+  public virtual Attributes CloneAfter(Attributes prev) {
+    return new Attributes(Name, Args, prev);
+  }
+
+  //////// Helpers for parsing attributes //////////////////
+
+  // Returns the memory location's attributes content and set the memory location to null (no attributes)
+  public static Attributes Consume(ref Attributes tmpStack) {
+    var result = tmpStack;
+    tmpStack = null;
+    return result;
+  }
+
+  // Empties the first attribute memory location while prepending its attributes to the second attribute memory location, in the same order
+  public static void MergeInto(ref Attributes tmpStack, ref Attributes attributesStack) {
+    MergeIntoReadonly(tmpStack, ref attributesStack);
+    tmpStack = null;
+  }
+
+  // Prepends the attributes tmpStack before the attributes contained in the memory location attributesStack 
+  private static void MergeIntoReadonly(Attributes tmpStack, ref Attributes attributesStack) {
+    if (tmpStack == null) {
+      return;
+    }
+    if (attributesStack == null) {
+      attributesStack = tmpStack;
+      return;
+    }
+    MergeIntoReadonly(tmpStack.Prev, ref attributesStack);
+    attributesStack = tmpStack.CloneAfter(attributesStack);
+  }
 }
 
 public static class AttributesExtensions {
@@ -221,6 +487,7 @@ public static IEnumerable<Attributes> AsEnumerable(this Attributes attr) {
   }
 }
 
+// {:..} Attributes parsed are built using this class
 public class UserSuppliedAttributes : Attributes {
   public readonly IToken OpenBrace;
   public readonly IToken CloseBrace;
@@ -237,11 +504,83 @@ public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, L
   }
 }
 
+// @-Attributes parsed are built using this class
+public class UserSuppliedAtAttribute : Attributes {
+  public static readonly string AtName = "@";
+  public readonly IToken AtSign;
+  public bool Builtin;  // set to true to indicate it was recognized as a builtin attribute
+  // Otherwise it's a user-defined one and Arg needs to be fully resolved
+  public UserSuppliedAtAttribute(IToken tok, Expression arg, Attributes prev)
+    : base(AtName, new List<Expression>() { arg }, prev) {
+    Contract.Requires(tok != null);
+    this.tok = tok;
+    this.AtSign = tok;
+  }
+
+  public Expression Arg => Args[0];
+
+  public override Attributes CloneAfter(Attributes prev) {
+    return new UserSuppliedAtAttribute(AtSign, Args[0], prev);
+  }
+
+  // Name of this @-Attribute, which is the part right after the @
+  public string UserSuppliedName =>
+    GetName(this);
+
+  // Pre-resolved bindings of this @-Attribute
+  public ActualBindings UserSuppliedPreResolveBindings =>
+    GetPreResolveBindings(this);
+
+  // Pre-resolved arguments of this @-Attributes. The order is the one provided by the user,
+  // not by any binding. Used for 
+  public IEnumerable<Expression> UserSuppliedPreResolveArguments =>
+    GetPreResolveArguments(this);
+
+  // Gets the name of an @-attribute. Attributes might be applied.
+  public static string GetName(Attributes a) {
+    if (a is UserSuppliedAtAttribute { Arg: ApplySuffix { Lhs: NameSegment { Name: var name } } }) {
+      return name;
+    }
+    if (a is UserSuppliedAtAttribute { Arg: NameSegment { Name: var singleName } }) {
+      return singleName;
+    }
+
+    return null;
+  }
+
+  // Gets the pre-resolved bindings of an @-Attribute.
+  // Returns an empty bindings if it's anything else
+  public static ActualBindings GetPreResolveBindings(Attributes a) {
+    if (a is UserSuppliedAtAttribute { Arg: ApplySuffix { Bindings: var bindings } }) {
+      return bindings;
+    }
+    return new ActualBindings(new List<ActualBinding>());
+  }
+
+  // Gets the list of pre-resolved arguments of an @-Attribute, and an empty list otherwise
+  public static IEnumerable<Expression> GetPreResolveArguments(Attributes a) {
+    if (a is UserSuppliedAtAttribute { UserSuppliedPreResolveBindings: var bindings }) {
+      return bindings.ArgumentBindings.Select(arg => arg.Actual);
+    }
+
+    return new List<Expression>();
+  }
+
+  // Gets the list of pre-resolved arguments of an @-Attribute, and the list of arguments
+  // for any other kind of attributes. Used for example to extract module options for parsing.
+  public static IEnumerable<Expression> GetUserSuppliedArguments(Attributes a) {
+    return a is UserSuppliedAtAttribute { UserSuppliedPreResolveArguments: var arguments } ? arguments : a.Args;
+  }
+
+  public override string ToString() => Prev + (Prev == null ? "" : " ") + "@" + Arg;
+}
+
 /// <summary>
 /// A class implementing this interface is one that can carry attributes.
 /// </summary>
 public interface IAttributeBearingDeclaration {
-  Attributes Attributes { get; }
+  Attributes Attributes { get; internal set; }
+  string WhatKind { get; }
 }
 
 public static class AttributeBearingDeclarationExtensions {