Fix: Factorization of all paths in the generated Rust AST

Source/DafnyCore.Test/GeneratedDafnyTest.cs

@@ -5,7 +5,12 @@ namespace DafnyCore.Test;
 
 public class GeneratedDafnyTest {
   [Fact]
-  public void TestDafnyGeneratedCode() {
+  public void TestDafnyCoverage() {
     DafnyToRustCompilerCoverage.RASTCoverage.__default.TestExpr();
   }
+
+  [Fact]
+  public void TestPathSimplification() {
+    FactorPathsOptimizationTest.__default.TestApply();
+  }
 }

Source/DafnyCore.Test/GeneratedFromDafny/FactorPathsOptimizationTest.cs

@@ -25,7 +25,7 @@ public static void ShouldBeEqual(RAST._IMod a, RAST._IMod b)
         Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Got:\n"), _0_sA), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"))).ToVerbatimString(false));
         Dafny.Helpers.Print((Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Expected:\n"), _1_sB), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"))).ToVerbatimString(false));
         if (!((_0_sA).Equals(_1_sB))) {
-          throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-path-simplification.dfy(12,6): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
+          throw new Dafny.HaltException("Backends/Rust/Dafny-compiler-rust-path-simplification.dfy(13,6): " + Dafny.Sequence<Dafny.Rune>.UnicodeFromString("expectation violation").ToVerbatimString(false));}
       }
     }
     public static void TestApply()
@@ -42,6 +42,8 @@ public static void TestApply()
       _4_Any = RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any"));
       FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), (_3_std__any__Any).AsType())))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (_3_std__any__Any).AsType(), ((((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_StructDecl(RAST.Struct.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"), Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), RAST.Fields.create_NamedFields(Dafny.Sequence<RAST._IField>.FromElements(RAST.Field.create(RAST.Visibility.create_PUB(), RAST.Formal.create(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("a"), _4_Any)))))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_Impl(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), _4_Any, (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
       FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_0_T__Decl), (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).AsType()).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements()))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject")))), RAST.ModDecl.create_ImplDecl(RAST.Impl.create_ImplFor(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(_1_T__Decl__simp), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("UpcastObject"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("x")))), (RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("test"))).Apply(Dafny.Sequence<RAST._IType>.FromElements(_2_T)), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""), Dafny.Sequence<RAST._IImplMember>.FromElements())))));
+      FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_ConstDecl(RAST.Constant.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummy"), (_3_std__any__Any).AsType(), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("doit"), Std.Wrappers.Option<RAST._IType>.create_Some(((RAST.__default.std__rc__Rc).AsType()).Apply1(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unknown")))), Std.Wrappers.Option<RAST._IExpr>.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("something"))).ApplyType(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_DynType((RAST.__default.std__default__Default).AsType())))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements(RAST.__default.std__default__Default__default, (((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd!"))).AsExpr()).Apply1(RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("obj"))))))), RAST.Expr.create_TypeAscription(RAST.Expr.create_ExprFromType(((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString"))).AsType()), ((RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType"))).AsType()))))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), _3_std__any__Any)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), RAST.__default.std__rc__Rc)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), RAST.__default.std__default__Default)), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString")))), RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), (RAST.__default.dafny__runtime).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummy"), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Any")), RAST.Expr.create_StmtExpr(RAST.Expr.create_DeclareVar(RAST.DeclareType.create_MUT(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("doit"), Std.Wrappers.Option<RAST._IType>.create_Some((RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Rc"))).Apply1(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("unknown")))), Std.Wrappers.Option<RAST._IExpr>.create_Some(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("something"))).ApplyType(Dafny.Sequence<RAST._IType>.FromElements(RAST.Type.create_DynType(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Default")))))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements(((RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Default"))).FSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("default"))).Apply(Dafny.Sequence<RAST._IExpr>.FromElements()), (RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("rd!"))).Apply1(RAST.Expr.create_Identifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("obj"))))))), RAST.Expr.create_TypeAscription(RAST.Expr.create_ExprFromType(RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyString"))), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("DafnyType")))))))));
+      FactorPathsOptimizationTest.__default.ShouldBeEqual(Dafny.Helpers.Id<Func<RAST._IMod, RAST._IMod>>(FactorPathsOptimization.__default.apply(RAST.__default.crate))(RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), Dafny.Sequence<RAST._IType>.FromElements(), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyExtern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("anothermodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyIntern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing"))))))), RAST.Mod.create_Mod(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("onemodule"), Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_TraitDecl(RAST.Trait.create(Dafny.Sequence<RAST._ITypeParamDecl>.FromElements(), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), Dafny.Sequence<RAST._IType>.FromElements(), Dafny.Sequence<RAST._IImplMember>.FromElements())), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyExtern"), (((RAST.__default.crate).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("anothermodule"))).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something"))).AsType(), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))), RAST.ModDecl.create_ConstDecl(RAST.Constant.create(Dafny.Sequence<Dafny.ISequence<Dafny.Rune>>.FromElements(), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("dummyIntern"), RAST.Type.create_TIdentifier(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Something")), RAST.Expr.create_RawExpr(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("nothing")))))));
     }
   }
 } // end of namespace FactorPathsOptimizationTest

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -185,9 +185,15 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
     //   }
     // They aren't in any namespace to make them universally accessible.
     private void EmitFuncExtensions(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) {
-      var funcExtensions = wr.NewNamedBlock("internal static class FuncExtensions");
+      // An extension for this arity will be provided in the Runtime which has to be linked.
+      var omitAritiesBefore16 = !Options.IncludeRuntime && Options.SystemModuleTranslationMode is not CommonOptionBag.SystemModuleMode.OmitAllOtherModules;
+      var name = omitAritiesBefore16 ? "FuncExtensionsAfterArity16" : "FuncExtensions";
+      var funcExtensions = wr.NewNamedBlock("public static class " + name);
       foreach (var kv in systemModuleManager.ArrowTypeDecls) {
         int arity = kv.Key;
+        if (omitAritiesBefore16 && arity <= 16) {
+          continue;
+        }
 
         List<string> TypeParameterList(string prefix) {
           var l = arity switch {

Source/DafnyCore/Backends/Dafny/AST.dfy

@@ -128,10 +128,11 @@ module {:extern "DAST"} DAST {
     | SupportsEquality
     | SupportsDefault
 
-  datatype Primitive = Int | Real | String | Bool | Char
+  datatype Primitive = Int | Real | String | Bool | Char | Native
 
+  // USIZE is for whatever target considers that native arrays can be indexed with
   datatype NewtypeRange =
-    | U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | BigInt
+    | U8 | I8 | U16 | I16 | U32 | I32 | U64 | I64 | U128 | I128 | USIZE | BigInt
     | NoRange
 
   datatype Attribute = Attribute(name: string, args: seq<string>)

Source/DafnyCore/Backends/Dafny/ASTBuilder.cs

@@ -1806,17 +1806,17 @@ public void AddBuildable(BuildableExpr item) {
       }
     }
 
-    public static DAST.Expression ToNativeU64(int number) {
+    public static DAST.Expression ToNativeUsize(int number) {
       var origType = DAST.Type.create_Primitive(DAST.Primitive.create_Int());
       var numberExpr = (DAST.Expression)DAST.Expression.create_Literal(
         DAST.Literal.create_IntLiteral(Sequence<Rune>.UnicodeFromString($"{number}"),
           origType)
       );
       return (DAST.Expression)DAST.Expression.create_Convert(numberExpr, origType, DAST.Type.create_UserDefined(
         DAST.ResolvedType.create_ResolvedType(
-        Sequence<Sequence<Rune>>.FromElements((Sequence<Rune>)Sequence<Rune>.UnicodeFromString("u64")),
+        Sequence<Sequence<Rune>>.FromElements((Sequence<Rune>)Sequence<Rune>.UnicodeFromString("usize")),
         Sequence<_IType>.Empty,
-        DAST.ResolvedTypeBase.create_Newtype(origType, DAST.NewtypeRange.create_U64(), true), Sequence<_IAttribute>.Empty,
+        DAST.ResolvedTypeBase.create_Newtype(origType, DAST.NewtypeRange.create_USIZE(), true), Sequence<_IAttribute>.Empty,
         Sequence<Sequence<Rune>>.Empty, Sequence<_IType>.Empty)
       ));
     }
@@ -1833,14 +1833,14 @@ public DAST.Expression Build() {
 
       DAST.Expression startExpr;
       if (start == null) {
-        startExpr = ToNativeU64(0);
+        startExpr = ToNativeUsize(0);
       } else {
         startExpr = (DAST.Expression)DAST.Expression.create_Ident(
           Sequence<Rune>.UnicodeFromString(start));
       }
 
       return (DAST.Expression)DAST.Expression.create_IntRange(
-        DAST.Type.create_Primitive(DAST.Primitive.create_Int()),
+        DAST.Type.create_Primitive(DAST.Primitive.create_Native()),
         startExpr, endExpr, true);
     }