Fix Default<G>()

dafny-lang · Mar 4, 2020 · 2ece678 · 2ece678
1 parent f60634f
commit 2ece678
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 2 deletions.
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
@@ -1125,7 +1125,13 @@ public partial class Helpers {
  System.Console.Write(ToString(g));
  }
  public static G Default<G>() {
- System.Type ty = typeof(G);
+ Type ty = typeof(G);
+ // TODO-RS: How to generalize this?
+ if (ty.Name.Equals("ISequence`1")) {
+ Type classType = Type.GetType("Dafny.Sequence`1");
+ Type parameterizedClassType = classType.MakeGenericType(ty.GenericTypeArguments);
+ ty = parameterizedClassType;
+ }
  System.Reflection.MethodInfo mInfo = ty.GetMethod("_DafnyDefaultValue");
  if (mInfo != null) {
  G g = (G)mInfo.Invoke(null, null);

diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs
@@ -1125,7 +1125,13 @@ public partial class Helpers {
  System.Console.Write(ToString(g));
  }
  public static G Default<G>() {
- System.Type ty = typeof(G);
+ Type ty = typeof(G);
+ // TODO-RS: How to generalize this?
+ if (ty.Name.Equals("ISequence`1")) {
+ Type classType = Type.GetType("Dafny.Sequence`1");
+ Type parameterizedClassType = classType.MakeGenericType(ty.GenericTypeArguments);
+ ty = parameterizedClassType;
+ }
  System.Reflection.MethodInfo mInfo = ty.GetMethod("_DafnyDefaultValue");
  if (mInfo != null) {
  G g = (G)mInfo.Invoke(null, null);