diff --git a/Source/AutoExtern/AutoProgram.cs b/Source/AutoExtern/AutoProgram.cs index 91fb34b75f5..6e954f0fdf4 100644 --- a/Source/AutoExtern/AutoProgram.cs +++ b/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(); + ?? []; 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 DisallowedNameWords = new List - {"type", "ORDINAL", "Keys", "Values", "Items", "IsLimit", "IsSucc", "Offset", "IsNat"}; + private static readonly List DisallowedNameWords = + ["type", "ORDINAL", "Keys", "Values", "Items", "IsLimit", "IsSucc", "Offset", "IsNat"]; private static readonly Regex DisallowedNameRe = new Regex($"^(_|({String.Join("|", DisallowedNameWords)})$)"); diff --git a/Source/DafnyCore.Test/ClonerTest.cs b/Source/DafnyCore.Test/ClonerTest.cs index 8d0dccc169a..2730f963463 100644 --- a/Source/DafnyCore.Test/ClonerTest.cs +++ b/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(), new List { formal1, formal2 }, - new List(), new List(), - new Specification(), new Specification(new List(), null), - new List(), new Specification(new List(), null), - new BlockStmt(rangeToken, new List()), null, Token.NoToken, false); + false, false, [], [formal1, formal2], + [], [], + new Specification(), new Specification([], null), + [], new Specification([], null), + new BlockStmt(rangeToken, []), null, Token.NoToken, false); dummyDecl.BodyStartTok = tokenBodyStart; var cloner = new Cloner(); diff --git a/Source/DafnyCore.Test/NodeTests.cs b/Source/DafnyCore.Test/NodeTests.cs index fd613cd726d..7753b30bb2d 100644 --- a/Source/DafnyCore.Test/NodeTests.cs +++ b/Source/DafnyCore.Test/NodeTests.cs @@ -8,7 +8,7 @@ public class NodeTests { class ConcreteNode : Node { public ConcreteNode(IOrigin origin, IEnumerable? children = null) { Origin = origin; - Children = children ?? Enumerable.Empty(); + Children = children ?? []; } public override IOrigin Origin { get; } diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index decc10cf47b..451667b6e6e 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/Source/DafnyCore/AST/Attributes.cs @@ -174,7 +174,7 @@ public static List> FindAllExpressions(Attributes attrs, string List> ret = null; for (; attrs != null; attrs = attrs.Prev) { if (attrs.Name == nm) { - ret = ret ?? new List>(); // 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(), _ => 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(), 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 BuiltinAtAttributes = new() { + public static readonly List 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() { arg }, prev) { + : base(AtName, [arg], prev) { Contract.Requires(origin != null); SetOrigin(origin); this.AtSign = origin; diff --git a/Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs index 6577be242e8..21e583941bb 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs @@ -31,7 +31,7 @@ public ApplyExpr(IOrigin origin, Expression fn, List 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) { diff --git a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs index b19fd085aee..981225d5bee 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs @@ -44,7 +44,7 @@ public ApplySuffix(IOrigin origin, IOrigin/*?*/ atLabel, Expression lhs, List { /// but not the declaration of the Lhs, we must also include the Lhs. /// public override IEnumerable Children => ResolvedExpression == null - ? new[] { Lhs } + ? [Lhs] : new[] { Lhs, ResolvedExpression }; [ContractInvariantMethod] diff --git a/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs index 75b5c6e5bcd..53aef1dc848 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs +++ b/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; } /// diff --git a/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs index c3aae1fcbac..542f371be51 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs +++ b/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(); + this.TypeApplicationJustMember = []; var typeMap = new Dictionary(); if (receiverType is UserDefinedType udt) { diff --git a/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs b/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs index 8b803a02863..d2b260425f8 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/NameSegment.cs @@ -26,7 +26,7 @@ public NameSegment Clone(Cloner cloner) { return new NameSegment(cloner, this); } - public override IEnumerable PreResolveChildren => OptTypeArguments ?? new List(); + public override IEnumerable PreResolveChildren => OptTypeArguments ?? []; public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { formatter.SetTypeLikeIndentation(indentBefore, OwnedTokens); foreach (var subType in PreResolveChildren.OfType()) { diff --git a/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs index 0aa0d2eb5d1..cec6a9df58d 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs +++ b/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]; } } diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs index 4f4cb90d6e8..767351cb741 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs @@ -84,8 +84,8 @@ protected ComprehensionExpr(Cloner cloner, ComprehensionExpr original) : base(cl public override IEnumerable PreResolveChildren => Attributes.AsEnumerable() - .Concat(Range != null && Range.Origin.line > 0 ? new List() { Range } : new List()) - .Concat(Term != null && Term.Origin.line > 0 ? new List { Term } : new List()); + .Concat(Range != null && Range.Origin.line > 0 ? [Range] : new List()) + .Concat(Term != null && Term.Origin.line > 0 ? [Term] : new List()); public override IEnumerable SubExpressions { get { diff --git a/Source/DafnyCore/AST/Expressions/ConcreteSyntaxExpression.cs b/Source/DafnyCore/AST/Expressions/ConcreteSyntaxExpression.cs index 26ebc0ed5cc..da4724898ce 100644 --- a/Source/DafnyCore/AST/Expressions/ConcreteSyntaxExpression.cs +++ b/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 Children => ResolvedExpression == null ? Array.Empty() : new[] { ResolvedExpression }; + public override IEnumerable Children => ResolvedExpression == null ? Array.Empty() : [ResolvedExpression + ]; public override IEnumerable SubExpressions { get { if (ResolvedExpression != null) { @@ -41,7 +42,7 @@ public override IEnumerable TerminalExpressions { } } - public virtual IEnumerable PreResolveSubExpressions => Enumerable.Empty(); + public virtual IEnumerable PreResolveSubExpressions => []; public override IEnumerable PreResolveChildren => PreResolveSubExpressions; public override IEnumerable ComponentTypes => ResolvedExpression.ComponentTypes; diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs index b585aa1de4c..8b6abf60316 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs +++ b/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 args = new List(); - args.Add(Expression.CreateBoolLiteral(c.Origin, splitMatch)); + List args = [ + Expression.CreateBoolLiteral(c.Origin, splitMatch) + ]; Attributes attrs = new Attributes("split", args, c.Attributes); c.Attributes = attrs; } diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs index 8992bc61164..1c937b8f691 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs +++ b/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(); + this.Arguments = []; } public IdPattern(Cloner cloner, IdPattern original) : base(cloner.Origin(original.Origin), original.IsGhost) { diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs index 1568b19b5ab..30e448275cc 100644 --- a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeUpdateExpr.cs @@ -63,7 +63,7 @@ public override IEnumerable SubExpressions { } public IEnumerable GetReferences() { - return LegalSourceConstructors == null ? Enumerable.Empty() + return LegalSourceConstructors == null ? [] : Updates.Zip(LegalSourceConstructors).Select(t => new Reference(t.First.Item1, t.Second.Formals.Find(f => f.Name == t.First.Item2))); } diff --git a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs index 9fd6c491373..ec729ef7f95 100644 --- a/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs +++ b/Source/DafnyCore/AST/Expressions/Datatypes/DatatypeValue.cs @@ -13,8 +13,8 @@ public class DatatypeValue : Expression, IHasReferences, ICloneable Children => new Node[] { Bindings }; [FilledInDuringResolution] public DatatypeCtor Ctor; - [FilledInDuringResolution] public List InferredTypeArgs = new List(); - [FilledInDuringResolution] public List InferredPreTypeArgs = new List(); + [FilledInDuringResolution] public List InferredTypeArgs = []; + [FilledInDuringResolution] public List InferredPreTypeArgs = []; [FilledInDuringResolution] public bool IsCoCall; [ContractInvariantMethod] void ObjectInvariant() { diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 74e9e6ac2c4..882e88e833c 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -125,7 +125,7 @@ public virtual IEnumerable SubExpressions { public IEnumerable DescendantsAndSelf { get { Stack todo = new(); - List result = new(); + List result = []; todo.Push(this); while (todo.Any()) { var current = todo.Pop(); diff --git a/Source/DafnyCore/AST/Expressions/Specification.cs b/Source/DafnyCore/AST/Expressions/Specification.cs index e9529f2a7e2..cb45cd494ee 100644 --- a/Source/DafnyCore/AST/Expressions/Specification.cs +++ b/Source/DafnyCore/AST/Expressions/Specification.cs @@ -13,7 +13,7 @@ private void ObjectInvariant() { } public Specification() { - Expressions = new List(); + Expressions = []; Attributes = null; } diff --git a/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs b/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs index c9ec6c273e9..46cff1003e5 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs +++ b/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". /// public static void ExtractSingleRange(List qvars, out List bvars, [CanBeNull] out Expression range) { - bvars = new List(); + bvars = []; range = null; foreach (var qvar in qvars) { diff --git a/Source/DafnyCore/AST/Expressions/Variables/CasePattern.cs b/Source/DafnyCore/AST/Expressions/Variables/CasePattern.cs index 2e89f8e0b93..f0eaf3e05ca 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/CasePattern.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/CasePattern.cs @@ -26,7 +26,7 @@ public class CasePattern : NodeWithComputedRange [FilledInDuringResolution] public Expression Expr; // an r-value version of the CasePattern; public void MakeAConstructor() { - this.Arguments = new List>(); + this.Arguments = []; } public CasePattern(Cloner cloner, CasePattern original) : base(cloner, original) { @@ -75,7 +75,7 @@ public void AssembleExpr(List dtvTypeArgs) { this.Expr = new IdentifierExpr(this.Origin, this.Var); } else { var dtValue = new DatatypeValue(this.Origin, this.Ctor.EnclosingDatatype.Name, this.Id, - this.Arguments == null ? new List() : this.Arguments.ConvertAll(arg => arg.Expr)); + this.Arguments == null ? [] : this.Arguments.ConvertAll(arg => arg.Expr)); dtValue.Ctor = this.Ctor; // resolve here dtValue.InferredTypeArgs.AddRange(dtvTypeArgs); // resolve here dtValue.Type = new UserDefinedType(this.Origin, this.Ctor.EnclosingDatatype.Name, this.Ctor.EnclosingDatatype, dtvTypeArgs); @@ -96,7 +96,7 @@ public void AssembleExprPreType(List dtvPreTypeArgs) { }; } else { var dtValue = new DatatypeValue(this.Origin, this.Ctor.EnclosingDatatype.Name, this.Id, - this.Arguments == null ? new List() : this.Arguments.ConvertAll(arg => arg.Expr)) { + this.Arguments == null ? [] : this.Arguments.ConvertAll(arg => arg.Expr)) { Ctor = this.Ctor, PreType = new DPreType(this.Ctor.EnclosingDatatype, dtvPreTypeArgs) }; diff --git a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs index 07a83ddb972..b77e1933188 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/LetExpr.cs @@ -57,7 +57,7 @@ public static LetExpr Havoc(IOrigin tok, Type type = null) { type ??= new InferredTypeProxy(); var boundVar = new BoundVar(tok, "x", type); var casePatterns = new List>() { new(tok, boundVar) }; - return new LetExpr(tok, casePatterns, new List() { CreateBoolLiteral(tok, true) }, + return new LetExpr(tok, casePatterns, [CreateBoolLiteral(tok, true)], new IdentifierExpr(tok, boundVar), false) { Type = type }; diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs index b4f14067005..9f01fd1786c 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs @@ -40,7 +40,7 @@ public string AssignUniqueName(VerificationIdGenerator generator) { return uniqueName ??= generator.FreshId(Name + "#"); } - static char[] specialChars = { '\'', '_', '?', '\\', '#' }; + static char[] specialChars = ['\'', '_', '?', '\\', '#']; /// /// Mangle name nm by replacing and escaping characters most likely to cause issues when compiling and /// when translating to Boogie. This transformation is injective. diff --git a/Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs b/Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs index 11de95a29f0..9b299f5c12f 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/ResolverIdentifierExpr.cs @@ -70,7 +70,7 @@ public ResolverIdentifierExpr(IOrigin origin, TopLevelDecl decl, List type PreType = decl is ModuleDecl ? new PreTypePlaceholderModule() : new PreTypePlaceholderType(); } public ResolverIdentifierExpr(IOrigin origin, TypeParameter tp) - : this(origin, tp, new List()) { + : this(origin, tp, []) { Contract.Requires(origin != null); Contract.Requires(tp != null); } diff --git a/Source/DafnyCore/AST/Grammar/IFileSystem.cs b/Source/DafnyCore/AST/Grammar/IFileSystem.cs index 8f078e965c0..b1c618f46ca 100644 --- a/Source/DafnyCore/AST/Grammar/IFileSystem.cs +++ b/Source/DafnyCore/AST/Grammar/IFileSystem.cs @@ -39,7 +39,7 @@ public bool Exists(Uri path) { public DirectoryInfoBase GetDirectoryInfoBase(string root) { var inMemoryFiles = files.Keys.Select(openFileUri => openFileUri.LocalPath); var inMemory = new InMemoryDirectoryInfoFromDotNet8(root, inMemoryFiles); - return new CombinedDirectoryInfo(new[] { inMemory, OnDiskFileSystem.Instance.GetDirectoryInfoBase(root) }); + return new CombinedDirectoryInfo([inMemory, OnDiskFileSystem.Instance.GetDirectoryInfoBase(root)]); } } diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index bc318beb0b3..3f63f3e2bfc 100644 --- a/Source/DafnyCore/AST/Grammar/ParseErrors.cs +++ b/Source/DafnyCore/AST/Grammar/ParseErrors.cs @@ -230,9 +230,7 @@ This attribute is obsolete and unmaintained. It will be removed from dafny in th Add(ErrorId.p_literal_string_required, @" The value of an options attribute cannot be a computed expression. It must be a literal string. -".TrimStart(), range => new List { - OneAction("enclose in quotes", range, "\"" + range.PrintOriginal() + "\"") -}); +".TrimStart(), range => [OneAction("enclose in quotes", range, "\"" + range.PrintOriginal() + "\"")]); // TODO - what about multiple leading underscores Add(ErrorId.p_no_leading_underscore, @@ -241,9 +239,7 @@ The value of an options attribute cannot be a computed expression. It must be a such identifiers are reserved for internal use. In match statements and expressions, an identifier that is a single underscore is used as a wild-card match. -".TrimStart(), range => new List { - OneAction("remove underscore", range, range.PrintOriginal().Substring(1)) - }); +".TrimStart(), range => [OneAction("remove underscore", range, range.PrintOriginal().Substring(1))]); Add(ErrorId.p_no_leading_underscore_2, @" @@ -251,9 +247,7 @@ that is a single underscore is used as a wild-card match. such identifiers are reserved for internal use. In match statements and expressions, an identifier that is a single underscore is used as a wild-card match. -".TrimStart(), range => new List { - OneAction("remove underscore", range, range.PrintOriginal().Substring(1)) - }); +".TrimStart(), range => [OneAction("remove underscore", range, range.PrintOriginal().Substring(1))]); Add(ErrorId.p_bitvector_too_large, @" @@ -283,10 +277,10 @@ Such an import would likely cause a circular module dependency error. The [syntax for a module declaration](https://dafny.org/latest/DafnyRef/DafnyRef#sec-modules) is either `module M { ... }` or `module M refines N { ... }` with optional attributes after the `module` keyword. This error message often occurs if the `refines` keyword is misspelled. -".TrimStart(), range => new List { - OneAction("replace '" + range.PrintOriginal() + "' with 'refines'", range, "refines"), - OneAction("remove '" + range.PrintOriginal() + "'", range, "", true) - }); +".TrimStart(), range => [ + OneAction("replace '" + range.PrintOriginal() + "' with 'refines'", range, "refines"), + OneAction("remove '" + range.PrintOriginal() + "'", range, "", true) + ]); Add(ErrorId.p_misplaced_least_or_greatest, @" @@ -387,10 +381,10 @@ The output of a predicate or function cannot be ghost. @" Because a mutable field does not have initializer, it must have a type (as in `var f: int`). `const` declarations may have initializers; if they do they do not need an explicit type. -".TrimStart(), range => new List { - OneAction("insert ': bool'", range, range.PrintOriginal() + ": bool"), - OneAction("insert ': int'", range, range.PrintOriginal() + ": int") - }); +".TrimStart(), range => [ + OneAction("insert ': bool'", range, range.PrintOriginal() + ": bool"), + OneAction("insert ': int'", range, range.PrintOriginal() + ": int") + ]); Add(ErrorId.p_no_init_for_var_field, @" @@ -414,10 +408,10 @@ The formal parameter name should be a simple identifier that is not a reserved w then the name must be given, as in `datatype D = D (i: int, nameonly j: int) {}` More detail is given [here](https://dafny.org/latest/DafnyRef/DafnyRef#sec-parameter-bindings). -".TrimStart(), range => new List { - OneAction("remove 'nameonly'", range, "", true), - OneAction("insert '_:'", range, range.PrintOriginal() + " _:") - }); +".TrimStart(), range => [ + OneAction("remove 'nameonly'", range, "", true), + OneAction("insert '_:'", range, range.PrintOriginal() + " _:") + ]); Add(ErrorId.p_should_be_yields_instead_of_returns, @" @@ -455,19 +449,19 @@ state properties of the otherwise uninterpreted or abstract type. The currently defined type characteristics are designated by `==` (equality - supporting), `0` (auto - initializable), `00` (non - empty), and `!new` (non - reference). ".TrimStart(), range => - range.Prev.val == "," ? - new List { - OneAction("remove comma", range.Prev, ""), - OneAction("insert '=='", range, "==" + range.PrintOriginal()), - OneAction("insert '0'", range, "0" + range.PrintOriginal()), - OneAction("insert '00'", range, "00" + range.PrintOriginal()), - OneAction("insert '!new'", range, "!new" + range.PrintOriginal()) } - : new List { + range.Prev.val == "," ? [ + OneAction("remove comma", range.Prev, ""), OneAction("insert '=='", range, "==" + range.PrintOriginal()), OneAction("insert '0'", range, "0" + range.PrintOriginal()), OneAction("insert '00'", range, "00" + range.PrintOriginal()), OneAction("insert '!new'", range, "!new" + range.PrintOriginal()) - }); + ] + : [ + OneAction("insert '=='", range, "==" + range.PrintOriginal()), + OneAction("insert '0'", range, "0" + range.PrintOriginal()), + OneAction("insert '00'", range, "00" + range.PrintOriginal()), + OneAction("insert '!new'", range, "!new" + range.PrintOriginal()) + ]); Add(ErrorId.p_illegal_type_characteristic, @" @@ -533,9 +527,7 @@ A reads clause lists the objects whose fields the function is allowed to read (o So it does not make sense to list `*` along with something more specific. If you mean that the function should be able to read anything, just list `*`. Otherwise, omit the `*` and list expressions containing all the objects that are read. -".TrimStart(), range => new List { - OneAction("remove *", IncludeComma(range), "", true) -}); +".TrimStart(), range => [OneAction("remove *", IncludeComma(range), "", true)]); Add(ErrorId.p_no_defaults_for_out_parameters, @" @@ -656,9 +648,9 @@ This error only occurs when the `experimentalPredicateAlwaysGhost` option is cho longer accepted. Use `function` for compiled, non-ghost functions and `ghost function` for non-compiled, ghost functions, and similarly for predicates. See [the documentation here](https://dafny.org/latest/DafnyRef/DafnyRef#sec-function-syntax). -".TrimStart(), range => new List { - OneAction("remove 'method'", range, "predicate", false), -}); +".TrimStart(), range => [ + OneAction("remove 'method'", range, "predicate", false) + ]); Add(ErrorId.p_deprecating_function_method, @" @@ -666,9 +658,9 @@ See [the documentation here](https://dafny.org/latest/DafnyRef/DafnyRef#sec-func longer accepted. Use `function` for compiled, non-ghost functions and `ghost function` for non-compiled, ghost functions, and similarly for predicates. See [the documentation here](https://dafny.org/latest/DafnyRef/DafnyRef#sec-function-syntax). -".TrimStart(), range => new List { - OneAction("remove 'method'", range, "function", false), -}); +".TrimStart(), range => [ + OneAction("remove 'method'", range, "function", false) + ]); Add(ErrorId.p_no_ghost_function_method, @" @@ -681,9 +673,9 @@ See [the documentation here](https://dafny.org/latest/DafnyRef/DafnyRef#sec-func and there is no longer any declaration of the form `function method`, and similarly for predicates. See [the documentation here](../DafnyRef/DafnyRef#sec-function-syntax). -".TrimStart(), range => new List { - OneAction("remove 'method'", range, "function", false), -}); +".TrimStart(), range => [ + OneAction("remove 'method'", range, "function", false) + ]); Add(ErrorId.p_no_ghost_predicate_method, @" @@ -696,26 +688,25 @@ See [the documentation here](../DafnyRef/DafnyRef#sec-function-syntax). and there is no longer any declaration of the form `function method`, and similarly for predicates. See [the documentation here](../DafnyRef/DafnyRef#sec-function-syntax). -".TrimStart(), range => new List { - OneAction("remove 'method'", range, "predicate", false), -}); +".TrimStart(), range => [ + OneAction("remove 'method'", range, "predicate", false) + ]); Add(ErrorId.p_migration_syntax, @" This error occurs only when using `migration3to4`. With this option, ghost functions are declared using `ghost function` and compiled functions using `function method`. Change `function` in the declaration to one of these. -".TrimStart(), range => new List { - OneAction("add 'ghost'", range, "ghost function", false), - OneAction("add 'method'", range, "function method", false), -}); +".TrimStart(), range => [ + OneAction("add 'ghost'", range, "ghost function", false), + OneAction("add 'method'", range, "function method", false) + ]); Add(ErrorId.p_no_ghost_formal, @" A ghost predicate or function effectively has all ghost formal parameters, so they cannot be declared ghost in addition. -".TrimStart(), range => range.PrintOriginal() != "ghost" ? - new List { } - : new List { OneAction("remove 'ghost'", range, "", true) } -); +".TrimStart(), range => range.PrintOriginal() != "ghost" ? [] + : [OneAction("remove 'ghost'", range, "", true)] + ); Add(ErrorId.p_no_decreases_for_extreme_predicates, @" @@ -727,19 +718,20 @@ See [the documentation here](../DafnyRef/DafnyRef#sec-function-syntax). @" A predicate is a function that returns `bool`. The return type here is something else. If you mean to have a non-`bool` return type, use `function` instead of `predicate`. -".TrimStart(), range => new List { - OneAction("remove type", new SourceOrigin(range.StartToken.Prev, range.EndToken), "", true), - OneAction("replace type with 'bool'", range, "bool", true) } -); +".TrimStart(), range => [ + OneAction("remove type", new SourceOrigin(range.StartToken.Prev, range.EndToken), "", true), + OneAction("replace type with 'bool'", range, "bool", true) + ] + ); Add(ErrorId.p_no_return_type_for_predicate, @" A `predicate` is simply a `function` that returns a `bool` value. Accordingly, the type is (required to be) omitted, unless the result is being named. So `predicate p(): (res: bool) { true }` is permitted. -".TrimStart(), range => new List { - OneAction("remove type", new SourceOrigin(range.StartToken.Prev, range.EndToken), "", true), - }); +".TrimStart(), range => [ + OneAction("remove type", new SourceOrigin(range.StartToken.Prev, range.EndToken), "", true) + ]); Add(ErrorId.p_no_wild_expression, @" @@ -762,12 +754,12 @@ This is not a legal start to a statement. Most commonly either * a `var` or `const` keyword is missing, and the `x:` is the beginning of a declaration, or * a `label` keyword is missing and the identifier is the label for the statement that follows. (The second error is somewhat common because in C/C++ and Java, there is no keyword introducing a label, just the identifier and the colon.) -".TrimStart(), range => new List { - OneAction("insert 'label'", range, "label " + range.PrintOriginal(), false), - OneAction("insert 'var'", range, "var " + range.PrintOriginal(), false), - OneAction("insert 'const'", range, "const " + range.PrintOriginal(), false), - OneAction("change ':' to ':='", range, range.PrintOriginal() + "=", false), - }); +".TrimStart(), range => [ + OneAction("insert 'label'", range, "label " + range.PrintOriginal(), false), + OneAction("insert 'var'", range, "var " + range.PrintOriginal(), false), + OneAction("insert 'const'", range, "const " + range.PrintOriginal(), false), + OneAction("change ':' to ':='", range, range.PrintOriginal() + "=", false) + ]); Add(ErrorId.p_initializing_display_only_for_1D_arrays, @" @@ -778,11 +770,11 @@ but multi-dimensional arrays cannot. The alternatives are to initialize the arra ".TrimStart()); ActionSignature sharedLambda = delegate (SourceOrigin range) { - return new List { + return [ OneAction("replace with ':='", range, ":=", false), OneAction("replace with ':-", range, ":-", false), - OneAction("replace with ':|'", range, ":|", false), - }; + OneAction("replace with ':|'", range, ":|", false) + ]; }; Add(ErrorId.p_no_equal_for_initializing, @@ -825,10 +817,10 @@ method m() { } ``` is legal, but not at all recommended. -".TrimStart(), range => new List { - OneAction("replace with 'to'", range, "to", false), - OneAction("replace with 'downto'", range, "downto", false), - }); +".TrimStart(), range => [ + OneAction("replace with 'to'", range, "to", false), + OneAction("replace with 'downto'", range, "downto", false) + ]); Add(ErrorId.p_no_decreases_expressions_with_star, @" @@ -866,13 +858,13 @@ But the sequence of operators must obey certain patterns similar to chaining exp in the body of the calc statement. But the operator has to be transitive: `!=` is not allowed; `==`, `<`, `<=`, '>' and '>=' are allowed. -".TrimStart(), range => new List { - OneAction("replace with '=='", range, "==", false), - OneAction("replace with '<'", range, "<", false), - OneAction("replace with '<='", range, "<=", false), - OneAction("replace with '>='", range, ">=", false), - OneAction("replace with '>'", range, ">", false), - }); +".TrimStart(), range => [ + OneAction("replace with '=='", range, "==", false), + OneAction("replace with '<'", range, "<", false), + OneAction("replace with '<='", range, "<=", false), + OneAction("replace with '>='", range, ">=", false), + OneAction("replace with '>'", range, ">", false) + ]); Add(ErrorId.p_invalid_calc_op_combination, @" @@ -1009,10 +1001,10 @@ As described [here](../DafnyRef/DafnyRef#sec-collection-types), (one of `==`, `!=`, `>`, `>=`, `<`, `<=`, `!!`, `in`, `!in`). But the parser saw just a `!` , which could be the beginning of `!=`, `!!`, or `!in`, but is not continued as such. So perhaps there is extraneous white space or something else entirely is intended. -".TrimStart(), range => new List { - OneAction("replace with `!=`", range, "!=", false), - OneAction("replace with `!!`", range, "!!", false), -}); +".TrimStart(), range => [ + OneAction("replace with `!=`", range, "!=", false), + OneAction("replace with `!!`", range, "!!", false) + ]); Add(ErrorId.p_invalid_relational_op, @" @@ -1046,10 +1038,10 @@ so this means a character literal can only contain a character that can be repre @" Bindings of the form `x := y` are used in map-display expressions, in which case they are enclosed in square brackets, not parentheses. `var c := ( 4 := 5 )` should be `var c := map[ 4 := 5 ]`. -".TrimStart(), range => new List { - OneAction("replace `( )` with `map[ ]`", range, "map[" + range.PrintOriginal()[1..^1] + "]", false), - OneAction("replace `( )` with `imap[ ]`", range, "imap[" + range.PrintOriginal()[1..^1] + "]", false), -}); +".TrimStart(), range => [ + OneAction("replace `( )` with `map[ ]`", range, "map[" + range.PrintOriginal()[1..^1] + "]", false), + OneAction("replace `( )` with `imap[ ]`", range, "imap[" + range.PrintOriginal()[1..^1] + "]", false) + ]); Add(ErrorId.p_must_be_multiset, @" diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index a2dee52d68f..2de47686c99 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -18,7 +18,7 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca dummyRhs = new ExprRhs(dummyExpr); dummyFrameExpr = new FrameExpression(dummyExpr.Origin, dummyExpr, null); dummyStmt = new ReturnStmt(Token.NoToken, null); - var dummyBlockStmt = new BlockStmt(Token.NoToken, new List()); + var dummyBlockStmt = new BlockStmt(Token.NoToken, []); dummyIfStmt = new IfStmt(Token.NoToken, false, null, dummyBlockStmt, null); theOptions = new DafnyOptions(options); @@ -646,7 +646,7 @@ int StringToInt(string s, int defaultValue, string errString, IOrigin tok) { readonly Statement/*!*/ dummyStmt; readonly Statement/*!*/ dummyIfStmt; public readonly FileModuleDefinition theModule; - public readonly List> SystemModuleModifiers = new(); + public readonly List> SystemModuleModifiers = []; DafnyOptions theOptions; int anonymousIds = 0; diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index 5a90611bf4b..6e02e53546e 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -570,7 +570,7 @@ void PrintModuleExportDecl(CompilationData compilation, ModuleExportDecl m, int if (id.Decl is TopLevelDecl) { PrintTopLevelDecls(compilation, new List { (TopLevelDecl)id.Decl }, indent + IndentAmount, null); } else if (id.Decl is MemberDecl) { - PrintMembers(new List { (MemberDecl)id.Decl }, indent + IndentAmount, project); + PrintMembers([(MemberDecl)id.Decl], indent + IndentAmount, project); } } Indent(indent); @@ -854,7 +854,7 @@ public void PrintDatatype(DatatypeDecl dt, int indent, DafnyProject dafnyProject string sep = ""; foreach (DatatypeCtor ctor in dt.Ctors) { wr.Write(sep); - PrintClassMethodHelper(ctor.IsGhost ? " ghost" : "", ctor.Attributes, ctor.Name, new List()); + PrintClassMethodHelper(ctor.IsGhost ? " ghost" : "", ctor.Attributes, ctor.Name, []); if (ctor.Formals.Count != 0) { PrintFormals(ctor.Formals, null); } @@ -1117,7 +1117,7 @@ internal void PrintFormals(List ff, ICallable/*?*/ context, string name wr.Write("["); PrintFormal(ff[0], false); wr.Write("]"); - ff = new List(ff.Skip(1)); + ff = [.. ff.Skip(1)]; } wr.Write("("); string sep = ""; diff --git a/Source/DafnyCore/AST/Grammar/ProgramParser.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs index 4a011f9669f..9296c48580c 100644 --- a/Source/DafnyCore/AST/Grammar/ProgramParser.cs +++ b/Source/DafnyCore/AST/Grammar/ProgramParser.cs @@ -276,7 +276,7 @@ protected virtual DfyParseFileResult ParseFile(DafnyOptions options, FileSnapsho Uri uri, CancellationToken cancellationToken) /* throws System.IO.IOException */ { Contract.Requires(uri != null); using var reader = fileSnapshot.Reader; - var text = SourcePreprocessor.ProcessDirectives(reader, new List()); + var text = SourcePreprocessor.ProcessDirectives(reader, []); return ParseFile(options, fileSnapshot.Version, text, uri, cancellationToken); } diff --git a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs index 00c0eb8ee4d..e6aea52a40f 100644 --- a/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs +++ b/Source/DafnyCore/AST/Grammar/SourcePreprocessor.cs @@ -62,7 +62,7 @@ public static string ProcessDirectives(TextReader reader, List /*!*/ def Contract.Ensures(Contract.Result() != null); string newline = null; StringBuilder sb = new StringBuilder(); - List /*!*/ ifDirectiveStates = new List(); // readState.Count is the current nesting level of #if's + List /*!*/ ifDirectiveStates = []; // readState.Count is the current nesting level of #if's int ignoreCutoff = -1; // -1 means we're not ignoring; for 0<=n, n means we're ignoring because of something at nesting level n while (true) //invariant -1 <= ignoreCutoff && ignoreCutoff < readState.Count; diff --git a/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs b/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs index 6242c26fc63..6b8b986a1a5 100644 --- a/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs +++ b/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs @@ -628,7 +628,7 @@ public bool SetIndentUpdateStmt(ConcreteAssignStatement stmt, int indent, bool i var rhss = stmt is AssignStatement updateStmt ? updateStmt.Rhss : stmt is AssignOrReturnStmt assignOrReturnStmt ? new List { assignOrReturnStmt.Rhs } .Concat(assignOrReturnStmt.Rhss).ToList() - : new List(); + : []; // For single Rhs that are of the form [new] X(args....), // we can even further decrease the indent so that the last parenthesis diff --git a/Source/DafnyCore/AST/Members/ConstantField.cs b/Source/DafnyCore/AST/Members/ConstantField.cs index 6aa3aeacc9a..7318d495490 100644 --- a/Source/DafnyCore/AST/Members/ConstantField.cs +++ b/Source/DafnyCore/AST/Members/ConstantField.cs @@ -28,8 +28,8 @@ public override bool CanBeRevealed() { public bool ContainsHide { get; set; } public new bool IsGhost { get { return this.isGhost; } } - public List TypeArgs { get { return new List(); } } - public List Ins { get { return new List(); } } + public List TypeArgs { get { return []; } } + public List Ins { get { return []; } } public ModuleDefinition EnclosingModule { get { return this.EnclosingClass.EnclosingModuleDefinition; } } public bool MustReverify { get { return false; } } public bool AllowsNontermination { get { throw new cce.UnreachableException(); } } diff --git a/Source/DafnyCore/AST/Members/Constructor.cs b/Source/DafnyCore/AST/Members/Constructor.cs index b5171440180..116991613d7 100644 --- a/Source/DafnyCore/AST/Members/Constructor.cs +++ b/Source/DafnyCore/AST/Members/Constructor.cs @@ -45,7 +45,7 @@ public Constructor(IOrigin origin, Name name, Specification decreases, DividedBlockStmt body, Attributes attributes, IOrigin signatureEllipsis) - : base(origin, name, false, isGhost, typeArgs, ins, new List(), req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { + : base(origin, name, false, isGhost, typeArgs, ins, [], req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(origin != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); diff --git a/Source/DafnyCore/AST/Members/ExtremePredicate.cs b/Source/DafnyCore/AST/Members/ExtremePredicate.cs index 5d2088c808d..492ff97215f 100644 --- a/Source/DafnyCore/AST/Members/ExtremePredicate.cs +++ b/Source/DafnyCore/AST/Members/ExtremePredicate.cs @@ -13,7 +13,7 @@ public bool KNat { return TypeOfK == KType.Nat; } } - [FilledInDuringResolution] public readonly List Uses = new List(); // used by verifier + [FilledInDuringResolution] public readonly List Uses = []; // used by verifier [FilledInDuringResolution] public PrefixPredicate PrefixPredicate; // (name registration) public override IEnumerable Children => base.Children.Concat(new[] { PrefixPredicate }); @@ -24,7 +24,7 @@ public ExtremePredicate(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, b List req, Specification reads, List ens, Expression body, Attributes attributes, IOrigin signatureEllipsis) : base(rangeOrigin, name, hasStaticKeyword, true, isOpaque, typeArgs, ins, result, Type.Bool, - req, reads, ens, new Specification(new List(), null), body, null, null, attributes, signatureEllipsis) { + req, reads, ens, new Specification([], null), body, null, null, attributes, signatureEllipsis) { TypeOfK = typeOfK; } diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index c9384adaa12..8f2cb901e92 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/Source/DafnyCore/AST/Members/Function.cs @@ -76,7 +76,7 @@ public override IEnumerable Assumptions(Declaration decl) { } foreach (var c in this.Descendants()) { - foreach (var a in (c as Node)?.Assumptions(this) ?? Enumerable.Empty()) { + foreach (var a in (c as Node)?.Assumptions(this) ?? []) { yield return a; } } @@ -149,8 +149,8 @@ public enum TailStatus { Concat(Ens.Select(e => e.E)). Concat(Decreases.Expressions). Concat(Ins). - Concat(Result != null ? new List() { Result } : new List()). - Concat(ResultType != null ? new List() { ResultType } : new List()). + Concat(Result != null ? [Result] : new List()). + Concat(ResultType != null ? [ResultType] : new List()). Concat(Body == null ? Enumerable.Empty() : new[] { Body }); public override IEnumerable PreResolveChildren => @@ -159,7 +159,7 @@ public enum TailStatus { Concat(Req). Concat(Ens). Concat(Decreases.Expressions.Where(expression => expression is not AutoGeneratedExpression)). - Concat(Ins).Concat(ResultType != null && ResultType.Origin.line > 0 ? new List() { ResultType } : new List()). + Concat(Ins).Concat(ResultType != null && ResultType.Origin.line > 0 ? [ResultType] : new List()). Concat(Body == null ? Enumerable.Empty() : new[] { Body }). Concat(ByMethodBody == null ? Enumerable.Empty() : new[] { ByMethodBody }); @@ -208,7 +208,7 @@ public bool AllowsNontermination { /// The field is filled in during resolution (and used toward the end of resolution, to attach a helpful "decreases" prefix to functions in clusters /// with co-recursive calls. /// - public readonly List AllCalls = new List(); + public readonly List AllCalls = []; public enum CoCallClusterInvolvement { None, // the SCC containing the function does not involve any co-recursive calls IsMutuallyRecursiveTarget, // the SCC contains co-recursive calls, and this function is the target of some non-self recursive call @@ -552,7 +552,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies rewriter, Dafn } var currentClass = EnclosingClass; - List addedReveals = new(); + List addedReveals = []; foreach (var func in rewriter.GetEnumerator(this, currentClass, SubExpressions)) { var revealStmt = diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index 68437269621..31b41fb98db 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -135,8 +135,8 @@ public bool ContainsHide { set => throw new NotSupportedException(); } bool ICodeContext.IsGhost { get { return true; } } - List ICodeContext.TypeArgs { get { return new List(); } } - List ICodeContext.Ins { get { return new List(); } } + List ICodeContext.TypeArgs { get { return []; } } + List ICodeContext.Ins { get { return []; } } ModuleDefinition IASTVisitorContext.EnclosingModule { get { return Module; } } bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } diff --git a/Source/DafnyCore/AST/Members/MemberDecl.cs b/Source/DafnyCore/AST/Members/MemberDecl.cs index 6f72e2204bd..98ffea0414e 100644 --- a/Source/DafnyCore/AST/Members/MemberDecl.cs +++ b/Source/DafnyCore/AST/Members/MemberDecl.cs @@ -115,7 +115,7 @@ public virtual string FullSanitizedName { } } - public virtual IEnumerable SubExpressions => Enumerable.Empty(); + public virtual IEnumerable SubExpressions => []; public override IEnumerable Assumptions(Declaration decl) { foreach (var a in base.Assumptions(this)) { @@ -148,7 +148,7 @@ public void RecursiveCallParameters(IOrigin tok, List typeParams, receiver.Type = ModuleResolver.GetReceiverType(tok, this); // resolve here } - arguments = new List(); + arguments = []; foreach (var inFormal in ins) { Expression inE; if (substMap.TryGetValue(inFormal, out inE)) { diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index efb84b83cf9..a012816966b 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/Source/DafnyCore/AST/Members/Method.cs @@ -78,7 +78,7 @@ public override IEnumerable Assumptions(Declaration decl) { } foreach (var c in this.Descendants()) { - foreach (var a in (c as Node)?.Assumptions(this) ?? Enumerable.Empty()) { + foreach (var a in (c as Node)?.Assumptions(this) ?? []) { yield return a; } } @@ -467,7 +467,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn } var currentClass = EnclosingClass; - List addedReveals = new(); + List addedReveals = []; foreach (var func in Rewriter.GetEnumerator(this, currentClass, SubExpressions)) { var revealStmt = diff --git a/Source/DafnyCore/AST/Members/SpecialField.cs b/Source/DafnyCore/AST/Members/SpecialField.cs index 1d930da163a..285a5651ec1 100644 --- a/Source/DafnyCore/AST/Members/SpecialField.cs +++ b/Source/DafnyCore/AST/Members/SpecialField.cs @@ -71,8 +71,8 @@ public DatatypeDiscriminator(IOrigin origin, Name name, ID specialId, object idP } public class DatatypeDestructor : SpecialField { - public readonly List EnclosingCtors = new List(); // is always a nonempty list - public readonly List CorrespondingFormals = new List(); // is always a nonempty list + public readonly List EnclosingCtors = []; // is always a nonempty list + public readonly List CorrespondingFormals = []; // is always a nonempty list [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(EnclosingCtors != null); diff --git a/Source/DafnyCore/AST/Modules/AccessibleMember.cs b/Source/DafnyCore/AST/Modules/AccessibleMember.cs index 151d038dad8..d9fb5a2e824 100644 --- a/Source/DafnyCore/AST/Modules/AccessibleMember.cs +++ b/Source/DafnyCore/AST/Modules/AccessibleMember.cs @@ -19,7 +19,7 @@ public AccessibleMember(List accessPath, bool isRevealed = true) { } public AccessibleMember(bool isRevealed = true) { - AccessPath = new List(); + AccessPath = []; IsRevealed = isRevealed; } diff --git a/Source/DafnyCore/AST/Modules/DefaultClassDecl.cs b/Source/DafnyCore/AST/Modules/DefaultClassDecl.cs index 5d0c4a0b474..3d4c7ee1f0a 100644 --- a/Source/DafnyCore/AST/Modules/DefaultClassDecl.cs +++ b/Source/DafnyCore/AST/Modules/DefaultClassDecl.cs @@ -12,7 +12,7 @@ public class DefaultClassDecl : TopLevelDeclWithMembers, RevealableTypeDecl { public TypeDeclSynonymInfo SynonymInfo { get; set; } public DefaultClassDecl(ModuleDefinition module, [Captured] List members) - : base(SourceOrigin.NoToken, new Name("_default"), module, new List(), members, null, false, null) { + : base(SourceOrigin.NoToken, new Name("_default"), module, [], members, null, false, null) { Contract.Requires(module != null); Contract.Requires(cce.NonNullElements(members)); this.NewSelfSynonym(); diff --git a/Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs b/Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs index bdfc6d8b488..861454f1c9c 100644 --- a/Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs @@ -5,13 +5,13 @@ namespace Microsoft.Dafny; public class DefaultModuleDefinition : ModuleDefinition, ICloneable { - public List Includes { get; } = new(); + public List Includes { get; } = []; public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) : base(cloner, original, original.NameNode) { } public DefaultModuleDefinition() - : base(SourceOrigin.NoToken, new Name("_module"), new List(), ModuleKindEnum.Concrete, false, + : base(SourceOrigin.NoToken, new Name("_module"), [], ModuleKindEnum.Concrete, false, null, null, null) { } diff --git a/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs b/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs index e0cbe4db640..551e146e0e6 100644 --- a/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs @@ -10,10 +10,10 @@ namespace Microsoft.Dafny; /// https://github.com/dafny-lang/dafny/issues/3027 /// public class FileModuleDefinition : ModuleDefinition { - public List Includes { get; } = new(); + public List Includes { get; } = []; public FileModuleDefinition(IOrigin token) : - base(token, new Name("_module"), new List(), + base(token, new Name("_module"), [], ModuleKindEnum.Concrete, false, null, null, null) { { } diff --git a/Source/DafnyCore/AST/Modules/ModuleDecl.cs b/Source/DafnyCore/AST/Modules/ModuleDecl.cs index 43356564d16..658ed86ba8c 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDecl.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDecl.cs @@ -46,7 +46,7 @@ protected ModuleDecl(Cloner cloner, ModuleDecl original, ModuleDefinition parent } protected ModuleDecl(DafnyOptions options, IOrigin origin, Name name, ModuleDefinition parent, bool opened, bool isRefining, Guid cloneId) - : base(origin, name, parent, new List(), null, isRefining) { + : base(origin, name, parent, [], null, isRefining) { Options = options; Height = -1; Signature = null; @@ -66,7 +66,7 @@ public virtual string GetTriviaContainingDocstring() { } var tokens = OwnedTokens.Any() ? OwnedTokens : - PreResolveChildren.Any() ? PreResolveChildren.First().OwnedTokens : Enumerable.Empty(); + PreResolveChildren.Any() ? PreResolveChildren.First().OwnedTokens : []; foreach (var token in tokens) { if (token.val == "{") { if ((token.Prev.TrailingTrivia + token.LeadingTrivia).Trim() is { } tentativeTrivia and not "") { diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index c604abdc537..65047f0d466 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -79,11 +79,11 @@ public string FullName { public DefaultClassDecl DefaultClass { get; set; } - public readonly List SourceDecls = new(); + public readonly List SourceDecls = []; [FilledInDuringResolution] - public readonly List ResolvedPrefixNamedModules = new(); + public readonly List ResolvedPrefixNamedModules = []; [FilledInDuringResolution] - public readonly List PrefixNamedModules = new(); // filled in by the parser; emptied by the resolver + public readonly List PrefixNamedModules = []; // filled in by the parser; emptied by the resolver public CallRedirector CallRedirector { get; set; } @@ -169,7 +169,7 @@ public ModuleDefinition(IOrigin tok, Name name, List prefixIds, ModuleK this.IsFacade = isFacade; if (Name != "_System") { - DefaultClass = new DefaultClassDecl(this, new List()); + DefaultClass = new DefaultClassDecl(this, []); } } @@ -632,7 +632,7 @@ public void ProcessPrefixNamedModules() { foreach (var (name, prefixNamedModules) in prefixModulesByFirstPart) { var prefixNameModule = prefixNamedModules.First(); var firstPartToken = prefixNameModule.Parts[0]; - var modDef = new ModuleDefinition(SourceOrigin.NoToken, new Name(firstPartToken, name), new List(), ModuleKindEnum.Concrete, + var modDef = new ModuleDefinition(SourceOrigin.NoToken, new Name(firstPartToken, name), [], ModuleKindEnum.Concrete, false, null, this, null); // Add the new module to the top-level declarations of its parent and then bind its names as usual @@ -705,9 +705,7 @@ private static PrefixNameModule ShortenPrefix(PrefixNameModule prefixNameModule) } private static readonly List<(string, string)> incompatibleAttributePairs = - new() { - ("rlimit", "resource_limit") - }; + [("rlimit", "resource_limit")]; private void CheckIncompatibleAttributes(ModuleResolver resolver, Attributes attrs) { foreach (var pair in incompatibleAttributePairs) { diff --git a/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs b/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs index a8f02386389..b8be14a1370 100644 --- a/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs +++ b/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs @@ -13,7 +13,7 @@ public class ModuleExportDecl : ModuleDecl, ICanFormat { public readonly bool IsDefault; public List Exports; // list of TopLevelDecl that are included in the export public List Extends; // list of exports that are extended - [FilledInDuringResolution] public readonly List ExtendDecls = new(); + [FilledInDuringResolution] public readonly List ExtendDecls = []; public bool RevealAll; // only kept for initial rewriting, then discarded public bool ProvideAll; public override IEnumerable Children => Exports; diff --git a/Source/DafnyCore/AST/Modules/ScopeCloner.cs b/Source/DafnyCore/AST/Modules/ScopeCloner.cs index 6147d1301af..3a9e399fc25 100644 --- a/Source/DafnyCore/AST/Modules/ScopeCloner.cs +++ b/Source/DafnyCore/AST/Modules/ScopeCloner.cs @@ -49,7 +49,7 @@ public override ModuleDefinition CloneModuleDefinition(ModuleDefinition m, Modul } if (!declmap.ContainsKey(def)) { - declmap.Add(def, new List()); + declmap.Add(def, []); sigmap.Add(def, new ModuleSignature()); vismap.Add(def, new VisibilityScope()); } @@ -93,10 +93,10 @@ public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition n if (d is (RevealableTypeDecl or TopLevelDeclWithMembers) and not DefaultClassDecl && !RevealedInScope(d)) { var tps = d.TypeArgs.ConvertAll(CloneTypeParam); var characteristics = TypeParameter.GetExplicitCharacteristics(d); - var members = based is TopLevelDeclWithMembers tm ? tm.Members : new List(); + var members = based is TopLevelDeclWithMembers tm ? tm.Members : []; // copy the newParent traits only if "d" is already an AbstractTypeDecl and is being export-revealed var otd = new AbstractTypeDecl(Origin(d.Origin), d.NameNode.Clone(this), newParent, characteristics, tps, - new List(), // omit the newParent traits + [], // omit the newParent traits members, CloneAttributes(d.Attributes), d.IsRefining); based = otd; if (d is ClassLikeDecl { IsReferenceTypeDecl: true } cl) { @@ -126,7 +126,7 @@ public override Function CloneFunction(Function f, string newName = null) { Contract.Assert(basef.Body != null); // a function-by-method has a nonempty .Body if (RevealedInScope(f)) { // For an "export reveals", use an empty (but not absent) by-method part. - basef.ByMethodBody = new BlockStmt(basef.ByMethodBody.Origin, new List()); + basef.ByMethodBody = new BlockStmt(basef.ByMethodBody.Origin, []); } else { // For an "export provides", remove the by-method part altogether. basef.ByMethodTok = null; diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 3007867104d..1ba164453e1 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs @@ -12,12 +12,12 @@ public class AssignOrReturnStmt : ConcreteAssignStatement, ICloneable Rhss; public readonly AttributedToken KeywordToken; - [FilledInDuringResolution] public readonly List ResolvedStatements = new(); + [FilledInDuringResolution] public readonly List ResolvedStatements = []; public override IEnumerable SubStatements => ResolvedStatements; public override IEnumerable Children => ResolvedStatements; - public override IEnumerable PreResolveSubStatements => Enumerable.Empty(); + public override IEnumerable PreResolveSubStatements => []; [ContractInvariantMethod] void ObjectInvariant() { @@ -263,7 +263,7 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract, for (int k = (expectExtract ? 1 : 0); k < Lhss.Count; ++k) { lhss2.Add(Lhss[k]); } - List rhss2 = new List() { Rhs }; + List rhss2 = [Rhs]; if (Rhss != null) { Rhss.ForEach(e => rhss2.Add(e)); } @@ -312,13 +312,15 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract, // "if temp.IsFailure()" new IfStmt(Origin, false, resolver.VarDotMethod(Origin, temp, "IsFailure"), // THEN: { out := temp.PropagateFailure(); return; } - new BlockStmt(Origin, new List() { + new BlockStmt(Origin, [ new AssignStatement(Origin, - new List() { ident }, - new List() { new ExprRhs(resolver.VarDotMethod(Origin, temp, "PropagateFailure")) } + [ident], + [new ExprRhs(resolver.VarDotMethod(Origin, temp, "PropagateFailure"))] ), - new ReturnStmt(Origin, null), - }), + + new ReturnStmt(Origin, null) + + ]), // ELSE: no else block null )); @@ -329,8 +331,8 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract, var lhs = Lhss[0]; ResolvedStatements.Add( new AssignStatement(Origin, - new List() { lhsExtract }, - new List() { new ExprRhs(resolver.VarDotMethod(Origin, temp, "Extract")) } + [lhsExtract], + [new ExprRhs(resolver.VarDotMethod(Origin, temp, "Extract"))] )); // The following check is not necessary, because the ghost mismatch is caught later. // However the error message here is much clearer. diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs index 204dc277d5b..cd1530df19e 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs @@ -16,12 +16,12 @@ public class AssignStatement : ConcreteAssignStatement, ICloneable SubStatements => Children.OfType(); public override IEnumerable NonSpecificationSubExpressions => - ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : Enumerable.Empty(); + ResolvedStatements == null ? Rhss.SelectMany(r => r.NonSpecificationSubExpressions) : []; public override IEnumerable Children => ResolvedStatements ?? Lhss.Concat(Rhss); public override IEnumerable PreResolveChildren => Lhss.Concat(Rhss); - public override IEnumerable PreResolveSubStatements => Enumerable.Empty(); + public override IEnumerable PreResolveSubStatements => []; [ContractInvariantMethod] void ObjectInvariant() { @@ -86,7 +86,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti IOrigin firstEffectfulRhs = null; MethodCallInformation methodCallInfo = null; - ResolvedStatements = new(); + ResolvedStatements = []; foreach (var rhs in Rhss) { bool isEffectful; if (rhs is TypeRhs) { diff --git a/Source/DafnyCore/AST/Statements/Assignment/TypeRhs.cs b/Source/DafnyCore/AST/Statements/Assignment/TypeRhs.cs index 99e19b86be1..26cecea8dbb 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/TypeRhs.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/TypeRhs.cs @@ -67,7 +67,7 @@ public TypeRhs(Cloner cloner, TypeRhs original) if (original.ArrayDimensions != null) { if (original.InitDisplay != null) { Contract.Assert(original.ArrayDimensions.Count == 1); - ArrayDimensions = new List { cloner.CloneExpr(original.ArrayDimensions[0]) }; + ArrayDimensions = [cloner.CloneExpr(original.ArrayDimensions[0])]; InitDisplay = original.InitDisplay.ConvertAll(cloner.CloneExpr); } else { ArrayDimensions = original.ArrayDimensions.Select(cloner.CloneExpr).ToList(); @@ -115,7 +115,7 @@ public TypeRhs(IOrigin origin, Type type, Expression dim, List initD Contract.Requires(dim != null); Contract.Requires(initDisplay != null); EType = type; - ArrayDimensions = new List { dim }; + ArrayDimensions = [dim]; InitDisplay = initDisplay; } public TypeRhs(IOrigin origin, Type type) @@ -205,5 +205,5 @@ public override IEnumerable Children { (Bindings != null ? Arguments : null) ?? Enumerable.Empty()); - public override IEnumerable PreResolveSubStatements => Enumerable.Empty(); + public override IEnumerable PreResolveSubStatements => []; } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/BlockByProofStmt.cs b/Source/DafnyCore/AST/Statements/BlockByProofStmt.cs index ebade64175a..2eca3001817 100644 --- a/Source/DafnyCore/AST/Statements/BlockByProofStmt.cs +++ b/Source/DafnyCore/AST/Statements/BlockByProofStmt.cs @@ -35,7 +35,7 @@ internal static void ResolveByProof(INewOrOldResolver resolver, BlockStmt proof, var prevLblStmts = resolver.EnclosingStatementLabels; var prevLoopStack = resolver.LoopStack; resolver.EnclosingStatementLabels = new Scope(resolver.Options); - resolver.LoopStack = new List(); + resolver.LoopStack = []; resolver.ResolveStatement(proof, resolutionContext); resolver.EnclosingStatementLabels = prevLblStmts; resolver.LoopStack = prevLoopStack; diff --git a/Source/DafnyCore/AST/Statements/CalcStmt.cs b/Source/DafnyCore/AST/Statements/CalcStmt.cs index ab141b12989..e8d67809d19 100644 --- a/Source/DafnyCore/AST/Statements/CalcStmt.cs +++ b/Source/DafnyCore/AST/Statements/CalcStmt.cs @@ -207,7 +207,7 @@ public CalcOp GetInferredDefaultOp() { public static readonly CalcOp DefaultOp = new BinaryCalcOp(BinaryExpr.Opcode.Eq); - public override IEnumerable Children => Steps.Concat(Result != null ? new Node[] { Result } : new Node[] { }).Concat(Hints); + public override IEnumerable Children => Steps.Concat(Result != null ? [Result] : new Node[] { }).Concat(Hints); public override IEnumerable PreResolveChildren => Lines.Take(Lines.Count > 0 ? Lines.Count - 1 : 0).Concat(Hints.Where(hintBatch => hintBatch.Body.Count() != 0)); [ContractInvariantMethod] @@ -236,7 +236,7 @@ public CalcStmt(IOrigin origin, CalcOp userSuppliedOp, List lines, L UserSuppliedOp = userSuppliedOp; Lines = lines; Hints = hints; - Steps = new List(); + Steps = []; StepOps = stepOps; Result = null; Attributes = attrs; @@ -264,7 +264,7 @@ public CalcStmt(Cloner cloner, CalcStmt original) : base(cloner, original) { Result = cloner.CloneExpr(original.Result); Op = original.Op; } else { - Steps = new List(); + Steps = []; } } diff --git a/Source/DafnyCore/AST/Statements/Statement.cs b/Source/DafnyCore/AST/Statements/Statement.cs index 03452a29d13..7e5e09184e1 100644 --- a/Source/DafnyCore/AST/Statements/Statement.cs +++ b/Source/DafnyCore/AST/Statements/Statement.cs @@ -72,7 +72,7 @@ public virtual IEnumerable SubStatements { public IEnumerable DescendantsAndSelf { get { Stack todo = new(); - List result = new(); + List result = []; todo.Push(this); while (todo.Any()) { var current = todo.Pop(); @@ -159,7 +159,7 @@ public static VarDeclStmt CreateLocalVariable(IOrigin tok, string name, Expressi var variableUpdateStmt = new AssignStatement(tok, Util.Singleton(variableExpr), Util.Singleton(new ExprRhs(value))); var variableAssignStmt = new SingleAssignStmt(tok, variableUpdateStmt.Lhss[0], variableUpdateStmt.Rhss[0]); - variableUpdateStmt.ResolvedStatements = new List() { variableAssignStmt }; + variableUpdateStmt.ResolvedStatements = [variableAssignStmt]; return new VarDeclStmt(tok, Util.Singleton(variable), variableUpdateStmt); } @@ -185,7 +185,7 @@ public override string ToString() { Concat( PreResolveSubStatements).Concat(PreResolveSubExpressions); - public virtual IEnumerable GetAssignedLocals() => Enumerable.Empty(); + public virtual IEnumerable GetAssignedLocals() => []; /// diff --git a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs index 154267b0823..42a619d2520 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs @@ -18,7 +18,7 @@ public AssertStmt(Cloner cloner, AssertStmt original) : base(cloner, original) { public static AssertStmt CreateErrorAssert(INode node, string message, Expression guard = null) { var errorMessage = new StringLiteralExpr(node.Origin, message, true); errorMessage.Type = new SeqType(Type.Char); - var attr = new Attributes("error", new List { errorMessage }, null); + var attr = new Attributes("error", [errorMessage], null); guard ??= Expression.CreateBoolLiteral(node.Origin, false); var assertFalse = new AssertStmt(node.Origin, guard, null, attr); assertFalse.IsGhost = true; diff --git a/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs b/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs index c31ca6f9e06..efd43255923 100644 --- a/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs @@ -12,16 +12,16 @@ public class HideRevealStmt : Statement, ICloneable, ICanFormat, public string KindVerb => Mode == HideRevealCmd.Modes.Hide ? "hidden" : "revealed"; public readonly List Exprs; [FilledInDuringResolution] - public readonly List LabeledAsserts = new(); // to indicate that "Expr" denotes a labeled assertion + public readonly List LabeledAsserts = []; // to indicate that "Expr" denotes a labeled assertion [FilledInDuringResolution] - public readonly List ResolvedStatements = new(); - [FilledInDuringResolution] public List OffsetMembers = new(); + public readonly List ResolvedStatements = []; + [FilledInDuringResolution] public List OffsetMembers = []; public HideRevealCmd.Modes Mode { get; private set; } public bool Wildcard { get; private set; } public override IEnumerable SubStatements => ResolvedStatements; - public override IEnumerable PreResolveSubStatements => Enumerable.Empty(); + public override IEnumerable PreResolveSubStatements => []; [ContractInvariantMethod] void ObjectInvariant() { @@ -121,9 +121,9 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext re var revealCallee = ((MemberSelectExpr)((ConcreteSyntaxExpression)exprClone).ResolvedExpression); if (revealCallee != null) { - var call = new CallStmt(Origin, new List(), + var call = new CallStmt(Origin, [], revealCallee, - new List(), effectiveExpr.Center); + [], effectiveExpr.Center); ResolvedStatements.Add(call); } } else { diff --git a/Source/DafnyCore/AST/Substituter.cs b/Source/DafnyCore/AST/Substituter.cs index 432b5c954fe..2c10f636d08 100644 --- a/Source/DafnyCore/AST/Substituter.cs +++ b/Source/DafnyCore/AST/Substituter.cs @@ -304,7 +304,7 @@ public virtual Expression Substitute(Expression expr) { var cases = new List(); foreach (var mc in nestedMatchExpr.Cases) { - List discoveredBvs = new(); + List discoveredBvs = []; ExtendedPattern SubstituteForPattern(ExtendedPattern pattern) { switch (pattern) { case DisjunctivePattern disjunctivePattern: @@ -494,7 +494,7 @@ private Expression LetExpr(LetExpr letExpr) { // keep copies of the substitution maps so we can reuse them at desugaring time var newSubstMap = new Dictionary(substMap); var newTypeMap = new Dictionary(typeMap); - return new BoogieGenerator.SubstLetExpr(letExpr.Origin, newLHSs, new List { rhs }, body, letExpr.Exact, letExpr, newSubstMap, newTypeMap, newBounds); + return new BoogieGenerator.SubstLetExpr(letExpr.Origin, newLHSs, [rhs], body, letExpr.Exact, letExpr, newSubstMap, newTypeMap, newBounds); } } @@ -683,7 +683,7 @@ Func, Type, VT, VT> cloneVt Expression substE = Substitute(elist[i]); if (substE != elist[i] && newElist == null) { - newElist = new List(); + newElist = []; for (int j = 0; j < i; j++) { newElist.Add(elist[j]); } @@ -781,7 +781,7 @@ protected virtual Statement SubstStmt(Statement stmt) { } // r.TargetStmt will be filled in as later if (!BreaksToBeResolved.TryGetValue(s, out var breaks)) { - breaks = new List(); + breaks = []; BreaksToBeResolved.Add(s, breaks); } breaks.Add(rr); diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index 2c8c02fa49f..dfd4ad059f7 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -73,7 +73,7 @@ public byte[] MyHash { [FilledInDuringResolution] public SpecialField ORDINAL_Offset; // used by the translator public readonly SubsetTypeDecl NatDecl; - public UserDefinedType Nat() { return new UserDefinedType(Token.NoToken, "nat", NatDecl, new List()); } + public UserDefinedType Nat() { return new UserDefinedType(Token.NoToken, "nat", NatDecl, []); } public readonly TraitDecl ObjectDecl; public UserDefinedType ObjectQ() { Contract.Assume(ObjectDecl != null); @@ -87,14 +87,14 @@ public Type ObjectSetType() { } public SystemModuleManager(DafnyOptions options) { - SystemModule = new(SourceOrigin.NoToken, new Name("_System"), new List(), + SystemModule = new(SourceOrigin.NoToken, new Name("_System"), [], ModuleKindEnum.Concrete, false, null, null, null); this.Options = options; SystemModule.Height = -1; // the system module doesn't get a height assigned later, so we set it here to something below everything else // create type synonym 'string' var str = new TypeSynonymDecl(SourceOrigin.NoToken, new Name("string"), new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false), - new List(), SystemModule, new SeqType(new CharType()), null); + [], SystemModule, new SeqType(new CharType()), null); SystemModule.SourceDecls.Add(str); // create subset type 'nat' var bvNat = new BoundVar(Token.NoToken, "x", Type.Int); @@ -102,11 +102,11 @@ public SystemModuleManager(DafnyOptions options) { var ax = AxiomAttribute(); NatDecl = new SubsetTypeDecl(SourceOrigin.NoToken, new Name("nat"), new TypeParameter.TypeParameterCharacteristics(TypeParameter.EqualitySupportValue.InferredRequired, Type.AutoInitInfo.CompilableValue, false), - new List(), SystemModule, bvNat, natConstraint, SubsetTypeDecl.WKind.CompiledZero, null, ax); + [], SystemModule, bvNat, natConstraint, SubsetTypeDecl.WKind.CompiledZero, null, ax); ((RedirectingTypeDecl)NatDecl).ConstraintIsCompilable = true; SystemModule.SourceDecls.Add(NatDecl); // create trait 'object' - ObjectDecl = new TraitDecl(SourceOrigin.NoToken, new Name("object"), SystemModule, new List(), new List(), DontCompile(), false, null); + ObjectDecl = new TraitDecl(SourceOrigin.NoToken, new Name("object"), SystemModule, [], [], DontCompile(), false, null); SystemModule.SourceDecls.Add(ObjectDecl); // add one-dimensional arrays, since they may arise during type checking // Arrays of other dimensions may be added during parsing as the parser detects the need for these @@ -121,7 +121,7 @@ public SystemModuleManager(DafnyOptions options) { // Several methods and fields rely on 1-argument arrow types CreateArrowTypeDecl(1); - valuetypeDecls = new[] { + valuetypeDecls = [ new ValuetypeDecl("bool", SystemModule, t => t.IsBoolType, typeArgs => Type.Bool), new ValuetypeDecl("char", SystemModule, t => t.IsCharType, typeArgs => Type.Char), new ValuetypeDecl("int", SystemModule, t => t.IsNumericBased(Type.NumericPersuasion.Int), typeArgs => Type.Int), @@ -130,26 +130,24 @@ public SystemModuleManager(DafnyOptions options) { new ValuetypeDecl("_bv", SystemModule, t => t.IsBitVectorType && !Options.Get(CommonOptionBag.TypeSystemRefresh), null), // "_bv" represents a family of classes, so no typeTester or type creator is supplied (it's used only in the legacy resolver) new ValuetypeDecl("set", SystemModule, - new List() { TypeParameter.TPVarianceSyntax.Covariant_Strict }, + [TypeParameter.TPVarianceSyntax.Covariant_Strict], t => t.AsSetType is { Finite: true }, typeArgs => new SetType(true, typeArgs[0])), new ValuetypeDecl("iset", SystemModule, - new List() { TypeParameter.TPVarianceSyntax.Covariant_Permissive }, + [TypeParameter.TPVarianceSyntax.Covariant_Permissive], t => t.IsISetType, typeArgs => new SetType(false, typeArgs[0])), new ValuetypeDecl("seq", SystemModule, - new List() { TypeParameter.TPVarianceSyntax.Covariant_Strict }, + [TypeParameter.TPVarianceSyntax.Covariant_Strict], t => t.AsSeqType != null, typeArgs => new SeqType(typeArgs[0])), new ValuetypeDecl("multiset", SystemModule, - new List() { TypeParameter.TPVarianceSyntax.Covariant_Strict }, + [TypeParameter.TPVarianceSyntax.Covariant_Strict], t => t.AsMultiSetType != null, typeArgs => new MultiSetType(typeArgs[0])), new ValuetypeDecl("map", SystemModule, - new List() - { TypeParameter.TPVarianceSyntax.Covariant_Strict, TypeParameter.TPVarianceSyntax.Covariant_Strict }, + [TypeParameter.TPVarianceSyntax.Covariant_Strict, TypeParameter.TPVarianceSyntax.Covariant_Strict], t => t.IsMapType, typeArgs => new MapType(true, typeArgs[0], typeArgs[1])), new ValuetypeDecl("imap", SystemModule, - new List() - { TypeParameter.TPVarianceSyntax.Covariant_Permissive, TypeParameter.TPVarianceSyntax.Covariant_Strict }, + [TypeParameter.TPVarianceSyntax.Covariant_Permissive, TypeParameter.TPVarianceSyntax.Covariant_Strict], t => t.IsIMapType, typeArgs => new MapType(false, typeArgs[0], typeArgs[1])) - }; + ]; SystemModule.SourceDecls.AddRange(valuetypeDecls); // Resolution error handling relies on being able to get to the 0-tuple declaration TupleType(Token.NoToken, 0, true); @@ -210,9 +208,9 @@ void AddMember(MemberDecl member, ValuetypeVariety valuetypeVariety) { public void AddRotateMember(ValuetypeDecl enclosingType, string name, Type resultType) { var formals = new List { new Formal(Token.NoToken, "w", Type.Nat(), true, false, null) }; var rotateMember = new SpecialFunction(SourceOrigin.NoToken, name, SystemModule, false, false, - new List(), formals, resultType, - new List(), new Specification(new List(), null), new List(), - new Specification(new List(), null), null, null, null); + [], formals, resultType, + [], new Specification([], null), [], + new Specification([], null), null, null, null); rotateMember.EnclosingClass = enclosingType; rotateMember.AddVisibilityScope(SystemModule.VisibilityScope, false); enclosingType.Members.Add(rotateMember); @@ -220,11 +218,11 @@ public void AddRotateMember(ValuetypeDecl enclosingType, string name, Type resul private Attributes DontCompile() { var flse = Expression.CreateBoolLiteral(Token.NoToken, false); - return new Attributes("compile", new List() { flse }, null); + return new Attributes("compile", [flse], null); } public static Attributes AxiomAttribute(Attributes prev = null) { - return new Attributes("axiom", new List(), prev); + return new Attributes("axiom", [], prev); } /// @@ -233,7 +231,7 @@ public static Attributes AxiomAttribute(Attributes prev = null) { public UserDefinedType ArrayType(int dims, Type arg, bool allowCreationOfNewClass) { Contract.Requires(1 <= dims); Contract.Requires(arg != null); - var (result, mod) = ArrayType(Token.NoToken, dims, new List { arg }, allowCreationOfNewClass); + var (result, mod) = ArrayType(Token.NoToken, dims, [arg], allowCreationOfNewClass); mod(this); return result; } @@ -307,13 +305,13 @@ Function CreateMember(string name, Type resultType, Function readsFunction = nul }; var readsFrame = new List { new FrameExpression(tok, readsIS, null) }; var function = new Function(SourceOrigin.NoToken, new Name(name), false, true, false, - new List(), args, null, resultType, - new List(), new Specification(readsFrame, null), new List(), - new Specification(new List(), null), + [], args, null, resultType, + [], new Specification(readsFrame, null), [], + new Specification([], null), null, null, null, null, null); readsIS.Function = readsFunction ?? function; // just so we can really claim the member declarations are resolved readsIS.TypeApplication_AtEnclosingClass = tys; // ditto - readsIS.TypeApplication_JustFunction = new List(); // ditto + readsIS.TypeApplication_JustFunction = []; // ditto return function; } @@ -378,10 +376,10 @@ private Expression ArrowSubtypeConstraint(IOrigin tok, BoundVar id, Function mem args.Add(new IdentifierExpr(tok, bv)); bounds.Add(new SpecialAllocIndependenceAllocatedBoundedPool()); } - Expression body = Expression.CreateResolvedCall(tok, f, member, args, new List(), this); + Expression body = Expression.CreateResolvedCall(tok, f, member, args, [], this); body.Type = member.ResultType; // resolve here if (!total) { - Expression emptySet = new SetDisplayExpr(tok, true, new List()); + Expression emptySet = new SetDisplayExpr(tok, true, []); emptySet.Type = member.ResultType; // resolve here body = Expression.CreateEq(body, emptySet, member.ResultType); } diff --git a/Source/DafnyCore/AST/TypeDeclarations/ArrayClassDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ArrayClassDecl.cs index a002c6b0bab..12e93b85865 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ArrayClassDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ArrayClassDecl.cs @@ -9,8 +9,10 @@ public class ArrayClassDecl : ClassDecl { public readonly int Dims; public ArrayClassDecl(int dims, ModuleDefinition module, Attributes attrs) : base(SourceOrigin.NoToken, new Name(SystemModuleManager.ArrayClassName(dims)), module, - new List(new TypeParameter[] { new TypeParameter(SourceOrigin.NoToken, new Name("arg"), TypeParameter.TPVarianceSyntax.NonVariant_Strict) }), - new List(), attrs, false, null) { + [ + new TypeParameter(SourceOrigin.NoToken, new Name("arg"), TypeParameter.TPVarianceSyntax.NonVariant_Strict) + ], + [], attrs, false, null) { Contract.Requires(1 <= dims); Contract.Requires(module != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/ArrowTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ArrowTypeDecl.cs index bdb25e93a24..c5923e39448 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ArrowTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ArrowTypeDecl.cs @@ -11,7 +11,7 @@ public class ArrowTypeDecl : ValuetypeDecl { public ArrowTypeDecl(List tps, Function req, Function reads, ModuleDefinition module, Attributes attributes) : base(ArrowType.ArrowTypeName(tps.Count - 1), module, tps, - new List { req, reads }, attributes, + [req, reads], attributes, ty => ty.NormalizeExpandKeepConstraints() is UserDefinedType { ResolvedClass: ArrowTypeDecl arrowTypeDecl } && arrowTypeDecl.Arity == tps.Count - 1, null) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs index c64d1571fc6..2cae5901581 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs @@ -22,7 +22,7 @@ void ObjectInvariant() { // TODO: One could imagine having a precondition on datatype constructors [FilledInDuringResolution] public DatatypeDecl EnclosingDatatype; [FilledInDuringResolution] public SpecialField QueryField; - [FilledInDuringResolution] public List Destructors = new List(); // includes both implicit (not mentionable in source) and explicit destructors + [FilledInDuringResolution] public List Destructors = []; // includes both implicit (not mentionable in source) and explicit destructors public DatatypeCtor(IOrigin origin, Name name, bool isGhost, [Captured] List formals, Attributes attributes) : base(origin, name, attributes, false) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs index a75322f7ea2..297eb83ab3c 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs @@ -57,7 +57,7 @@ public bool ContainsHide { bool ICodeContext.IsGhost { get { return true; } } List ICodeContext.TypeArgs { get { return TypeArgs; } } - List ICodeContext.Ins { get { return new List(); } } + List ICodeContext.Ins { get { return []; } } ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } } bool ICodeContext.MustReverify { get { return false; } } bool ICodeContext.AllowsNontermination { get { return false; } } diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs index 31af8d68bcb..f7ca2d7bf9e 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs @@ -142,7 +142,7 @@ public override string ToString() { // For Boogie internal VerificationIdGenerator IdGenerator = new(); - public override IEnumerable Children => Enumerable.Empty(); // Attributes should be enumerated by the parent, as they could be placed in different places + public override IEnumerable Children => []; // Attributes should be enumerated by the parent, as they could be placed in different places public override IEnumerable PreResolveChildren => Children; public abstract SymbolKind? Kind { get; } public abstract string GetDescription(DafnyOptions options); diff --git a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs index ff462344cf0..9a5d810dbbd 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs @@ -38,7 +38,7 @@ public IteratorDecl(IOrigin origin, Name name, ModuleDefinition module, List yieldRequires, List yieldEnsures, BlockStmt body, Attributes attributes, IOrigin signatureEllipsis) - : base(origin, name, module, typeArgs, new List(), attributes, signatureEllipsis != null, null) { + : base(origin, name, module, typeArgs, [], attributes, signatureEllipsis != null, null) { Contract.Requires(origin != null); Contract.Requires(name != null); Contract.Requires(module != null); @@ -64,9 +64,9 @@ public IteratorDecl(IOrigin origin, Name name, ModuleDefinition module, List(); - OutsHistoryFields = new List(); - DecreasesFields = new List(); + OutsFields = []; + OutsHistoryFields = []; + DecreasesFields = []; YieldCountVariable = new LocalVariable(origin, "_yieldCount", new EverIncreasingType(), true); YieldCountVariable.type = YieldCountVariable.SyntacticType; // resolve YieldCountVariable here @@ -207,7 +207,7 @@ public void CreateIteratorMethodSpecs(ModuleResolver resolver) { foreach (var p in OutsHistoryFields) { // ensures this.ys == []; ens.Add(new AttributedExpression(new BinaryExpr(p.Origin, BinaryExpr.Opcode.Eq, - new ExprDotName(p.Origin, new ThisExpr(p.Origin), p.NameNode, null), new SeqDisplayExpr(p.Origin, new List())))); + new ExprDotName(p.Origin, new ThisExpr(p.Origin), p.NameNode, null), new SeqDisplayExpr(p.Origin, [])))); } // ensures this.Valid(); var valid_call = AutoContractsRewriter.CreateUnresolvedValidCall(tok); @@ -216,7 +216,7 @@ public void CreateIteratorMethodSpecs(ModuleResolver resolver) { // ensures this._new == {}; ens.Add(new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, new ExprDotName(tok, new ThisExpr(tok), new Name("_new"), null), - new SetDisplayExpr(tok, true, new List())))); + new SetDisplayExpr(tok, true, [])))); // ensures this._decreases0 == old(DecreasesClause[0]) && ...; Contract.Assert(Decreases.Expressions.Count == DecreasesFields.Count); for (int i = 0; i < Decreases.Expressions.Count; i++) { @@ -267,7 +267,7 @@ public void CreateIteratorMethodSpecs(ModuleResolver resolver) { var ite = new ITEExpr(tok, false, new IdentifierExpr(tok, "more"), new BinaryExpr(tok, BinaryExpr.Opcode.Add, new OldExpr(tok, new ExprDotName(tok, new ThisExpr(tok), ys.NameNode, null)), - new SeqDisplayExpr(tok, new List() { new ExprDotName(tok, new ThisExpr(tok), y.NameNode, null) })), + new SeqDisplayExpr(tok, [new ExprDotName(tok, new ThisExpr(tok), y.NameNode, null)])), new OldExpr(tok, new ExprDotName(tok, new ThisExpr(tok), ys.NameNode, null))); var eq = new BinaryExpr(tok, BinaryExpr.Opcode.Eq, new ExprDotName(tok, new ThisExpr(tok), ys.NameNode, null), ite); ens.Add(new AttributedExpression(eq)); @@ -319,7 +319,7 @@ private void AddConstructorFramePostconditions(AutoGeneratedOrigin tok, List(); + modSetSingletons = []; frameSet = new SetDisplayExpr(tok, true, modSetSingletons); foreach (var fr in Modifies.Expressions) { if (fr.FieldName != null) { @@ -436,32 +436,32 @@ public void Resolve(ModuleResolver resolver) { // iterator type) does. // --- here comes the constructor var init = new Constructor(rangeToken, new Name(NameNode.Origin, "_ctor"), false, - new List(), Ins, - new List(), + [], Ins, + [], new Specification(), - new Specification(new List(), null), - new List(), - new Specification(new List(), null), + new Specification([], null), + [], + new Specification([], null), null, SystemModuleManager.AxiomAttribute(), null); // --- here comes predicate Valid() var valid = new Predicate(rangeToken, new Name(NameNode.Origin, "Valid"), false, true, false, - new List(), - new List(), + [], + [], null, - new List(), + [], new Specification(), - new List(), - new Specification(new List(), null), + [], + new Specification([], null), null, Predicate.BodyOriginKind.OriginalOrInherited, null, null, SystemModuleManager.AxiomAttribute(), null); // --- here comes method MoveNext var moveNext = new Method(rangeToken, new Name(NameNode.Origin, "MoveNext"), false, false, - new List(), - new List(), new List() { new Formal(Origin, "more", Type.Bool, false, false, null) }, - new List(), + [], + [], [new Formal(Origin, "more", Type.Bool, false, false, null)], + [], new Specification(), - new Specification(new List(), null), - new List(), - new Specification(new List(), null), + new Specification([], null), + [], + new Specification([], null), null, SystemModuleManager.AxiomAttribute(Attributes.Find(Attributes, "print")), null); // add these implicit members to the class init.EnclosingClass = this; diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index c778d79f23f..2efc6031a1c 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -133,7 +133,7 @@ bool ICodeContext.IsGhost { get { throw new NotSupportedException(); } // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper } List ICodeContext.TypeArgs { get { return TypeArgs; } } - List ICodeContext.Ins { get { return new List(); } } + List ICodeContext.Ins { get { return []; } } ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } } bool ICodeContext.MustReverify { get { return false; } } bool ICodeContext.AllowsNontermination { get { return false; } } diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs index f6ba7866d21..78cf075efdc 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs @@ -57,7 +57,7 @@ public SubsetTypeDecl(IOrigin origin, Name name, TypeParameter.TypeParameterChar Expression RedirectingTypeDecl.Witness => Witness; public override List ParentTypes(List typeArgs, bool includeTypeBounds) { - return new List { RhsWithArgument(typeArgs) }; + return [RhsWithArgument(typeArgs)]; } public bool ShouldVerify => true; // This could be made more accurate public ModuleDefinition ContainingModule => EnclosingModuleDefinition; diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs index 8fc96714927..ba2a5551e47 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs @@ -104,7 +104,7 @@ public TopLevelDecl ViewAsClass { public virtual List ParentTypes(List typeArgs, bool includeTypeBounds) { Contract.Requires(typeArgs != null); Contract.Requires(this.TypeArgs.Count == typeArgs.Count); - return new List(); + return []; } public bool AllowsAllocation => true; diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs index 771fe3bc267..e6d990a886b 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs @@ -14,14 +14,14 @@ public abstract class TopLevelDeclWithMembers : TopLevelDecl, IHasSymbolChildren public ImmutableList MembersBeforeResolution; // The following fields keep track of parent traits - public readonly List InheritedMembers = new(); // these are instance members declared in parent traits + public readonly List InheritedMembers = []; // these are instance members declared in parent traits public readonly List ParentTraits; // these are the types that are parsed after the keyword 'extends'; note, for a successfully resolved program, these are UserDefinedType's where .ResolvedClass is NonNullTypeDecl public readonly Dictionary ParentFormalTypeParametersToActuals = new Dictionary(); // maps parent traits' type parameters to actuals /// /// TraitParentHeads contains the head of each distinct trait parent. It is initialized during resolution. /// - public readonly List ParentTraitHeads = new List(); + public readonly List ParentTraitHeads = []; internal bool HeadDerivesFrom(TopLevelDecl b) { Contract.Requires(b != null); @@ -53,10 +53,10 @@ public void Record(TraitDecl traitHead, UserDefinedType parentType) { Contract.Requires(parentType.ResolvedClass is NonNullTypeDecl nntd && nntd.ViewAsClass == traitHead); if (!info.TryGetValue(traitHead, out var list)) { - list = new List<(Type, List)>(); + list = []; info.Add(traitHead, list); } - list.Add((parentType, new List())); + list.Add((parentType, [])); } public void Extend(TraitDecl parent, InheritanceInformationClass parentInfo, Dictionary typeMap) { @@ -67,7 +67,7 @@ public void Extend(TraitDecl parent, InheritanceInformationClass parentInfo, Dic foreach (var entry in parentInfo.info) { var traitHead = entry.Key; if (!info.TryGetValue(traitHead, out var list)) { - list = new List<(Type, List)>(); + list = []; info.Add(traitHead, list); } foreach (var pair in entry.Value) { @@ -96,7 +96,7 @@ protected TopLevelDeclWithMembers(IOrigin origin, Name name, ModuleDefinition mo Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Requires(cce.NonNullElements(members)); Members = members; - ParentTraits = traits ?? new List(); + ParentTraits = traits ?? []; SetMembersBeforeResolution(); } @@ -236,7 +236,7 @@ public void RegisterMembers(ModuleResolver resolver, Dictionary(new List() { new IdentifierExpr(extremePredicate.Origin, k.Name) }, null), + new Specification([new IdentifierExpr(extremePredicate.Origin, k.Name)], null), cloner.CloneExpr(extremePredicate.Body), SystemModuleManager.AxiomAttribute(), extremePredicate); diff --git a/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs index 3d28bb44f43..a1303f262f3 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs @@ -36,7 +36,7 @@ public TupleTypeDecl(List argumentGhostness, ModuleDefinition systemModule private TupleTypeDecl(ModuleDefinition systemModule, List typeArgs, List argumentGhostness, Attributes attributes) : base(SourceOrigin.NoToken, new Name(SystemModuleManager.TupleTypeName(argumentGhostness)), systemModule, typeArgs, CreateConstructors(typeArgs, argumentGhostness), - new List(), new List(), attributes, false) { + [], [], attributes, false) { Contract.Requires(systemModule != null); Contract.Requires(typeArgs != null); Contract.Assert(Ctors.Count == 1); @@ -88,7 +88,7 @@ private static List CreateConstructors(List typeArg } string ctorName = SystemModuleManager.TupleTypeCtorName(typeArgs.Count); var ctor = new DatatypeCtor(SourceOrigin.NoToken, new Name(ctorName), false, formals, null); - return new List() { ctor }; + return [ctor]; } public override string SanitizedName => diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index 306045b3b65..d9cb6a7c043 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -81,7 +81,7 @@ bool RedirectingTypeDecl.ConstraintIsCompilable { bool ICodeContext.IsGhost => throw new NotSupportedException(); // if .IsGhost is needed, the object should always be wrapped in an CodeContextWrapper List ICodeContext.TypeArgs => TypeArgs; - List ICodeContext.Ins => new(); + List ICodeContext.Ins => []; ModuleDefinition IASTVisitorContext.EnclosingModule { get { return EnclosingModuleDefinition; } } bool ICodeContext.MustReverify { get { return false; } } bool ICodeContext.AllowsNontermination { get { return false; } } diff --git a/Source/DafnyCore/AST/TypeDeclarations/ValuetypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ValuetypeDecl.cs index 99417211c77..3033b550fa0 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ValuetypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ValuetypeDecl.cs @@ -16,7 +16,7 @@ public class ValuetypeDecl : TopLevelDeclWithMembers { public override bool AcceptThis => true; public ValuetypeDecl(string name, ModuleDefinition module, Func typeTester, Func, Type> typeCreator /*?*/) - : base(SourceOrigin.NoToken, new Name(name), module, new List(), new List(), null, false, null) { + : base(SourceOrigin.NoToken, new Name(name), module, [], [], null, false, null) { Contract.Requires(name != null); Contract.Requires(module != null); Contract.Requires(typeTester != null); diff --git a/Source/DafnyCore/AST/Types/MapType.cs b/Source/DafnyCore/AST/Types/MapType.cs index 062bb0ffacf..2bb20359bec 100644 --- a/Source/DafnyCore/AST/Types/MapType.cs +++ b/Source/DafnyCore/AST/Types/MapType.cs @@ -29,7 +29,7 @@ public MapType(Cloner cloner, MapType original) : base(cloner, original) { Finite = original.Finite; range = cloner.CloneType(original.Range); var arg = HasTypeArg() ? Arg : null; - TypeArgs = new List() { arg, range }; + TypeArgs = [arg, range]; } public Type Domain { diff --git a/Source/DafnyCore/AST/Types/TypeParameter.cs b/Source/DafnyCore/AST/Types/TypeParameter.cs index c3aad802008..0e7730275bb 100644 --- a/Source/DafnyCore/AST/Types/TypeParameter.cs +++ b/Source/DafnyCore/AST/Types/TypeParameter.cs @@ -188,7 +188,7 @@ public IEnumerable TypeBoundHeads { public TypeParameter(IOrigin origin, Name name, TPVarianceSyntax varianceS, TypeParameterCharacteristics characteristics, List typeBounds) - : base(origin, name, null, new List(), null, false) { + : base(origin, name, null, [], null, false) { Contract.Requires(origin != null); Contract.Requires(name != null); Characteristics = characteristics; @@ -197,7 +197,7 @@ public TypeParameter(IOrigin origin, Name name, TPVarianceSyntax varianceS, Type } public TypeParameter(IOrigin origin, Name name, TPVarianceSyntax varianceS) - : this(origin, name, varianceS, new TypeParameterCharacteristics(false), new List()) { + : this(origin, name, varianceS, new TypeParameterCharacteristics(false), []) { Contract.Requires(origin != null); Contract.Requires(name != null); } @@ -260,6 +260,6 @@ public static Dictionary SubstitutionMap(List ParentTypes(List typeArgs, bool includeTypeBounds) { - return includeTypeBounds ? TypeBounds : new List(); + return includeTypeBounds ? TypeBounds : []; } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Types/Types.cs b/Source/DafnyCore/AST/Types/Types.cs index b6c76c5fc53..37041e01890 100644 --- a/Source/DafnyCore/AST/Types/Types.cs +++ b/Source/DafnyCore/AST/Types/Types.cs @@ -32,19 +32,19 @@ public static Type ResolvedString() { public static readonly BigOrdinalType BigOrdinal = new BigOrdinalType(); private static ThreadLocal> _scopes = new(); - private static List Scopes => _scopes.Value ??= new(); + private static List Scopes => _scopes.Value ??= []; [ThreadStatic] private static bool scopesEnabled = false; - public virtual IEnumerable Nodes => Enumerable.Empty(); + public virtual IEnumerable Nodes => []; public static void PushScope(VisibilityScope scope) { Scopes.Add(scope); } public static void ResetScopes() { - _scopes.Value = new(); + _scopes.Value = []; scopesEnabled = false; } @@ -98,7 +98,7 @@ public string TypeArgsToString(DafnyOptions options, ModuleDefinition/*?*/ conte } // Type arguments to the type - public List TypeArgs = new List(); + public List TypeArgs = []; /// /// Add to "tps" the free type parameters in "this". @@ -493,9 +493,9 @@ AutoInitInfo CharacteristicToAutoInitInfo(TypeParameter.TypeParameterCharacteris // This requires more recursion and bookkeeping than we care to try out return AutoInitInfo.MaybeEmpty; } - coDatatypesBeingVisited = new List(coDatatypesBeingVisited); + coDatatypesBeingVisited = [.. coDatatypesBeingVisited]; } else { - coDatatypesBeingVisited = new List(); + coDatatypesBeingVisited = []; } coDatatypesBeingVisited.Add(udt); } @@ -899,15 +899,15 @@ public static bool IsSupertype(Type super, Type sub) { Contract.Requires(type != null); if (type is BasicType || type is ArtificialType) { // there are no type parameters - return new List(); + return []; } else if (type is MapType) { - return new List { TypeParameter.TPVariance.Co, TypeParameter.TPVariance.Co }; + return [TypeParameter.TPVariance.Co, TypeParameter.TPVariance.Co]; } else if (type is CollectionType) { - return new List { TypeParameter.TPVariance.Co }; + return [TypeParameter.TPVariance.Co]; } else { var udf = (UserDefinedType)type; if (udf.TypeArgs.Count == 0) { - return new List(); + return []; } // look up the declaration of the formal type parameters var cl = udf.ResolvedClass; @@ -1211,7 +1211,7 @@ public static List GetTowerOfSubsetTypes(Type type, bool typeSynonymsAreSi var parent = sst.RhsWithArgument(type.TypeArgs); tower = GetTowerOfSubsetTypes(parent, typeSynonymsAreSignificant); } else { - tower = new List(); + tower = []; } tower.Add(type); return tower; @@ -1677,7 +1677,7 @@ public bool ContainsProxy(TypeProxy proxy) { } public virtual List ParentTypes(bool includeTypeBounds) { - return new List(); + return []; } /// @@ -2149,8 +2149,8 @@ public override CollectionBoundedPool GetBoundedPool(Expression source) { public abstract class TypeProxy : Type { public override IEnumerable Children => Enumerable.Empty(); [FilledInDuringResolution] public Type T; - public readonly List SupertypeConstraints = new List(); - public readonly List SubtypeConstraints = new List(); + public readonly List SupertypeConstraints = []; + public readonly List SubtypeConstraints = []; public override Type Subst(IDictionary subst) { if (T == null) { diff --git a/Source/DafnyCore/AST/Types/UserDefinedType.cs b/Source/DafnyCore/AST/Types/UserDefinedType.cs index e7076751bb4..ce802f4a01b 100644 --- a/Source/DafnyCore/AST/Types/UserDefinedType.cs +++ b/Source/DafnyCore/AST/Types/UserDefinedType.cs @@ -62,7 +62,7 @@ public UserDefinedType(IOrigin origin, Expression namePath) : base(origin) { this.TypeArgs = n.OptTypeArguments; } if (this.TypeArgs == null) { - this.TypeArgs = new List(); // TODO: is this really the thing to do? + this.TypeArgs = []; // TODO: is this really the thing to do? } this.NamePath = namePath; } @@ -215,7 +215,7 @@ public UserDefinedType(IOrigin origin, TypeParameter tp) : base(origin) { Contract.Requires(origin != null); Contract.Requires(tp != null); this.Name = tp.Name; - this.TypeArgs = new List(); + this.TypeArgs = []; this.ResolvedClass = tp; var ns = new NameSegment(origin, tp.Name, null); var r = new ResolverIdentifierExpr(origin, tp); @@ -265,7 +265,7 @@ public override Type Subst(IDictionary subst) { } if (s != p && newArgs == null) { // lazily construct newArgs - newArgs = new List(); + newArgs = []; for (int j = 0; j < i; j++) { newArgs.Add(TypeArgs[j]); } diff --git a/Source/DafnyCore/AST/VisibilityScope.cs b/Source/DafnyCore/AST/VisibilityScope.cs index 9876211cff0..3217583a6c9 100644 --- a/Source/DafnyCore/AST/VisibilityScope.cs +++ b/Source/DafnyCore/AST/VisibilityScope.cs @@ -10,10 +10,10 @@ namespace Microsoft.Dafny { public class VisibilityScope { private static uint maxScopeId; - private readonly SortedSet scopeTokens = new(); + private readonly SortedSet scopeTokens = []; // Only for debugging - private readonly SortedSet scopeIds = new(); + private readonly SortedSet scopeIds = []; private static bool Overlaps(SortedSet set1, SortedSet set2) { // This conditional implements a performance optimization, diff --git a/Source/DafnyCore/AlphaConvertingSubstituter.cs b/Source/DafnyCore/AlphaConvertingSubstituter.cs index d6640e8a891..b4d5bb21e11 100644 --- a/Source/DafnyCore/AlphaConvertingSubstituter.cs +++ b/Source/DafnyCore/AlphaConvertingSubstituter.cs @@ -15,7 +15,7 @@ public AlphaConvertingSubstituter(Expression receiverReplacement, Dictionary CreateBoundVarSubstitutions(List vars, bool forceSubstitutionOfBoundVars) { - var newBoundVars = vars.Count == 0 ? vars : new List(); + var newBoundVars = vars.Count == 0 ? vars : []; foreach (var bv in vars) { var tt = bv.Type.Subst(typeMap); var newBv = new BoundVar(bv.Origin, "_'" + bv.Name, tt); diff --git a/Source/DafnyCore/Auditor/AuditReport.cs b/Source/DafnyCore/Auditor/AuditReport.cs index c5f11d9d4c8..67976f13d94 100644 --- a/Source/DafnyCore/Auditor/AuditReport.cs +++ b/Source/DafnyCore/Auditor/AuditReport.cs @@ -16,8 +16,8 @@ public class AuditReport { private Dictionary> allAssumptionsByDecl = new(); // All three fields below are filtered by AddAssumptions() - private HashSet declsWithEntries = new(); - private HashSet modulesWithEntries = new(); + private HashSet declsWithEntries = []; + private HashSet modulesWithEntries = []; private Dictionary> assumptionsByDecl = new(); public AuditReport(DafnyOptions options) { @@ -50,7 +50,7 @@ public IEnumerable>> AllAssump public IEnumerable AllAssumptionsForDecl(Declaration decl) { return allAssumptionsByDecl.TryGetValue(decl, out var assumptions) - ? assumptions : Enumerable.Empty(); + ? assumptions : []; } private string RenderRow(string beg, string sep, string end, IEnumerable cells) { diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 3e76ddfc6f6..fc46c7f8bd9 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -192,7 +192,7 @@ private void EmitFuncExtensions(SystemModuleManager systemModuleManager, Concret List TypeParameterList(string prefix) { var l = arity switch { - 1 => new List { prefix }, + 1 => [prefix], _ => Enumerable.Range(1, arity).Select(i => $"{prefix}{i}").ToList() }; l.Add($"{prefix}Result"); @@ -424,7 +424,7 @@ protected override IClassWriter CreateTrait(string name, bool isExtern, List typeParameters, List/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) { wr.Write($"public {kind} {IdProtect(name)}{TypeParameters(typeParameters)}"); - var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? new List(); + var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? []; if (realSuperClasses.Any()) { wr.Write($" : {realSuperClasses.Comma(trait => TypeName(trait, wr, tok))}"); } @@ -2874,7 +2874,7 @@ private void EmitSeqConstructionExprFromLambda(Expression lengthExpr, BoundVar b var ixVar = IdName(boundVar); wrLoopBody.WriteLine("var {0} = ({1}) {2};", ixVar, TypeName(indexType, wrLoopBody, body.Origin), intIxVar); - var wrArrName = EmitArrayUpdate(new List> { wr => wr.Write(ixVar) }, body, wrLoopBody); + var wrArrName = EmitArrayUpdate([wr => wr.Write(ixVar)], body, wrLoopBody); wrArrName.Write(arrVar); EndStmt(wrLoopBody); diff --git a/Source/DafnyCore/Backends/CoverageInstrumenter.cs b/Source/DafnyCore/Backends/CoverageInstrumenter.cs index 5dbae937ef8..9ec90ad5709 100644 --- a/Source/DafnyCore/Backends/CoverageInstrumenter.cs +++ b/Source/DafnyCore/Backends/CoverageInstrumenter.cs @@ -14,7 +14,7 @@ public CoverageInstrumenter(SinglePassCodeGenerator codeGenerator) { this.codeGenerator = codeGenerator; if (codeGenerator.Options?.CoverageLegendFile != null || codeGenerator.Options?.Get(CommonOptionBag.ExecutionCoverageReport) != null) { - legend = new List<(IOrigin, string)>(); + legend = []; } if (codeGenerator.Options?.Get(CommonOptionBag.ExecutionCoverageReport) != null) { diff --git a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs index dc8d8715169..a39abb721f2 100644 --- a/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs @@ -60,8 +60,8 @@ public CppCodeGenerator(DafnyOptions options, ErrorReporter reporter, ReadOnlyCo Feature.RuntimeCoverageReport }; - private List datatypeDecls = new(); - private List classDefaults = new(); + private List datatypeDecls = []; + private List classDefaults = []; /* * Unlike other Dafny and Dafny's other backends, C++ cares about @@ -641,7 +641,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre GetNativeInfo(nt.NativeType.Sel, out var nt_name, out var literalSuffice, out var needsCastAfterArithmetic); var wDefault = w.NewBlock(string.Format("static {0} get_Default()", nt_name)); - var udt = new UserDefinedType(nt.Origin, nt.Name, nt, new List()); + var udt = new UserDefinedType(nt.Origin, nt.Name, nt, []); var d = TypeInitializationValue(udt, wr, nt.Origin, false, false); wDefault.WriteLine("return {0};", d); diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs index 3b7f6eeb867..994e4ce30a1 100644 --- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs +++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs @@ -17,7 +17,7 @@ interface Container { } class ProgramBuilder : ModuleContainer { - readonly List items = new(); + readonly List items = []; public void AddModule(Module item) { items.Add(item); @@ -56,7 +56,7 @@ class ModuleBuilder : ClassContainer, TraitContainer, NewtypeContainer, Datatype readonly ModuleContainer parent; readonly string name; readonly Sequence attributes; - readonly List body = new(); + readonly List body = []; private readonly bool requiresExterns; private string docString; @@ -125,8 +125,8 @@ class ClassBuilder : ClassLike { readonly string enclosingModule; readonly List typeParams; readonly List superClasses; - readonly List fields = new(); - readonly List body = new(); + readonly List fields = []; + readonly List body = []; readonly ISequence<_IAttribute> attributes; private string docString; @@ -177,7 +177,7 @@ class TraitBuilder : ClassLike { readonly string name; readonly List typeParams; private readonly List parents; - readonly List body = new(); + readonly List body = []; private ISequence<_IAttribute> attributes; private string docString; private _ITraitType traitType; @@ -259,7 +259,7 @@ public NewtypeBuilder(NewtypeContainer parent, string name, List ty this.witness = witness; this.attributes = attributes; this.docString = docString; - this.methods = new(); + this.methods = []; } public void AddMethod(DAST.Method item) { @@ -354,7 +354,7 @@ class DatatypeBuilder : ClassLike { readonly List typeParams; readonly List ctors; readonly bool isCo; - readonly List body = new(); + readonly List body = []; private ISequence<_IAttribute> attributes; private string docString; private List superTraitTypes; @@ -425,7 +425,7 @@ class MethodBuilder : StatementContainer { readonly Sequence params_; readonly List outTypes; readonly List> outVars; - readonly List body = new(); + readonly List body = []; private ISequence<_IAttribute> attributes; private ISequence docString; @@ -470,7 +470,7 @@ public void AddBuildable(BuildableStatement item) { } public DAST.Method Build() { - List builtStatements = new(); + List builtStatements = []; StatementContainer.RecursivelyBuild(body, builtStatements); return (DAST.Method)DAST.Method.create( docString, @@ -644,7 +644,7 @@ public DAST.Statement Build() { Sequence.UnicodeFromString(name), type, Option.create_None()); } else { var builtValue = new List(); - ExprContainer.RecursivelyBuild(new List { value }, builtValue); + ExprContainer.RecursivelyBuild([value], builtValue); return (DAST.Statement)DAST.Statement.create_DeclareVar(Sequence.UnicodeFromString(name), type, Option.create_Some(builtValue[0])); } } @@ -701,7 +701,7 @@ public DAST.Statement Build() { rhs = ExprContainer.UnsupportedToExpr("Cannot assign null value to variable: " + lhs); } else { var builtValue = new List(); - ExprContainer.RecursivelyBuild(new List { value }, builtValue); + ExprContainer.RecursivelyBuild([value], builtValue); rhs = builtValue[0]; } @@ -711,8 +711,8 @@ public DAST.Statement Build() { class IfElseBuilder : ExprContainer, StatementContainer, BuildableStatement { object condition = null; - readonly List ifBody = new(); - readonly List elseBody = new(); + readonly List ifBody = []; + readonly List elseBody = []; public object Condition => condition; @@ -767,15 +767,14 @@ public ElseBuilder Else() { } public DAST.Statement Build() { - List builtCondition = new(); - ExprContainer.RecursivelyBuild(new List { - condition ?? ExprContainer.UnsupportedToExpr("condition to if expression") - }, builtCondition); + List builtCondition = []; + ExprContainer.RecursivelyBuild( + [condition ?? ExprContainer.UnsupportedToExpr("condition to if expression")], builtCondition); - List builtIfStatements = new(); + List builtIfStatements = []; StatementContainer.RecursivelyBuild(ifBody, builtIfStatements); - List builtElseStatements = new(); + List builtElseStatements = []; StatementContainer.RecursivelyBuild(elseBody, builtElseStatements); return (DAST.Statement)DAST.Statement.create_If( @@ -816,7 +815,7 @@ public void AddUnsupported(string why) { class WhileBuilder : ExprContainer, StatementContainer, BuildableStatement { object condition = null; - readonly List body = new(); + readonly List body = []; public object Condition => condition; public void AddExpr(DAST.Expression value) { @@ -850,10 +849,10 @@ public List ForkList() { } public DAST.Statement Build() { - List builtCondition = new(); - ExprContainer.RecursivelyBuild(new List { condition }, builtCondition); + List builtCondition = []; + ExprContainer.RecursivelyBuild([condition], builtCondition); - List builtStatements = new(); + List builtStatements = []; StatementContainer.RecursivelyBuild(body, builtStatements); return (DAST.Statement)DAST.Statement.create_While( @@ -871,7 +870,7 @@ class ForeachBuilder : ExprContainer, StatementContainer, BuildableStatement { readonly string boundName; readonly DAST.Type boundType; object over = null; - readonly List body = new(); + readonly List body = []; public ForeachBuilder(string boundName, DAST.Type boundType) { this.boundName = boundName; @@ -909,12 +908,10 @@ public List ForkList() { } public DAST.Statement Build() { - List builtOver = new(); - ExprContainer.RecursivelyBuild(new List { - over ?? ExprContainer.UnsupportedToExpr("Foreach over is null") - }, builtOver); + List builtOver = []; + ExprContainer.RecursivelyBuild([over ?? ExprContainer.UnsupportedToExpr("Foreach over is null")], builtOver); - List builtStatements = new(); + List builtStatements = []; StatementContainer.RecursivelyBuild(body, builtStatements); return (DAST.Statement)DAST.Statement.create_Foreach( @@ -931,7 +928,7 @@ public void AddUnsupported(string why) { } class TailRecursiveBuilder : StatementContainer, BuildableStatement { - readonly List body = new(); + readonly List body = []; public TailRecursiveBuilder() { } @@ -950,7 +947,7 @@ public List ForkList() { } public DAST.Statement Build() { - List builtStatements = new(); + List builtStatements = []; StatementContainer.RecursivelyBuild(body, builtStatements); return (DAST.Statement)DAST.Statement.create_TailRecursive( @@ -967,7 +964,7 @@ class CallStmtBuilder : ExprContainer, BuildableStatement { object on = null; DAST.CallName name = null; List typeArgs = null; - readonly List args = new(); + readonly List args = []; List> outs = null; public readonly ISequence<_IFormal> Signature; @@ -1016,10 +1013,10 @@ public void SetOuts(List> outs) { } public DAST.Statement Build() { - List builtOn = new(); - ExprContainer.RecursivelyBuild(new List { on }, builtOn); + List builtOn = []; + ExprContainer.RecursivelyBuild([on], builtOn); - List builtArgs = new(); + List builtArgs = []; ExprContainer.RecursivelyBuild(args, builtArgs); return (DAST.Statement)DAST.Statement.create_Call( @@ -1062,7 +1059,7 @@ public DAST.Statement Build() { if (value == null) { return (DAST.Statement)DAST.Statement.create_EarlyReturn(); } - ExprContainer.RecursivelyBuild(new List { value }, builtValue); + ExprContainer.RecursivelyBuild([value], builtValue); return (DAST.Statement)DAST.Statement.create_Return(builtValue[0]); } @@ -1074,7 +1071,7 @@ public void AddUnsupported(string why) { class LabeledBuilder : BuildableStatement, StatementContainer { readonly string label; - readonly List statements = new(); + readonly List statements = []; public LabeledBuilder(string label) { this.label = label; @@ -1099,7 +1096,7 @@ public List ForkList() { } public DAST.Statement Build() { - List builtStatements = new(); + List builtStatements = []; StatementContainer.RecursivelyBuild(statements, builtStatements); return (DAST.Statement)DAST.Statement.create_Labeled( @@ -1132,7 +1129,7 @@ public List ForkList() { } class StatementBuffer : StatementContainer { - readonly List statements = new(); + readonly List statements = []; public void AddStatement(DAST.Statement item) { statements.Add(item); @@ -1407,7 +1404,7 @@ public DAST.AssignLhs Build() { Console.WriteLine(stackTrace); } var builtArrayExpr = new List(); - ExprContainer.RecursivelyBuild(new List { arrayExpr }, builtArrayExpr); + ExprContainer.RecursivelyBuild([arrayExpr], builtArrayExpr); return (DAST.AssignLhs)DAST.AssignLhs.create_Index(builtArrayExpr[0], Sequence.FromArray(indices.ToArray())); } @@ -1423,7 +1420,7 @@ interface BuildableExpr { class BinOpBuilder : ExprContainer, BuildableExpr { private readonly Func internalBuilder; - readonly List operands = new(); + readonly List operands = []; private readonly string op; public BinOpBuilder(DAST.BinOp op, DAST.Type leftType, DAST.Type rightType, DAST.Type resType) { @@ -1468,7 +1465,7 @@ class CallExprBuilder : ExprContainer, BuildableExpr { object on = null; DAST.CallName name = null; List typeArgs = null; - readonly List args = new(); + readonly List args = []; List> outs = null; public ISequence<_IFormal> Signature { get; } @@ -1519,7 +1516,7 @@ public void SetOuts(List> outs) { public DAST.Expression Build() { var builtOn = new List(); - ExprContainer.RecursivelyBuild(new List { on }, builtOn); + ExprContainer.RecursivelyBuild([on], builtOn); var builtArgs = new List(); ExprContainer.RecursivelyBuild(args, builtArgs); @@ -1527,7 +1524,7 @@ public DAST.Expression Build() { return (DAST.Expression)DAST.Expression.create_Call( builtOn[0], name, - Sequence.FromArray((typeArgs ?? new()).ToArray()), + Sequence.FromArray((typeArgs ?? []).ToArray()), Sequence.FromArray(builtArgs.ToArray()) ); } @@ -1539,7 +1536,7 @@ public void AddUnsupported(string why) { class ApplyExprBuilder : ExprContainer, BuildableExpr { object on = null; - readonly List args = new(); + readonly List args = []; public ApplyExprBuilder() { } @@ -1561,7 +1558,7 @@ public void AddBuildable(BuildableExpr value) { public DAST.Expression Build() { var builtOn = new List(); - ExprContainer.RecursivelyBuild(new List { on }, builtOn); + ExprContainer.RecursivelyBuild([on], builtOn); var builtArgs = new List(); ExprContainer.RecursivelyBuild(args, builtArgs); @@ -1580,7 +1577,7 @@ public void AddUnsupported(string why) { class LambdaExprBuilder : StatementContainer, BuildableExpr { readonly List formals; readonly DAST.Type retType; - readonly List body = new(); + readonly List body = []; public LambdaExprBuilder(List formals, DAST.Type retType) { this.formals = formals; @@ -1651,12 +1648,13 @@ public void AddBuildable(BuildableExpr item) { public DAST.Expression Build() { var builtBody = new List(); - ExprContainer.RecursivelyBuild(new List { body ?? ExprContainer.UnsupportedToExpr("IIFEExprBuilder with empty body") }, builtBody); + ExprContainer.RecursivelyBuild([body ?? ExprContainer.UnsupportedToExpr("IIFEExprBuilder with empty body")], builtBody); var builtValue = new List(); - ExprContainer.RecursivelyBuild(new List { value - ?? ExprContainer.UnsupportedToExpr("IIFEExprBuilder with empty value") - }, builtValue); + ExprContainer.RecursivelyBuild([ + value + ?? ExprContainer.UnsupportedToExpr("IIFEExprBuilder with empty value") + ], builtValue); return (DAST.Expression)DAST.Expression.create_IIFE( Sequence.UnicodeFromString(name), @@ -1719,7 +1717,7 @@ public void AddBuildable(BuildableExpr item) { public DAST.Expression Build() { var builtBody = new List(); - ExprContainer.RecursivelyBuild(new List { body }, builtBody); + ExprContainer.RecursivelyBuild([body], builtBody); return (DAST.Expression)DAST.Expression.create_BetaRedex( Sequence<_System.Tuple2>.FromArray(bindings.ToArray()), @@ -1765,7 +1763,7 @@ public DAST.Expression Build() { if (value == null) { v = ExprContainer.UnsupportedToExpr($"Conversion from {fromType} to {toType} of something missing"); } else { - ExprContainer.RecursivelyBuild(new List { value }, builtValue); + ExprContainer.RecursivelyBuild([value], builtValue); v = builtValue[0]; } @@ -1809,7 +1807,7 @@ public void AddBuildable(BuildableExpr item) { public DAST.Expression Build() { var builtValue = new List(); - ExprContainer.RecursivelyBuild(new List { value }, builtValue); + ExprContainer.RecursivelyBuild([value], builtValue); return (DAST.Expression)DAST.Expression.create_Index( builtValue[0], @@ -1869,7 +1867,7 @@ public DAST.Expression Build() { if (bound == null) { endExpr = ExprContainer.UnsupportedToExpr($"NativeRangeBuilder has no upper bound"); } else { - ExprContainer.RecursivelyBuild(new List { bound }, builtValue); + ExprContainer.RecursivelyBuild([bound], builtValue); endExpr = builtValue[0]; } @@ -1926,7 +1924,7 @@ public DAST.Expression Build() { if (array == null) { arrayExpr = ExprContainer.UnsupportedToExpr($"ArrayLengthBuilder has no array"); } else { - ExprContainer.RecursivelyBuild(new List { array }, builtValue); + ExprContainer.RecursivelyBuild([array], builtValue); arrayExpr = builtValue[0]; } diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index ba17c4a4d15..fbb1ea3c1ac 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -106,7 +106,7 @@ public void AddUnsupportedFeature(IOrigin tok, Feature feature) { Feature.NonNativeNewtypes }; - private readonly List Imports = new() { DafnyDefaultModule }; + private readonly List Imports = [DafnyDefaultModule]; private const string DafnyRuntimeModule = "_dafny"; private const string DafnyDefaultModule = "module_"; @@ -248,7 +248,7 @@ protected override IClassWriter CreateTrait(string name, bool isExtern, List GenTypeArgDecl(tp)).ToList(); - List parents = new(); + List parents = []; if (trait.IsReferenceTypeDecl) { parents.Add((DAST.Type)DAST.Type.create_Object()); } @@ -284,7 +284,7 @@ private static bool isTpSupported(TypeParameter tp, [CanBeNull] out string why) protected override IClassWriter DeclareDatatype(DatatypeDecl dt, ConcreteSyntaxTree wr) { if (currentBuilder is DatatypeContainer builder) { - List typeParams = new(); + List typeParams = []; foreach (var tp in dt.TypeArgs) { typeParams.Add(GenTypeArgDecl(tp)); } @@ -328,7 +328,7 @@ from arg in ctor.Formals protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) { if (currentBuilder is NewtypeContainer builder) { - List witnessStmts = new(); + List witnessStmts = []; DAST.Expression witness = null; var statementBuf = new StatementBuffer(); if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) { @@ -360,7 +360,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre } return new ClassWriter(this, false, builder.Newtype( - nt.GetCompileName(Options), new(), + nt.GetCompileName(Options), [], GenType(nt.BaseType), NativeTypeToNewtypeRange(nt, false), constraint, witnessStmts, witness, ParseAttributes(nt.Attributes), GetDocString(nt))); } else { @@ -449,7 +449,7 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree var erasedType = sst.Rhs.NormalizeExpand(); - List witnessStmts = new(); + List witnessStmts = []; DAST.Expression witness = null; var statementBuf = new StatementBuffer(); if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) { @@ -463,7 +463,7 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree witnessStmts = statementBuf.PopAll(); } - List typeParams = new(); + List typeParams = []; foreach (var tp in sst.TypeArgs) { typeParams.Add(GenTypeArgDecl(tp, tp.Name)); // TODO: Test if we can remove the second argument } @@ -481,7 +481,7 @@ protected override void GetNativeInfo(NativeType.Selection sel, out string name, private Sequence GenFormals(List formals) { - List paramsList = new(); + List paramsList = []; foreach (var param in formals) { if (!param.IsGhost) { paramsList.Add((DAST.Formal)DAST.Formal.create_Formal( @@ -528,7 +528,7 @@ private class ClassWriter : IClassWriter { private readonly DafnyCodeGenerator compiler; private readonly ClassLike builder; private readonly bool hasTypeArgs; - private readonly List methods = new(); + private readonly List methods = []; public ClassWriter(DafnyCodeGenerator compiler, bool hasTypeArgs, ClassLike builder) { this.compiler = compiler; @@ -547,8 +547,8 @@ public ConcreteSyntaxTree CreateMethod(Method m, List var params_ = compiler.GenFormals(m.Ins); - List> outVars = new(); - List outTypes = new(); + List> outVars = []; + List outTypes = []; foreach (var outVar in m.Outs) { if (!outVar.IsGhost) { outVars.Add(Sequence.UnicodeFromString(compiler.IdProtect(outVar.GetOrCreateCompileName(m.CodeGenIdGenerator)))); @@ -622,9 +622,7 @@ public ConcreteSyntaxTree CreateFunction(string name, List)Sequence.Empty, - new() { - compiler.GenType(resultType) - }, null + [], (Sequence)Sequence.Empty, + [compiler.GenType(resultType)], null ); methods.Add(builder); @@ -1024,10 +1020,10 @@ public override bool NeedsCustomReceiverNotTrait(MemberDecl member) { protected override void EmitStaticExternMethodQualifier(string qual, ConcreteSyntaxTree wr) { if (GetExprBuilder(wr, out var builder)) { builder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_ExternCompanion( - Sequence>.FromArray(new[] { + Sequence>.FromArray([ Defs.__default.DAFNY__EXTERN__MODULE, Sequence.UnicodeFromString(qual) - }) + ]) )); } else { throw new InvalidOperationException(); @@ -1684,9 +1680,10 @@ private DAST.Type FullTypeNameAST(UserDefinedType udt, MemberDecl member = null) } private ISequence> PathFromTopLevel(TopLevelDecl topLevel) { - List> path = new(); - path.Add(Sequence.UnicodeFromString(topLevel.EnclosingModuleDefinition.GetCompileName(Options))); - path.Add(Sequence.UnicodeFromString(topLevel.GetCompileName(Options))); + List> path = [ + Sequence.UnicodeFromString(topLevel.EnclosingModuleDefinition.GetCompileName(Options)), + Sequence.UnicodeFromString(topLevel.GetCompileName(Options)) + ]; return Sequence>.FromArray(path.ToArray()); } @@ -1880,7 +1877,7 @@ protected override void EmitDatatypeValue(DatatypeValue dtv, string typeDescript if (GetExprBuilder(wr, out var builder) && currentBuilder is ExprBuffer buf) { List contents = buf.PopAll(); currentBuilder = buf.parent; // pop early to make sure the receiving builder is in the expected state - List<_System._ITuple2, DAST.Expression>> namedContents = new(); + List<_System._ITuple2, DAST.Expression>> namedContents = []; int argI = 0; for (int i = 0; i < dtv.Ctor.Formals.Count; i++) { @@ -2439,9 +2436,9 @@ protected override ConcreteSyntaxTree EmitCallToIsMethod(RedirectingTypeDecl dec return wrRhs; } - var signature = Sequence<_IFormal>.FromArray(new[] { + var signature = Sequence<_IFormal>.FromArray([ new DAST.Formal(Sequence.UnicodeFromString("_dummy_"), GenType(type), Sequence.Empty) - }); + ]); var c = builder.Builder.Call(signature); c.SetName((DAST.CallName)DAST.CallName.create_CallName(Sequence.UnicodeFromString("is"), Option<_IType>.create_None(), Option<_IFormal>.create_None(), false, signature)); @@ -2548,7 +2545,7 @@ protected override void EmitDatatypeBoundedPool(IVariable bv, string propertySuf if (GetExprConverter(wr, wStmts, out var exprBuilder, out var convert)) { if (bv.Type.IsDatatype && bv.Type.AsDatatype is { } datatypeDecl) { - var signature = Sequence<_IFormal>.FromArray(new _IFormal[] { }); + var signature = Sequence<_IFormal>.FromArray([]); var c = exprBuilder.Builder.Call(signature); c.SetName((DAST.CallName)DAST.CallName.create_CallName(Sequence.UnicodeFromString("_AllSingletonConstructors"), Option<_IType>.create_None(), Option<_IFormal>.create_None(), false, signature)); @@ -2576,13 +2573,13 @@ protected override void CreateIIFE(string bvName, Type bvType, IOrigin bvTok, Ty protected override ConcreteSyntaxTree CreateIIFE0(Type resultType, IOrigin resultTok, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { EmitLambdaApply(wr, out var wLambda, out var wArg); - return CreateLambda(new(), null, new(), resultType, wLambda, wStmts); + return CreateLambda([], null, [], resultType, wLambda, wStmts); } protected override ConcreteSyntaxTree CreateIIFE1(int source, Type resultType, IOrigin resultTok, string bvName, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { EmitLambdaApply(wr, out var wLambda, out var wArg); - var ret = CreateLambda(new() { Type.Int }, null, new() { bvName }, resultType, wLambda, wStmts); + var ret = CreateLambda([Type.Int], null, [bvName], resultType, wLambda, wStmts); EmitLiteralExpr(wArg, new LiteralExpr(null, source) { Type = Type.Int }); @@ -3066,8 +3063,8 @@ protected override void EmitSetBuilder_Add(CollectionType ct, string collName, E if (GetStatementBuilder(wr, out var builder)) { var stmtBuilder = new CallStmtBuilder(Sequence<_IFormal>.Empty); stmtBuilder.SetName((DAST.CallName)DAST.CallName.create_SetBuilderAdd()); - stmtBuilder.SetTypeArgs(new List { }); - stmtBuilder.SetOuts(new List> { }); ; + stmtBuilder.SetTypeArgs([]); + stmtBuilder.SetOuts([]); ; stmtBuilder.AddExpr((DAST.Expression)DAST.Expression.create_Ident(Sequence.UnicodeFromString(collName))); stmtBuilder.AddExpr(ConvertExpression(elmt, builder)); builder.Builder.AddBuildable(stmtBuilder); @@ -3098,8 +3095,8 @@ protected override ConcreteSyntaxTree EmitMapBuilder_Add(MapType mt, IOrigin tok if (GetStatementBuilder(wr, out var builder)) { var stmtBuilder = new CallStmtBuilder(Sequence<_IFormal>.Empty); stmtBuilder.SetName((DAST.CallName)DAST.CallName.create_MapBuilderAdd()); - stmtBuilder.SetTypeArgs(new List { }); - stmtBuilder.SetOuts(new List> { }); ; + stmtBuilder.SetTypeArgs([]); + stmtBuilder.SetOuts([]); ; stmtBuilder.AddExpr((DAST.Expression)DAST.Expression.create_Ident(Sequence.UnicodeFromString(collName))); var keyBuilder = CreateExprBuilder(); stmtBuilder.AddBuildable((ExprBuffer)keyBuilder.Builder); @@ -3185,8 +3182,8 @@ protected override void GetCollectionBuilder_Build(CollectionType ct, IOrigin to callExpr.SetName((DAST.CallName)DAST.CallName.create_SetBuilderBuild()); } - callExpr.SetTypeArgs(new List { }); - callExpr.SetOuts(new List> { }); ; + callExpr.SetTypeArgs([]); + callExpr.SetOuts([]); ; callExpr.AddExpr((DAST.Expression)DAST.Expression.create_Ident(Sequence.UnicodeFromString(collName))); builder.Builder.AddBuildable(callExpr); } else { diff --git a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs index 2012cf6d474..5aff07dae1d 100644 --- a/Source/DafnyCore/Backends/DafnyExecutableBackend.cs +++ b/Source/DafnyCore/Backends/DafnyExecutableBackend.cs @@ -16,7 +16,7 @@ public abstract class DafnyExecutableBackend : ExecutableBackend { protected DafnyWrittenCodeGenerator DafnyCodeGenerator; - public List ImportedFiles = new(); + public List ImportedFiles = []; protected DafnyExecutableBackend(DafnyOptions options) : base(options) { } diff --git a/Source/DafnyCore/Backends/ExecutableBackend.cs b/Source/DafnyCore/Backends/ExecutableBackend.cs index 23e22670091..63ed85d5cb8 100644 --- a/Source/DafnyCore/Backends/ExecutableBackend.cs +++ b/Source/DafnyCore/Backends/ExecutableBackend.cs @@ -108,7 +108,7 @@ private static ModuleDefinition CreateOuterModule(string moduleName) { ModuleDefinition module = null; foreach (var outerModule in outerModules) { - var thisModule = new ModuleDefinition(SourceOrigin.NoToken, new Name(outerModule), new List(), + var thisModule = new ModuleDefinition(SourceOrigin.NoToken, new Name(outerModule), [], ModuleKindEnum.Concrete, false, null, null, null) { EnclosingModule = module @@ -155,7 +155,7 @@ public ProcessStartInfo PrepareProcessStartInfo(string programName, IEnumerable< CreateNoWindow = false, // https://github.com/dotnet/runtime/issues/68259 RedirectStandardOutput = true, }; - foreach (var arg in args ?? Enumerable.Empty()) { + foreach (var arg in args ?? []) { psi.ArgumentList.Add(arg); } return psi; diff --git a/Source/DafnyCore/Backends/GoLang/GoBackend.cs b/Source/DafnyCore/Backends/GoLang/GoBackend.cs index 7ef9f0dedff..42702a2e8d4 100644 --- a/Source/DafnyCore/Backends/GoLang/GoBackend.cs +++ b/Source/DafnyCore/Backends/GoLang/GoBackend.cs @@ -125,7 +125,7 @@ private async Task SendToNewGoProcess(string dafnyProgramName, string targ return true; } - List goArgs = new(); + List goArgs = []; if (run) { goArgs.Add("run"); } else { diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs index 12dfa815b05..ca15e2061b9 100644 --- a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs +++ b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs @@ -60,17 +60,16 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) { } private readonly Dictionary ModuleImports = new(); - private readonly List ImportsNotFromDafnyModules = new(StandardImports); + private readonly List ImportsNotFromDafnyModules = [.. StandardImports]; private string ModuleName; private ModuleDefinition CurrentModule; private ConcreteSyntaxTree RootImportWriter; private ConcreteSyntaxTree RootImportDummyWriter; private string MainModuleName; - private static List StandardImports = - new List { - new Import { Name = "os", Path = "os" }, - }; + private static List StandardImports = [ + new Import { Name = "os", Path = "os" } + ]; private static string DummyTypeName = "Dummy__"; private static string ImportPrefix = "m_"; @@ -1294,7 +1293,7 @@ public void DeclareField(string name, TopLevelDecl enclosingDecl, bool isStatic, public void InitializeField(Field field, Type instantiatedFieldType, TopLevelDeclWithMembers enclosingClass) { var tok = field.Origin; var lvalue = CodeGenerator.EmitMemberSelect(w => w.Write("_this"), UserDefinedType.FromTopLevelDecl(tok, enclosingClass), field, - new List(), enclosingClass.ParentFormalTypeParametersToActuals, instantiatedFieldType); + [], enclosingClass.ParentFormalTypeParametersToActuals, instantiatedFieldType); var wRHS = lvalue.EmitWrite(FieldInitWriter(false)); CodeGenerator.EmitCoercionIfNecessary(instantiatedFieldType, field.Type, tok, wRHS); wRHS.Write(CodeGenerator.PlaceboValue(instantiatedFieldType, ErrorWriter(), tok)); @@ -1322,8 +1321,8 @@ public void Finish() { ConcreteSyntaxTree abstractWriter, ConcreteSyntaxTree concreteWriter, bool forBodyInheritance, bool lookasideBody) { var fnOverridden = (member as Function)?.OverriddenFunction?.Original; - return CreateSubroutine(name, typeArgs, formals, new List(), resultType, - fnOverridden?.Ins, fnOverridden == null ? null : new List(), fnOverridden?.ResultType, + return CreateSubroutine(name, typeArgs, formals, [], resultType, + fnOverridden?.Ins, fnOverridden == null ? null : [], fnOverridden?.ResultType, tok, isStatic, createBody, ownerContext, ownerName, member, abstractWriter, concreteWriter, forBodyInheritance, lookasideBody); } @@ -1558,7 +1557,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IOrig protected ConcreteSyntaxTree/*?*/ CreateGetter(string name, Type resultType, IOrigin tok, bool isStatic, bool createBody, MemberDecl/*?*/ member, TopLevelDecl ownerContext, string ownerName, ConcreteSyntaxTree abstractWriter, ConcreteSyntaxTree concreteWriter, bool forBodyInheritance) { - return CreateFunction(name, new List(), new List(), resultType, + return CreateFunction(name, [], [], resultType, tok, isStatic, createBody, member, ownerContext, ownerName, abstractWriter, concreteWriter, forBodyInheritance, false); } @@ -1569,8 +1568,8 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IOrig var getterWriter = CreateGetter(name, resultType, tok, false, createBody, member, ownerContext, ownerName, abstractWriter, concreteWriter, forBodyInheritance); var valueParam = new Formal(tok, "value", resultType, true, false, null); - setterWriter = CreateSubroutine(name + "_set_", new List(), new List() { valueParam }, new List(), null, - new List() { valueParam }, new List(), null, + setterWriter = CreateSubroutine(name + "_set_", [], [valueParam], [], null, + [valueParam], [], null, tok, false, createBody, ownerContext, ownerName, member, abstractWriter, concreteWriter, forBodyInheritance, false); return getterWriter; @@ -2624,7 +2623,7 @@ public override string PublicIdProtect(string name) { return res; }).join("")) */ - public readonly HashSet ReservedModuleNames = new() { + public readonly HashSet ReservedModuleNames = [ "c", "archive", "bufio", @@ -2672,7 +2671,7 @@ public override string PublicIdProtect(string name) { "time", "unicode", "unsafe" - }; + ]; public string PublicModuleIdProtect(string name) { if (ReservedModuleNames.Contains(name.ToLower())) { @@ -3259,7 +3258,7 @@ protected override void EmitSeqConstructionExpr(SeqConstructionExpr expr, bool i var fromType = (ArrowType)expr.Initializer.Type.NormalizeExpand(); var atd = (ArrowTypeDecl)fromType.ResolvedClass; var tParam = new UserDefinedType(expr.Origin, new TypeParameter(expr.Origin, new Name("X"), TypeParameter.TPVarianceSyntax.NonVariant_Strict)); - var toType = new ArrowType(expr.Origin, atd, new List() { Type.Int }, tParam); + var toType = new ArrowType(expr.Origin, atd, [Type.Int], tParam); var initWr = EmitCoercionIfNecessary(fromType, toType, expr.Origin, wr); initWr.Append(Expr(expr.Initializer, inLetExprBody, wStmts)); wr.Write(")"); diff --git a/Source/DafnyCore/Backends/InternalBackendsPluginConfiguration.cs b/Source/DafnyCore/Backends/InternalBackendsPluginConfiguration.cs index ebd3651fad5..d8b1c1deb96 100644 --- a/Source/DafnyCore/Backends/InternalBackendsPluginConfiguration.cs +++ b/Source/DafnyCore/Backends/InternalBackendsPluginConfiguration.cs @@ -6,7 +6,7 @@ internal class InternalBackendsPluginConfiguration : Plugins.PluginConfiguration public static readonly InternalBackendsPluginConfiguration Singleton = new(); public override IExecutableBackend[] GetCompilers(DafnyOptions options) { - return new IExecutableBackend[] { + return [ new CsharpBackend(options), new JavaScriptBackend(options), new GoBackend(options), @@ -16,6 +16,6 @@ public override IExecutableBackend[] GetCompilers(DafnyOptions options) { new LibraryBackend(options), new RustBackend(options), new ResolvedDesugaredExecutableDafnyBackend(options) - }; + ]; } } \ No newline at end of file diff --git a/Source/DafnyCore/Backends/Java/JavaBackend.cs b/Source/DafnyCore/Backends/Java/JavaBackend.cs index a0dd281c25d..82678ae7132 100644 --- a/Source/DafnyCore/Backends/Java/JavaBackend.cs +++ b/Source/DafnyCore/Backends/Java/JavaBackend.cs @@ -133,8 +133,8 @@ private void EmitRuntimeJar(string targetDirectory) { public async Task CreateJar(string/*?*/ entryPointName, string jarPath, string rootDirectory, List files, TextWriter outputWriter) { Directory.CreateDirectory(Path.GetDirectoryName(jarPath)); var args = entryPointName == null ? // If null, then no entry point is added - new List { "cf", jarPath } - : new List { "cfe", jarPath, entryPointName }; + ["cf", jarPath] + : new List { "cfe", jarPath, entryPointName }; var jarCreationProcess = PrepareProcessStartInfo("jar", args.Concat(files)); jarCreationProcess.WorkingDirectory = rootDirectory; return 0 == await RunProcess(jarCreationProcess, outputWriter, outputWriter, "Error while creating jar file: " + jarPath); diff --git a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs index 89c86b482ad..4bbab1a1226 100644 --- a/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs @@ -67,7 +67,7 @@ string FormatTypeDescriptorVariable(TypeParameter tp) => private string ModuleName; private string ModulePath; - private readonly List Instrumenters = new(); + private readonly List Instrumenters = []; public void AddInstrumenter(GenericCompilationInstrumenter compilationInstrumenter) { Instrumenters.Add(compilationInstrumenter); @@ -708,7 +708,7 @@ private string TypeName(Type type, ConcreteSyntaxTree wr, IOrigin tok, bool boxe } // When accessing a static member, leave off the type arguments if (member != null) { - return TypeName_UDT(s, new List(), new List(), wr, udt.Origin, erased); + return TypeName_UDT(s, [], [], wr, udt.Origin, erased); } else { return TypeName_UDT(s, udt, wr, udt.Origin, erased); } @@ -1536,7 +1536,7 @@ protected override ConcreteSyntaxTree EmitArraySelect(List indices, private ConcreteSyntaxTree EmitArraySelect(int dimCount, out List wIndices, Type elmtType, ConcreteSyntaxTree wr) { elmtType = DatatypeWrapperEraser.SimplifyType(Options, elmtType); - wIndices = new List(); + wIndices = []; ConcreteSyntaxTree w; if (dimCount == 1) { if (elmtType.IsTypeParameter) { @@ -2600,7 +2600,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IOrig } else if (cl is DatatypeDecl dt) { relevantTypeArgs = udt.TypeArgs; } else { - relevantTypeArgs = new List(); + relevantTypeArgs = []; for (int i = 0; i < cl.TypeArgs.Count; i++) { if (NeedsTypeDescriptor(cl.TypeArgs[i])) { relevantTypeArgs.Add(udt.TypeArgs[i]); @@ -2652,7 +2652,7 @@ protected override void EmitMapBuilder_New(ConcreteSyntaxTree wr, MapComprehensi } protected override void OrganizeModules(Program program, out List modules) { - modules = new List(); + modules = []; foreach (var m in program.CompileModules) { if (!m.IsDefaultModule && !m.Name.Equals("_System")) { modules.Add(m); diff --git a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs index a75fd312f41..9550e900a7c 100644 --- a/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs +++ b/Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs @@ -598,7 +598,7 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre // In JavaScript, the companion class of a newtype (which is what is being declared here) doubles as a // type descriptor for the newtype. The Default() method for that type descriptor is declared here. var wDefault = w.NewBlock("static get Default()"); - var udt = new UserDefinedType(nt.Origin, nt.Name, nt, new List()); + var udt = new UserDefinedType(nt.Origin, nt.Name, nt, []); var d = TypeInitializationValue(udt, wr, nt.Origin, false, false); wDefault.WriteLine("return {0};", d); diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs index e95837a998b..b34c109afd9 100644 --- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs @@ -233,7 +233,7 @@ private static string MangleName(string name) { protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List typeParameters, TopLevelDecl cls, List superClasses, IOrigin tok, ConcreteSyntaxTree wr) { - var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? new List(); + var realSuperClasses = superClasses?.Where(trait => !trait.IsObject).ToList() ?? []; var baseClasses = realSuperClasses.Any() ? $"({realSuperClasses.Comma(trait => TypeName(trait, wr, tok))})" : ""; @@ -1265,12 +1265,12 @@ public override string PublicIdProtect(string name) { } - private readonly HashSet ReservedModuleNames = new() { + private readonly HashSet ReservedModuleNames = [ "itertools", "math", "typing", "sys" - }; + ]; private string PublicModuleIdProtect(string name) { if (ReservedModuleNames.Contains(name)) { diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs index 2bec6432580..d6d4549a63d 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs @@ -153,7 +153,7 @@ void writeObj(ConcreteSyntaxTree w) { if (e.Seq.Type.IsArrayType) { if (e.SelectOne) { Contract.Assert(e.E0 != null && e.E1 == null); - var w = EmitArraySelect(new List() { e.E0 }, e.Type, inLetExprBody, wr, wStmts); + var w = EmitArraySelect([e.E0], e.Type, inLetExprBody, wr, wStmts); w = EmitCoercionIfNecessary( e.Seq.Type, e.Seq.Type.IsNonNullRefType || !e.Seq.Type.IsRefType @@ -410,8 +410,8 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn wBody = EmitQuantifierExpr(collection, quantifierExpr is ForallExpr, collectionElementType, bv, wBody); var native = AsNativeType(e.BoundVars[i].Type); var tmpVarName = ProtectedFreshId(e is ForallExpr ? "_forall_var_" : "_exists_var_"); - ConcreteSyntaxTree newWBody = CreateLambda(new List { collectionElementType }, e.Origin, - new List { tmpVarName }, Type.Bool, wBody, wStmts, untyped: true); + ConcreteSyntaxTree newWBody = CreateLambda([collectionElementType], e.Origin, + [tmpVarName], Type.Bool, wBody, wStmts, untyped: true); wStmts = newWBody.Fork(); newWBody = MaybeInjectSubtypeConstraintWrtTraits( tmpVarName, collectionElementType, bv.Type, @@ -550,8 +550,8 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn type = ty }; var _this = new ThisExpr(thisContext); - wr = EmitBetaRedex(new List() { IdName(receiver) }, new List() { _this }, - new List() { _this.Type }, lambdaExpr.Type, lambdaExpr.Origin, inLetExprBody, wr, ref wStmts); + wr = EmitBetaRedex([IdName(receiver)], [_this], + [_this.Type], lambdaExpr.Type, lambdaExpr.Origin, inLetExprBody, wr, ref wStmts); } wr = CaptureFreeVariables(e, false, out var su, inLetExprBody, wr, ref wStmts); @@ -697,7 +697,7 @@ private void EmitMatchExpr(MatchExpr e, bool inLetExprBody, ConcreteSyntaxTree w string source = ProtectedFreshId("_source"); ConcreteSyntaxTree w; - w = CreateLambda(new List() { e.Source.Type }, e.Origin, new List() { source }, e.Type, wLambda, + w = CreateLambda([e.Source.Type], e.Origin, [source], e.Type, wLambda, wStmts); if (e.Cases.Count == 0) { @@ -738,7 +738,7 @@ protected virtual void TrOptNestedMatchExpr(NestedMatchExpr match, Type resultTy private ConcreteSyntaxTree EmitAppliedLambda(ConcreteSyntaxTree output, ConcreteSyntaxTree wStmts, IOrigin token, Type resultType) { EmitLambdaApply(output, out var lambdaApplyTarget, out _); - return CreateLambda(new List(), token, new List(), resultType, lambdaApplyTarget, wStmts); + return CreateLambda([], token, [], resultType, lambdaApplyTarget, wStmts); } } } diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs index dffe4000596..a7db491d0d2 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs @@ -172,7 +172,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree // Wrap this UpdateStmt with a VarDecl containing this Local that we haven't emitted yet. stmts[innerExtractIndex] = new VarDeclStmt(enclosingVarDecl.Origin, - new List() { locals[0] }, + [locals[0]], (AssignStatement)stmts[innerExtractIndex]); } TrStmtList(stmts, wr); @@ -271,7 +271,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree Coverage.Instrument(s.Origin, "implicit else branch", wr); thenWriter = EmitIf(out guardWriter, false, thenWriter); EmitUnaryExpr(ResolvedUnaryOp.BoolNot, notFalse.E, false, guardWriter, wStmts); - TrStmtList(new List(), thenWriter); + TrStmtList([], thenWriter); } else { // let's compile the "then" branch wr = EmitIf(out guardWriter, false, wr); @@ -441,13 +441,13 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree var lhs = (MemberSelectExpr)s0.Lhs; L = 2; tupleTypeArgs = TypeArgumentName(lhs.Obj.Type, wr, lhs.Origin); - tupleTypeArgsList = new List { lhs.Obj.Type }; + tupleTypeArgsList = [lhs.Obj.Type]; } else if (s0.Lhs is SeqSelectExpr) { var lhs = (SeqSelectExpr)s0.Lhs; L = 3; // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple tupleTypeArgs = TypeArgumentName(lhs.Seq.Type, wr, lhs.Origin) + IntSelect; - tupleTypeArgsList = new List { lhs.Seq.Type, null }; + tupleTypeArgsList = [lhs.Seq.Type, null]; } else { var lhs = (MultiSelectExpr)s0.Lhs; L = 2 + lhs.Indices.Count; @@ -456,7 +456,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree return; } tupleTypeArgs = TypeArgumentName(lhs.Array.Type, wr, lhs.Origin); - tupleTypeArgsList = new List { lhs.Array.Type }; + tupleTypeArgsList = [lhs.Array.Type]; for (int i = 0; i < lhs.Indices.Count; i++) { // note, we might as well do the BigInteger-to-int cast for array indices here, before putting things into the Tuple rather than when they are extracted from the Tuple tupleTypeArgs += IntSelect; diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs index 61b7a2418d9..0849d31e729 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs @@ -518,7 +518,7 @@ protected virtual void EmitMultiAssignment(List lhsExprs, List(); + wRhss = []; var rhsVars = new List(); foreach (var rhsType in rhsTypes) { string target = ProtectedFreshId("_rhs"); @@ -528,7 +528,7 @@ protected virtual void EmitMultiAssignment(List lhsExprs, List lhssn; if (lhss.Count > 1) { - lhssn = new List(); + lhssn = []; for (int i = 0; i < lhss.Count; ++i) { Expression lexpr = lhsExprs[i].Resolved; ILvalue lhs = lhss[i]; @@ -549,7 +549,7 @@ protected virtual void EmitMultiAssignment(List lhsExprs, List>() { wIndex => EmitIdentifier(targetIndex, wIndex) }, lhsTypes[i]); + ILvalue newLhs = new ArrayLvalueImpl(this, targetArray, [wIndex => EmitIdentifier(targetIndex, wIndex)], lhsTypes[i]); lhssn.Add(newLhs); } else if (lexpr is MultiSelectExpr multiSelectExpr) { @@ -2076,7 +2076,7 @@ seqType.Arg.AsSeqType is not { } subSeqType || } void OrderedBySCC(List decls, TopLevelDeclWithMembers c) { - List consts = new List(); + List consts = []; foreach (var decl in decls) { if (decl is ConstantField) { consts.Add((ConstantField)decl); @@ -2254,7 +2254,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite } else if (f is ConstantField) { var cf = (ConstantField)f; if (cf.IsStatic && !SupportsStaticsInGenericClasses && cf.EnclosingClass.TypeArgs.Count != 0) { - var wBody = classWriter.CreateFunction(IdName(cf), CombineAllTypeArguments(cf), new List(), cf.Type, cf.Origin, true, true, member, false, false); + var wBody = classWriter.CreateFunction(IdName(cf), CombineAllTypeArguments(cf), [], cf.Type, cf.Origin, true, true, member, false, false); Contract.Assert(wBody != null); // since the previous line asked for a body if (cf.Rhs != null) { CompileReturnBody(cf.Rhs, f.Type, wBody, null); @@ -2271,7 +2271,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite // because a newtype value is always represented as some existing type. // Likewise, an instance const with a RHS in a trait needs to be modeled as a static function (in the companion class) // that takes a parameter, because trait-equivalents in target languages don't allow implementations. - wBody = classWriter.CreateFunction(IdName(cf), CombineAllTypeArguments(cf), new List(), cf.Type, cf.Origin, InstanceConstAreStatic(), true, cf, false, true); + wBody = classWriter.CreateFunction(IdName(cf), CombineAllTypeArguments(cf), [], cf.Type, cf.Origin, InstanceConstAreStatic(), true, cf, false, true); Contract.Assert(wBody != null); // since the previous line asked for a body if (c is TraitDecl) { // also declare a function for the field in the interface @@ -2400,7 +2400,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite var typeArgs = CombineAllTypeArguments(cf); var typeDescriptors = ForTypeDescriptors(typeArgs, cf.EnclosingClass, cf, false); if (NeedsTypeDescriptors(typeDescriptors)) { - return classWriter.CreateFunction(name, typeArgs, new List(), cf.Type, cf.Origin, isStatic, createBody, cf, forBodyInheritance, false); + return classWriter.CreateFunction(name, typeArgs, [], cf.Type, cf.Origin, isStatic, createBody, cf, forBodyInheritance, false); } else { return classWriter.CreateGetter(name, enclosingDecl, cf.Type, cf.Origin, isStatic, true, createBody, cf, forBodyInheritance); } @@ -2684,7 +2684,7 @@ protected int WriteRuntimeTypeDescriptorsFormals(List /// private void CheckForCapitalizationConflicts(IEnumerable canChange, IEnumerable cantChange = null) where T : Declaration { if (cantChange == null) { - cantChange = Enumerable.Empty(); + cantChange = []; } IDictionary declsByCapName = new Dictionary(); ISet fixedNames = new HashSet(from decl in cantChange select Capitalize(decl.GetCompileName(Options))); @@ -2732,7 +2732,7 @@ protected string Capitalize(string str) { protected virtual string PrefixForForcedCapitalization { get => "Cap_"; } private static void MarkCapitalizationConflict(Declaration decl) { - decl.Attributes = new Attributes(CapitalizationConflictAttribute, new List(), decl.Attributes); + decl.Attributes = new Attributes(CapitalizationConflictAttribute, [], decl.Attributes); } protected static bool HasCapitalizationConflict(Declaration decl) { @@ -2769,13 +2769,13 @@ private void CompileFunction(Function f, IClassWriter cw, bool lookasideBody) { unit = new LiteralExpr(f.Origin, n); unit.Type = f.ResultType; } else if (resultType.AsSetType != null) { - unit = new SetDisplayExpr(f.Origin, !resultType.IsISetType, new List()); + unit = new SetDisplayExpr(f.Origin, !resultType.IsISetType, []); unit.Type = f.ResultType; } else if (resultType.AsMultiSetType != null) { - unit = new MultiSetDisplayExpr(f.Origin, new List()); + unit = new MultiSetDisplayExpr(f.Origin, []); unit.Type = f.ResultType; } else if (resultType.AsSeqType != null) { - unit = new SeqDisplayExpr(f.Origin, new List()); + unit = new SeqDisplayExpr(f.Origin, []); unit.Type = f.ResultType; } else { Contract.Assert(false); // unexpected type @@ -3292,7 +3292,7 @@ void TrStmtNonempty(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree wS Contract.Requires(wr != null); TrStmt(stmt, wr, wStmts); if (stmt.IsGhost) { - TrStmtList(new List(), EmitBlock(wr)); + TrStmtList([], EmitBlock(wr)); } } @@ -3502,7 +3502,7 @@ Type CompileCollection(BoundedPool bound, IVariable bv, bool inLetExprBody, bool } else if (bound is DatatypeBoundedPool) { var b = (DatatypeBoundedPool)bound; collectionWriter = (wr) => EmitDatatypeBoundedPool(bv, propertySuffix, inLetExprBody, wr, wStmts); - return new UserDefinedType(bv.Origin, new NameSegment(bv.Origin, b.Decl.Name, new())) { + return new UserDefinedType(bv.Origin, new NameSegment(bv.Origin, b.Decl.Name, [])) { ResolvedClass = b.Decl }; } else { @@ -3822,7 +3822,7 @@ protected virtual ILvalue SeqSelectLvalue(SeqSelectExpr ll, ConcreteSyntaxTree w if (ll.Seq.Type.IsArrayType || ll.Seq.Type.NormalizeToAncestorType().AsSeqType != null) { index = ArrayIndexToNativeInt(index, ll.E0.Type); } - return new ArrayLvalueImpl(this, arr, new List>() { wIndex => wIndex.Write(index) }, ll.Type); + return new ArrayLvalueImpl(this, arr, [wIndex => wIndex.Write(index)], ll.Type); } protected virtual ILvalue MultiSelectLvalue(MultiSelectExpr ll, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) { @@ -4157,9 +4157,11 @@ void TrRhsArray(TypeRhs typeRhs, string nw, ConcreteSyntaxTree wr, ConcreteSynta var ii = 0; foreach (var v in typeRhs.InitDisplay) { pwStmts = wStmts.Fork(); - var (wArray, wElement) = EmitArrayUpdate(new List> { wIndex => EmitExprAsNativeInt(new LiteralExpr(null, ii) { - Type = Type.Int - }, false, wIndex, wStmts) }, v.Type, wStmts); + var (wArray, wElement) = EmitArrayUpdate([ + wIndex => EmitExprAsNativeInt(new LiteralExpr(null, ii) { + Type = Type.Int + }, false, wIndex, wStmts) + ], v.Type, wStmts); if (ii == 0 && nwElement0 != null) { EmitIdentifier(nwElement0, wElement); } else { @@ -5150,8 +5152,8 @@ void CreateFreeVarSubstitution(Expression expr, out List bvars, out Li var fvs = FreeVariablesUtil.ComputeFreeVariables(Options, expr); var sm = new Dictionary(); - bvars = new List(); - fexprs = new List(); + bvars = []; + fexprs = []; foreach (var fv in fvs) { if (fv.IsGhost) { continue; diff --git a/Source/DafnyCore/CompileNestedMatch/MatchAst.cs b/Source/DafnyCore/CompileNestedMatch/MatchAst.cs index 4db02cd01c5..031ac1d9e5d 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchAst.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchAst.cs @@ -8,7 +8,7 @@ public class MatchExpr : Expression, IMatch, ICloneable { // a Match private Expression source; private List cases; public readonly MatchingContext Context; - [FilledInDuringResolution] public List MissingCases { get; } = new(); + [FilledInDuringResolution] public List MissingCases { get; } = []; public readonly bool UsesOptionalBraces; public MatchExpr OrigUnresolved; // the resolver makes this clone of the MatchExpr before it starts desugaring it @@ -122,7 +122,7 @@ void ObjectInvariant() { private Expression source; private List cases; public readonly MatchingContext Context; - [FilledInDuringResolution] public List MissingCases { get; } = new(); + [FilledInDuringResolution] public List MissingCases { get; } = []; public readonly bool UsesOptionalBraces; public MatchStmt Clone(Cloner cloner) { diff --git a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs index ebb7252d4fa..b400770885c 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs @@ -94,7 +94,7 @@ private Expression CompileNestedMatchExpr(NestedMatchExpr nestedMatchExpr) { }; } - return new MatchExpr(nestedMatchExpr.Origin, nestedMatchExpr.Source, new List(), + return new MatchExpr(nestedMatchExpr.Origin, nestedMatchExpr.Source, [], nestedMatchExpr.UsesOptionalBraces) { Type = nestedMatchExpr.Type }; @@ -126,7 +126,7 @@ private Statement CompileNestedMatchStmt(NestedMatchStmt nestedMatchStmt) { return AssertStmt.CreateErrorAssert(nestedMatchStmt, NoCasesMessage); } - return new MatchStmt(nestedMatchStmt.Origin, nestedMatchStmt.Source, new List(), nestedMatchStmt.UsesOptionalBraces, nestedMatchStmt.Attributes); + return new MatchStmt(nestedMatchStmt.Origin, nestedMatchStmt.Source, [], nestedMatchStmt.UsesOptionalBraces, nestedMatchStmt.Attributes); } if (compiledMatch.Node is Statement statement) { @@ -444,7 +444,7 @@ private CaseBody CompileHeadsContainingLiteralPattern(MatchCompilationState mti, } // Create a list of alternatives - List ifBlockLiterals = new List(); + List ifBlockLiterals = []; foreach (var path in paths) { var head = GetPatternHead(path); var lit = GetLiteralExpressionFromPattern(head); @@ -539,7 +539,7 @@ private CaseBody CreateIfElseIfChain(MatchCompilationState mti, MatchingContext Type = Type.Bool }; - var contextStr = context.FillHole(new IdCtx($"c: {matchee.Type}", new List())).AbstractAllHoles().ToString(); + var contextStr = context.FillHole(new IdCtx($"c: {matchee.Type}", [])).AbstractAllHoles().ToString(); var errorMessage = mti.Match.Source.Type.AsDatatype == null ? $"missing case in match {mti.Match.MatchTypeName}: not all possibilities for selector of type {matchee.Type} have been covered" : $"missing case in match {mti.Match.MatchTypeName}: {contextStr} (not all possibilities for constant 'c' have been covered)"; @@ -599,7 +599,7 @@ private List UnboxStmt(Statement statement) { return block.Body; } - return new List() { statement }; + return [statement]; } private BlockStmt BlockStmtOfCStmt(IOrigin rangeOrigin, Statement stmt) { @@ -648,7 +648,7 @@ private record StmtPatternPath(IOrigin Tok, int CaseId, List Pa IReadOnlyList Body, Attributes Attributes) : PatternPath(Tok, CaseId, Patterns) { public StmtPatternPath(int caseId, NestedMatchCaseStmt x, Attributes attrs = null) : - this(x.Origin, caseId, new List() { x.Pat }, + this(x.Origin, caseId, [x.Pat], new List(x.Body), attrs) { Contract.Requires(!(x.Pat is DisjunctivePattern)); // No nested or patterns } @@ -666,7 +666,7 @@ private record ExprPatternPath(IOrigin Tok, int CaseId, List Pa Expression Body, Attributes Attributes) : PatternPath(Tok, CaseId, Patterns) { public ExprPatternPath(int caseId, NestedMatchCaseExpr x, Attributes attrs = null) : this(x.Origin, caseId, - new List() { x.Pat }, x.Body, attrs) { + [x.Pat], x.Body, attrs) { } public override string ToString() { @@ -714,7 +714,7 @@ private PatternPath LetBind(IdPattern var, Expression genExpr, PatternPath bodyP type = type }; var casePattern = new CasePattern(caseLocal.Origin.EndToken, caseLocal); - casePattern.AssembleExpr(new List()); + casePattern.AssembleExpr([]); var caseLet = new VarDeclPattern(caseLocal.Origin, casePattern, expr, false) { IsGhost = isGhost }; @@ -733,7 +733,7 @@ private PatternPath LetBind(IdPattern var, Expression genExpr, PatternPath bodyP var cBVar = (BoundVar)var.BoundVar; cBVar.IsGhost = isGhost; var cPat = new CasePattern(cBVar.Origin, cBVar); - cPat.AssembleExpr(new List()); + cPat.AssembleExpr([]); var cPats = new List>(); cPats.Add(cPat); var exprs = new List(); diff --git a/Source/DafnyCore/CounterExampleGeneration/Constraint.cs b/Source/DafnyCore/CounterExampleGeneration/Constraint.cs index ca41a5d6f78..163071eb8b5 100644 --- a/Source/DafnyCore/CounterExampleGeneration/Constraint.cs +++ b/Source/DafnyCore/CounterExampleGeneration/Constraint.cs @@ -172,7 +172,7 @@ public class IdentifierExprConstraint : DefinitionConstraint { private readonly string name; public IdentifierExprConstraint(PartialValue definedValue, string name) - : base(new List(), definedValue, new List()) { + : base(new List(), definedValue, []) { this.name = name; } @@ -187,7 +187,7 @@ public class ArraySelectionConstraint : DefinitionConstraint { public ArraySelectionConstraint(PartialValue definedValue, PartialValue array, List indices) : base(new List() { array }, definedValue, - new List() { new ArrayLengthConstraint(array, indices) }) { + [new ArrayLengthConstraint(array, indices)]) { Array = array; this.indices = indices; } @@ -204,7 +204,7 @@ public class LiteralExprConstraint : DefinitionConstraint { public readonly Expression LiteralExpr; public LiteralExprConstraint(PartialValue definedValue, Expression literalExpr) - : base(new List(), definedValue, new List()) { + : base(new List(), definedValue, []) { LiteralExpr = literalExpr; } @@ -234,12 +234,12 @@ public override Expression RightHandSide(Dictionary de public class MemberSelectExprDatatypeConstraint : MemberSelectExprConstraint { public MemberSelectExprDatatypeConstraint(PartialValue definedValue, PartialValue obj, string memberName) - : base(definedValue, obj, memberName, new List()) { } + : base(definedValue, obj, memberName, []) { } } public class MemberSelectExprClassConstraint : MemberSelectExprConstraint { public MemberSelectExprClassConstraint(PartialValue definedValue, PartialValue obj, string memberName) - : base(definedValue, obj, memberName, new List { new NotNullConstraint(obj) }) { + : base(definedValue, obj, memberName, [new NotNullConstraint(obj)]) { } } @@ -254,7 +254,7 @@ public DatatypeValueConstraint( string datatypeName, string constructorName, IReadOnlyCollection unnamedDestructors) - : base(unnamedDestructors, definedValue, new List()) { + : base(unnamedDestructors, definedValue, []) { UnnamedDestructors = unnamedDestructors; this.constructorName = constructorName; this.datatypeName = datatypeName; @@ -275,7 +275,7 @@ public class SeqSelectExprConstraint : DefinitionConstraint { public SeqSelectExprConstraint(PartialValue definedValue, PartialValue seq, PartialValue index) : base( new List { seq, index }, definedValue, - new List { new CardinalityGtThanConstraint(seq, index) }) { + [new CardinalityGtThanConstraint(seq, index)]) { Seq = seq; Index = index; } @@ -298,9 +298,7 @@ public class MapSelectExprConstraint : DefinitionConstraint { public MapSelectExprConstraint(PartialValue definedValue, PartialValue map, PartialValue key) : base( - new List { map, key }, definedValue, new List { - new ContainmentConstraint(key, map, true) - }) { + new List { map, key }, definedValue, [new ContainmentConstraint(key, map, true)]) { Map = map; Key = key; } @@ -318,7 +316,7 @@ public class SeqSelectExprWithLiteralConstraint : DefinitionConstraint { public SeqSelectExprWithLiteralConstraint(PartialValue definedValue, PartialValue seq, LiteralExpr index) : base( new List { seq }, definedValue, - new List { new CardinalityGtThanLiteralConstraint(seq, index) }) { + [new CardinalityGtThanLiteralConstraint(seq, index)]) { Seq = seq; Index = index; } @@ -334,7 +332,7 @@ public class CardinalityConstraint : DefinitionConstraint { public CardinalityConstraint(PartialValue definedValue, PartialValue collection) : base( - new List { collection }, definedValue, new List()) { + new List { collection }, definedValue, []) { Collection = collection; } @@ -348,7 +346,7 @@ public class SeqDisplayConstraint : DefinitionConstraint { public SeqDisplayConstraint(PartialValue definedValue, List elements) : base(elements, definedValue, - new List()) { + []) { this.elements = elements; } @@ -406,9 +404,8 @@ public FunctionCallConstraint( string functionName, bool receiverIsReferenceType) : base(args.Append(receiver), definedValue, receiverIsReferenceType - ? new List - { new NotNullConstraint(receiver), new FunctionCallRequiresConstraint(receiver, args, functionName) } - : new List { new FunctionCallRequiresConstraint(receiver, args, functionName) }) { + ? [new NotNullConstraint(receiver), new FunctionCallRequiresConstraint(receiver, args, functionName)] + : [new FunctionCallRequiresConstraint(receiver, args, functionName)]) { this.args = args; this.receiver = receiver; this.functionName = functionName; diff --git a/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs index db9cfd2ab7a..a2d1addef87 100644 --- a/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyCore/CounterExampleGeneration/DafnyModel.cs @@ -23,7 +23,7 @@ public class DafnyModel { public readonly List LoopGuards; private readonly DafnyOptions options; public readonly Model Model; - public readonly List States = new(); + public readonly List States = []; public static readonly UserDefinedType UnknownType = new(new Token(), "?", null); private readonly ModelFuncWrapper fSelect, fSetMember, fSeqLength, fSeqIndex, fBox, @@ -33,13 +33,13 @@ public class DafnyModel { fSeqUpdate, fSeqCreate, fU2Real, fU2Bool, fU2Int, fMapDomain, fMapElements, fMapValues, fMapBuild, fMapEmpty, fIs, fIsBox, fUnbox, fLs, fLz; private readonly Dictionary datatypeValues = new(); - private readonly List bitvectorFunctions = new(); + private readonly List bitvectorFunctions = []; // the model will begin assigning characters starting from this utf value private static readonly Regex UnderscoreRemovalRegex = new("__"); // This set is used by GetDafnyType to prevent infinite recursion - private HashSet exploredElements = new(); + private HashSet exploredElements = []; private readonly Dictionary concretizedValues = new(); @@ -50,7 +50,7 @@ public DafnyModel(Model model, DafnyOptions options) { CoreOptions.TypeEncoding.Arguments => 1, _ => 0 }; - fSelect = ModelFuncWrapper.MergeFunctions(this, new List { "MapType0Select", "MapType1Select" }, 2); + fSelect = ModelFuncWrapper.MergeFunctions(this, ["MapType0Select", "MapType1Select"], 2); fSetMember = new ModelFuncWrapper(this, "Set#IsMember", 2, 0); fSeqLength = new ModelFuncWrapper(this, "Seq#Length", 1, 0); fSeqBuild = new ModelFuncWrapper(this, "Seq#Build", 2, 0); @@ -90,7 +90,7 @@ public DafnyModel(Model model, DafnyOptions options) { fLz = new ModelFuncWrapper(this, "$LZ", 0, 0); InitDataTypes(); RegisterReservedBitVectors(); - LoopGuards = new List(); + LoopGuards = []; foreach (var s in model.States) { var sn = new PartialState(this, s); States.Add(sn); @@ -272,7 +272,7 @@ private void RegisterReservedBitVectors() { /// Get the Dafny type of an element internal Type GetFormattedDafnyType(Model.Element element) { - exploredElements = new HashSet(); + exploredElements = []; return DafnyModelTypeUtils.GetInDafnyFormat(GetDafnyType(element)); } @@ -317,7 +317,7 @@ private Type GetDafnyType(Model.Element element) { /// Return all elements x that satisfy ($Is element x) /// private List GetIsResults(Model.Element element) { - List result = new(); + List result = []; foreach (var tuple in fIs.AppsWithArg(0, element)) { if (((Model.Boolean)tuple.Result).Value) { result.Add(tuple.Args[1]); @@ -469,7 +469,7 @@ public void GetExpansion(PartialState state, PartialValue value) { switch (value.Type) { case SeqType: { if (fSeqEmpty.AppWithResult(value.Element) != null) { - var _ = new LiteralExprConstraint(value, new SeqDisplayExpr(Token.NoToken, new List())); + var _ = new LiteralExprConstraint(value, new SeqDisplayExpr(Token.NoToken, [])); return; } var lenghtTuple = fSeqLength.AppWithArg(0, value.Element); @@ -484,7 +484,7 @@ public void GetExpansion(PartialState state, PartialValue value) { } // Sequences can be constructed with the build operator: - List elements = new(); + List elements = []; Model.Element substring = value.Element; while (fSeqBuild.AppWithResult(substring) != null) { @@ -535,7 +535,7 @@ public void GetExpansion(PartialState state, PartialValue value) { } } if (fSetEmpty.AppWithResult(value.Element) != null) { - var _ = new LiteralExprConstraint(value, new SetDisplayExpr(Token.NoToken, true, new List())); + var _ = new LiteralExprConstraint(value, new SetDisplayExpr(Token.NoToken, true, [])); return; } @@ -601,7 +601,7 @@ public void GetExpansion(PartialState state, PartialValue value) { if (!result.Any() && fMapEmpty.AppWithResult(value.Element) != null) { - var _ = new LiteralExprConstraint(value, new MapDisplayExpr(Token.NoToken, true, new List())); + var _ = new LiteralExprConstraint(value, new MapDisplayExpr(Token.NoToken, true, [])); } return; @@ -834,7 +834,7 @@ private IEnumerable AddMappingHelper(PartialState state, PartialVa .Select(ReconstructType).OfType() .Where(type => type.Name != UnknownType.Name); var types = possiblyNullableTypes.Select(DafnyModelTypeUtils.GetNonNullable).OfType().ToList(); - List result = new(); + List result = []; var builtInDatatypeDestructor = new Regex("^.*[^_](__)*_q$"); var canCallFunctions = new HashSet(); foreach (var app in element.References) { @@ -866,8 +866,8 @@ private IEnumerable AddMappingHelper(PartialState state, PartialVa .Select(ReconstructType).OfType() .Where(type => type.Name != UnknownType.Name); var types = possiblyNullableTypes.Select(DafnyModelTypeUtils.GetNonNullable).OfType().ToList(); - List applications = new(); - List wellFormed = new(); + List applications = []; + List wellFormed = []; foreach (var app in element.References) { if (app.Args.Length == 0 || (!Equals(app.Args[0], element) && (heap == null || !Equals(app.Args[0], heap) || app.Args.Length == 1 || !Equals(app.Args[1], element))) || !types.Any(type => app.Func.Name.StartsWith(type.Name + ".")) || @@ -899,7 +899,7 @@ private IEnumerable AddMappingHelper(PartialState state, PartialVa /// private List GetFieldNames(Model.Element? elt) { if (elt == null) { - return new List(); + return []; } var dims = fDim.OptEval(elt)?.AsInt(); if (dims is null or 0) { // meaning elt is not an array index @@ -928,10 +928,10 @@ private List GetFieldNames(Model.Element? elt) { elt = dimTuple.Args[0]; } } - return new List() { + return [ "[" + string.Join(",", indices.ToList().ConvertAll(element => element == null ? "null" : element.ToString())) + "]" - }; + ]; } /// Unboxes an element, if possible diff --git a/Source/DafnyCore/CounterExampleGeneration/ModelFuncWrapper.cs b/Source/DafnyCore/CounterExampleGeneration/ModelFuncWrapper.cs index 5970115bc65..d45dd5d7ee4 100644 --- a/Source/DafnyCore/CounterExampleGeneration/ModelFuncWrapper.cs +++ b/Source/DafnyCore/CounterExampleGeneration/ModelFuncWrapper.cs @@ -111,7 +111,7 @@ internal static ModelFuncWrapper MergeFunctions(DafnyModel model, List n public class ModelFuncTupleWrapper { - static readonly Model.Element[] EmptyArgs = Array.Empty(); + static readonly Model.Element[] EmptyArgs = []; public readonly Model.Element Result; public readonly Model.Element[] Args; diff --git a/Source/DafnyCore/CounterExampleGeneration/PartialState.cs b/Source/DafnyCore/CounterExampleGeneration/PartialState.cs index 381207828e1..81a984779df 100644 --- a/Source/DafnyCore/CounterExampleGeneration/PartialState.cs +++ b/Source/DafnyCore/CounterExampleGeneration/PartialState.cs @@ -14,7 +14,7 @@ public class PartialState { public bool IsLoopEntryState => FullStateName.Contains(CaptureStateExtensions.AfterLoopIterationsStateMarker); // ghost variables introduced by the counterexample whose values must be true for the counterexample to hold: - public List LoopGuards = new(); + public List LoopGuards = []; public readonly Dictionary> KnownVariableNames = new(); private readonly List initialPartialValues; internal readonly DafnyModel Model; @@ -31,7 +31,7 @@ public class PartialState { internal PartialState(DafnyModel model, Model.CapturedState state) { Model = model; State = state; - initialPartialValues = new List(); + initialPartialValues = []; SetupBoundVars(); SetupVars(); } @@ -42,10 +42,10 @@ internal PartialState(DafnyModel model, Model.CapturedState state) { /// /// Set of partial values public HashSet ExpandedVariableSet() { - HashSet expandedSet = new(); + HashSet expandedSet = []; // The following is the queue for elements to be added to the set. The 2nd // element of a tuple is the depth of the variable w.r.t. the original set - List> varsToAdd = new(); + List> varsToAdd = []; initialPartialValues.ForEach(variable => varsToAdd.Add(new(variable, 0))); while (varsToAdd.Count != 0) { var (next, depth) = varsToAdd[0]; @@ -150,8 +150,8 @@ public Statement AsAssumption() { if (!IsLoopEntryState) { return new AssumeStmt(SourceOrigin.NoToken, expression, null); } - return new AssignStatement(SourceOrigin.NoToken, new List() { new IdentifierExpr(Token.NoToken, LoopGuards.Last()) }, - new List() { new ExprRhs(expression) }); + return new AssignStatement(SourceOrigin.NoToken, [new IdentifierExpr(Token.NoToken, LoopGuards.Last())], + [new ExprRhs(expression)]); } /// @@ -187,7 +187,7 @@ private void SetupVars() { initialPartialValues.Add(value); var _ = new IdentifierExprConstraint(value, v.Split("#").First()); if (!KnownVariableNames.ContainsKey(value)) { - KnownVariableNames[value] = new List(); + KnownVariableNames[value] = []; } KnownVariableNames[value].Add(v.Split("#").First()); } @@ -221,7 +221,7 @@ private void SetupBoundVars() { initialPartialValues.Add(value); var _ = new IdentifierExprConstraint(value, name); if (!KnownVariableNames.ContainsKey(value)) { - KnownVariableNames[value] = new(); + KnownVariableNames[value] = []; } KnownVariableNames[value].Add(name); } @@ -259,7 +259,7 @@ private static string ShortenName(string name, int fnLimit) { var loc = TryParseSourceLocation(name); if (loc != null) { var fn = loc.Filename; - int idx = fn.LastIndexOfAny(new[] { '\\', '/' }); + int idx = fn.LastIndexOfAny(['\\', '/']); if (idx > 0) { fn = fn[(idx + 1)..]; } diff --git a/Source/DafnyCore/CounterExampleGeneration/PartialValue.cs b/Source/DafnyCore/CounterExampleGeneration/PartialValue.cs index c8125fbd65b..def9dc13a64 100644 --- a/Source/DafnyCore/CounterExampleGeneration/PartialValue.cs +++ b/Source/DafnyCore/CounterExampleGeneration/PartialValue.cs @@ -36,7 +36,7 @@ public static PartialValue Get(Model.Element element, PartialState state) { private PartialValue(Model.Element element, PartialState state) { Element = element; this.state = state; - Constraints = new(); + Constraints = []; haveExpanded = false; state.AllPartialValues[element] = this; type = state.Model.GetFormattedDafnyType(element); diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index 9b5db49f03b..cba421b9028 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -65,18 +65,18 @@ public void RegisterFiles(Program program) { public void RegisterFile(Uri uri) { if (!labelsByFile.ContainsKey(uri)) { - labelsByFile[uri] = new List(); + labelsByFile[uri] = []; } } private void RegisterFiles(Node astNode) { if (astNode.StartToken.ActualFilename != null) { - labelsByFile.GetOrCreate(astNode.StartToken.Uri, () => new List()); + labelsByFile.GetOrCreate(astNode.StartToken.Uri, () => []); } if (astNode is LiteralModuleDecl moduleDecl) { if (astNode.StartToken.ActualFilename != null) { - modulesByFile.GetOrCreate(astNode.StartToken.Uri, () => new HashSet()).Add(moduleDecl.ModuleDef); + modulesByFile.GetOrCreate(astNode.StartToken.Uri, () => []).Add(moduleDecl.ModuleDef); } RegisterFiles(moduleDecl.ModuleDef); diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs index 46e5e233631..f6552c6bcc2 100644 --- a/Source/DafnyCore/DafnyConsolePrinter.cs +++ b/Source/DafnyCore/DafnyConsolePrinter.cs @@ -60,7 +60,7 @@ string GetId(ICarriesAttributes construct) { } } - public ConcurrentBag VerificationResults { get; } = new(); + public ConcurrentBag VerificationResults { get; } = []; public override void AdvisoryWriteLine(TextWriter output, string format, params object[] args) { if (output == Console.Out) { diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs index 6a043edbbeb..aca110228b6 100644 --- a/Source/DafnyCore/DafnyOptions.cs +++ b/Source/DafnyCore/DafnyOptions.cs @@ -153,7 +153,7 @@ public static void ParseGeneralTraitsOption(Option LegacyUis = new(); + private static readonly List LegacyUis = []; public static void RegisterLegacyUi(Option option, Action, Bpl.CommandLineParseState, DafnyOptions> parse, @@ -309,7 +309,7 @@ public enum DiagnosticsFormats { public string DafnyPrelude = null; public string DafnyPrintFile = null; public bool AllowSourceFolders = false; - public List SourceFolders { get; } = new(); // list of folders, for those commands that permit processing all source files in folders + public List SourceFolders { get; } = []; // list of folders, for those commands that permit processing all source files in folders public enum ContractTestingMode { None, @@ -320,9 +320,9 @@ public enum ContractTestingMode { public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything public bool DafnyVerify = true; public string DafnyPrintResolvedFile = null; - public List DafnyPrintExportedViews = new List(); + public List DafnyPrintExportedViews = []; public bool Compile = true; - public List MainArgs = new List(); + public List MainArgs = []; public bool FormatCheck = false; public string CompilerName; @@ -355,7 +355,7 @@ public enum ContractTestingMode { public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version4; public int DefiniteAssignmentLevel { get; set; } = 1; - public HashSet LibraryFiles { get; set; } = new(); + public HashSet LibraryFiles { get; set; } = []; public ContractTestingMode TestContracts = ContractTestingMode.None; public bool ForbidNondeterminism { get; set; } @@ -394,7 +394,7 @@ public enum IncludesModes { new(new[] { SinglePassCodeGenerator.Plugin, InternalDocstringRewritersPluginConfiguration.Plugin }); private IList cliPluginCache; public IList Plugins => cliPluginCache ??= ComputePlugins(AdditionalPlugins, AdditionalPluginArguments); - public List AdditionalPlugins = new(); + public List AdditionalPlugins = []; public IList AdditionalPluginArguments = new List(); public static IList ComputePlugins(List additionalPlugins, IList allArguments) { @@ -443,7 +443,7 @@ public DafnyOptions(DafnyOptions src, bool useNullWriters = false) : this( src.Input, src.OutputWriter, src.ErrorWriter) { src.CopyTo(this, useNullWriters); CliRootSourceUris = new List(src.CliRootSourceUris); - ProverOptions = new List(src.ProverOptions); + ProverOptions = [.. src.ProverOptions]; Options = new Options( src.Options.OptionArguments.ToDictionary(kv => kv.Key, kv => kv.Value), src.Options.Arguments.ToDictionary(kv => kv.Key, kv => kv.Value)); @@ -1583,10 +1583,10 @@ public override void Error(string message, params string[] args) { /// Used by the parser to parse :options strings. /// class DafnyAttributeOptions : DafnyOptions { - public static readonly HashSet KnownOptions = new() { + public static readonly HashSet KnownOptions = [ "functionSyntax", "quantifierSyntax" - }; + ]; private readonly Errors errors; public IOrigin Token { get; set; } diff --git a/Source/DafnyCore/Generic/BatchErrorReporter.cs b/Source/DafnyCore/Generic/BatchErrorReporter.cs index abf2771d956..02175c704b1 100644 --- a/Source/DafnyCore/Generic/BatchErrorReporter.cs +++ b/Source/DafnyCore/Generic/BatchErrorReporter.cs @@ -5,7 +5,7 @@ namespace Microsoft.Dafny; public class BatchErrorReporter : ErrorReporter { public Dictionary> AllMessagesByLevel; - public readonly List AllMessages = new(); + public readonly List AllMessages = []; public void CopyDiagnostics(ErrorReporter intoReporter) { foreach (var diagnostic in AllMessages) { @@ -16,9 +16,9 @@ public void CopyDiagnostics(ErrorReporter intoReporter) { public BatchErrorReporter(DafnyOptions options) : base(options) { ErrorsOnly = false; AllMessagesByLevel = new Dictionary> { - [ErrorLevel.Error] = new(), - [ErrorLevel.Warning] = new(), - [ErrorLevel.Info] = new() + [ErrorLevel.Error] = [], + [ErrorLevel.Warning] = [], + [ErrorLevel.Info] = [] }; } diff --git a/Source/DafnyCore/Generic/ErrorRegistry.cs b/Source/DafnyCore/Generic/ErrorRegistry.cs index 4b5b2ffd471..4f1e9bb73ac 100644 --- a/Source/DafnyCore/Generic/ErrorRegistry.cs +++ b/Source/DafnyCore/Generic/ErrorRegistry.cs @@ -46,7 +46,7 @@ public static class ErrorRegistry { public static string NoneId => "none"; #nullable enable public static List? GetAction(string? errorId) { - return errorId != null && codeActionMap.TryGetValue(errorId, out var value) ? new List { value } : null; + return errorId != null && codeActionMap.TryGetValue(errorId, out var value) ? [value] : null; } #nullable disable @@ -67,7 +67,7 @@ public static ActionSignature Replace(string newContent, string overrideTitle = public static DafnyCodeActionEdit[] OneEdit(SourceOrigin range, string newContent, bool includeTrailingWhitespace = false) { - return new[] { new DafnyCodeActionEdit(range, newContent, includeTrailingWhitespace) }; + return [new DafnyCodeActionEdit(range, newContent, includeTrailingWhitespace)]; } public static DafnyAction OneAction(string title, IOrigin range, string newContent, bool includeTrailingWhitespace = false) { @@ -151,7 +151,7 @@ public static void Add(object errorId, string detail, ActionSignature codeAction private static List ReplacementAction(string title, SourceOrigin range, string newText) { var edit = new[] { new DafnyCodeActionEdit(range, newText) }; var action = new DafnyAction(title, edit); - return new List { action }; + return [action]; } private static List ReplacementAction(SourceOrigin range, string newText) { @@ -163,13 +163,13 @@ private static List ReplacementAction(SourceOrigin range, string ne private static List InsertAction(string title, SourceOrigin range, string newText) { var edits = new[] { new DafnyCodeActionEdit(range, range.PrintOriginal() + newText) }; var action = new DafnyAction(title, edits); - return new List { action }; + return [action]; } private static List RemoveAction(string title, SourceOrigin range, bool includeTrailingSpaces) { var edit = new[] { new DafnyCodeActionEdit(range, "", includeTrailingSpaces) }; var action = new DafnyAction(title, edit); - return new List { action }; + return [action]; } private static List RemoveAction(SourceOrigin range, bool includeTrailingSpaces) { diff --git a/Source/DafnyCore/Generic/Node.cs b/Source/DafnyCore/Generic/Node.cs index a4403036256..895cc88e2df 100644 --- a/Source/DafnyCore/Generic/Node.cs +++ b/Source/DafnyCore/Generic/Node.cs @@ -118,7 +118,7 @@ private static IEnumerable GetConcreteChildren(INode node) { // containing this node, or null if it is not contained in any. // public virtual IEnumerable Assumptions(Declaration decl) { - return Enumerable.Empty(); + return []; } public ISet Visit(Func beforeChildren = null, Action afterChildren = null, Action reportError = null) { diff --git a/Source/DafnyCore/Generic/OrderedDictionary.cs b/Source/DafnyCore/Generic/OrderedDictionary.cs index 2f6d72621c5..b326a998d95 100644 --- a/Source/DafnyCore/Generic/OrderedDictionary.cs +++ b/Source/DafnyCore/Generic/OrderedDictionary.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public class OrderedDictionary { private readonly Dictionary keyToValue = new(); - private readonly List keyOrder = new(); + private readonly List keyOrder = []; private readonly Func getKey; public OrderedDictionary(Func getKey) { diff --git a/Source/DafnyCore/Generic/SccGraph.cs b/Source/DafnyCore/Generic/SccGraph.cs index aed140270df..7debe2a3ae0 100644 --- a/Source/DafnyCore/Generic/SccGraph.cs +++ b/Source/DafnyCore/Generic/SccGraph.cs @@ -12,7 +12,7 @@ public class Graph where Node : class { public enum VisitedStatus { Unvisited, OnStack, Visited } public class Vertex { public readonly Node N; - public readonly List/*!*/ Successors = new List(); + public readonly List/*!*/ Successors = []; public List SccMembers; // non-null only for the representative of the SCC [ContractInvariantMethod] void ObjectInvariant() { @@ -106,8 +106,9 @@ Vertex GetVertex(Node n) { if (sccComputed) { Contract.Assert(topologicallySortedRepresentatives != null); // follows from object invariant v.SccRepresentative = v; - v.SccMembers = new List(); - v.SccMembers.Add(v); + v.SccMembers = [ + v + ]; v.SccId = topologicallySortedRepresentatives.Count; v.SccPredecessorCount = 0; topologicallySortedRepresentatives.Add(v); @@ -191,7 +192,7 @@ public List GetSCC(Node n) { ComputeSCCs(); Vertex repr = v.SccRepresentative; Contract.Assert(repr != null && repr.SccMembers != null); // follows from postcondition of ComputeSCCs - List nn = new List(); + List nn = []; foreach (Vertex w in repr.SccMembers) { nn.Add(w.N); } @@ -225,7 +226,7 @@ void ComputeSCCs() { if (sccComputed) { return; } // check if already computed // reset all SCC information - topologicallySortedRepresentatives = new List(); + topologicallySortedRepresentatives = []; foreach (Vertex v in vertices.Values) { v.Visited = VisitedStatus.Unvisited; v.SccMembers = null; @@ -274,7 +275,7 @@ void SearchC(Vertex/*!*/ v, Stack/*!*/ stack, ref int cnt) { // The SCC containing 'v' has now been computed. v.SccId = topologicallySortedRepresentatives.Count; topologicallySortedRepresentatives.Add(v); - v.SccMembers = new List(); + v.SccMembers = []; while (true) { Vertex x = stack.Pop(); x.Visited = VisitedStatus.Visited; @@ -369,7 +370,7 @@ public List TryFindCycle() { if (v.Visited == VisitedStatus.Unvisited) { List cycle = CycleSearch(v); if (cycle != null) { - List nodes = new List(); + List nodes = []; foreach (Vertex v_ in cycle) { nodes.Add(v_.N); } @@ -402,8 +403,9 @@ public List TryFindCycle() { // there is no cycle in the subtree rooted at succ, hence this path does not give rise to any cycles } else if (succ.Visited == VisitedStatus.OnStack) { // we found a cycle! - List cycle = new List(); - cycle.Add(succ); + List cycle = [ + succ + ]; if (v == succ) { // entire cycle has been found v.Visited = VisitedStatus.Visited; diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index df1874cf264..c4ff2ebd36c 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -144,7 +144,7 @@ public static string Plural(int n) { } public static List Map(IEnumerable xs, Func f) { - List ys = new List(); + List ys = []; foreach (A x in xs) { ys.Add(f(x)); } @@ -152,11 +152,11 @@ public static List Map(IEnumerable xs, Func f) { } public static List Nil() { - return new List(); + return []; } public static List Singleton(A x) { - return new List { x }; + return [x]; } public static List List(params A[] xs) { @@ -172,7 +172,7 @@ public static List Snoc(List xs, A x) { } public static List Concat(List xs, List ys) { - List cpy = new List(xs); + List cpy = [.. xs]; cpy.AddRange(ys); return cpy; } @@ -495,7 +495,7 @@ static Graph BuildFunctionCallGraph(Dafny.Program program) { if (decl is TopLevelDeclWithMembers c) { foreach (var member in c.Members) { if (member is Function f) { - List calls = new List(); + List calls = []; foreach (var e in f.Reads.Expressions) { if (e != null && e.E != null) { callFinder.Visit(e.E, calls); } } foreach (var e in f.Req) { if (e != null) { callFinder.Visit(e, calls); } } foreach (var e in f.Ens) { if (e != null) { callFinder.Visit(e, calls); } } @@ -673,7 +673,7 @@ public void AddInclude(Include include) { if (found) { existingDependencies.Add(include.CanonicalPath); } else { - dependencies[key] = new SortedSet() { include.CanonicalPath }; + dependencies[key] = [include.CanonicalPath]; } } @@ -686,7 +686,7 @@ public void AddIncludes(IEnumerable includes) { } public void PrintMap(DafnyOptions options) { - SortedSet leaves = new SortedSet(); // Files that don't themselves include any files + SortedSet leaves = []; // Files that don't themselves include any files foreach (string target in dependencies.Keys) { options.OutputWriter.Write(target); foreach (string dependency in dependencies[target]) { diff --git a/Source/DafnyCore/JsonDiagnostics.cs b/Source/DafnyCore/JsonDiagnostics.cs index 37c25d806e1..61cd5ca44d9 100644 --- a/Source/DafnyCore/JsonDiagnostics.cs +++ b/Source/DafnyCore/JsonDiagnostics.cs @@ -75,7 +75,7 @@ private static IEnumerable SerializeAuxInfo(ErrorInformation.AuxErrorI } public JsonNode ToJson() { - var auxRelated = related?.SelectMany(SerializeAuxInfo) ?? Enumerable.Empty(); + var auxRelated = related?.SelectMany(SerializeAuxInfo) ?? []; var innerRelated = SerializeInnerTokens(tok); return new JsonObject { ["location"] = SerializeToken(tok), diff --git a/Source/DafnyCore/LegacyUiForOption.cs b/Source/DafnyCore/LegacyUiForOption.cs index 12153fc1b61..d13262f759e 100644 --- a/Source/DafnyCore/LegacyUiForOption.cs +++ b/Source/DafnyCore/LegacyUiForOption.cs @@ -27,7 +27,7 @@ public static string GenerateHelp(string template, IEnumerable()); + var optionsForCategory = optionsByCategory.GetValueOrDefault(categoryName, []); foreach (var option in optionsForCategory.OrderBy(o => o.Name)) { var prefix = oldStyle ? "/" : "--"; diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index 8ade67e6e07..99371b3a513 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -14,12 +14,12 @@ public class CommonOptionBag { public static void EnsureStaticConstructorHasRun() { } - public enum ProgressLevel { None, Symbol, VerificationJobs } + public enum ProgressLevel { None, Symbol, Batch } public static readonly Option ProgressOption = new("--progress", $"While verifying, output information that helps track progress. " + $"Use '{ProgressLevel.Symbol}' to show progress across symbols such as methods and functions. " + - $"Verification of a symbol is usually split across several jobs. " + - $"Use {ProgressLevel.VerificationJobs} to additionally show progress across jobs."); + $"Verification of a symbol may be split across several assertion batches. " + + $"Use {ProgressLevel.Batch} to additionally show progress across batches."); public static readonly Option LogLocation = new("--log-location", "Sets the directory where to store log files") { @@ -124,18 +124,18 @@ public static IEnumerable SplitOptionValueIntoFiles(IEnumerable return result; } - public static readonly Option BuildFile = new(new[] { "--build", "-b" }, + public static readonly Option BuildFile = new(["--build", "-b"], "Specify the filepath that determines where to place and how to name build files.") { ArgumentHelpName = "file", IsHidden = true }; - public static readonly Option Output = new(new[] { "--output", "-o" }, + public static readonly Option Output = new(["--output", "-o"], "Specify the filename and location for the generated target language files.") { ArgumentHelpName = "file", }; - public static readonly Option> PluginOption = new(new[] { "--plugin" }, + public static readonly Option> PluginOption = new(["--plugin"], @" (experimental) One path to an assembly that contains at least one instantiatable class extending Microsoft.Dafny.Plugin.Rewriter. It @@ -179,7 +179,7 @@ Note that quantifier variable domains (<- ) are available in both syntax ArgumentHelpName = "version", }; - public static readonly Option Target = new(new[] { "--target", "-t" }, () => "cs", @" + public static readonly Option Target = new(["--target", "-t"], () => "cs", @" cs - Compile to .NET via C#. go - Compile to Go. js - Compile to JavaScript. diff --git a/Source/DafnyCore/Options/DafnyProject.cs b/Source/DafnyCore/Options/DafnyProject.cs index 59643078797..1abb0e8a031 100644 --- a/Source/DafnyCore/Options/DafnyProject.cs +++ b/Source/DafnyCore/Options/DafnyProject.cs @@ -69,8 +69,8 @@ public static async Task Open(IFileSystem fileSystem, Uri uri, IOr var directory = Path.GetDirectoryName(uri.LocalPath)!; result = new DafnyProject(fileSnapshot.Version, uri, model.Base == null ? null : new Uri(Path.GetFullPath(model.Base, directory!)), - model.Includes?.Select(p => Path.GetFullPath(p, directory)).ToHashSet() ?? new HashSet(), - model.Excludes?.Select(p => Path.GetFullPath(p, directory)).ToHashSet() ?? new HashSet(), + model.Includes?.Select(p => Path.GetFullPath(p, directory)).ToHashSet() ?? [], + model.Excludes?.Select(p => Path.GetFullPath(p, directory)).ToHashSet() ?? [], model.Options ?? new Dictionary()); if (result.Base != null) { diff --git a/Source/DafnyCore/Options/DeveloperOptionBag.cs b/Source/DafnyCore/Options/DeveloperOptionBag.cs index bff35feaa0b..7f9503f9d2c 100644 --- a/Source/DafnyCore/Options/DeveloperOptionBag.cs +++ b/Source/DafnyCore/Options/DeveloperOptionBag.cs @@ -78,6 +78,7 @@ static DeveloperOptionBag() { DafnyOptions.RegisterLegacyBinding(SplitPrint, (options, f) => { options.PrintSplitFile = f; + options.PrintSplitDeclarations = true; options.ExpandFilename(options.PrintSplitFile, x => options.PrintSplitFile = x, options.LogPrefix, options.FileTimestamp); }); diff --git a/Source/DafnyCore/Options/InMemoryDirectoryInfoFromDotNet8.cs b/Source/DafnyCore/Options/InMemoryDirectoryInfoFromDotNet8.cs index 2f8bc2dcebd..139cc2f54e1 100644 --- a/Source/DafnyCore/Options/InMemoryDirectoryInfoFromDotNet8.cs +++ b/Source/DafnyCore/Options/InMemoryDirectoryInfoFromDotNet8.cs @@ -12,7 +12,7 @@ namespace DafnyCore.Options; /// https://github.com/dotnet/runtime/issues/88135 /// public class InMemoryDirectoryInfoFromDotNet8 : DirectoryInfoBase { - private static readonly char[] DirectorySeparators = new[] { Path.DirectorySeparatorChar, Path.AltDirectorySeparatorChar }; + private static readonly char[] DirectorySeparators = [Path.DirectorySeparatorChar, Path.AltDirectorySeparatorChar]; private readonly IEnumerable _files; /// @@ -76,7 +76,7 @@ public override IEnumerable EnumerateFileSystemInfos() { } else { string name = file.Substring(0, endSegment); if (!dict.TryGetValue(name, out List? list)) { - dict[name] = new List { file }; + dict[name] = [file]; } else { list.Add(file); } diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 0ecaadeae78..046612bcbbe 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -401,7 +401,7 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT public static IEnumerable<(IOrigin Group, List Tasks)> GroupOverlappingRanges(IReadOnlyList ranges) { if (!ranges.Any()) { - return Enumerable.Empty<(IOrigin Group, List Tasks)>(); + return []; } var sortedTasks = ranges.OrderBy(r => BoogieGenerator.ToDafnyToken(true, r.Token).StartToken).ToList(); @@ -421,7 +421,7 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT currentGroup.Add(currentTask); } else { groups.Add((currentGroupRange, currentGroup)); - currentGroup = new List { currentTask }; + currentGroup = [currentTask]; currentGroupRange = currentTaskRange; } } @@ -519,9 +519,9 @@ public void CancelPendingUpdates() { lastToken = lastToken.Next; } // TODO: end position doesn't take into account trailing trivia: https://github.com/dafny-lang/dafny/issues/3415 - return new TextEditContainer(new TextEdit[] { - new() {NewText = result, Range = new Range(new Position(0,0), lastToken.GetLspPosition())} - }); + return new TextEditContainer([ + new() { NewText = result, Range = new Range(new Position(0, 0), lastToken.GetLspPosition()) } + ]); } @@ -537,7 +537,7 @@ public void Dispose() { public static List GetDiagnosticsFromResult(DafnyOptions options, Uri uri, ICanVerify canVerify, IVerificationTask task, VerificationRunResult result) { var errorReporter = new ObservableErrorReporter(options, uri); - List diagnostics = new(); + List diagnostics = []; errorReporter.Updates.Subscribe(d => diagnostics.Add(d.Diagnostic)); ReportDiagnosticsInResult(options, canVerify.NavigationToken.val, BoogieGenerator.ToDafnyToken(true, task.Token), diff --git a/Source/DafnyCore/Plugin.cs b/Source/DafnyCore/Plugin.cs index 347d0eff0e5..7216a0e6bd3 100644 --- a/Source/DafnyCore/Plugin.cs +++ b/Source/DafnyCore/Plugin.cs @@ -17,7 +17,7 @@ public interface Plugin { record ErrorPlugin(string AssemblyAndArgument, Exception Exception) : Plugin { public IEnumerable GetCompilers(DafnyOptions options) { - return Enumerable.Empty(); + return []; } public IEnumerable GetRewriters(ErrorReporter reporter) { @@ -25,11 +25,11 @@ public IEnumerable GetRewriters(ErrorReporter reporter) { } public IEnumerable GetDocstringRewriters(DafnyOptions options) { - return Enumerable.Empty(); + return []; } public IEnumerable GetCompilerInstrumenters(ErrorReporter reporter) { - return Enumerable.Empty(); + return []; } class ErrorRewriter : IRewriter { diff --git a/Source/DafnyCore/Plugins/PluginConfiguration.cs b/Source/DafnyCore/Plugins/PluginConfiguration.cs index 06bacc332ad..2552d272a44 100644 --- a/Source/DafnyCore/Plugins/PluginConfiguration.cs +++ b/Source/DafnyCore/Plugins/PluginConfiguration.cs @@ -28,7 +28,7 @@ public virtual void ParseArguments(string[] args) { /// /// a list of Rewriter that are going to be used in the resolution pipeline public virtual Rewriter[] GetRewriters(ErrorReporter errorReporter) { - return Array.Empty(); + return []; } /// @@ -37,7 +37,7 @@ public virtual Rewriter[] GetRewriters(ErrorReporter errorReporter) { /// /// A list of compilers implemented by this plugin public virtual IExecutableBackend[] GetCompilers(DafnyOptions options) { - return Array.Empty(); + return []; } /// @@ -46,7 +46,7 @@ public virtual IExecutableBackend[] GetCompilers(DafnyOptions options) { /// /// A list of docstring converters implemented by this plugin, applied from left to right public virtual DocstringRewriter[] GetDocstringRewriters(DafnyOptions options) { - return Array.Empty(); + return []; } /// @@ -55,6 +55,6 @@ public virtual DocstringRewriter[] GetDocstringRewriters(DafnyOptions options) { /// /// A list of compiler instrumenters implemented by this plugin public virtual CompilerInstrumenter[] GetCompilerInstrumenters(ErrorReporter reporter) { - return Array.Empty(); + return []; } } \ No newline at end of file diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index bdf2dcbce3f..7edb3c4db58 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -230,7 +230,7 @@ private static Dictionary> continue; } - assertionsProvenUsingFact.TryAdd(factDependency, new HashSet()); + assertionsProvenUsingFact.TryAdd(factDependency, []); bool IsNotSelfReferential(AssertCmdPartialCopy assert) => !manager.ProofDependenciesById.TryGetValue(assert.Id, out var assertDependency) diff --git a/Source/DafnyCore/Resolver/AmbiguousTopLevelDecl.cs b/Source/DafnyCore/Resolver/AmbiguousTopLevelDecl.cs index f284452f6c0..b6b72417648 100644 --- a/Source/DafnyCore/Resolver/AmbiguousTopLevelDecl.cs +++ b/Source/DafnyCore/Resolver/AmbiguousTopLevelDecl.cs @@ -42,7 +42,7 @@ public override string GetDescription(DafnyOptions options) { ISet IAmbiguousThing.Pool => pool; private AmbiguousTopLevelDecl(ModuleDefinition m, string name, ISet pool) - : base(pool.First().Origin, new Name(pool.First().Origin, name), m, new List(), null, false) { + : base(pool.First().Origin, new Name(pool.First().Origin, name), m, [], null, false) { Contract.Requires(name != null); Contract.Requires(pool != null && 2 <= pool.Count); this.pool = pool; diff --git a/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs b/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs index 81a6d12420f..7ad051202e0 100644 --- a/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs +++ b/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs @@ -161,7 +161,7 @@ public static Expression FrameArrowToObjectSet(Expression e) { Type = Type.Bool }; - var attributes = new Attributes("_reads", new List(), null); + var attributes = new Attributes("_reads", [], null); return new SetComprehension(e.Origin, true, boundVarDecls, inCollection, objUse, attributes) { Type = new SetType(true, elementType) }; @@ -325,8 +325,8 @@ private static List DiscoverAllBounds_Aux_MultipleVars(List public static List DiscoverAllBounds_SingleVar(VT v, Expression expr, out bool constraintConsistsSolelyOfRangeConstraints) where VT : IVariable { expr = Expression.CreateAnd(GetImpliedTypeConstraint(v, v.Type), expr); - return DiscoverAllBounds_Aux_SingleVar(new List { v }, 0, expr, true, - new List() { null }, out constraintConsistsSolelyOfRangeConstraints); + return DiscoverAllBounds_Aux_SingleVar([v], 0, expr, true, + [null], out constraintConsistsSolelyOfRangeConstraints); } /// diff --git a/Source/DafnyCore/Resolver/ClonerButIVariablesAreKeptOnce.cs b/Source/DafnyCore/Resolver/ClonerButIVariablesAreKeptOnce.cs index 4ce95ff2879..70607a05bd5 100644 --- a/Source/DafnyCore/Resolver/ClonerButIVariablesAreKeptOnce.cs +++ b/Source/DafnyCore/Resolver/ClonerButIVariablesAreKeptOnce.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; class ClonerButIVariablesAreKeptOnce : ClonerKeepParensExpressions { - private readonly HashSet alreadyCloned = new(); + private readonly HashSet alreadyCloned = []; private VT CloneIVariableHelper(VT local, Func returnMethod) where VT : IVariable { if (!alreadyCloned.Contains(local)) { diff --git a/Source/DafnyCore/Resolver/CoCallResolution.cs b/Source/DafnyCore/Resolver/CoCallResolution.cs index 003ed4f4aa8..a4245a821a8 100644 --- a/Source/DafnyCore/Resolver/CoCallResolution.cs +++ b/Source/DafnyCore/Resolver/CoCallResolution.cs @@ -9,7 +9,7 @@ class CoCallResolution { readonly Function currentFunction; readonly bool dealsWithCodatatypes; public bool HasIntraClusterCallsInDestructiveContexts = false; - public readonly List FinalCandidates = new List(); + public readonly List FinalCandidates = []; public CoCallResolution(Function currentFunction, bool dealsWithCodatatypes) { Contract.Requires(currentFunction != null); diff --git a/Source/DafnyCore/Resolver/FillInDefaultLoopDecreasesVisitor.cs b/Source/DafnyCore/Resolver/FillInDefaultLoopDecreasesVisitor.cs index 8d65bd814a2..0c020845af1 100644 --- a/Source/DafnyCore/Resolver/FillInDefaultLoopDecreasesVisitor.cs +++ b/Source/DafnyCore/Resolver/FillInDefaultLoopDecreasesVisitor.cs @@ -142,15 +142,15 @@ private static void FillInDefaultLoopDecreases(ModuleResolver resolver, LoopStmt break; } if (bin.E0.Type.AsSetType != null) { - neutralValue = new SetDisplayExpr(bin.Origin, bin.E0.Type.AsSetType.Finite, new List()) { + neutralValue = new SetDisplayExpr(bin.Origin, bin.E0.Type.AsSetType.Finite, []) { Type = bin.E0.Type.NormalizeExpand() }; } else if (bin.E0.Type.AsMultiSetType != null) { - neutralValue = new MultiSetDisplayExpr(bin.Origin, new List()) { + neutralValue = new MultiSetDisplayExpr(bin.Origin, []) { Type = bin.E0.Type.NormalizeExpand() }; } else if (bin.E0.Type.AsSeqType != null) { - neutralValue = new SeqDisplayExpr(bin.Origin, new List()) { + neutralValue = new SeqDisplayExpr(bin.Origin, []) { Type = bin.E0.Type.NormalizeExpand() }; } else if (bin.E0.Type.IsNumericBased(Type.NumericPersuasion.Real)) { diff --git a/Source/DafnyCore/Resolver/InferDecreasesClause.cs b/Source/DafnyCore/Resolver/InferDecreasesClause.cs index 4f1337a3da6..33a9b1e8076 100644 --- a/Source/DafnyCore/Resolver/InferDecreasesClause.cs +++ b/Source/DafnyCore/Resolver/InferDecreasesClause.cs @@ -145,7 +145,7 @@ public Expression FrameToObjectSet(List fexprs) { Contract.Requires(fexprs != null); Contract.Ensures(Contract.Result() != null); - List sets = new List(); + List sets = []; List singletons = null; var idGen = new VerificationIdGenerator(); // drop wildcards altogether in the following iterations @@ -157,7 +157,7 @@ public Expression FrameToObjectSet(List fexprs) { if (eType.IsRefType) { // e represents a singleton set if (singletons == null) { - singletons = new List(); + singletons = []; } singletons.Add(e); @@ -177,10 +177,10 @@ public Expression FrameToObjectSet(List fexprs) { ResolvedOp = resolvedOpcode, Type = Type.Bool }; - var s = new SetComprehension(e.Origin, true, new List() { bvDecl }, bvInE, bv, - new Attributes("trigger", new List { bvInE }, null)) { + var s = new SetComprehension(e.Origin, true, [bvDecl], bvInE, bv, + new Attributes("trigger", [bvInE], null)) { Type = resolver.SystemModuleManager.ObjectSetType(), - Bounds = new List() { boundedPool } + Bounds = [boundedPool] }; sets.Add(s); @@ -199,7 +199,7 @@ public Expression FrameToObjectSet(List fexprs) { } if (sets.Count == 0) { - var emptySet = new SetDisplayExpr(Token.NoToken, true, new List()) { + var emptySet = new SetDisplayExpr(Token.NoToken, true, []) { Type = resolver.SystemModuleManager.ObjectSetType() }; return emptySet; diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 0aa3a165156..2538fe2ddb3 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -43,7 +43,7 @@ public partial class ModuleResolver : INewOrOldResolver { public ErrorReporter Reporter => reporter; public Scope Scope => scope; - public List TypeConstraintErrorsToBeReported { get; } = new(); + public List TypeConstraintErrorsToBeReported { get; } = []; private bool RevealedInScope(Declaration d) { Contract.Requires(d != null); @@ -67,7 +67,7 @@ public string FreshTempVarName(string prefix, ICodeContext context) { return freshTempVarName; } - public readonly HashSet revealableTypes = new(); + public readonly HashSet revealableTypes = []; //types that have been seen by the resolver - used for constraining type inference during exports public Dictionary> moduleClassMembers = new(); @@ -437,7 +437,7 @@ public void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature s // definition is. Datatype and type-synonym declarations undergo some inference from their definitions. // Such inference should not be done for provided declarations, since different views of the module // would then get different inferred properties. - decl.Attributes = new Attributes("_provided", new List(), decl.Attributes); + decl.Attributes = new Attributes("_provided", [], decl.Attributes); reporter.Info(MessageSource.Resolver, decl.Origin, "{:_provided}"); } } @@ -794,7 +794,7 @@ public void RegisterByMethod(Function f, TopLevelDeclWithMembers cl) { reads = f.Reads; if (!reads.Expressions.Any()) { reads = new Specification(); - var emptySet = new SetDisplayExpr(tok, true, new List()); + var emptySet = new SetDisplayExpr(tok, true, []); reads.Expressions.Add(new FrameExpression(tok, emptySet, null)); } } else { @@ -802,8 +802,8 @@ public void RegisterByMethod(Function f, TopLevelDeclWithMembers cl) { } var method = new Method(f.Origin.MakeAutoGenerated(), new Name(new AutoGeneratedOrigin(f.NameNode.Origin)), f.HasStaticKeyword, false, f.TypeArgs, - f.Ins, new List() { resultVar }, - f.Req, reads, new Specification(new List(), null), new List() { post }, f.Decreases, + f.Ins, [resultVar], + f.Req, reads, new Specification([], null), [post], f.Decreases, f.ByMethodBody, f.Attributes, null, true); Contract.Assert(f.ByMethodDecl == null); method.InheritVisibility(f); @@ -818,7 +818,7 @@ private ModuleSignature MakeAbstractSignature(ModuleSignature origin, string nam Contract.Requires(moduleSignatures != null); var errCount = reporter.Count(ErrorLevel.Error); - var module = new ModuleDefinition(SourceOrigin.NoToken, new Name(name + ".Abs"), new List(), ModuleKindEnum.Abstract, true, null, null, null); + var module = new ModuleDefinition(SourceOrigin.NoToken, new Name(name + ".Abs"), [], ModuleKindEnum.Abstract, true, null, null, null); module.Height = height; foreach (var kv in origin.TopLevels) { if (!(kv.Value is NonNullTypeDecl or DefaultClassDecl)) { @@ -1100,19 +1100,26 @@ void ResolveTypeParameterBounds(IOrigin tok, List typeParameters, } } - public static readonly List NativeTypes = new List() { + public static readonly List NativeTypes = [ new NativeType("byte", 0, 0x100, 8, NativeType.Selection.Byte), new NativeType("sbyte", -0x80, 0x80, 0, NativeType.Selection.SByte), new NativeType("ushort", 0, 0x1_0000, 16, NativeType.Selection.UShort), new NativeType("short", -0x8000, 0x8000, 0, NativeType.Selection.Short), new NativeType("uint", 0, 0x1_0000_0000, 32, NativeType.Selection.UInt), new NativeType("int", -0x8000_0000, 0x8000_0000, 0, NativeType.Selection.Int), - new NativeType("number", -0x1f_ffff_ffff_ffff, 0x20_0000_0000_0000, 0, NativeType.Selection.Number), // JavaScript integers - new NativeType("ulong", 0, new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000), 64, NativeType.Selection.ULong), + new NativeType("number", -0x1f_ffff_ffff_ffff, 0x20_0000_0000_0000, 0, + NativeType.Selection.Number), // JavaScript integers + new NativeType("ulong", 0, new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000), 64, + NativeType.Selection.ULong), new NativeType("long", Int64.MinValue, 0x8000_0000_0000_0000, 0, NativeType.Selection.Long), - new NativeType("udoublelong", 0, new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000), 128, NativeType.Selection.UDoubleLong), - new NativeType("doublelong", new BigInteger(-0x8000_0000_0000_0000)* new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000), new BigInteger(0x8000_0000_0000_0000)* new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000), 0, NativeType.Selection.DoubleLong), - }; + new NativeType("udoublelong", 0, + new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000) * + new BigInteger(0x1_0000_0000), 128, NativeType.Selection.UDoubleLong), + new NativeType("doublelong", + new BigInteger(-0x8000_0000_0000_0000) * new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000), + new BigInteger(0x8000_0000_0000_0000) * new BigInteger(0x1_0000_0000) * new BigInteger(0x1_0000_0000), 0, + NativeType.Selection.DoubleLong) + ]; public void ResolveTopLevelDecls_Core(List declarations, Graph datatypeDependencies, Graph codatatypeDependencies, @@ -1798,23 +1805,23 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List decl methodSel.TypeApplicationJustMember = prefixLemma.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.Origin, tp)); methodSel.Type = new InferredTypeProxy(); - var recursiveCall = new CallStmt(com.Origin, new List(), methodSel, + var recursiveCall = new CallStmt(com.Origin, [], methodSel, recursiveCallArgs.ConvertAll(e => new ActualBinding(null, e))); recursiveCall.IsGhost = prefixLemma.IsGhost; // resolve here var range = smaller; // The range will be strengthened later with the call's precondition, substituted // appropriately (which can only be done once the precondition has been resolved). - var attrs = new Attributes("_autorequires", new List(), null); + var attrs = new Attributes("_autorequires", [], null); #if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE // don't add the :_trustWellformed attribute #else - attrs = new Attributes("_trustWellformed", new List(), attrs); + attrs = new Attributes("_trustWellformed", [], attrs); #endif - attrs = new Attributes("auto_generated", new List(), attrs); - var forallBody = new BlockStmt(mainBody.Origin, new List() { recursiveCall }); + attrs = new Attributes("auto_generated", [], attrs); + var forallBody = new BlockStmt(mainBody.Origin, [recursiveCall]); var forallStmt = new ForallStmt(mainBody.Origin, bvs, attrs, range, - new List(), forallBody); - els = new BlockStmt(mainBody.Origin, new List() { forallStmt }); + [], forallBody); + els = new BlockStmt(mainBody.Origin, [forallStmt]); } else { kk = new IdentifierExpr(k.Origin, k.Name); els = null; @@ -1822,7 +1829,7 @@ private void FillInPostConditionsAndBodiesOfPrefixLemmas(List decl var kPositive = new BinaryExpr(com.Origin, BinaryExpr.Opcode.Lt, new LiteralExpr(com.Origin, 0), kk); var condBody = new IfStmt(mainBody.Origin, false, kPositive, mainBody, els); - prefixLemma.Body = new BlockStmt(mainBody.Origin, new List() { condBody }); + prefixLemma.Body = new BlockStmt(mainBody.Origin, [condBody]); } // The prefix lemma now has all its components, so it's finally time we resolve it @@ -2315,9 +2322,9 @@ private void AddRotateMember(ValuetypeDecl bitvectorTypeDecl, string name, int w }; var resultType = new BitvectorType(Options, width); var rotateMember = new SpecialFunction(SourceOrigin.NoToken, name, ProgramResolver.SystemModuleManager.SystemModule, false, false, - new List(), formals, resultType, - new List(), new Specification(), new List(), - new Specification(new List(), null), null, null, null) { + [], formals, resultType, + [], new Specification(), [], + new Specification([], null), null, null, null) { EnclosingClass = bitvectorTypeDecl }; rotateMember.AddVisibilityScope(ProgramResolver.SystemModuleManager.SystemModule.VisibilityScope, false); @@ -3192,14 +3199,15 @@ internal Type ResolvedArrayType(IOrigin tok, int dims, Type arg, ResolutionConte Contract.Requires(tok != null); Contract.Requires(1 <= dims); Contract.Requires(arg != null); - var (at, modBuiltins) = SystemModuleManager.ArrayType(tok, dims, new List { arg }, false, useClassNameType); + var (at, modBuiltins) = SystemModuleManager.ArrayType(tok, dims, [arg], false, useClassNameType); modBuiltins(SystemModuleManager); ResolveType(tok, at, resolutionContext, ResolveTypeOptionEnum.DontInfer, null); return at; } public Expression VarDotMethod(IOrigin tok, string varName, string methodName) { - return new ApplySuffix(tok, null, new ExprDotName(tok, new IdentifierExpr(tok, varName), new Name(methodName), null), new List(), Token.NoToken); + return new ApplySuffix(tok, null, new ExprDotName(tok, new IdentifierExpr(tok, varName), new Name(methodName), null), + [], Token.NoToken); } public Expression makeTemp(String prefix, AssignOrReturnStmt s, ResolutionContext resolutionContext, Expression ex) { @@ -3378,12 +3386,13 @@ public static UserDefinedType GetReceiverType(IOrigin tok, MemberDecl member) { } internal Expression VarDotFunction(IOrigin tok, string varName, string functionName) { - return new ApplySuffix(tok, null, new ExprDotName(tok, new IdentifierExpr(tok, varName), new Name(functionName), null), new List(), Token.NoToken); + return new ApplySuffix(tok, null, new ExprDotName(tok, new IdentifierExpr(tok, varName), new Name(functionName), null), + [], Token.NoToken); } // TODO search for occurrences of "new LetExpr" which could benefit from this helper internal LetExpr LetPatIn(IOrigin tok, CasePattern lhs, Expression rhs, Expression body) { - return new LetExpr(tok, new List>() { lhs }, new List() { rhs }, body, true); + return new LetExpr(tok, [lhs], [rhs], body, true); } internal LetExpr LetVarIn(IOrigin tok, string name, Type tp, Expression rhs, Expression body) { @@ -3571,7 +3580,7 @@ void ResolveCasePattern(CasePattern pat, Type sourceType, ResolutionCont } } - internal readonly List allDefaultValueExpressions = new(); + internal readonly List allDefaultValueExpressions = []; /// /// This method is called at the tail end of Pass1 of the Resolver. @@ -3772,7 +3781,7 @@ public override string Msg { return base.Msg; } - var elementTypes = RemoveAmbiguity(new object[] { rawExprElementType, rawExpectedElementType }); + var elementTypes = RemoveAmbiguity([rawExprElementType, rawExpectedElementType]); Contract.Assert(elementTypes.Length == 2); var exprElementType = elementTypes[0].ToString(); var expectedElementType = elementTypes[1].ToString(); diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index ac71d0f166d..e103a0047d3 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -20,7 +20,7 @@ namespace Microsoft.Dafny { public partial class ModuleResolver { - public List loopStack = new List(); // the enclosing loops (from which it is possible to break out) + public List loopStack = []; // the enclosing loops (from which it is possible to break out) public Scope