Skip to content

Commit

Permalink
format standard library
Browse files Browse the repository at this point in the history
  • Loading branch information
@josecorella
josecorella committed Aug 26, 2024
1 parent 03c3511 commit 4c5f9a3
Show file tree
Hide file tree
Showing 2 changed files with 95 additions and 63 deletions.
44 changes: 29 additions & 15 deletions StandardLibrary/runtimes/java/src/main/java/String_Compile/__default.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,36 +2,50 @@

/**
* This is a thunk for the actual Dafny-generated StandardLibrary_mString_Compile.__default class.
*
*
* The module names generated for Java changed between Dafny 4.2 and 4.7,
* and although `--legacy-module-names` mostly retains the old names,
* StandardLibrary.String was previously compiled to String_Compile instead of the expected
* StandardLibrary_mString_Compile because of a bug,
* and it would have been very difficult to reproduce the exact bug behavior with `--legacy-module-names`.
*
*
* Instead we just create an "alias" for this case.
*/
public class __default {
public __default() {
}
public static dafny.DafnySequence<? extends java.math.BigInteger> Int2Digits(java.math.BigInteger n, java.math.BigInteger base)
{

public __default() {}

public static dafny.DafnySequence<? extends java.math.BigInteger> Int2Digits(
java.math.BigInteger n,
java.math.BigInteger base
) {
return StandardLibrary_mString_Compile.__default.Int2Digits(n, base);
}
public static dafny.DafnySequence<? extends Character> Digits2String(dafny.DafnySequence<? extends java.math.BigInteger> digits, dafny.DafnySequence<? extends Character> chars)
{
return StandardLibrary_mString_Compile.__default.Digits2String(digits, chars);

public static dafny.DafnySequence<? extends Character> Digits2String(
dafny.DafnySequence<? extends java.math.BigInteger> digits,
dafny.DafnySequence<? extends Character> chars
) {
return StandardLibrary_mString_Compile.__default.Digits2String(
digits,
chars
);
}
public static dafny.DafnySequence<? extends Character> Int2String(java.math.BigInteger n, dafny.DafnySequence<? extends Character> chars)
{

public static dafny.DafnySequence<? extends Character> Int2String(
java.math.BigInteger n,
dafny.DafnySequence<? extends Character> chars
) {
return StandardLibrary_mString_Compile.__default.Int2String(n, chars);
}
public static dafny.DafnySequence<? extends Character> Base10Int2String(java.math.BigInteger n)
{

public static dafny.DafnySequence<? extends Character> Base10Int2String(
java.math.BigInteger n
) {
return StandardLibrary_mString_Compile.__default.Base10Int2String(n);
}
public static dafny.DafnySequence<? extends Character> Base10()
{

public static dafny.DafnySequence<? extends Character> Base10() {
return StandardLibrary_mString_Compile.__default.Base10();
}
}
114 changes: 66 additions & 48 deletions StandardLibrary/runtimes/net/Dafny47-Patch.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,55 +10,73 @@
*
* Instead we just create an "alias" for this case.
*/
namespace String_Compile {
namespace String_Compile
{

public partial class __default {
public static Dafny.ISequence<BigInteger> Int2Digits(BigInteger n, BigInteger @base)
public partial class __default
{
Dafny.ISequence<BigInteger> _208___accumulator = Dafny.Sequence<BigInteger>.FromElements();
TAIL_CALL_START: ;
if ((n).Sign == 0) {
return Dafny.Sequence<BigInteger>.Concat(Dafny.Sequence<BigInteger>.FromElements(), _208___accumulator);
} else {
_208___accumulator = Dafny.Sequence<BigInteger>.Concat(Dafny.Sequence<BigInteger>.FromElements(Dafny.Helpers.EuclideanModulus(n, @base)), _208___accumulator);
BigInteger _in38 = Dafny.Helpers.EuclideanDivision(n, @base);
BigInteger _in39 = @base;
n = _in38;
@base = _in39;
goto TAIL_CALL_START;
}
public static Dafny.ISequence<BigInteger> Int2Digits(BigInteger n, BigInteger @base)
{
Dafny.ISequence<BigInteger> _208___accumulator = Dafny.Sequence<BigInteger>.FromElements();
TAIL_CALL_START:;
if ((n).Sign == 0)
{
return Dafny.Sequence<BigInteger>.Concat(Dafny.Sequence<BigInteger>.FromElements(), _208___accumulator);
}
else
{
_208___accumulator = Dafny.Sequence<BigInteger>.Concat(Dafny.Sequence<BigInteger>.FromElements(Dafny.Helpers.EuclideanModulus(n, @base)), _208___accumulator);
BigInteger _in38 = Dafny.Helpers.EuclideanDivision(n, @base);
BigInteger _in39 = @base;
n = _in38;
@base = _in39;
goto TAIL_CALL_START;
}
}
public static Dafny.ISequence<char> Digits2String(Dafny.ISequence<BigInteger> digits, Dafny.ISequence<char> chars)
{
Dafny.ISequence<char> _209___accumulator = Dafny.Sequence<char>.FromElements();
TAIL_CALL_START:;
if ((digits).Equals(Dafny.Sequence<BigInteger>.FromElements()))
{
return Dafny.Sequence<char>.Concat(_209___accumulator, Dafny.Sequence<char>.FromString(""));
}
else
{
_209___accumulator = Dafny.Sequence<char>.Concat(_209___accumulator, Dafny.Sequence<char>.FromElements((chars).Select((digits).Select(BigInteger.Zero))));
Dafny.ISequence<BigInteger> _in40 = (digits).Drop(BigInteger.One);
Dafny.ISequence<char> _in41 = chars;
digits = _in40;
chars = _in41;
goto TAIL_CALL_START;
}
}
public static Dafny.ISequence<char> Int2String(BigInteger n, Dafny.ISequence<char> chars)
{
BigInteger _210_base = new BigInteger((chars).Count);
if ((n).Sign == 0)
{
return Dafny.Sequence<char>.FromString("0");
}
else if ((n).Sign == 1)
{
return String_Compile.__default.Digits2String(String_Compile.__default.Int2Digits(n, _210_base), chars);
}
else
{
return Dafny.Sequence<char>.Concat(Dafny.Sequence<char>.FromString("-"), String_Compile.__default.Digits2String(String_Compile.__default.Int2Digits((BigInteger.Zero) - (n), _210_base), chars));
}
}
public static Dafny.ISequence<char> Base10Int2String(BigInteger n)
{
return String_Compile.__default.Int2String(n, String_Compile.__default.Base10);
}
public static Dafny.ISequence<char> Base10
{
get
{
return Dafny.Sequence<char>.FromElements('0', '1', '2', '3', '4', '5', '6', '7', '8', '9');
}
}
}
public static Dafny.ISequence<char> Digits2String(Dafny.ISequence<BigInteger> digits, Dafny.ISequence<char> chars)
{
Dafny.ISequence<char> _209___accumulator = Dafny.Sequence<char>.FromElements();
TAIL_CALL_START: ;
if ((digits).Equals(Dafny.Sequence<BigInteger>.FromElements())) {
return Dafny.Sequence<char>.Concat(_209___accumulator, Dafny.Sequence<char>.FromString(""));
} else {
_209___accumulator = Dafny.Sequence<char>.Concat(_209___accumulator, Dafny.Sequence<char>.FromElements((chars).Select((digits).Select(BigInteger.Zero))));
Dafny.ISequence<BigInteger> _in40 = (digits).Drop(BigInteger.One);
Dafny.ISequence<char> _in41 = chars;
digits = _in40;
chars = _in41;
goto TAIL_CALL_START;
}
}
public static Dafny.ISequence<char> Int2String(BigInteger n, Dafny.ISequence<char> chars)
{
BigInteger _210_base = new BigInteger((chars).Count);
if ((n).Sign == 0) {
return Dafny.Sequence<char>.FromString("0");
} else if ((n).Sign == 1) {
return String_Compile.__default.Digits2String(String_Compile.__default.Int2Digits(n, _210_base), chars);
} else {
return Dafny.Sequence<char>.Concat(Dafny.Sequence<char>.FromString("-"), String_Compile.__default.Digits2String(String_Compile.__default.Int2Digits((BigInteger.Zero) - (n), _210_base), chars));
}
}
public static Dafny.ISequence<char> Base10Int2String(BigInteger n) {
return String_Compile.__default.Int2String(n, String_Compile.__default.Base10);
}
public static Dafny.ISequence<char> Base10 { get {
return Dafny.Sequence<char>.FromElements('0', '1', '2', '3', '4', '5', '6', '7', '8', '9');
} }
}
} // end of namespace String_Compile

0 comments on commit 4c5f9a3

Please sign in to comment.