Fix Rust compilation errors for unused types and constant fields

<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>
dafny-lang · Aug 21, 2023 · d25ece5 · d25ece5
1 parent e06c0e5
commit d25ece5
Show file tree

Hide file tree

Showing 3 changed files with 6,665 additions and 6,591 deletions.
diff --git a/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs b/Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs
@@ -1310,6 +1310,16 @@ member.EnclosingClass is DatatypeDecl
             member.IsStatic,
             expectedType.AsArrowType.Arity
           ), null);
+        } else if (internalAccess && (member is ConstantField || member.EnclosingClass is TraitDecl)) {
+          return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select(
+            objExpr,
+            Sequence<Rune>.UnicodeFromString("_" + member.GetCompileName(Options)),
+            false,
+            member.EnclosingClass is DatatypeDecl
+          ), (DAST.AssignLhs)DAST.AssignLhs.create_Select(
+            objExpr,
+            Sequence<Rune>.UnicodeFromString("_" + member.GetCompileName(Options))
+          ));
         } else {
           return new ExprLvalue((DAST.Expression)DAST.Expression.create_Select(
             objExpr,

diff --git a/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Compilers/Rust/Dafny-compiler-rust.dfy
@@ -90,10 +90,18 @@ module {:extern "DCOMP"} DCOMP {
         fieldI := fieldI + 1;
       }
 
-      s := "#[derive(Default)]\npub struct r#" + c.name + typeParams + " {\n" + fields +  "\n}";
+      var typeParamI := 0;
+      while typeParamI < |c.typeParams| {
+        var tpeGen := GenType(c.typeParams[typeParamI], false, false);
+        fields := fields + "_phantom_type_param_" + natToString(typeParamI) + ": ::std::marker::PhantomData<" + tpeGen + ">,\n";
+
+        typeParamI := typeParamI + 1;
+      }
+
+      s := "#[derive(::std::default::Default)]\npub struct r#" + c.name + typeParams + " {\n" + fields +  "\n}";
 
       var implBody, traitBodies := GenClassImplBody(c.body, false, Type.Path([], [], ResolvedType.Datatype(path)), {});
-      implBody := "pub fn new() -> Self {\n" + "r#" + c.name + " {\n" + fieldInits + "\n}\n}\n" + implBody;
+      implBody := "pub fn new() -> Self {\n::std::default::Default::default()\n}\n" + implBody;
 
       s := s + "\n" + "impl " + constrainedTypeParams + " r#" + c.name + typeParams + " {\n" + implBody + "\n}";
       if (|c.superClasses| > 0) {
@@ -284,6 +292,10 @@ module {:extern "DCOMP"} DCOMP {
               k := k + 1;
             }
 
+            if |c.typeParams| > 0 {
+              methodBody := methodBody + "r#" + c.name + "::_PhantomVariant(..) => panic!(),\n";
+            }
+
             methodBody := methodBody + "}\n";
 
             implBody := implBody + "pub fn r#" + formal.name + "(&self) -> &" + formalType + " {\n" + methodBody + "}\n";
@@ -294,6 +306,21 @@ module {:extern "DCOMP"} DCOMP {
         i := i + 1;
       }
 
+      if |c.typeParams| > 0 {
+        ctors := ctors + "_PhantomVariant(";
+        var typeI := 0;
+        while typeI < |c.typeParams| {
+          if typeI > 0 {
+            ctors := ctors + ", ";
+          }
+
+          var genTp := GenType(c.typeParams[typeI], false, false);
+          ctors := ctors + "::std::marker::PhantomData::<" + genTp + ">";
+          typeI := typeI + 1;
+        }
+        ctors := ctors + ")";
+      }
+
       var enumBody := "#[derive(PartialEq)]\npub enum r#" + c.name + typeParams + " {\n" + ctors +  "\n}" + "\n" + "impl " + constrainedTypeParams + " r#" + c.name + typeParams + " {\n" + implBody + "\n}";
 
       var identEraseImpls := "impl " + constrainedTypeParams + " ::dafny_runtime::DafnyErasable for r#" + c.name + typeParams + " {\n" + "type Erased = Self;\nfn erase(&self) -> &Self::Erased { self }\nfn erase_owned(self) -> Self::Erased { self }}\n";
@@ -333,6 +360,10 @@ module {:extern "DCOMP"} DCOMP {
         i := i + 1;
       }
 
+      if |c.typeParams| > 0 {
+        printImpl := printImpl + "r#" + c.name + "::_PhantomVariant(..) => {panic!()\n}\n";
+      }
+
       printImpl := printImpl + "}\n}\n}\n";
 
       var defaultImpl := "";