feat!: Switch --function-syntax, --quantifier-syntax, and --unicode-c…

…har to Dafny 4.0 defaults (#3623)

Partially addresses #2548 (more default switches still coming).

CI is not fully enabled on the target branch yet.

Co-authored-by: davidcok <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>

.github/workflows/msbuild.yml

@@ -3,9 +3,14 @@ name: Build and Test
 on:
  workflow_dispatch:
  pull_request:
- branches: [ master ]
+ branches: [ master , main-4.0 ]
  push:
 
+concurrency:
+ group: build-${{ github.event.pull_request.number || github.ref }}
+ cancel-in-progress: true
+
+
 env:
  dotnet-version: 6.0.x # SDK Version for building Dafny
 

Source/AutoExtern.Test/Tutorial/ClientApp/LibraryModel.dfy.template

@@ -7,7 +7,7 @@ module {:extern "App"} {:compile false} App {}
 module {:compile false} {:extern "ExactArithmetic"} App.ExactArithmetic {
  import opened System
  type {:compile false} {:extern} Decimal {
- function method ToStr(): (s: System.String)
+ function ToStr(): (s: System.String)
  }
 }
 

Source/AutoExtern/Program.cs

@@ -216,7 +216,7 @@ internal class Enum : PrettyPrintable {
  var nm = Name.OfSyntax(syntax, model);
  PpBlockOpen(wr, indent, "class", nm, null, null, null);
  PpChildren(wr, indent, Members);
- PpChild(wr, indent, $"function method {{:extern}} Equals(other: {nm.DafnyId}): bool");
+ PpChild(wr, indent, $"function {{:extern}} Equals(other: {nm.DafnyId}): bool");
  PpBlockClose(wr, indent);
  }
 }

Source/DafnyCore/AST/Function.cs

@@ -280,9 +280,9 @@ public enum CoCallClusterInvolvement {
  public virtual bool ReadsHeap { get { return Reads.Count != 0; } }
 
  public static readonly Option<string> FunctionSyntaxOption = new("--function-syntax",
- () => "3",
+ () => "4",
  @"
-The syntax for functions is changing from Dafny version 3 to version 4. This switch gives early access to the new syntax, and also provides a mode to help with migration.
+The syntax for functions changed from Dafny version 3 to version 4. This switch controls access to the new syntax, and also provides a mode to help with migration.
 
 3 - Compiled functions are written `function method` and `predicate method`. Ghost functions are written `function` and `predicate`.
 4 - Compiled functions are written `function` and `predicate`. Ghost functions are written `ghost function` and `ghost predicate`.

Source/DafnyCore/DafnyOptions.cs

@@ -63,8 +63,8 @@ public class DafnyOptions : Bpl.CommandLineOptions {
 
  RegisterLegacyUi(CommonOptionBag.Output, ParseFileInfo, "Compilation options", "out");
  RegisterLegacyUi(CommonOptionBag.UnicodeCharacters, ParseBoolean, "Language feature selection", "unicodeChar", @"
-0 (default) - The char type represents any UTF-16 code unit.
-1 - The char type represents any Unicode scalar value.".TrimStart());
+0 - The char type represents any UTF-16 code unit.
+1 (default) - The char type represents any Unicode scalar value.".TrimStart());
  RegisterLegacyUi(CommonOptionBag.Plugin, ParseStringElement, "Plugins", defaultValue: new List<string>());
  RegisterLegacyUi(CommonOptionBag.Prelude, ParseFileInfo, "Input configuration", "dprelude");
 
@@ -294,8 +294,8 @@ public enum ContractTestingMode {
  public bool PrintFunctionCallGraph = false;
  public bool WarnShadowing = false;
  public int DefiniteAssignmentLevel = 1; // [0..2] 2 and 3 have the same effect, 4 turns off an array initialisation check, unless --enforce-determinism is used.
- public FunctionSyntaxOptions FunctionSyntax = FunctionSyntaxOptions.Version3;
- public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version3;
+ public FunctionSyntaxOptions FunctionSyntax = FunctionSyntaxOptions.Version4;
+ public QuantifierSyntaxOptions QuantifierSyntax = QuantifierSyntaxOptions.Version4;
  public HashSet<string> LibraryFiles { get; set; } = new();
  public ContractTestingMode TestContracts = ContractTestingMode.None;
 
@@ -1261,10 +1261,10 @@ public enum IncludesModes {
  4. This switch gives early access to the new syntax, and also
  provides a mode to help with migration.
 
- 3 (default) - Compiled functions are written `function method` and
+ 3 - Compiled functions are written `function method` and
  `predicate method`. Ghost functions are written `function` and
  `predicate`.
- 4 - Compiled functions are written `function` and `predicate`. Ghost
+ 4 (default) - Compiled functions are written `function` and `predicate`. Ghost
  functions are written `ghost function` and `ghost predicate`.
  migration3to4 - Compiled functions are written `function method` and
  `predicate method`. Ghost functions are written `ghost function`
@@ -1294,10 +1294,10 @@ public enum IncludesModes {
  <Range>) are allowed. This switch gives early access to the new
  syntax.
 
- 3 (default) - Ranges are only allowed after all quantified variables
+ 3 - Ranges are only allowed after all quantified variables
  are declared. (e.g. set x, y | 0 <= x < |s| && y in s[x] && 0 <=
  y :: y)
- 4 - Ranges are allowed after each quantified variable declaration.
+ 4 (default) - Ranges are allowed after each quantified variable declaration.
  (e.g. set x | 0 <= x < |s|, y <- s[x] | 0 <= y :: y)
 
  Note that quantifier variable domains (<- <Domain>) are available in

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -106,7 +106,7 @@ public class CommonOptionBag {
  }
  }
 
- return QuantifierSyntaxOptions.Version3;
+ return QuantifierSyntaxOptions.Version4;
  }, true, @"
 The syntax for quantification domains is changing from Dafny version 3 to version 4, more specifically where quantifier ranges (|
 <Range>) are allowed. This switch gives early access to the new syntax.
@@ -133,7 +133,7 @@ public class CommonOptionBag {
  ArgumentHelpName = "language",
  };
 
- public static readonly Option<bool> UnicodeCharacters = new("--unicode-char", () => false,
+ public static readonly Option<bool> UnicodeCharacters = new("--unicode-char", () => true,
  @"
 false - The char type represents any UTF-16 code unit.
 true - The char type represents any Unicode scalar value.".TrimStart()) {

Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs

@@ -64,7 +64,7 @@ public class SimpleLinearVerificationGutterStatusTester : LinearVerificationGutt
  | | | I I | | | I I | | | :
  . | | | I I | | | I I | | | :ghost const maxId := 200;
  | | | I I | | | I I | | | :
- . | | | I I | | | I I | | | :predicate isIssueIdValid(issueId: int) {
+ . | | | I I | | | I I | | | :ghost predicate isIssueIdValid(issueId: int) {
  . | | | I I | | | I I | | | : 101 <= issueId < maxId
  . | | | I I | | | I I | | | :}
  | | | I I | | | I I | | | :
@@ -177,7 +177,7 @@ public class SimpleLinearVerificationGutterStatusTester : LinearVerificationGutt
  . S [O][O]: ensures test2(a - b)
  . S [S][ ]: ensures true
  | | | :
- . | | | :predicate method test2(x: nat) {
+ . | | | :predicate test2(x: nat) {
  . | | | : true
  . | | | :}");
  }
@@ -189,14 +189,14 @@ public class SimpleLinearVerificationGutterStatusTester : LinearVerificationGutt
  . | | | :method test() {
  . | | | :}
  | | | :
- . S [S][ ]:function method {:extern} test4(a: nat, b: nat): nat
+ . S [S][ ]:function {:extern} test4(a: nat, b: nat): nat
  . S [S][ ]: ensures true
  . S [=][=]: ensures test2(a - b)
  . S [S][ ]: ensures true
  . S [O][O]: ensures test2(a - b)
  . S [S][ ]: ensures true
  | | | :
- . | | | :predicate method test2(x: nat) {
+ . | | | :predicate test2(x: nat) {
  . | | | : true
  . | | | :}");
  }

Source/DafnyLanguageServer.Test/Lookup/DefinitionTest.cs

@@ -57,7 +57,7 @@ match this
  static method create() returns (ret: A)
 }
 datatype Result<T, E> = Ok(value: T) | Err({>1:error<}: E) {
- function method PropagateFailure<U>(): Result<U, E>
+ function PropagateFailure<U>(): Result<U, E>
  requires Err?
  {
  Err(this.er><ror)
@@ -87,7 +87,7 @@ static method create() returns (ret: A)
  var source = @"
 module [>Zaz<] {
  trait [>E<] {
- static function method [>Foo<](): E
+ static function [>Foo<](): E
  }
 }
 
@@ -218,7 +218,7 @@ class A {
 
  constructor() {}
 
- function method [>GetX<](): int
+ function [>GetX<](): int
  reads this`><x
  {
  this.x
@@ -312,7 +312,7 @@ class A {
  var definition = (await RequestDefinition(documentItem, (4, 13)).AsTask()).Single();
  var location = definition.Location;
  Assert.AreEqual(DocumentUri.FromFileSystemPath(Path.Combine(Directory.GetCurrentDirectory(), "Lookup/TestFiles/foreign.dfy")), location.Uri);
- Assert.AreEqual(new Range((5, 18), (5, 22)), location.Range);
+ Assert.AreEqual(new Range((5, 11), (5, 15)), location.Range);
  }
 
  [TestMethod]

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

@@ -113,7 +113,7 @@ public class HoverTest : ClientBasedLanguageServerTest {
  }
 }
 
-function method F(dt: DT): int {
+function F(dt: DT): int {
  match dt {
  case C => 0
  case A | B => var x := (y => y)(1); assert x == 1; 0
@@ -122,7 +122,7 @@ public class HoverTest : ClientBasedLanguageServerTest {
  ^[```dafny\ny: int\n```]
  }
 }
-function method F2(dt: DT): int {
+function F2(dt: DT): int {
  match dt {
  case C => 0
  case _ => var x := (y => y)(1); assert x == 1; 0
@@ -394,7 +394,7 @@ class Sub extends Base {}
  [TestMethod]
  public async Task HoveringForAllBoundVarInPredicateReturnsBoundVarInferredType() {
  await AssertHover(@"
-predicate f(i: int) {
+ghost predicate f(i: int) {
  forall j :: j + i == i + j
  ^[```dafny\nj: int\n```]
  ^[```dafny\nj: int\n```]
@@ -419,7 +419,7 @@ predicate even(n: nat)
  [TestMethod]
  public async Task HoveringLetInReturnsInferredType() {
  await AssertHover(@"
-function method test(n: nat): nat {
+function test(n: nat): nat {
  var i := n * 2;
  ^[```dafny\ni: int\n```]
  ^[```dafny\nn: nat\n```]
@@ -456,7 +456,7 @@ function f(i: int): (r: int)
  public async Task HoverIngInferredVariable() {
  await AssertHover(@"
 datatype Pos = Pos(line: int)
-function method f(i: int): Pos {
+function f(i: int): Pos {
  if i <= 3 then Pos(i)
  else
  var r := f(i - 2);

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -232,7 +232,7 @@ method Test2(i: int)
  [TestMethod, Timeout(MaxTestExecutionTimeMs)]
  public async Task DoNotExtendPastExpressions2() {
  var documentItem = await GetDocumentItem(@"
-function method Id<T>(t: T): T { t }
+function Id<T>(t: T): T { t }
 datatype Test = Test(i: int)
 {
  method Tester(other: Test) {
@@ -271,7 +271,7 @@ method Test2(i: int)
  ((this.Tester? || this.Tester2?) && this.next.Valid()) || (this.Test3? && !this.next.Valid())
  }
 
- function method apply(): int requires Valid() {
+ function apply(): int requires Valid() {
  2
  }
  static method Test(c: ValidTester) {
@@ -308,7 +308,7 @@ method Test2(i: int)
  assert Id(other).CanAct();
  }
 }
-function method Id<T>(t: T): T { t }
+function Id<T>(t: T): T { t }
 
 ", "testfile2.dfy");
  await AssertHoverMatches(documentItem, (9, 20),
@@ -337,7 +337,7 @@ method Test2(i: int)
  i == j || -i == j
 }
 
-function method Toast(i: int): int
+function Toast(i: int): int
  requires P(i)
 
 method Test(i: int) returns (j: nat)
@@ -375,7 +375,7 @@ ensures Q(i, j)
  | Cons(head: int, tail: X)
  | Nil
  {
- predicate method Valid() {
+ predicate Valid() {
  this.Cons? && tail.Valid()
  }
  }

Source/DafnyLanguageServer.Test/Lookup/TestFiles/foreign.dfy

@@ -3,7 +3,7 @@
 
  constructor() {}
 
- function method GetX(): int
+ function GetX(): int
  reads this
  {
  this.x

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -98,7 +98,7 @@ then bullspec(s[1..],u[1..])
  i <= 0
 }
 
-function method Call(i: int): int
+function Call(i: int): int
  requires P(i)
 
 method Test(i: int) returns (j: int)
@@ -171,7 +171,7 @@ lemma Randomlemma()
  [TestMethod]
  public async Task NoCrashWhenPressingEnterAfterSelectingAllTextAndInputtingText() {
  var source = @"
-predicate method {:opaque} m() {
+predicate {:opaque} m() {
  true
 }
 ".TrimStart();
@@ -191,7 +191,7 @@ lemma Randomlemma()
  [TestMethod]
  public async Task OpeningOpaqueFunctionWorks() {
  var source = @"
-predicate method {:opaque} m() {
+predicate {:opaque} m() {
  true
 }".TrimStart();
  var documentItem = CreateTestDocument(source);
@@ -785,7 +785,7 @@ requires IsFailure()
  [TestMethod]
  public async Task OpeningDocumentWithTimeoutReportsTimeoutDiagnostic() {
  var source = @"
-function method {:unroll 100} Ack(m: nat, n: nat): nat
+function {:unroll 100} Ack(m: nat, n: nat): nat
  decreases m, n
 {
  if m == 0 then
@@ -855,7 +855,7 @@ method other(i: int, j: int)
 // ^^^^^^^^^^^
 }
 
-function method other(i: int, j: int): int
+function other(i: int, j: int): int
  requires i < j {
  2
 }

Source/DafnyLanguageServer.Test/Synchronization/TextReplacementTest.cs

@@ -244,8 +244,8 @@ reads this
 
  [TestMethod]
  public async Task ReplaceCompleteDocumentContent() {
- var source = "function GetConstant(): int { 1 }";
- var change = "function method ReturnSame(x: int): int { x }";
+ var source = "ghost function GetConstant(): int { 1 }";
+ var change = "function ReturnSame(x: int): int { x }";
  var documentItem = CreateTestDocument(source);
  await Client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
  await ApplyChangeAndWaitCompletionAsync(documentItem, null, change);

Source/DafnyLanguageServer.Test/Various/CancelVerificationTest.cs

@@ -57,21 +57,21 @@ public class CancelVerificationTest : ClientBasedLanguageServerTest {
  var documentItem = CreateTestDocument(SlowToVerify2);
  client.OpenDocument(documentItem);
  Assert.IsTrue(await client.RunSymbolVerification(documentItem, new Position(11, 23), CancellationToken));
- Assert.IsTrue(await client.RunSymbolVerification(documentItem, new Position(0, 30), CancellationToken));
+ Assert.IsTrue(await client.RunSymbolVerification(documentItem, new Position(0, 23), CancellationToken));
 
  await WaitForStatus(new Range(11, 23, 11, 27), PublishedVerificationStatus.Running, CancellationToken);
 
  // Should cancel the previous request.
  ApplyChange(ref documentItem, new Range((12, 9), (12, 23)), "true");
 
  Assert.IsTrue(await client.RunSymbolVerification(documentItem, new Position(11, 23), CancellationToken));
- Assert.IsTrue(await client.RunSymbolVerification(documentItem, new Position(0, 30), CancellationToken));
+ Assert.IsTrue(await client.RunSymbolVerification(documentItem, new Position(0, 23), CancellationToken));
  await AssertNothingIsQueued(documentItem);
  }
 
  private static string SlowToVerify2 =>
  @"
-function method {:unroll 100} Ack(m: nat, n: nat): nat
+function {:unroll 100} Ack(m: nat, n: nat): nat
  decreases m, n
 {
  if m == 0 then

Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs

@@ -1027,7 +1027,7 @@ class Cla__ss {
 
  newtype nat64 = x | 0 <= x <= NAT64_MAX
 
- function method plus(a: nat64, b: nat64): nat64 {
+ function plus(a: nat64, b: nat64): nat64 {
  a + b
  }".TrimStart();
  var documentItem = CreateTestDocument(source);