Merge branch 'master' into ajewell/unmute

Source/AutoExtern/AutoProgram.cs

@@ -215,7 +215,7 @@ private bool IsSkippedBaseType(BaseTypeSyntax bt) {
     syntax.BaseList?.Types
       .Where(bt => !IsSkippedBaseType(bt))
       .Select(bt => new Type(bt.Type, model))
-    ?? Enumerable.Empty<Type>();
+    ?? [];
 
   public override void Pp(TextWriter wr, string indent) {
     var baseTypes = BaseTypes.ToList();
@@ -388,8 +388,8 @@ public override void Pp(TextWriter wr, string indent) {
 internal class Name {
   private const string EscapePrefix = "CSharp_";
 
-  private static readonly List<string> DisallowedNameWords = new List<string>
-    {"type", "ORDINAL", "Keys", "Values", "Items", "IsLimit", "IsSucc", "Offset", "IsNat"};
+  private static readonly List<string> DisallowedNameWords =
+    ["type", "ORDINAL", "Keys", "Values", "Items", "IsLimit", "IsSucc", "Offset", "IsNat"];
   private static readonly Regex DisallowedNameRe =
     new Regex($"^(_|({String.Join("|", DisallowedNameWords)})$)");
 

Source/DafnyCore.Test/ClonerTest.cs

@@ -33,11 +33,11 @@ public void ClonerKeepsBodyStartTok() {
       IsTypeExplicit = false
     };
     var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
-      false, false, new List<TypeParameter>(), new List<Formal> { formal1, formal2 },
-      new List<Formal>(), new List<AttributedExpression>(),
-      new Specification<FrameExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null),
-      new List<AttributedExpression>(), new Specification<Expression>(new List<Expression>(), null),
-      new BlockStmt(rangeToken, new List<Statement>()), null, Token.NoToken, false);
+      false, false, [], [formal1, formal2],
+      [], [],
+      new Specification<FrameExpression>(), new Specification<FrameExpression>([], null),
+      [], new Specification<Expression>([], null),
+      new BlockStmt(rangeToken, []), null, Token.NoToken, false);
 
     dummyDecl.BodyStartTok = tokenBodyStart;
     var cloner = new Cloner();

Source/DafnyCore.Test/NodeTests.cs

@@ -8,7 +8,7 @@ public class NodeTests {
   class ConcreteNode : Node {
     public ConcreteNode(IOrigin origin, IEnumerable<INode>? children = null) {
       Origin = origin;
-      Children = children ?? Enumerable.Empty<INode>();
+      Children = children ?? [];
     }
 
     public override IOrigin Origin { get; }

Source/DafnyCore/AST/Attributes.cs

@@ -174,7 +174,7 @@ public static List<List<Expression>> FindAllExpressions(Attributes attrs, string
     List<List<Expression>> ret = null;
     for (; attrs != null; attrs = attrs.Prev) {
       if (attrs.Name == nm) {
-        ret = ret ?? new List<List<Expression>>();   // Avoid allocating the list in the common case where we don't find nm
+        ret = ret ?? [];   // Avoid allocating the list in the common case where we don't find nm
         ret.Add(attrs.Args);
       }
     }
@@ -280,7 +280,7 @@ public static void SetIndents(Attributes attrs, int indentBefore, TokenNewIndent
   // Helper to create a built-in @-attribute
   static BuiltInAtAttributeSyntax BuiltIn(string name) {
     return new BuiltInAtAttributeSyntax(
-      name, new List<BuiltInAtAttributeArgSyntax>(), _ => true);
+      name, [], _ => true);
   }
 
   // Helper to create an old-style attribute
@@ -330,7 +330,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
     atAttribute.Arg.Type = Type.Int; // Dummy type to avoid crashes
     var intDecl = resolver.SystemModuleManager.valuetypeDecls.First(valueTypeDecl => valueTypeDecl.Name == PreType.TypeNameInt);
 
-    atAttribute.Arg.PreType = new DPreType(intDecl, new List<PreType>(), null);
+    atAttribute.Arg.PreType = new DPreType(intDecl, [], null);
 
     switch (name) {
       case "AssumeCrossModuleTermination": {
@@ -480,101 +480,143 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
   // 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() {
+  public static readonly List<BuiltInAtAttributeSyntax> BuiltinAtAttributes = [
     BuiltIn("AssumeCrossModuleTermination")
       .Filter(attributeHost => attributeHost is ClassDecl or TraitDecl),
+
     BuiltIn("AutoContracts")
       .Filter(attributeHost => attributeHost is ClassDecl),
+
     BuiltIn("AutoRequires")
       .Filter(attributeHost => attributeHost is Function),
+
     BuiltIn("AutoRevealDependenciesAll").WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
       .Filter(attributeHost => attributeHost is MethodOrFunction),
+
     BuiltIn("AutoRevealDependencies").WithArg("level", Type.Int)
       .Filter(attributeHost => attributeHost is MethodOrFunction),
+
     BuiltIn("Axiom")
       .Filter(attributeHost => attributeHost is MethodOrFunction),
+
     BuiltIn("Compile")
       .WithArg(TupleItem0Name, Type.Bool, DefaultBool(true))
       .Filter(attributeHost =>
         attributeHost is TopLevelDecl and not TypeParameter or MemberDecl or ModuleDefinition),
+
     BuiltIn("Concurrent")
       .Filter(attributeHost =>
         attributeHost is MethodOrFunction),
+
     BuiltIn("DisableNonlinearArithmetic")
       .WithArg("disable", Type.Bool, DefaultBool(true))
       .Filter(attributeHost =>
         attributeHost is ModuleDefinition),
+
     BuiltIn("Fuel")
       .WithArg("low", Type.Int, DefaultInt(1))
       .WithArg("high", Type.Int, DefaultInt(2))
       .WithArg("functionName", Type.ResolvedString(), DefaultString(""))
       .Filter(attributeHost => attributeHost is MethodOrFunction or AssertStmt),
+
     BuiltIn("IsolateAssertions")
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("NativeUInt8")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeInt8")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeUInt16")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeInt16")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeUInt32")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeInt32")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeInt53")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeUInt64")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeInt64")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeUInt128")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeInt128")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeInt")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeNone")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("NativeIntOrReal")
       .Filter(attributeHost => attributeHost is NewtypeDecl),
+
     BuiltIn("Options")
       .WithArg(TupleItem0Name, Type.ResolvedString())
       .Filter(attributeHost => attributeHost is ModuleDecl or ModuleDefinition),
+
     BuiltIn("Print")
       .Filter(attributeHost => attributeHost is Method),
+
     BuiltIn("Priority").WithArg(TupleItem0Name, Type.Int)
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("ResourceLimit").WithArg(TupleItem0Name, Type.ResolvedString())
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("Synthesize")
       .Filter(attributeHost => attributeHost is Method),
+
     BuiltIn("TimeLimit").WithArg(TupleItem0Name, Type.Int)
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("TimeLimitMultiplier").WithArg(TupleItem0Name, Type.Int)
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("TailRecursion")
       .Filter(attributeHost => attributeHost is MethodOrFunction),
+
     BuiltIn("Test")
       .Filter(attributeHost => attributeHost is MethodOrFunction),
+
     BuiltIn("TestEntry")
       .Filter(attributeHost => attributeHost is MethodOrFunction),
+
     BuiltIn("TestInline").WithArg("level", Type.Int, DefaultInt(1))
       .Filter(attributeHost => attributeHost is MethodOrFunction),
+
     BuiltIn("Transparent")
       .Filter(attributeHost => attributeHost is Function),
+
     BuiltIn("VcsMaxCost").WithArg(TupleItem0Name, Type.Int)
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("VcsMaxKeepGoingSplits").WithArg(TupleItem0Name, Type.Int)
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("VcsMaxSplits").WithArg(TupleItem0Name, Type.Int)
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("Verify")
       .Filter(attributeHost => attributeHost is ICanVerify),
+
     BuiltIn("VerifyOnly")
-      .Filter(attributeHost => attributeHost is ICanVerify),
-  };
+      .Filter(attributeHost => attributeHost is ICanVerify)
+
+  ];
 
   ////// Helpers to create default values for the @-attribute definitions above //////
 
@@ -708,7 +750,7 @@ public class UserSuppliedAtAttribute : Attributes {
   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(IOrigin origin, Expression arg, Attributes prev)
-    : base(AtName, new List<Expression>() { arg }, prev) {
+    : base(AtName, [arg], prev) {
     Contract.Requires(origin != null);
     SetOrigin(origin);
     this.AtSign = origin;

Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs

@@ -31,7 +31,7 @@ public ApplyExpr(IOrigin origin, Expression fn, List<Expression> args, Token clo
     Function = fn;
     Args = args;
     CloseParen = closeParen;
-    FormatTokens = closeParen != null ? new[] { closeParen } : null;
+    FormatTokens = closeParen != null ? [closeParen] : null;
   }
 
   public ApplyExpr Clone(Cloner cloner) {

Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs

@@ -44,7 +44,7 @@ public ApplySuffix(IOrigin origin, IOrigin/*?*/ atLabel, Expression lhs, List<Ac
     CloseParen = closeParen;
     Bindings = new ActualBindings(args);
     if (closeParen != null) {
-      FormatTokens = new[] { closeParen };
+      FormatTokens = [closeParen];
     }
   }
 

Source/DafnyCore/AST/Expressions/Applications/ExprDotName.cs

@@ -16,7 +16,7 @@ public class ExprDotName : SuffixExpr, ICloneable<ExprDotName> {
   /// but not the declaration of the Lhs, we must also include the Lhs.
   /// </summary>
   public override IEnumerable<INode> Children => ResolvedExpression == null
-    ? new[] { Lhs }
+    ? [Lhs]
     : new[] { Lhs, ResolvedExpression };
 
   [ContractInvariantMethod]

Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs

@@ -106,7 +106,7 @@ public FunctionCallExpr(IOrigin origin, Name fn, Expression receiver, IOrigin op
     this.CloseParen = closeParen;
     this.AtLabel = atLabel;
     this.Bindings = bindings;
-    this.FormatTokens = closeParen != null ? new[] { closeParen } : null;
+    this.FormatTokens = closeParen != null ? [closeParen] : null;
   }
 
   /// <summary>

Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs

@@ -238,7 +238,7 @@ public MemberSelectExpr(IOrigin origin, Expression obj, Field field)
 
     var receiverType = obj.Type.NormalizeExpand();
     this.TypeApplicationAtEnclosingClass = receiverType.TypeArgs;
-    this.TypeApplicationJustMember = new List<Type>();
+    this.TypeApplicationJustMember = [];
 
     var typeMap = new Dictionary<TypeParameter, Type>();
     if (receiverType is UserDefinedType udt) {

Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs

@@ -26,7 +26,7 @@ public NameSegment Clone(Cloner cloner) {
     return new NameSegment(cloner, this);
   }
 
-  public override IEnumerable<INode> PreResolveChildren => OptTypeArguments ?? new List<Type>();
+  public override IEnumerable<INode> PreResolveChildren => OptTypeArguments ?? [];
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     formatter.SetTypeLikeIndentation(indentBefore, OwnedTokens);
     foreach (var subType in PreResolveChildren.OfType<Type>()) {

Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs

@@ -36,7 +36,7 @@ public SeqSelectExpr(IOrigin origin, bool selectOne, Expression seq, Expression
     E1 = e1;
     CloseParen = closeParen;
     if (closeParen != null) {
-      FormatTokens = new[] { closeParen };
+      FormatTokens = [closeParen];
     }
   }
 

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

@@ -84,8 +84,8 @@ protected ComprehensionExpr(Cloner cloner, ComprehensionExpr original) : base(cl
 
   public override IEnumerable<INode> PreResolveChildren =>
     Attributes.AsEnumerable()
-      .Concat<Node>(Range != null && Range.Origin.line > 0 ? new List<Node>() { Range } : new List<Node>())
-    .Concat(Term != null && Term.Origin.line > 0 ? new List<Node> { Term } : new List<Node>());
+      .Concat<Node>(Range != null && Range.Origin.line > 0 ? [Range] : new List<Node>())
+    .Concat(Term != null && Term.Origin.line > 0 ? [Term] : new List<Node>());
 
   public override IEnumerable<Expression> SubExpressions {
     get {

Source/DafnyCore/AST/Expressions/ConcreteSyntaxExpression.cs

@@ -24,7 +24,8 @@ protected ConcreteSyntaxExpression(Cloner cloner, ConcreteSyntaxExpression origi
   protected ConcreteSyntaxExpression(IOrigin origin)
     : base(origin) {
   }
-  public override IEnumerable<INode> Children => ResolvedExpression == null ? Array.Empty<Node>() : new[] { ResolvedExpression };
+  public override IEnumerable<INode> Children => ResolvedExpression == null ? Array.Empty<Node>() : [ResolvedExpression
+  ];
   public override IEnumerable<Expression> SubExpressions {
     get {
       if (ResolvedExpression != null) {
@@ -41,7 +42,7 @@ public override IEnumerable<Expression> TerminalExpressions {
     }
   }
 
-  public virtual IEnumerable<Expression> PreResolveSubExpressions => Enumerable.Empty<Expression>();
+  public virtual IEnumerable<Expression> PreResolveSubExpressions => [];
   public override IEnumerable<INode> PreResolveChildren => PreResolveSubExpressions;
 
   public override IEnumerable<Type> ComponentTypes => ResolvedExpression.ComponentTypes;

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

@@ -22,8 +22,9 @@ private void InitializeAttributes() {
     Attributes.ContainsBool(Attributes, "split", ref splitMatch);
     foreach (var c in Cases) {
       if (!Attributes.Contains(c.Attributes, "split")) {
-        List<Expression> args = new List<Expression>();
-        args.Add(Expression.CreateBoolLiteral(c.Origin, splitMatch));
+        List<Expression> args = [
+          Expression.CreateBoolLiteral(c.Origin, splitMatch)
+        ];
         Attributes attrs = new Attributes("split", args, c.Attributes);
         c.Attributes = attrs;
       }

Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs

@@ -27,7 +27,7 @@ public class IdPattern : ExtendedPattern, IHasReferences {
   public const string WildcardString = "_";
 
   public void MakeAConstructor() {
-    this.Arguments = new List<ExtendedPattern>();
+    this.Arguments = [];
   }
 
   public IdPattern(Cloner cloner, IdPattern original) : base(cloner.Origin(original.Origin), original.IsGhost) {

Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs

@@ -63,7 +63,7 @@ public override IEnumerable<Expression> SubExpressions {
   }
 
   public IEnumerable<Reference> GetReferences() {
-    return LegalSourceConstructors == null ? Enumerable.Empty<Reference>()
+    return LegalSourceConstructors == null ? []
       : Updates.Zip(LegalSourceConstructors).Select(t =>
         new Reference(t.First.Item1, t.Second.Formals.Find(f => f.Name == t.First.Item2)));
   }

Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs

@@ -13,8 +13,8 @@ public class DatatypeValue : Expression, IHasReferences, ICloneable<DatatypeValu
   public override IEnumerable<INode> Children => new Node[] { Bindings };
 
   [FilledInDuringResolution] public DatatypeCtor Ctor;
-  [FilledInDuringResolution] public List<Type> InferredTypeArgs = new List<Type>();
-  [FilledInDuringResolution] public List<PreType> InferredPreTypeArgs = new List<PreType>();
+  [FilledInDuringResolution] public List<Type> InferredTypeArgs = [];
+  [FilledInDuringResolution] public List<PreType> InferredPreTypeArgs = [];
   [FilledInDuringResolution] public bool IsCoCall;
   [ContractInvariantMethod]
   void ObjectInvariant() {

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -125,7 +125,7 @@ public virtual IEnumerable<Expression> SubExpressions {
   public IEnumerable<Expression> DescendantsAndSelf {
     get {
       Stack<Expression> todo = new();
-      List<Expression> result = new();
+      List<Expression> result = [];
       todo.Push(this);
       while (todo.Any()) {
         var current = todo.Pop();

Source/DafnyCore/AST/Expressions/Specification.cs

@@ -13,7 +13,7 @@ private void ObjectInvariant() {
   }
 
   public Specification() {
-    Expressions = new List<T>();
+    Expressions = [];
     Attributes = null;
   }
 

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

@@ -53,7 +53,7 @@ public QuantifiedVar(IOrigin tok, string name, Type type, Expression domain, Exp
   /// Some quantification contexts (such as comprehensions) will replace this with "true".
   /// </summary>
   public static void ExtractSingleRange(List<QuantifiedVar> qvars, out List<BoundVar> bvars, [CanBeNull] out Expression range) {
-    bvars = new List<BoundVar>();
+    bvars = [];
     range = null;
 
     foreach (var qvar in qvars) {