Feat simplified rust identifiers

Source/DafnyCore/Backends/Dafny/ASTBuilder.cs

@@ -188,7 +188,7 @@ public void AddMethod(DAST.Method item) {
     }
 
     public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      parent.AddUnsupported("var/const for trait - " + item.dtor_name);
     }
 
     public object Finish() {
@@ -240,11 +240,11 @@ public NewtypeBuilder(NewtypeContainer parent, string name, List<TypeArgDecl> ty
     }
 
     public void AddMethod(DAST.Method item) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      parent.AddUnsupported("method for newtypes - " + item.dtor_name);
     }
 
     public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      parent.AddUnsupported("const for newtypes - " + item.dtor_name);
     }
 
     public object Finish() {
@@ -344,7 +344,7 @@ public void AddMethod(DAST.Method item) {
     }
 
     public void AddField(DAST.Formal item, bool isConstant, _IOption<DAST._IExpression> defaultValue) {
-      throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests);
+      parent.AddUnsupported("const for datatypes - " + item.dtor_name);
     }
 
     public object Finish() {

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -1578,12 +1578,13 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
     }
 
     protected override void EmitStringLiteral(string str, bool isVerbatim, ConcreteSyntaxTree wr) {
-      throw new UnsupportedInvalidOperationException("<i>EmitStringLiteral</i>");
+      AddUnsupported("EmitStringLiteral");
     }
 
     protected override ConcreteSyntaxTree EmitBitvectorTruncation(BitvectorType bvType, [CanBeNull] NativeType nativeType,
       bool surroundByUnchecked, ConcreteSyntaxTree wr) {
-      throw new UnsupportedInvalidOperationException("<i>EmitBitvectorTruncation</i>");
+      AddUnsupported("EmitBitvectorTruncation");
+      return wr;
     }
 
     protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLeft, ConcreteSyntaxTree wr,

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy

@@ -37,14 +37,16 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
      (|i| == 3 && i[2] in "0123456789"))
   }
 
+  // Given a Dafny-expanded fully qualified name with # or ., where ' has been replaced by _k, ? by _q and _ by __
+  // detect if there are of the strings above
   predicate has_special(i: string) {
     if |i| == 0 then false
     else if i[0] == '.' then true
     else if i[0] == '#' then true // otherwise "escapeName("r#") becomes "r#""
     else if i[0] == '_' then
       if 2 <= |i| then
-        if i[1] != '_' then true
-        else has_special(i[2..])
+        if i[1] == '_' then has_special(i[2..])
+        else true
       else
         true
     else
@@ -88,6 +90,7 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
 
   predicate is_dafny_generated_id(i: string) {
     && |i| > 0 && i[0] == '_' && !has_special(i[1..])
+    && (i != "_self" && i != "_Self")
     && (|i| >= 2 ==> i[1] != 'T') // To avoid conflict with tuple builders _T<digits>
   }
 
@@ -101,21 +104,21 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
   }
 
   function escapeIdent(i: string): string {
-    if is_tuple_numeric(i) then
+    if is_tuple_numeric(i) then // _42 remains the same
       i
-    else if is_tuple_builder(i) then
+    else if is_tuple_builder(i) then // ___hMake42 becomes _T42
       better_tuple_builder_name(i)
-    else if i == "self" || i == "Self" then
-      "r#_" + i
+    else if i == "self" || i == "Self" then // self becomes _self
+      "_" + i
     else if i in reserved_rust then
       "r#" + i
-    else if is_idiomatic_rust_id(i) then
+    else if is_idiomatic_rust_id(i) then // some__id becomes some_id
       idiomatic_rust(i)
-    else if is_dafny_generated_id(i) then
+    else if is_dafny_generated_id(i) then // _module remains _module
       i // Dafny-generated identifiers like "_module", cannot be written in Dafny itself
-    else
+    else // u16 becomes _u16, namespace.IsSomething_q becomes _namespace_dIsSomething_q
       var r := replaceDots(i);
-      "r#_" + r
+      "_" + r
   }
 
   // To be used when escaping variables

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy

@@ -88,15 +88,25 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
     else
     if i[0] == '_' then
       |i| >= 2 &&
-      i[1] in "_qkh" && IsDafnyEncodedIdTail(i[2..])
+      i[1] in ESCAPING && IsDafnyEncodedIdTail(i[2..])
     else
-      i[0] in "aqkhd." &&
+      (i[0] in SAMPLE_LETTERS || i[0] == '.') &&
       IsDafnyEncodedIdTail(i[1..])
   }
 
-  predicate IsDafnyEncodedId(i: string) {
-    if |i| == 0 then true
-    else i[0] in "aqkhd" && IsDafnyEncodedIdTail(i[1..])
+  // Subset of characters supported in Dafny identifiers, for proof purposes
+  const SAMPLE_LETTERS := "aqkhd"
+
+  // Letters that can come after a "_" in Dafny identifiers
+  // __ => _
+  // _q => ?
+  // _k => '
+  // _h => #
+  const ESCAPING := "_qkh"
+
+  ghost predicate IsDafnyEncodedId(i: string) {
+    if |i| == 0 then false
+    else i[0] in SAMPLE_LETTERS && IsDafnyEncodedIdTail(i[1..])
   }
 
   lemma DafnyEscapeCorrect(s: string)
@@ -194,7 +204,7 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
     ensures escapeIdent("_m") == "_m" // any hidden variable
     ensures escapeIdent("___hMake1") == "_T1" // tuple deconstructor
     ensures escapeIdent("h__w") == "h_w" // only letters and underscore
-    ensures escapeIdent("h_kw") == "r#_h_kw" //contains special char
+    ensures escapeIdent("h_kw") == "_h_kw" //contains special char
     ensures escapeIdent("fn") == "r#fn" // Keyword
   {
     assert has_special("h_kw");
@@ -225,26 +235,26 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
   }
 
   function UnescapeIdent(s: string): string {
-    if |s| >= 2 && s[0..2] == "r#" then
-      if |s| >= 3 && s[2] == '_' then
-        ReverseReplaceDots(s[3..]) // General escape
-      else
-        s[2..] // Keyword
-    else if |s| >= 1 && s[0] == '_' then
-      if |s| >= 2 && s[1] == 'T' then
-        "___hMake" + s[2..] // Tuple builder
-      else if is_tuple_numeric(s) then
+    if |s| >= 1 && s[0] == '_' then
+      if is_tuple_numeric(s) then
         s
+      else if |s| >= 2 && s[1] == 'T' then
+        "___hMake" + s[2..] // Tuple builder
+      else if s == "_self" || s == "_Self" then
+        s[1..]
       else
-        s
+        ReverseReplaceDots(s[1..]) // We remove the extra "_" prefix and place dots again
+    else if |s| >= 2 && s[0..2] == "r#" then
+      s[2..] // Reserved identifier
     else // Idiomatic rust
       ReverseIdiomaticRust(s)
   }
 
-  lemma TupleIdentInvertible(s: string)
-    requires is_tuple_numeric(s)
-    ensures UnescapeIdent(escapeIdent(s)) == s
-  {}
+  lemma TupleIdentInvertible(i: string)
+    requires is_tuple_numeric(i)
+    ensures UnescapeIdent(escapeIdent(i)) == i
+  {
+  }
 
   lemma {:rlimit 500} TupleBuilderInvertible(i: string)
     requires !is_tuple_numeric(i)
@@ -302,14 +312,24 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
     }
   }
 
-  lemma {:rlimit 800} EscapeIdentInvertibleForDafnyGeneratedId(s: string)
-    requires !is_tuple_numeric(s)
-    requires !is_tuple_builder(s)
-    requires s !in reserved_rust
-    requires !is_idiomatic_rust_id(s)
-    requires is_dafny_generated_id(s)
-    ensures UnescapeIdent(escapeIdent(s)) == s
+  lemma {:rlimit 800} EscapeIdentInvertibleForDafnyGeneratedId(i: string)
+    requires IsDafnyEncodedId(i)
+    requires !is_tuple_numeric(i)
+    requires !is_tuple_builder(i)
+    requires i !in reserved_rust
+    requires !is_idiomatic_rust_id(i)
+    requires is_dafny_generated_id(i)
+    ensures UnescapeIdent(escapeIdent(i)) == i
   {
+    assert escapeIdent(i) == i;
+    var s := i;
+    assert |s| >= 1 && s[0] == '_';
+    assert !(|s| >= 2 && s[1] == 'T');
+    assert !(s == "_self" || s == "_Self");
+    calc {
+      UnescapeIdent(s);
+      s;
+    }
   }
 
   lemma {:rlimit 800} EverythingElseInvertible(i: string)
@@ -322,16 +342,24 @@ module {:extern "DafnyToRustCompilerProofs"} DafnyToRustCompilerProofs {
     ensures UnescapeIdent(escapeIdent(i)) == i
   {
     var r := replaceDots(i);
-    var s := "r#_" + r;
-    assert |s| >= 2 && s[0..2] == "r#";
-    assert |s| >= 3 && s[2] == '_';
-    assert s[3..] == r;
-    calc {
-      UnescapeIdent(escapeIdent(i));
-      UnescapeIdent(s);
-      ReverseReplaceDots(replaceDots(i));
-      { ReplaceDotsInvertible(i); }
-      i;
+    var s := "_" + r;
+    assert escapeIdent(i) == s;
+    assert |s| >= 1 && s[0] == '_';
+    assert !(|s| >= 2 && s[1] == 'T');
+    assert !(s == "_self" || s == "_Self");
+    assert |i| > 0;
+    if i[0] == '_' {
+      assert i[0] == '_'; // So if i[0] is not '_'
+      assert UnescapeIdent(escapeIdent(i)) == i;
+    } else {
+      calc {
+        UnescapeIdent(s);
+        ReverseReplaceDots(s[1..]);
+        ReverseReplaceDots(r);
+        ReverseReplaceDots(replaceDots(i));
+        { ReplaceDotsInvertible(i); }
+        i;
+      }
     }
   }
 

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) {