Fix: Ability to cast a datatype to its trait when overriding functions (

#4824)

This PR fixes #4823
There were two issues there:
- The function override check was casting to ClassLikeDecl, when it
should now be TopLevelDeclWithMembers as IndDatatypeDecl can also
override trait declarations.
- The generated axiom used to rely on types being unboxed, but since now
we might compare a trait with a datatype value, we need to ensure
correct boxing for Boogie to type-check.
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/DooFile.cs

@@ -54,7 +54,7 @@ public static ManifestData Read(TextReader reader) {
  }
 
  public void Write(TextWriter writer) {
- writer.Write(Toml.FromModel(this, new TomlModelOptions()));
+ writer.Write(Toml.FromModel(this, new TomlModelOptions()).Replace("\r\n", "\n"));
  }
  }
 
@@ -103,7 +103,9 @@ private static DooFile Read(ZipArchive archive) {
  }
 
  public DooFile(Program dafnyProgram) {
- var tw = new StringWriter();
+ var tw = new StringWriter {
+ NewLine = "\n"
+ };
  var pr = new Printer(tw, ProgramSerializationOptions, PrintModes.Serialization);
  // afterResolver is false because we don't yet have a way to safely skip resolution
  // when reading the program back into memory.
@@ -191,7 +193,7 @@ public void Write(ConcreteSyntaxTree wr) {
  var manifestWr = wr.NewFile(ManifestFileEntry);
  using var manifestWriter = new StringWriter();
  Manifest.Write(manifestWriter);
- manifestWr.Write(manifestWriter.ToString());
+ manifestWr.Write(manifestWriter.ToString().Replace("\r\n", "\n"));
 
  var programTextWr = wr.NewFile(ProgramFileEntry);
  programTextWr.Write(ProgramText);

Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy

@@ -666,7 +666,7 @@ module Std.Collections.Seq {
  Some((s[..i], s[(i + 1)..]))
  }
 
- lemma WillSplitOnDelim<T>(s: seq<T>, delim: T, prefix: seq<T>)
+ lemma {:rlimit 1000} {:vcs_split_on_every_assert} WillSplitOnDelim<T>(s: seq<T>, delim: T, prefix: seq<T>)
  requires |prefix| < |s|
  requires forall i :: 0 <= i < |prefix| ==> prefix[i] == s[i]
  requires delim !in prefix && s[|prefix|] == delim

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy

@@ -0,0 +1,11 @@
+// RUN: %baredafny verify %args --type-system-refresh --general-traits=datatype "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+trait Test<T> {
+ function Cast(t: T): Test<T>
+}
+
+datatype Impl extends Test<Impl> = ImplConstructor()
+{
+ function Cast(t: Impl): Test<Impl> { t }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4823.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/dev/news/4823.fix

@@ -0,0 +1 @@
+Ability to cast a datatype to its trait when overriding functions