fix: Make FuncExtensions internal again, handle it in DafnyGeneratedF…

…romDafnyPost.py instead (#5860)

### Description
#5757 made `FuncExtensions` in the C# runtime public instead of
internal, which is not ideal since it increases the API surface area of
the runtime and is a one-way door (and causes false positives in
prerelease regressions testing). It was done because it seemed to be
necessary, but the actual root cause was dropping these extension
methods when post-processing Dafny's output. This PR reverts the change
and special-cases the class in the python script instead.

### How has this been tested?
Existing tests.

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

---------

Co-authored-by: Mikael Mayer <[email protected]>

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -185,15 +185,10 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
     //   }
     // They aren't in any namespace to make them universally accessible.
     private void EmitFuncExtensions(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) {
-      // 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);
+      var funcExtensions = wr.NewNamedBlock("internal static class FuncExtensions");
+      wr.WriteLine("// end of class FuncExtensions");
       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/DafnyGeneratedFromDafnyPost.py

@@ -67,6 +67,18 @@
 
     print(f"File generated: {file_path}")
 
+  # Special-case the FuncExtensions class, which isn't declared inside a namespace
+  func_extensions_pattern = re.compile(r'(internal\s+static\s+class\s+FuncExtensions\s*{[\s\S]*?}\s*//\s*end\s*of\s*class\s*FuncExtensions)')
+  match = func_extensions_pattern.search(content)
+  func_extensions_content = match[0]
+
+  file_content = f"{prelude}\n\n{func_extensions_content}"
+  file_path = f"{output}/FuncExtensions.cs"
+  with open(file_path, 'w') as file:
+    file.write(file_content)
+
+  print(f"File generated: {file_path}")
+
 # Now delete the file output.cs
 os.remove(output + '.cs')
 print("File deleted: " + output + '.cs')

Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs

@@ -0,0 +1,38 @@
+// Dafny program the_program compiled into C#
+// To recompile, you will need the libraries
+//     System.Runtime.Numerics.dll System.Collections.Immutable.dll
+// but the 'dotnet' tool in net6.0 should pick those up automatically.
+// Optionally, you may want to include compiler switches like
+//     /debug /nowarn:162,164,168,183,219,436,1717,1718
+
+using System;
+using System.Numerics;
+using System.Collections;
+#pragma warning disable CS0164 // This label has not been referenced
+#pragma warning disable CS0162 // Unreachable code detected
+#pragma warning disable CS1717 // Assignment made to same variable
+
+internal static class FuncExtensions {
+  public static Func<U, UResult> DowncastClone<T, TResult, U, UResult>(this Func<T, TResult> F, Func<U, T> ArgConv, Func<TResult, UResult> ResConv) {
+    return arg => ResConv(F(ArgConv(arg)));
+  }
+  public static Func<UResult> DowncastClone<TResult, UResult>(this Func<TResult> F, Func<TResult, UResult> ResConv) {
+    return () => ResConv(F());
+  }
+  public static Func<U1, U2, UResult> DowncastClone<T1, T2, TResult, U1, U2, UResult>(this Func<T1, T2, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2)));
+  }
+  public static Func<U1, U2, U3, UResult> DowncastClone<T1, T2, T3, TResult, U1, U2, U3, UResult>(this Func<T1, T2, T3, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3)));
+  }
+  public static Func<U1, U2, U3, U4, UResult> DowncastClone<T1, T2, T3, T4, TResult, U1, U2, U3, U4, UResult>(this Func<T1, T2, T3, T4, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3, arg4) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4)));
+  }
+  public static Func<U1, U2, U3, U4, U5, U6, U7, UResult> DowncastClone<T1, T2, T3, T4, T5, T6, T7, TResult, U1, U2, U3, U4, U5, U6, U7, UResult>(this Func<T1, T2, T3, T4, T5, T6, T7, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<U5, T5> ArgConv5, Func<U6, T6> ArgConv6, Func<U7, T7> ArgConv7, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3, arg4, arg5, arg6, arg7) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5), ArgConv6(arg6), ArgConv7(arg7)));
+  }
+  public static Func<U1, U2, U3, U4, U5, UResult> DowncastClone<T1, T2, T3, T4, T5, TResult, U1, U2, U3, U4, U5, UResult>(this Func<T1, T2, T3, T4, T5, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<U5, T5> ArgConv5, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3, arg4, arg5) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5)));
+  }
+}
+// end of class FuncExtensions

Source/DafnyRuntime/DafnyRuntimeSystemModule.cs

@@ -503,7 +503,7 @@ public static T[] InitNewArray1<T>(T z, BigInteger size0) {
     }
   }
 } // end of namespace Dafny
-public static class FuncExtensions {
+internal static class FuncExtensions {
   public static Func<U, UResult> DowncastClone<T, TResult, U, UResult>(this Func<T, TResult> F, Func<U, T> ArgConv, Func<TResult, UResult> ResConv) {
     return arg => ResConv(F(ArgConv(arg)));
   }
@@ -556,6 +556,7 @@ public static Func<U1, U2, U3, U4, U5, U6, U7, U8, U9, U10, U11, U12, U13, U14,
     return (arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5), ArgConv6(arg6), ArgConv7(arg7), ArgConv8(arg8), ArgConv9(arg9), ArgConv10(arg10), ArgConv11(arg11), ArgConv12(arg12), ArgConv13(arg13), ArgConv14(arg14), ArgConv15(arg15), ArgConv16(arg16)));
   }
 }
+// end of class FuncExtensions
 #endif
 namespace _System {