Implement unbounded ints/rationals in the Rust backend

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

.github/workflows/integration-tests-reusable.yml

@@ -139,7 +139,7 @@ jobs:
         DAFNY_RELEASE: ${{ github.workspace }}\unzippedRelease\dafny
       run: |
         cmd /c mklink D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1 D:\a\dafny\dafny\unzippedRelease\dafny\z3\bin\z3-4.12.1.exe
-        dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" dafny/Source/IntegrationTests/IntegrationTests.csproj
+        dotnet test --logger trx --logger "console;verbosity=normal" --collect:"XPlat Code Coverage" --settings dafnySource/IntegrationTests/coverlet.runsettings dafny/Source/IntegrationTests/IntegrationTests.csproj
     - name: Generate tests (non-Windows)
       ## This step creates lit tests from examples in documentation
       ## These are then picked up by the integration tests below 

.github/workflows/xunit-tests-reusable.yml

@@ -66,25 +66,25 @@ jobs:
     - name: Build
       run: dotnet build --no-restore ${{env.solutionPath}}
     - name: Run DafnyCore Tests
-      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyCore.Test
+      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyCore.Test/coverlet.runsettings Source/DafnyCore.Test
     - name: Run DafnyLanguageServer Tests
       run: |
         ## Run twice to catch unstable code (Issue #2673)
-        dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyLanguageServer.Test
+        dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test
         ## On the second run, collect test coverage data
         ##  Note that, for some mysterious reason, --collect doesn't work with the DafnyLanguageServer.Test package
         dotnet coverage collect -o DafnyLanguageServer.Test.coverage dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx Source/DafnyLanguageServer.Test
 
     - name: Run DafnyDriver Tests
-      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyDriver.Test
+      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyDriver.Test/coverlet.runsettings Source/DafnyDriver.Test
     - name: Run DafnyPipeline Tests
-      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyPipeline.Test
+      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyPipeline.Test/coverlet.runsettings Source/DafnyPipeline.Test
     - name: Run DafnyTestGeneration Tests
-      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyTestGeneration.Test
+      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyTestGeneration.Test/coverlet.runsettings Source/DafnyTestGeneration.Test
     - name: Run AutoExtern Tests
-      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/AutoExtern.Test
+      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/AutoExtern.Test/coverlet.runsettings Source/AutoExtern.Test
     - name: Run DafnyRuntime Tests
-      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" Source/DafnyRuntime.Tests
+      run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyRuntime.Tests/coverlet.runsettings Source/DafnyRuntime.Tests
     - uses: actions/upload-artifact@v3
       if: always()
       with:

Source/AutoExtern.Test/coverlet.runsettings

@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<RunSettings>
+  <DataCollectionRunSettings>
+    <DataCollectors>
+      <DataCollector friendlyName="XPlat Code Coverage">
+        <Configuration>
+          <Exclude>[*]DAST.*,[*]DCOMP.*</Exclude>
+        </Configuration>
+      </DataCollector>
+    </DataCollectors>
+  </DataCollectionRunSettings>
+</RunSettings>

Source/DafnyCore.Test/coverlet.runsettings

@@ -0,0 +1,12 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<RunSettings>
+  <DataCollectionRunSettings>
+    <DataCollectors>
+      <DataCollector friendlyName="XPlat Code Coverage">
+        <Configuration>
+          <Exclude>[*]DAST.*,[*]DCOMP.*</Exclude>
+        </Configuration>
+      </DataCollector>
+    </DataCollectors>
+  </DataCollectionRunSettings>
+</RunSettings>

Source/DafnyCore/Compilers/Dafny/AST.dfy

@@ -15,9 +15,9 @@ module {:extern "DAST"} DAST {
     Primitive(Primitive) | Passthrough(string) |
     TypeArg(Ident)
 
-  datatype Primitive = String | Bool | Char
+  datatype Primitive = Int | Real | String | Bool | Char
 
-  datatype ResolvedType = Datatype(path: seq<Ident>) | Trait(path: seq<Ident>) | Newtype
+  datatype ResolvedType = Datatype(path: seq<Ident>) | Trait(path: seq<Ident>) | Newtype(Type)
 
   datatype Ident = Ident(id: string)
 
@@ -62,8 +62,7 @@ module {:extern "DAST"} DAST {
     New(path: seq<Ident>, args: seq<Expression>) |
     NewArray(dims: seq<Expression>) |
     DatatypeValue(path: seq<Ident>, variant: string, isCo: bool, contents: seq<(string, Expression)>) |
-    SubsetUpgrade(value: Expression, typ: Type) |
-    SubsetDowngrade(value: Expression) |
+    Convert(value: Expression, from: Type, typ: Type) |
     SeqValue(elements: seq<Expression>) |
     SetValue(elements: seq<Expression>) |
     This() |
@@ -82,5 +81,5 @@ module {:extern "DAST"} DAST {
 
   datatype UnaryOp = Not | BitwiseNot | Cardinality
 
-  datatype Literal = BoolLiteral(bool) | IntLiteral(int) | DecLiteral(string) | StringLiteral(string) | CharLiteral(char) | Null
+  datatype Literal = BoolLiteral(bool) | IntLiteral(string, Type) | DecLiteral(string, string, Type) | StringLiteral(string) | CharLiteral(char) | Null
 }

Source/DafnyCore/Compilers/Dafny/ASTBuilder.cs

@@ -831,14 +831,8 @@ IIFEExprBuilder IIFE(string name, DAST.Type tpe) {
       return ret;
     }
 
-    SubsetUpgradeBuilder SubsetUpgrade(DAST.Type tpe) {
-      var ret = new SubsetUpgradeBuilder(tpe);
-      AddBuildable(ret);
-      return ret;
-    }
-
-    SubsetDowngradeBuilder SubsetDowngrade() {
-      var ret = new SubsetDowngradeBuilder();
+    ConvertBuilder Convert(DAST.Type fromType, DAST.Type toType) {
+      var ret = new ConvertBuilder(fromType, toType);
       AddBuildable(ret);
       return ret;
     }
@@ -1062,12 +1056,14 @@ public void AddBuildable(BuildableExpr item) {
   }
 }
 
-class SubsetUpgradeBuilder : ExprContainer, BuildableExpr {
-  readonly DAST.Type tpe;
+class ConvertBuilder : ExprContainer, BuildableExpr {
+  readonly DAST.Type fromType;
+  readonly DAST.Type toType;
   object value = null;
 
-  public SubsetUpgradeBuilder(DAST.Type tpe) {
-    this.tpe = tpe;
+  public ConvertBuilder(DAST.Type fromType, DAST.Type toType) {
+    this.fromType = fromType;
+    this.toType = toType;
   }
 
   public void AddExpr(DAST.Expression item) {
@@ -1090,38 +1086,10 @@ public DAST.Expression Build() {
     var builtValue = new List<DAST.Expression>();
     ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
 
-    return (DAST.Expression)DAST.Expression.create_SubsetUpgrade(
+    return (DAST.Expression)DAST.Expression.create_Convert(
       builtValue[0],
-      tpe
-    );
-  }
-}
-
-class SubsetDowngradeBuilder : ExprContainer, BuildableExpr {
-  object value = null;
-
-  public void AddExpr(DAST.Expression item) {
-    if (value != null) {
-      throw new InvalidOperationException();
-    } else {
-      value = item;
-    }
-  }
-
-  public void AddBuildable(BuildableExpr item) {
-    if (value != null) {
-      throw new InvalidOperationException();
-    } else {
-      value = item;
-    }
-  }
-
-  public DAST.Expression Build() {
-    var builtValue = new List<DAST.Expression>();
-    ExprContainer.RecursivelyBuild(new List<object> { value }, builtValue);
-
-    return (DAST.Expression)DAST.Expression.create_SubsetDowngrade(
-      builtValue[0]
+      fromType,
+      toType
     );
   }
 }

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -132,13 +132,13 @@ private static string MangleName(string name) {
     protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type from, Type to, IToken tok, ConcreteSyntaxTree wr) {
       if (from.AsSubsetType == null && to.AsSubsetType != null) {
         if (wr is BuilderSyntaxTree<ExprContainer> stmt) {
-          return new BuilderSyntaxTree<ExprContainer>(stmt.Builder.SubsetUpgrade(GenType(to)));
+          return new BuilderSyntaxTree<ExprContainer>(stmt.Builder.Convert(GenType(from), GenType(to)));
         } else {
           return base.EmitCoercionIfNecessary(from, to, tok, wr);
         }
       } else if (from.AsSubsetType != null && to.AsSubsetType == null) {
         if (wr is BuilderSyntaxTree<ExprContainer> stmt) {
-          return new BuilderSyntaxTree<ExprContainer>(stmt.Builder.SubsetDowngrade());
+          return new BuilderSyntaxTree<ExprContainer>(stmt.Builder.Convert(GenType(from), GenType(to)));
         } else {
           return base.EmitCoercionIfNecessary(from, to, tok, wr);
         }
@@ -234,9 +234,9 @@ private DAST.Type GenType(Type typ) {
       if (xType is BoolType) {
         return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Bool());
       } else if (xType is IntType) {
-        return (DAST.Type)DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("i64"));
+        return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Int());
       } else if (xType is RealType) {
-        return (DAST.Type)DAST.Type.create_Passthrough(Sequence<Rune>.UnicodeFromString("f32"));
+        return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_Real());
       } else if (xType.IsStringType) {
         return (DAST.Type)DAST.Type.create_Primitive(DAST.Primitive.create_String());
       } else if (xType.IsCharType) {
@@ -274,6 +274,8 @@ private DAST.Type GenType(Type typ) {
         var keyType = map.Domain;
         var valueType = map.Range;
         return (DAST.Type)DAST.Type.create_Map(GenType(keyType), GenType(valueType));
+      } else if (xType is BitvectorType) {
+        throw new NotImplementedException("Bitvector types");
       } else {
         throw new NotImplementedException("Type name for " + xType + " (" + typ.GetType() + ")");
       }
@@ -971,6 +973,7 @@ protected override void EmitIdentifier(string ident, ConcreteSyntaxTree wr) {
     protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
       if (wr is BuilderSyntaxTree<ExprContainer> builder) {
         DAST.Expression baseExpr;
+
         switch (e) {
           case CharLiteralExpr c:
             var codePoint = Util.UnescapedCharacters(Options, (string)c.Value, false).Single();
@@ -986,6 +989,15 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
           case StaticReceiverExpr:
             throw new NotImplementedException();
           default:
+            DAST.Type baseType;
+            if (e.Type.AsNewtype != null) {
+              baseType = GenType(e.Type.AsNewtype.BaseType);
+            } else if (e.Type.AsSubsetType != null) {
+              baseType = GenType(e.Type.AsSubsetType.Rhs);
+            } else {
+              baseType = GenType(e.Type);
+            }
+
             switch (e.Value) {
               case null:
                 baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_Null());
@@ -994,11 +1006,28 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
                 baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_BoolLiteral(value));
                 break;
               case BigInteger integer:
-                baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_IntLiteral(integer));
+                baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_IntLiteral(
+                  Sequence<Rune>.UnicodeFromString(integer.ToString()),
+                  baseType
+                ));
                 break;
               case BigDec n:
+                var mantissaStr = n.Mantissa.ToString();
+                var denominator = "1";
+                if (n.Exponent > 0) {
+                  for (var i = 0; i < n.Exponent; i++) {
+                    mantissaStr += "0";
+                  }
+                } else {
+                  for (var i = 0; i < -n.Exponent; i++) {
+                    denominator += "0";
+                  }
+                }
+
                 baseExpr = (DAST.Expression)DAST.Expression.create_Literal(DAST.Literal.create_DecLiteral(
-                  Sequence<Rune>.UnicodeFromString(n.ToString())
+                  Sequence<Rune>.UnicodeFromString(mantissaStr),
+                  Sequence<Rune>.UnicodeFromString(denominator),
+                  baseType
                 ));
                 break;
               default:
@@ -1008,8 +1037,10 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
             break;
         }
 
-        if (e.Type.AsNewtype != null || e.Type.AsSubsetType != null) {
-          baseExpr = (DAST.Expression)DAST.Expression.create_SubsetUpgrade(baseExpr, GenType(e.Type));
+        if (e.Type.AsNewtype != null) {
+          baseExpr = (DAST.Expression)DAST.Expression.create_Convert(baseExpr, GenType(e.Type.AsNewtype.BaseType), GenType(e.Type));
+        } else if (e.Type.AsSubsetType != null) {
+          baseExpr = (DAST.Expression)DAST.Expression.create_Convert(baseExpr, GenType(e.Type.AsSubsetType.Rhs), GenType(e.Type));
         }
 
         builder.Builder.AddExpr(baseExpr);
@@ -1062,14 +1093,14 @@ private DAST.Type FullTypeNameAST(UserDefinedType udt, MemberDecl member = null)
           Sequence<DAST.Type>.FromArray(arrow.Args.Select(m => GenType(m)).ToArray()),
           GenType(arrow.Result)
         );
+      } else if (udt.IsArrayType) {
+        return (DAST.Type)DAST.Type.create_Array(GenType(udt.TypeArgs[0]));
       }
 
       var cl = udt.ResolvedClass;
       switch (cl) {
         case TypeParameter:
           return (DAST.Type)DAST.Type.create_TypeArg(Sequence<Rune>.UnicodeFromString(IdProtect(udt.GetCompileName(Options))));
-        case ArrayClassDecl:
-          return (DAST.Type)DAST.Type.create_Array(GenType(udt.TypeArgs[0]));
         case TupleTypeDecl:
           return (DAST.Type)DAST.Type.create_Tuple(Sequence<DAST.Type>.FromArray(
             udt.TypeArgs.Select(m => GenType(m)).ToArray()
@@ -1097,17 +1128,17 @@ private DAST.Type TypeNameASTFromTopLevel(TopLevelDecl topLevel, List<Type> type
       }
 
       ResolvedType resolvedType;
-      if (topLevel is NewtypeDecl) {
-        resolvedType = (DAST.ResolvedType)DAST.ResolvedType.create_Newtype();
+      if (topLevel is NewtypeDecl newType) {
+        resolvedType = (DAST.ResolvedType)DAST.ResolvedType.create_Newtype(GenType(newType.BaseType));
       } else if (topLevel is TraitDecl) {
         resolvedType = (DAST.ResolvedType)DAST.ResolvedType.create_Trait(path);
       } else if (topLevel is DatatypeDecl) {
         resolvedType = (DAST.ResolvedType)DAST.ResolvedType.create_Datatype(path);
       } else if (topLevel is ClassDecl) {
         // TODO(shadaj): have a separate type when we properly support classes
         resolvedType = (DAST.ResolvedType)DAST.ResolvedType.create_Datatype(path);
-      } else if (topLevel is SubsetTypeDecl) {
-        resolvedType = (DAST.ResolvedType)DAST.ResolvedType.create_Newtype();
+      } else if (topLevel is SubsetTypeDecl subsetType) {
+        resolvedType = (DAST.ResolvedType)DAST.ResolvedType.create_Newtype(GenType(subsetType.Rhs));
       } else {
         throw new InvalidOperationException(topLevel.GetType().ToString());
       }
@@ -1563,7 +1594,14 @@ protected override void EmitIsZero(string varName, ConcreteSyntaxTree wr) {
 
     protected override void EmitConversionExpr(ConversionExpr e, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
       if (wr is BuilderSyntaxTree<ExprContainer> builder) {
-        throw new NotImplementedException();
+        if (e.ToType.Equals(e.E.Type)) {
+          EmitExpr(e.E, inLetExprBody, builder, wStmts);
+        } else {
+          EmitExpr(e.E, inLetExprBody, new BuilderSyntaxTree<ExprContainer>(builder.Builder.Convert(
+            GenType(e.E.Type),
+            GenType(e.ToType)
+          )), wStmts);
+        }
       } else {
         throw new InvalidOperationException();
       }