Verified java

Scripts/dafny

@@ -17,7 +17,7 @@ if [ "${MY_OS:0:5}" == "MINGW" ] || [ "${MY_OS:0:6}" == "CYGWIN" ]; then
 else
     DAFNY_EXE_NAME="Dafny.dll"
 fi
-DAFNY="$DAFNY_ROOT/Binaries/$DAFNY_EXE_NAME"
+DAFNY="$DAFNY_ROOT/Binaries/net8.0/$DAFNY_EXE_NAME"
 if [[ ! -e "$DAFNY" ]]; then
     echo "Error: $DAFNY_EXE_NAME not found at $DAFNY."
     exit 1

Source/AutoExtern.Test/AutoExtern.Test.csproj

@@ -2,7 +2,7 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
     <IsPackable>false</IsPackable>

Source/AutoExtern.Test/Minimal/Library.csproj

@@ -1,7 +1,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
   <PropertyGroup>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
   </PropertyGroup>

Source/AutoExtern.Test/Tutorial/ClientApp/ClientApp.csproj

@@ -2,7 +2,7 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <NoWarn>CS3021; CS0162</NoWarn>
     <!-- <Nullable>enable</Nullable> -->

Source/AutoExtern.Test/Tutorial/Library/Library.csproj

@@ -1,7 +1,7 @@
 <Project Sdk="Microsoft.NET.Sdk">
 
   <PropertyGroup>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
   </PropertyGroup>

Source/AutoExtern/AutoExtern.csproj

@@ -2,7 +2,7 @@
 
   <PropertyGroup>
     <OutputType>Exe</OutputType>
-    <TargetFramework>net6.0</TargetFramework>
+    <TargetFramework>net8.0</TargetFramework>
     <ImplicitUsings>enable</ImplicitUsings>
     <Nullable>enable</Nullable>
     <GenerateAssemblyInfo>false</GenerateAssemblyInfo>

Source/CompilerBuilder.Test/CompilerBuilder.Test.csproj

@@ -0,0 +1,27 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+    <PropertyGroup>
+        <TargetFramework>net8.0</TargetFramework>
+        <ImplicitUsings>enable</ImplicitUsings>
+        <Nullable>enable</Nullable>
+
+        <IsPackable>false</IsPackable>
+        <IsTestProject>true</IsTestProject>
+    </PropertyGroup>
+
+    <ItemGroup>
+        <PackageReference Include="coverlet.collector" Version="6.0.0"/>
+        <PackageReference Include="Microsoft.NET.Test.Sdk" Version="17.8.0"/>
+        <PackageReference Include="xunit" Version="2.5.3"/>
+        <PackageReference Include="xunit.runner.visualstudio" Version="2.5.3"/>
+    </ItemGroup>
+
+    <ItemGroup>
+        <Using Include="Xunit"/>
+    </ItemGroup>
+
+    <ItemGroup>
+      <ProjectReference Include="..\CompilerBuilder\CompilerBuilder.csproj" />
+    </ItemGroup>
+
+</Project>

Source/CompilerBuilder.Test/TestGrammars.cs

@@ -0,0 +1,117 @@
+using CompilerBuilder.Grammars;
+
+namespace CompilerBuilder.Test;
+
+using static GrammarBuilder;
+
+public class TestGrammars {
+
+  [Fact]
+  public void TestNumber() {
+    var number = Number;
+    var parsed = number.ToParser().Parse("123124").Success!.Value;
+    Assert.Equal(123124, parsed);
+  }
+
+  [Fact]
+  public void TestIdentifier() {
+    var number = Identifier;
+    var parsed = number.ToParser().Parse("abcdefg").Success!.Value;
+    Assert.Equal("abcdefg", parsed);
+  }
+
+  [Fact]
+  public void TestKeyword() {
+    var parser = Keyword("hello").Then(Constant(true));
+    var parsed = parser.ToParser().Parse("hello").Success!.Value;
+    Assert.True(parsed);
+
+    var byeResult = parser.ToParser().Parse("bye");
+    Assert.Contains("Expected", byeResult.Failure!.Message);
+  }
+
+  [Fact]
+  public void TestChoice() {
+    var numberOrIdentifier = Number.UpCast<int, object>().Or(Identifier.UpCast<string, object>());
+    Assert.Equal(123124, numberOrIdentifier.ToParser().Parse("123124").Success!.Value);
+    Assert.Equal("abcefg", numberOrIdentifier.ToParser().Parse("abcefg").Success!.Value);
+    Assert.Null(numberOrIdentifier.ToParser().Parse("!@!@$#").Success);
+  }
+
+  record Person {
+    public int Age;
+    public string Name;
+  }
+
+  [Fact]
+  public void TestSequence() {
+    var person =
+      Constructor<Person>().
+        Then(Number, (p) => p.Age).
+        Then(Identifier, (p) => p.Name);
+    var result = person.ToParser().Parse("123124Jan");
+    Assert.Equal(123124, result.Success!.Value.Age);
+    Assert.Equal("Jan", result.Success!.Value.Name);
+    Assert.Null(person.ToParser().Parse("1231").Success);
+  }
+
+  [Fact]
+  public void TestMany() {
+    var person =
+      Constructor<Person>().
+        Then(Number, (p) => p.Age).
+        Then(Identifier, (p) => p.Name);
+    var persons = person.Many();
+    var parser = persons.ToParser();
+    var goodResult = parser.Parse("123124Jan12313Henk12Remy");
+    Assert.Equal(3, goodResult.Success!.Value.Count());
+    Assert.Equal("Remy", goodResult.Success!.Value.ElementAt(2).Name);
+    var badResult = parser.Parse("123124Jan12313Henk12");
+    Assert.Null(badResult.Success);
+  }
+
+  [Fact]
+  public void LeftRecursive() {
+    var parser = Recursive<int>(self => Number.Or(self.Then("^")), "LeftRecursiveTest");
+    var result = parser.ToParser().Parse("13^^^");
+    Assert.Equal(13, result.Success!.Value);
+  }
+
+  record PersonWithTrivia {
+    public int Age;
+    public string Name;
+    public List<string> Trivia = new();
+
+    public PersonWithTrivia() {
+      Age = 0;
+      Name = null;
+    }
+  }
+
+  [Fact]
+  public void ManualTrivia() {
+    var trivia = Comments.SlashSlashLineComment().Or(Whitespace).Or(Comments.BlockComment()).Many();
+    var person =
+      Constructor<PersonWithTrivia>().
+        Then(Number, (p) => p.Age).
+        Then(trivia, (p) => p.Trivia).
+        Then(Identifier, (p) => p.Name);
+    var input = "123  Remy";
+    var result = person.ToParser().Parse(input);
+    Assert.NotNull(result.Success);
+    Assert.Equal("  ", result.Success?.Value.Trivia[0]);
+
+    var input2 = @"123// line comment
+
+// another linecomment
+/** block 
+
+comment
+*/
+Remy";
+    var result2 = person.ToParser().Parse(input2);
+    Assert.NotNull(result2.Success);
+    Assert.Equal("// another linecomment\n", result2.Success?.Value.Trivia[2]);
+  }
+
+}

Source/CompilerBuilder.Test/TestParsing.cs

@@ -0,0 +1,133 @@
+namespace CompilerBuilder.Test;
+
+using static ParserBuilder;
+
+public class TestParsing {
+
+  [Fact]
+  public void TestNumber() {
+    var number = Number;
+    var parsed = number.Parse("123124").ForceSuccess.Value;
+    Assert.Equal(123124, parsed);
+  }
+
+  [Fact]
+  public void TestChar() {
+    var parsed = CharInSingleQuotes.Parse("'d'").ForceSuccess.Value;
+    Assert.Equal("d", parsed);
+  }
+
+  [Fact]
+  public void TestIdentifier() {
+    var number = Identifier;
+    var result = number.Parse("abcdefg");
+    var parsed = result.ForceSuccess.Value;
+    Assert.Equal("abcdefg", parsed);
+  }
+
+  [Fact]
+  public void TestKeyword() {
+    var parser = Keyword("hello").Then(Constant(true));
+    var parsed = parser.Parse("hello").Success!.Value;
+    Assert.True(parsed);
+
+    var byeResult = parser.Parse("bye");
+    Assert.Contains("Expected", byeResult.Failure!.Message);
+  }
+
+  [Fact]
+  public void TestChoice() {
+    var numberOrIdentifier = Fail<object>("a number or identifier").
+      Or(Number.Map(i => (object)i).Or(Identifier.Map(s => (object)s)));
+    Assert.Equal(123124, numberOrIdentifier.Parse("123124").Success!.Value);
+    Assert.Equal("abcefg", numberOrIdentifier.Parse("abcefg").Success!.Value);
+    Assert.Null(numberOrIdentifier.Parse("!@!@$#").Success);
+
+    Assert.Equal("'!@#!@' is not the end of the text", numberOrIdentifier.Parse("123124!@#!@#").Failure!.Message);
+    Assert.Equal("'!@#!@' is not a number or identifier", numberOrIdentifier.Parse("!@#!@#").Failure!.Message);
+  }
+
+  record Person {
+    public int Age;
+    public string Name;
+  }
+
+  [Fact]
+  public void TestSequence() {
+    var person =
+      Value(() => new Person()).
+        Then(Number, (p, v) => p.Age = v).
+        Then(Identifier, (p, v) => p.Name = v);
+    var result = person.Parse("123124Jan");
+    Assert.Equal(123124, result.Success!.Value.Age);
+    Assert.Equal("Jan", result.Success!.Value.Name);
+    Assert.Null(person.Parse("1231").Success);
+
+    Assert.Equal("'!@#!@' is not an identifier", person.Parse("123124!@#!@#").Failure!.Message);
+  }
+
+  [Fact]
+  public void TestMany() {
+    var person =
+      Value(() => new Person()).
+        Then("^").
+        Then(Number, (p, v) => p.Age = v).
+        Then(Identifier, (p, v) => p.Name = v);
+    var persons = person.Many();
+    var goodResult = persons.Parse("^123124Jan^12313Henk^12Remy");
+    Assert.Equal(3, goodResult.ForceSuccess.Value.Count);
+    Assert.Equal("Remy", goodResult.ForceSuccess.Value[2].Name);
+    var badResult = persons.Parse("^123124Jan^12313Henk^12");
+    Assert.Null(badResult.Success);
+  }
+
+  [Fact]
+  public void LeftRecursive() {
+    var parser = Recursive<int>(self => Number.Or(self.Then("^")), "LeftRecursiveTest");
+    var result = parser.Parse("13^^^");
+    Assert.Equal(13, result.ForceSuccess.Value);
+  }
+
+  class PersonWithTrivia {
+    public int Age;
+    public string Name;
+    public List<string> Trivia = new();
+
+    public PersonWithTrivia() {
+      Age = 0;
+      Name = null;
+    }
+  }
+
+  [Fact]
+  public void ManualTrivia() {
+    var trivia = SlashSlashLineComment.Or(Whitespace).Many();
+    var person =
+      Value(() => new PersonWithTrivia()).
+        Then(Number, (p, v) => p.Age = v).
+        Then(trivia, (p, newTrivia) => p.Trivia.AddRange(newTrivia)).
+        Then(Identifier, (p, v) => p.Name = v);
+    var input = "123  Remy";
+    var result = person.Parse(input);
+    Assert.NotNull(result.Success);
+    Assert.Equal(123, result.Success?.Value.Age);
+    Assert.Equal("  ", result.Success?.Value.Trivia[0]);
+
+    var input2 = @"123// line comment
+
+// another linecomment
+Remy";
+    var result2 = person.Parse(input2);
+    Assert.NotNull(result2.Success);
+    Assert.Equal("// another linecomment\n", result2.Success?.Value.Trivia[2]);
+  }
+
+  // There were a lot of issues in the following that this file should test, but did not.
+  // Things like nested recursive things
+  // And not dropping intermediate results when growing a seed.
+  // class Div {
+  //   int Foo(int x) {
+  //     return 3 / x;
+  //   }
+  // }
+}

Source/CompilerBuilder.Test/TestPrinting.cs

@@ -0,0 +1,6 @@
+namespace CompilerBuilder.Test;
+
+
+public class TestPrinting {
+
+}

Source/CompilerBuilder/CompilerBuilder.csproj

@@ -0,0 +1,15 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+    <PropertyGroup>
+        <OutputType>Library</OutputType>
+        <TargetFramework>net8.0</TargetFramework>
+        <ImplicitUsings>enable</ImplicitUsings>
+        <Nullable>enable</Nullable>
+    </PropertyGroup>
+
+    <ItemGroup>
+        <PackageReference Include="Boogie.ExecutionEngine" Version="3.2.2" />
+        <PackageReference Include="Microsoft.Extensions.FileSystemGlobbing" Version="5.0.0" />
+    </ItemGroup>
+
+</Project>

Source/DafnyCore/Rewriters/AutoGeneratedToken.cs → Source/CompilerBuilder/Generic/AutoGeneratedToken.cs

@@ -26,10 +26,6 @@ public static bool Is(IToken tok) {
     return false;
   }
 
-  public static Expression WrapExpression(Expression expr) {
-    return Expression.CreateParensExpression(new AutoGeneratedToken(expr.tok), expr);
-  }
-
   public override IToken WithVal(string newVal) {
     return new AutoGeneratedToken(WrappedToken.WithVal(newVal));
   }