made pr

dafny-lang · Oct 18, 2024 · db9f88f · db9f88f
1 parent 16fe74c
commit db9f88f
Show file tree

Hide file tree

Showing 3 changed files with 47 additions and 47 deletions.
diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs
@@ -344,7 +344,7 @@ public void AddMethod(DAST.Method item) {
  }
 
  public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
- parent.AddUnsupported("const for datatypes - " +  item.dtor_name);
+ parent.AddUnsupported("const for datatypes - " + item.dtor_name);
  }
 
  public object Finish() {

diff --git a/Source/DafnyCore/GeneratedFromDafny/Defs.cs b/Source/DafnyCore/GeneratedFromDafny/Defs.cs
@@ -28,12 +28,12 @@ public static bool has__special(Dafny.ISequence<Dafny.Rune> i) {
  return true;
  } else if (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_'))) {
  if ((new BigInteger(2)) <= (new BigInteger((i).Count))) {
- if (((i).Select(BigInteger.One)) != (new Dafny.Rune('_'))) {
- return true;
- } else {
+ if (((i).Select(BigInteger.One)) == (new Dafny.Rune('_'))) {
  Dafny.ISequence<Dafny.Rune> _in0 = (i).Drop(new BigInteger(2));
  i = _in0;
  goto TAIL_CALL_START;
+ } else {
+ return true;
  }
  } else {
  return true;
@@ -85,7 +85,7 @@ public static bool is__tuple__builder(Dafny.ISequence<Dafny.Rune> i) {
  return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_T"), (i).Drop(new BigInteger(8)));
  }
  public static bool is__dafny__generated__id(Dafny.ISequence<Dafny.Rune> i) {
- return ((((new BigInteger((i).Count)).Sign == 1) && (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_')))) && (!(Defs.__default.has__special((i).Drop(BigInteger.One))))) && (!((new BigInteger((i).Count)) >= (new BigInteger(2))) || (((i).Select(BigInteger.One)) != (new Dafny.Rune('T'))));
+ return (((((new BigInteger((i).Count)).Sign == 1) && (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_')))) && (!(Defs.__default.has__special((i).Drop(BigInteger.One))))) && ((!(i).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_self"))) && (!(i).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_Self"))))) && (!((new BigInteger((i).Count)) >= (new BigInteger(2))) || (((i).Select(BigInteger.One)) != (new Dafny.Rune('T'))));
  }
  public static bool is__idiomatic__rust__id(Dafny.ISequence<Dafny.Rune> i) {
  return ((((new BigInteger((i).Count)).Sign == 1) && (!(Defs.__default.has__special(i)))) && (!(Defs.__default.reserved__rust).Contains(i))) && (!(Defs.__default.reserved__rust__need__prefix).Contains(i));
@@ -99,7 +99,7 @@ public static bool is__idiomatic__rust__id(Dafny.ISequence<Dafny.Rune> i) {
  } else if (Defs.__default.is__tuple__builder(i)) {
  return Defs.__default.better__tuple__builder__name(i);
  } else if (((i).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("self"))) || ((i).Equals(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Self")))) {
- return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("r#_"), i);
+ return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_"), i);
  } else if ((Defs.__default.reserved__rust).Contains(i)) {
  return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("r#"), i);
  } else if (Defs.__default.is__idiomatic__rust__id(i)) {
@@ -108,7 +108,7 @@ public static bool is__idiomatic__rust__id(Dafny.ISequence<Dafny.Rune> i) {
  return i;
  } else {
  Dafny.ISequence<Dafny.Rune> _0_r = Defs.__default.replaceDots(i);
- return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("r#_"), _0_r);
+ return Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("_"), _0_r);
  }
  }
  public static Dafny.ISequence<Dafny.Rune> escapeVar(Dafny.ISequence<Dafny.Rune> f) {