Java fixes

Binaries/DafnyRuntime.go

@@ -439,8 +439,8 @@ func (seq Seq) Cardinality() Int {
 }
 
 // CardinalityInt finds the length of the sequence as an int.
-func (seq Seq) CardinalityInt() Int {
-	return seq.Len()
+func (seq Seq) CardinalityInt() int {
+	return seq.LenInt()
 }
 
 // Contains finds whether the value is equal to any element in the sequence.

Source/Dafny/Compiler-go.cs

@@ -3383,13 +3383,7 @@ static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram
       var tgtFilename = Path.Combine(tgtDir, pkgName + ".go");
 
       Directory.CreateDirectory(tgtDir);
-      using (var rd = new StreamReader(new FileStream(externFilename, FileMode.Open, FileAccess.Read))) {
-        using (var wr = new StreamWriter(new FileStream(tgtFilename, FileMode.OpenOrCreate, FileAccess.Write))) {
-          while (rd.ReadLine() is string line) {
-            wr.WriteLine(line);
-          }
-        }
-      }
+      File.Copy(externFilename, tgtFilename, overwrite: true);
 
       string relTgtFilename;
       var cwd = Directory.GetCurrentDirectory();

Source/Dafny/Compiler-js.cs

@@ -63,6 +63,13 @@ protected override IClassWriter CreateClass(string name, bool isExtern, string/*
         WriteRuntimeTypeDescriptorsFormals(typeParameters, false, w);
       }
       var fieldWriter = w.NewBlock(")");
+      if (isExtern) {
+        fieldWriter.Write("super(");
+        if (typeParameters != null) {
+          WriteRuntimeTypeDescriptorsFormals(typeParameters, false, w);
+        }
+        fieldWriter.WriteLine(");");
+      }
       if (fullPrintName != null) {
         fieldWriter.WriteLine("this._tname = \"{0}\";", fullPrintName);
       }

Source/Dafny/Compiler.cs

@@ -90,6 +90,7 @@ protected interface IClassWriter {
       TextWriter/*?*/ ErrorWriter();
       void Finish();
     }
+    protected virtual bool IncludeExternMembers { get => false; }
     protected IClassWriter CreateClass(string name, List<TypeParameter>/*?*/ typeParameters, TargetWriter wr) {
       return CreateClass(name, false, null, typeParameters, null, null, wr);
     }
@@ -697,7 +698,7 @@ public void Compile(Program program, TargetWriter wrx) {
             }
             var classIsExtern = false;
             if (include) {
-              classIsExtern = !DafnyOptions.O.DisallowExterns && Attributes.Contains(cl.Attributes, "extern");
+              classIsExtern = !DafnyOptions.O.DisallowExterns && Attributes.Contains(cl.Attributes, "extern") || cl.IsDefaultClass && Attributes.Contains(cl.Module.Attributes, "extern");
               if (classIsExtern && cl.Members.TrueForAll(member => member.IsGhost || Attributes.Contains(member.Attributes, "extern"))) {
                 include = false;
               }
@@ -1012,7 +1013,6 @@ void CompileClassMembers(TopLevelDeclWithMembers c, IClassWriter classWriter) {
         }
       }
 
-      List<TypeParameter> l = new List<TypeParameter>();
       foreach (MemberDecl member in c.Members) {
         if (member is Field) {
           var f = (Field)member;
@@ -1082,14 +1082,13 @@ void CompileClassMembers(TopLevelDeclWithMembers c, IClassWriter classWriter) {
           } else if (c is TraitDecl && !FieldsInTraits && !f.IsStatic) {
             TargetWriter wSet;
             classWriter.CreateGetterSetter(IdName(f), f.Type, f.tok, false, false, member, out wSet);
-          } else if (c is ClassDecl && f.Type.IsTypeParameter) {
-            EmitTypeParams(classWriter, l, f, errorWr);
           } else {
             classWriter.DeclareField(IdName(f), f.IsStatic, false, f.Type, f.tok, DefaultValue(f.Type, errorWr, f.tok, true));
           }
         } else if (member is Function) {
           var f = (Function)member;
-          if (f.Body == null && !(c is TraitDecl && !f.IsStatic) && !(!DafnyOptions.O.DisallowExterns && Attributes.Contains(f.Attributes, "dllimport"))) {
+          if (f.Body == null && !(c is TraitDecl && !f.IsStatic) &&
+              !(!DafnyOptions.O.DisallowExterns && (Attributes.Contains(f.Attributes, "dllimport") || IncludeExternMembers && Attributes.Contains(f.Attributes, "extern")))) {
             // A (ghost or non-ghost) function must always have a body, except if it's an instance function in a trait.
             if (Attributes.Contains(f.Attributes, "axiom") || (!DafnyOptions.O.DisallowExterns && Attributes.Contains(f.Attributes, "extern"))) {
               // suppress error message
@@ -1112,7 +1111,8 @@ void CompileClassMembers(TopLevelDeclWithMembers c, IClassWriter classWriter) {
           }
         } else if (member is Method) {
           var m = (Method)member;
-          if (m.Body == null && !(c is TraitDecl && !m.IsStatic) && !(!DafnyOptions.O.DisallowExterns && Attributes.Contains(m.Attributes, "dllimport"))) {
+          if (m.Body == null && !(c is TraitDecl && !m.IsStatic) &&
+              !(!DafnyOptions.O.DisallowExterns && (Attributes.Contains(m.Attributes, "dllimport") || IncludeExternMembers && Attributes.Contains(m.Attributes, "extern")))) {
             // A (ghost or non-ghost) method must always have a body, except if it's an instance method in a trait.
             if (Attributes.Contains(m.Attributes, "axiom") || (!DafnyOptions.O.DisallowExterns && Attributes.Contains(m.Attributes, "extern"))) {
               // suppress error message
@@ -1137,24 +1137,10 @@ void CompileClassMembers(TopLevelDeclWithMembers c, IClassWriter classWriter) {
           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member
         }
       }
-      if (l.Count > 0){
-        CreateDefaultConstructor(c, classWriter, l);
-      }
 
       thisContext = null;
     }
 
-    protected virtual void CreateDefaultConstructor(TopLevelDeclWithMembers c, IClassWriter cw, List<TypeParameter> l) {
-      Contract.Requires(c != null);
-      Contract.Requires(cw != null);
-    }
-
-    protected virtual void EmitTypeParams(IClassWriter classWriter, List<TypeParameter> l, Field f, TextWriter errorWr) {
-      classWriter.DeclareField(IdName(f), f.IsStatic, false, f.Type, f.tok,
-        DefaultValue(f.Type, errorWr, f.tok, true));
-
-    }
-
     void CheckHandleWellformed(ClassDecl cl, TextWriter/*?*/ errorWr) {
       Contract.Requires(cl != null);
       var isHandle = true;
@@ -1254,7 +1240,7 @@ private void CompileFunction(Function f, IClassWriter cw) {
       Contract.Requires(f != null);
       Contract.Requires(cw != null);
 
-      var w = cw.CreateFunction(IdName(f), f.TypeArgs, f.Formals, f.ResultType, f.tok, f.IsStatic, true, f);
+      var w = cw.CreateFunction(IdName(f), f.TypeArgs, f.Formals, f.ResultType, f.tok, f.IsStatic, !f.IsExtern(out _, out _), f);
       if (w != null) {
         CompileReturnBody(f.Body, w);
       }
@@ -1264,7 +1250,7 @@ private void CompileMethod(Method m, IClassWriter cw) {
       Contract.Requires(cw != null);
       Contract.Requires(m != null);
 
-      var w = cw.CreateMethod(m, true);
+      var w = cw.CreateMethod(m, !m.IsExtern(out _, out _));
       if (w != null) {
         int nonGhostOutsCount = 0;
         foreach (var p in m.Outs) {

Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyMap.java

@@ -130,6 +130,10 @@ public int size() {
         return innerMap.size();
     }
 
+    public int cardinalityInt() {
+        return size();
+    }
+
     @Override
     public boolean isEmpty() {
         return innerMap.isEmpty();

Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnyMultiset.java

@@ -70,6 +70,14 @@ public BigInteger cardinality() {
         return b;
     }
 
+    public int cardinalityInt() {
+        int b = 0;
+        for (BigInteger big : innerMap.values()) {
+            b += big.intValue();
+        }
+        return b;
+    }
+
     // Determines if the current object is a subset of the DafnyMultiSet passed in. Requires that the input
     // Dafny MultiSet is not null.
     public boolean isSubsetOf(DafnyMultiset<T> other) {

Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySequence.java

@@ -136,6 +136,10 @@ public T select(BigInteger i) {
 
     public abstract int length();
 
+    public final int cardinalityInt() {
+        return length();
+    }
+
     public abstract DafnySequence<T> update(int i, T t);
 
     public DafnySequence<T> update(BigInteger b, T t) {

Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/DafnySet.java

@@ -1,5 +1,6 @@
 package dafny;
 
+import java.math.BigInteger;
 import java.util.*;
 
 // A class that is equivalent to the implementation of Set in Dafny
@@ -104,6 +105,10 @@ public int size() {
         return innerSet.size();
     }
 
+    public int cardinalityInt() {
+        return size();
+    }
+
     public boolean isEmpty() {
         return innerSet.isEmpty();
     }

Test/comp/AllDafny.java

@@ -0,0 +1,5 @@
+package Library;
+
+public class AllDafny extends _ExternBase_AllDafny {
+    // All functionality implemented by generated base class
+}

Test/comp/AllExtern.java

@@ -1,6 +1,5 @@
 package Library;
 
-// The Java compiler doesn't support Dafny methods in extern libraries
 public class AllExtern {
     public static void P() {
         System.out.println("AllExtern.P");

Test/comp/Class.dfy

@@ -123,6 +123,7 @@ method Main() {
   // Upcast via function call
   CallEm(c, t, i);
   DependentStaticConsts.Test();
+  NewtypeWithMethods.Test();
 }
 
 module Module1 {
@@ -150,3 +151,25 @@ module DependentStaticConsts {
     print Suite[B], " ", Suite[D], "\n";  // hi later
   }
 }
+
+newtype NewtypeWithMethods = x | 0 <= x < 42 {
+  function method double() : int {
+    this as int * 2
+  }
+
+  method divide(d : NewtypeWithMethods) returns (q : int, r : int) requires d != 0 {
+    q := (this / d) as int;
+    r := (this % d) as int;
+  }
+
+  static method Test() {
+    var a : NewtypeWithMethods := 21;
+    var b : NewtypeWithMethods;
+    b := 4;
+    var q : int;
+    var r : int;
+    q, r := a.divide(b);
+
+    print a, " ", b, " ", a.double(), " ", q, " ", r, "\n";
+  }
+}

Test/comp/Class.dfy.expect

@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 12 verified, 0 errors
 true true false
 103 103 103 106 106 106
 203 17 0 18 8 9 69 70
@@ -9,8 +9,9 @@ true true false
 0 18 9 70
 0 18 9 70
 hi later
+21 4 42 5 1
 
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 12 verified, 0 errors
 true true false
 103 103 103 106 106 106
 203 17 0 18 8 9 69 70
@@ -20,8 +21,9 @@ true true false
 0 18 9 70
 0 18 9 70
 hi later
+21 4 42 5 1
 
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 12 verified, 0 errors
 true true false
 103 103 103 106 106 106
 203 17 0 18 8 9 69 70
@@ -31,8 +33,9 @@ true true false
 0 18 9 70
 0 18 9 70
 hi later
+21 4 42 5 1
 
-Dafny program verifier finished with 8 verified, 0 errors
+Dafny program verifier finished with 12 verified, 0 errors
 true true false
 103 103 103 106 106 106
 203 17 0 18 8 9 69 70
@@ -42,3 +45,4 @@ true true false
 0 18 9 70
 0 18 9 70
 hi later
+21 4 42 5 1

Test/comp/Extern.dfy

@@ -1,18 +1,22 @@
 // RUN: %dafny /compile:3 /compileTarget:cs "%s" Extern2.cs > "%t"
 // RUN: %dafny /compile:3 /compileTarget:js "%s" Extern3.js >> "%t"
 // RUN: %dafny /compile:3 /compileTarget:go "%s" Extern4.go >> "%t"
-// RUN: %dafny /compile:3 /compileTarget:java "%s" LibClass.java Mixed.java AllExtern.java >> "%t"
+// RUN: %dafny /compile:3 /compileTarget:java "%s" LibClass.java OtherClass.java AllDafny.java Mixed.java AllExtern.java >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main() {
   print "Hello\n";
   var x, y := Library.LibClass.CallMeInt(30);
   var z := Library.LibClass.CallMeNative(44, true);
-  print x, " ", y, " ", z, "\n";
+  var w := Library.LibClass.CallMeInAnotherClass();
+  print x, " ", y, " ", z, " ", w, "\n";
 
   Library.AllDafny.M();
   Library.Mixed.M();
-  Library.Mixed.P();
+  print Library.Mixed.F(), "\n";
+  var m := new Library.Mixed();
+  m.IM();
+  print m.IF(), "\n";
   Library.AllExtern.P();
   assert Library.AllDafny.Seven() == Library.Mixed.Seven() == Library.AllExtern.Seven();
 }
@@ -22,16 +26,24 @@ module {:extern "Library"} Library {
   class {:extern "LibClass"} LibClass {
     static method {:extern} CallMeInt(x: int) returns (y: int, z: int)
     static method {:extern} CallMeNative(x: MyInt, b: bool) returns (y: MyInt)
+    static method {:extern "Library.OtherClass", "CallMe"} CallMeInAnotherClass() returns (w : object)
   }
 
-  class AllDafny {
+  class {:extern} AllDafny {
     static function Seven(): int { 7 }
     static method M() { print "AllDafny.M\n"; }
   }
   class {:extern} Mixed {
+    constructor() { }
     static function Seven(): int { 7 }
-    static method M() { print "Mixed.M\n"; }
+    static method M() { print "Extern static method says: "; P(); }
     static method {:extern} P()
+    method IM() { print "Extern instance method says: "; IP(); }
+    method {:extern} IP()
+    static function method F() : int { 1000 + G() }
+    static function method {:extern} G() : int
+    function method IF() : int { 2000 + IG() }
+    function method {:extern} IG() : int
   }
   class {:extern} AllExtern {
     static function Seven(): int { 7 }

Test/comp/Extern.dfy.expect

@@ -1,32 +1,40 @@
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
 Hello
-31 62 45
+31 62 45 OtherClass.CallMe
 AllDafny.M
-Mixed.M
-Mixed.P
+Extern static method says: Mixed.P
+1001
+Extern instance method says: Mixed.IP
+2002
 AllExtern.P
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
 Hello
-31 62 45
+31 62 45 OtherClass.CallMe
 AllDafny.M
-Mixed.M
-Mixed.P
+Extern static method says: Mixed.P
+1001
+Extern instance method says: Mixed.IP
+2002
 AllExtern.P
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
 Hello
-31 62 45
+31 62 45 OtherClass.CallMe
 AllDafny.M
-Mixed.M
-Mixed.P
+Extern static method says: Mixed.P
+1001
+Extern instance method says: Mixed.IP
+2002
 AllExtern.P
 
-Dafny program verifier finished with 2 verified, 0 errors
+Dafny program verifier finished with 6 verified, 0 errors
 Hello
-31 62 45
+31 62 45 OtherClass.CallMe
 AllDafny.M
-Mixed.M
-Mixed.P
+Extern static method says: Mixed.P
+1001
+Extern instance method says: Mixed.IP
+2002
 AllExtern.P