Split out tests for extern constructors

Extern constructors are currently broken on Go and JavaScript, so I'm moving
that functionality from the tests in Extern.dfy and moving it to the new
ExternCtors.dfy, which only has RUN lines for C# and Java.  I've included the
extern code that *should* make the tests work (but currently doesn't).

Test/comp/Extern.dfy

@@ -14,7 +14,7 @@ method Main() {
   Library.AllDafny.M();
   Library.Mixed.M();
   print Library.Mixed.F(), "\n";
-  var m := new Library.Mixed(2);
+  var m := new Library.Mixed();
   m.IM();
   print m.IF(), "\n";
   Library.AllExtern.P();
@@ -34,7 +34,7 @@ module {:extern "Library"} Library {
     static method M() { print "AllDafny.M\n"; }
   }
   class {:extern} Mixed {
-    constructor {:extern} (n: int)
+    constructor() { }
     static function Seven(): int { 7 }
     static method M() { print "Extern static method says: "; P(); }
     static method {:extern} P()

Test/comp/Extern2.cs

@@ -22,12 +22,6 @@ public static object CallMe() {
 
   // must be partial, since Dafny will also generate some methods into this class
   public partial class Mixed {
-    private readonly BigInteger n;
-
-    public Mixed(BigInteger n) {
-      this.n = n;
-    }
-
     public static void P() {
       System.Console.WriteLine("Mixed.P");
     }
@@ -38,7 +32,7 @@ public static BigInteger G() {
       return 1;
     }
     public BigInteger IG() {
-      return n;
+      return 2;
     }
   }
   // It's okay for the following class to not be partial, since Dafny won't be adding

Test/comp/Extern3.js

@@ -15,10 +15,14 @@ let Library = (function() {
     }
   };
 
-  $module.Mixed = class Mixed {
-    constructor(n) {
-      this.n = n;
+  $module.OtherClass = class OtherClass {
+    static CallMe() {
+      return "OtherClass.CallMe";
     }
+  }
+
+  $module.Mixed = class Mixed {
+    constructor() { }
 
     // static method P()
     static P() {
@@ -34,7 +38,7 @@ let Library = (function() {
     }
 
     IG() {
-      return this.n;
+      return new BigNumber(2);
     }
   }
   $module.AllExtern = class AllExtern {
@@ -45,9 +49,3 @@ let Library = (function() {
 
   return $module;
 })();
-
-let OtherClass = class OtherClass {
-  static CallMe() {
-    return "OtherClass.CallMe";
-  }
-}

Test/comp/Extern4.go

@@ -29,7 +29,7 @@ type CompanionStruct_OtherClass_ struct{}
 
 var OtherClass = CompanionStruct_OtherClass_{}
 
-func (CompanionStruct_OtherClass_) CallMe() {
+func (CompanionStruct_OtherClass_) CallMe() interface{} {
   return "OtherClass.CallMe"
 }
 
@@ -43,22 +43,26 @@ func (AllDafny) M() {
   fmt.Print("AllDafny.M\n")
 }
 
-type Mixed struct{ n dafny.Int }
+type Mixed struct{}
 type CompanionStruct_Mixed_ struct{}
 var Companion_Mixed_ = CompanionStruct_Mixed_{}
-func New_Mixed_(n dafny.Int) *Mixed {
-  return &Mixed{n}
+
+func New_Mixed_() *Mixed {
+  return &Mixed{}
 }
+
+func (m *Mixed) Ctor__() { }
+
 // The Go compiler doesn't support Dafny methods in extern libraries
 func (CompanionStruct_Mixed_) M() {
-  fmt.Print("Extern static code says: ")
+  fmt.Print("Extern static method says: ")
   Companion_Mixed_.P()
 }
 func (CompanionStruct_Mixed_) P() {
   fmt.Print("Mixed.P\n")
 }
 func (m *Mixed) IM() {
-  fmt.Print("Extern instance code says: ")
+  fmt.Print("Extern instance method says: ")
   m.IP()
 }
 func (*Mixed) IP() {
@@ -74,7 +78,7 @@ func (m *Mixed) IF() dafny.Int {
   return dafny.IntOf(2000).Plus(m.IG())
 }
 func (m *Mixed) IG() dafny.Int {
-  return m.n
+  return dafny.IntOf(2)
 }
 
 type AllExtern struct{}

Test/comp/ExternCtors-externs/Class.java

@@ -0,0 +1,19 @@
+package Library;
+
+import java.math.BigInteger;
+
+public class Class extends _ExternBase_Class {
+    private final BigInteger n;
+
+    public Class(BigInteger n) {
+        this.n = n;
+    }
+
+    public static void SayHi() {
+        System.out.println("Hello!");
+    }
+
+    public BigInteger Get() {
+        return n;
+    }
+}

Test/comp/ExternCtors-externs/Library.cs

@@ -0,0 +1,19 @@
+using System.Numerics;
+
+namespace Library {
+  public partial class Class {
+    private readonly BigInteger n;
+
+    public Class(BigInteger n) {
+      this.n = n;
+    }
+
+    public static void SayHi() {
+      System.Console.WriteLine("Hello!");
+    }
+
+    public BigInteger Get() {
+      return n;
+    }
+  }
+}

Test/comp/ExternCtors-externs/Library.go

@@ -0,0 +1,31 @@
+// FIXME: Test currently fails on Go
+
+package Library
+
+import (
+	"dafny"
+	"fmt"
+)
+
+type Class struct{ n dafny.Int }
+
+func New_Class_(n dafny.Int) *Class {
+	return &Class{n}
+}
+
+func (obj *Class) Get() dafny.Int {
+	return obj.n
+}
+
+// have to implement this because the Go backend can't mix Dafny and Go code :-\
+
+func (obj *Class) Print() {
+	fmt.Printf("My value is %d\n", obj.n)
+}
+
+type CompanionStruct_Class_ struct{}
+var Companion_Class_ = CompanionStruct_Class_{}
+
+func (CompanionStruct_Class_) SayHi() {
+	fmt.Println("Hello!");
+}

Test/comp/ExternCtors-externs/Library.js

@@ -0,0 +1,21 @@
+// FIXME Test currently fails on JavaScript
+
+let Library = (function() {
+    let $module = {};
+
+    $module.Class = class Class {
+        constructor(n) {
+            this.n = n;
+        }
+
+        static SayHi() {
+            process.stdout.write("Hello!\n");
+        }
+
+        Get() {
+            return this.n;
+        }
+    }
+
+    return $module;
+})();

Test/comp/ExternCtors.dfy

@@ -0,0 +1,23 @@
+// RUN: %dafny /compile:3 /compileTarget:cs "%s" ExternCtors-externs/Library.cs > "%t"
+// RUN: %dafny /compile:3 /compileTarget:java "%s" ExternCtors-externs/Class.java >> "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// FIXME: Extern constructors are currently broken in Go and JavaScript,
+// so they are omitted
+
+method Main() {
+  Library.Class.SayHi();
+  var obj := new Library.Class(42);
+  obj.Print();
+}
+
+module {:extern "Library"} Library {
+  class {:extern} Class {
+    constructor {:extern} (n: int)
+    static method {:extern} SayHi()
+    function method {:extern} Get() : int
+    method Print() {
+      print "My value is ", Get(), "\n";
+    }
+  }
+}

Test/comp/ExternCtors.dfy.expect

@@ -0,0 +1,8 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
+Hello!
+My value is 42
+
+Dafny program verifier finished with 1 verified, 0 errors
+Hello!
+My value is 42

Test/comp/Mixed.java

@@ -3,12 +3,6 @@
 import java.math.BigInteger;
 
 public class Mixed extends _ExternBase_Mixed {
-    private final BigInteger n;
-
-    public Mixed(BigInteger n) {
-        this.n = n;
-    }
-
     public static void P() {
         System.out.println("Mixed.P");
     }
@@ -21,6 +15,6 @@ public static BigInteger G() {
     }
     @Override
     public BigInteger IG() {
-        return n;
+        return BigInteger.valueOf(2);
     }
 }