Skip to content

Commit

Permalink
Regen GeneratedFromDafny code
Browse files Browse the repository at this point in the history
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed May 30, 2024
1 parent a61d607 commit 846ad62
Show file tree
Hide file tree
Showing 11 changed files with 5,562 additions and 13,100 deletions.
15,057 changes: 4,268 additions & 10,789 deletions Source/DafnyCore/GeneratedFromDafny/DCOMP.cs
View file

Large diffs are not rendered by default.

3,008 changes: 953 additions & 2,055 deletions Source/DafnyCore/GeneratedFromDafny/RAST.cs
View file

Large diffs are not rendered by default.

8 changes: 4 additions & 4 deletions Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_DivInternals.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,19 +14,19 @@ namespace Std.Arithmetic.DivInternals {
public partial class __default {
public static BigInteger DivPos(BigInteger x, BigInteger d)
{
BigInteger _150___accumulator = BigInteger.Zero;
BigInteger _136___accumulator = BigInteger.Zero;
TAIL_CALL_START: ;
if ((x).Sign == -1) {
_150___accumulator = (_150___accumulator) + (new BigInteger(-1));
_136___accumulator = (_136___accumulator) + (new BigInteger(-1));
BigInteger _in38 = (x) + (d);
BigInteger _in39 = d;
x = _in38;
d = _in39;
goto TAIL_CALL_START;
} else if ((x) < (d)) {
return (BigInteger.Zero) + (_150___accumulator);
return (BigInteger.Zero) + (_136___accumulator);
} else {
_150___accumulator = (_150___accumulator) + (BigInteger.One);
_136___accumulator = (_136___accumulator) + (BigInteger.One);
BigInteger _in40 = (x) - (d);
BigInteger _in41 = d;
x = _in40;
Expand Down
6 changes: 3 additions & 3 deletions Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Logarithm.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,12 @@ namespace Std.Arithmetic.Logarithm {
public partial class __default {
public static BigInteger Log(BigInteger @base, BigInteger pow)
{
BigInteger _152___accumulator = BigInteger.Zero;
BigInteger _138___accumulator = BigInteger.Zero;
TAIL_CALL_START: ;
if ((pow) < (@base)) {
return (BigInteger.Zero) + (_152___accumulator);
return (BigInteger.Zero) + (_138___accumulator);
} else {
_152___accumulator = (_152___accumulator) + (BigInteger.One);
_138___accumulator = (_138___accumulator) + (BigInteger.One);
BigInteger _in44 = @base;
BigInteger _in45 = Dafny.Helpers.EuclideanDivision(pow, @base);
@base = _in44;
Expand Down
6 changes: 3 additions & 3 deletions Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_MulInternals.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,12 @@ namespace Std.Arithmetic.MulInternals {
public partial class __default {
public static BigInteger MulPos(BigInteger x, BigInteger y)
{
BigInteger _149___accumulator = BigInteger.Zero;
BigInteger _135___accumulator = BigInteger.Zero;
TAIL_CALL_START: ;
if ((x).Sign == 0) {
return (BigInteger.Zero) + (_149___accumulator);
return (BigInteger.Zero) + (_135___accumulator);
} else {
_149___accumulator = (_149___accumulator) + (y);
_135___accumulator = (_135___accumulator) + (y);
BigInteger _in32 = (x) - (BigInteger.One);
BigInteger _in33 = y;
x = _in32;
Expand Down
6 changes: 3 additions & 3 deletions Source/DafnyCore/GeneratedFromDafny/Std_Arithmetic_Power.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,12 @@ namespace Std.Arithmetic.Power {
public partial class __default {
public static BigInteger Pow(BigInteger b, BigInteger e)
{
BigInteger _151___accumulator = BigInteger.One;
BigInteger _137___accumulator = BigInteger.One;
TAIL_CALL_START: ;
if ((e).Sign == 0) {
return (BigInteger.One) * (_151___accumulator);
return (BigInteger.One) * (_137___accumulator);
} else {
_151___accumulator = (_151___accumulator) * (b);
_137___accumulator = (_137___accumulator) * (b);
BigInteger _in42 = b;
BigInteger _in43 = (e) - (BigInteger.One);
b = _in42;
Expand Down
178 changes: 89 additions & 89 deletions Source/DafnyCore/GeneratedFromDafny/Std_Collections_Seq.cs
View file

Large diffs are not rendered by default.

28 changes: 14 additions & 14 deletions Source/DafnyCore/GeneratedFromDafny/Std_Strings_CharStrEscaping.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,12 +14,12 @@ namespace Std.Strings.CharStrEscaping {
public partial class __default {
public static Dafny.ISequence<Dafny.Rune> Escape(Dafny.ISequence<Dafny.Rune> str, Dafny.ISet<Dafny.Rune> mustEscape, Dafny.Rune escape)
{
Dafny.ISequence<Dafny.Rune> _191___accumulator = Dafny.Sequence<Dafny.Rune>.FromElements();
Dafny.ISequence<Dafny.Rune> _177___accumulator = Dafny.Sequence<Dafny.Rune>.FromElements();
TAIL_CALL_START: ;
if ((str).Equals(Dafny.Sequence<Dafny.Rune>.FromElements())) {
return Dafny.Sequence<Dafny.Rune>.Concat(_191___accumulator, str);
return Dafny.Sequence<Dafny.Rune>.Concat(_177___accumulator, str);
} else if ((mustEscape).Contains((str).Select(BigInteger.Zero))) {
_191___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_191___accumulator, Dafny.Sequence<Dafny.Rune>.FromElements(escape, (str).Select(BigInteger.Zero)));
_177___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_177___accumulator, Dafny.Sequence<Dafny.Rune>.FromElements(escape, (str).Select(BigInteger.Zero)));
Dafny.ISequence<Dafny.Rune> _in56 = (str).Drop(BigInteger.One);
Dafny.ISet<Dafny.Rune> _in57 = mustEscape;
Dafny.Rune _in58 = escape;
Expand All @@ -28,7 +28,7 @@ public static Dafny.ISequence<Dafny.Rune> Escape(Dafny.ISequence<Dafny.Rune> str
escape = _in58;
goto TAIL_CALL_START;
} else {
_191___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_191___accumulator, Dafny.Sequence<Dafny.Rune>.FromElements((str).Select(BigInteger.Zero)));
_177___accumulator = Dafny.Sequence<Dafny.Rune>.Concat(_177___accumulator, Dafny.Sequence<Dafny.Rune>.FromElements((str).Select(BigInteger.Zero)));
Dafny.ISequence<Dafny.Rune> _in59 = (str).Drop(BigInteger.One);
Dafny.ISet<Dafny.Rune> _in60 = mustEscape;
Dafny.Rune _in61 = escape;
Expand All @@ -44,23 +44,23 @@ public static Std.Wrappers._IOption<Dafny.ISequence<Dafny.Rune>> Unescape(Dafny.
return Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(str);
} else if (((str).Select(BigInteger.Zero)) == (escape)) {
if ((new BigInteger((str).Count)) > (BigInteger.One)) {
Std.Wrappers._IOption<Dafny.ISequence<Dafny.Rune>> _192_valueOrError0 = Std.Strings.CharStrEscaping.__default.Unescape((str).Drop(new BigInteger(2)), escape);
if ((_192_valueOrError0).IsFailure()) {
return (_192_valueOrError0).PropagateFailure<Dafny.ISequence<Dafny.Rune>>();
Std.Wrappers._IOption<Dafny.ISequence<Dafny.Rune>> _178_valueOrError0 = Std.Strings.CharStrEscaping.__default.Unescape((str).Drop(new BigInteger(2)), escape);
if ((_178_valueOrError0).IsFailure()) {
return (_178_valueOrError0).PropagateFailure<Dafny.ISequence<Dafny.Rune>>();
} else {
Dafny.ISequence<Dafny.Rune> _193_tl = (_192_valueOrError0).Extract();
return Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.FromElements((str).Select(BigInteger.One)), _193_tl));
Dafny.ISequence<Dafny.Rune> _179_tl = (_178_valueOrError0).Extract();
return Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.FromElements((str).Select(BigInteger.One)), _179_tl));
}
} else {
return Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_None();
}
} else {
Std.Wrappers._IOption<Dafny.ISequence<Dafny.Rune>> _194_valueOrError1 = Std.Strings.CharStrEscaping.__default.Unescape((str).Drop(BigInteger.One), escape);
if ((_194_valueOrError1).IsFailure()) {
return (_194_valueOrError1).PropagateFailure<Dafny.ISequence<Dafny.Rune>>();
Std.Wrappers._IOption<Dafny.ISequence<Dafny.Rune>> _180_valueOrError1 = Std.Strings.CharStrEscaping.__default.Unescape((str).Drop(BigInteger.One), escape);
if ((_180_valueOrError1).IsFailure()) {
return (_180_valueOrError1).PropagateFailure<Dafny.ISequence<Dafny.Rune>>();
} else {
Dafny.ISequence<Dafny.Rune> _195_tl = (_194_valueOrError1).Extract();
return Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.FromElements((str).Select(BigInteger.Zero)), _195_tl));
Dafny.ISequence<Dafny.Rune> _181_tl = (_180_valueOrError1).Extract();
return Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.FromElements((str).Select(BigInteger.Zero)), _181_tl));
}
}
}
Expand Down
Loading

0 comments on commit 846ad62

Please sign in to comment.