Use replaceable modules to ensure that the notarget interface is the …

…same as the language specific ones

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -583,7 +583,12 @@ public void PrintModuleDefinition(CompilationData compilation, ModuleDefinition
       }
       wr.Write("{0} ", module.Name);
       if (module.Implements != null) {
-        wr.Write("refines {0} ", module.Implements.Target);
+        var kindString = module.Implements.Kind switch {
+          ImplementationKind.Refinement => "refines",
+          ImplementationKind.Replacement => "replaces",
+          _ => throw new ArgumentOutOfRangeException()
+        };
+        wr.Write($"{kindString} {module.Implements.Target} ");
       }
       if (!module.TopLevelDecls.Any()) {
         wr.WriteLine("{ }");

Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java

@@ -7,11 +7,13 @@ public class AtomicBox<T> {
     private volatile T val;
 
     public AtomicBox(T t) {
-        val = t;
     }
 
-    public AtomicBox(dafny.TypeDescriptor td, T t) {
-        this(t);
+    public AtomicBox(dafny.TypeDescriptor td) {
+    }
+
+    public void __ctor(T t) {
+        val = t;
     }
 
     public void Put(T t) {

Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs

@@ -10,6 +10,8 @@ public MutableMap() {
             map = new ConcurrentDictionary<K, V>();
         }
 
+        public void __ctor() { }
+
         public Dafny.ISet<K> Keys() {
             return Dafny.Set<K>.FromCollection(map.Keys);
         }
@@ -58,11 +60,14 @@ public class AtomicBox<T> {
         private T val;
         private Lock l;
 
-        public AtomicBox(T t) {
-            val = t;
+        public AtomicBox() {
             l = new Lock();
         }
 
+        public void __ctor(T t) {
+          val = t;
+        }
+
         public void Put(T t) {
             l.__Lock();
             val = t;
@@ -81,6 +86,9 @@ public class Lock {
 
         private static System.Threading.Mutex mut = new System.Threading.Mutex();
 
+        public void __ctor() {
+        }
+
         public void __Lock() {
             mut.WaitOne();
         }

Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java

@@ -6,6 +6,8 @@ public class Lock {
 
     private final ReentrantLock lock = new ReentrantLock();
 
+    public void __ctor() {}
+
     public void __Lock() {
         lock.lock();
     }

Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java

@@ -19,6 +19,8 @@ public MutableMap(dafny.TypeDescriptor<K> td_K, dafny.TypeDescriptor<V> td_V) {
         this.td_V = td_V;
         map = new ConcurrentHashMap<K, V>();
     }
+
+    public void __ctor() { }
 
     public dafny.DafnySet<K> Keys() {
         return new dafny.DafnySet<K>(Collections.list(map.keys()));

Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js

@@ -3,9 +3,9 @@
 *  SPDX-License-Identifier: MIT
 *******************************************************************************/
 
-var Std_ConcurrentInterface = Std_ConcurrentInterface || {};
-var FileIOInternalExterns = FileIOInternalExterns || {};
-FileIOInternalExterns.__default = (function() {
+var Std_Concurrent = Std_Concurrent || {};
+var Std_FileIOInternalExterns = Std_FileIOInternalExterns || {};
+Std_FileIOInternalExterns.__default = (function() {
   const buffer = require("buffer");
   const fs = require("fs");
   const nodePath = require("path");

Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy

@@ -6,7 +6,6 @@ Std.GoConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -34,8 +33,6 @@ Std.GoConcurrent replaces Concurrent {
   class {:extern} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 

Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy

@@ -3,7 +3,6 @@ module {:extern} Std.JavaConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -31,8 +30,6 @@ module {:extern} Std.JavaConcurrent replaces Concurrent {
   class {:extern "AtomicBox"} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 

Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy

@@ -4,7 +4,6 @@ module {:compile false} Std.JavaScriptConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -32,8 +31,6 @@ module {:compile false} Std.JavaScriptConcurrent replaces Concurrent {
   class {:extern} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 

Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy

@@ -3,7 +3,6 @@ module {:extern} {:compile false} Std.CSharpConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -31,8 +30,6 @@ module {:extern} {:compile false} Std.CSharpConcurrent replaces Concurrent {
   class {:extern} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 

Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy → Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-java-cs-js-go-py.dfy

@@ -47,6 +47,10 @@ replaceable module Std.Concurrent {
     // Invariant on values this box may hold
     ghost const inv: T -> bool
 
+    constructor (ghost inv: T -> bool, t: T)
+      requires inv(t)
+      ensures this.inv == inv
+
     method Get() returns (t: T)
       reads {}
       ensures inv(t)
@@ -68,6 +72,9 @@ replaceable module Std.Concurrent {
     // Invariant on key-value pairs this map may hold
     ghost const inv: (K, V) -> bool
 
+    constructor (ghost inv: (K, V) -> bool)
+      ensures this.inv == inv
+
     method Keys() returns (keys: set<K>)
       reads {}
       ensures forall k <- keys :: exists v :: inv(k, v)

Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy

@@ -3,7 +3,6 @@ module {:compile false} Std.PythonConcurrent replaces Concurrent {
   class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
-      ensures this.inv == inv
 
     ghost predicate Valid()
     {
@@ -31,8 +30,6 @@ module {:compile false} Std.PythonConcurrent replaces Concurrent {
   class {:extern} AtomicBox<T> ... {
 
     constructor {:extern} {:axiom} (ghost inv: T -> bool, t: T)
-      requires inv(t)
-      ensures this.inv == inv
 
     ghost predicate Valid() { true }
 

Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy

@@ -13,7 +13,7 @@ module
   // But it makes debugging the translated output a little clearer.
   {:compile false}
 {:extern}
-{:dummyImportMember "Dummy_", true}
+{:dummyImportMember "Dummy__", true}
 Std.GoFileIOInternalExterns replaces FileIOInternalExterns {
   method
     {:extern}

Source/DafnyStandardLibraries/src/Std_Concurrent.py

@@ -10,6 +10,9 @@
 
 
 class MutableMap:
+    def ctor__(self):
+        pass
+
     def __init__(self) -> None:
         self.map = dict()
         self.lock = Lock()
@@ -66,8 +69,12 @@ def Size(self):
 
 
 class AtomicBox:
-    def __init__(self, t) -> None:
+    def __init__(self) -> None:
+        pass
+
+    def ctor__(self, t):
         self.boxed = t
+        pass
 
     def Get(self):
         return self.boxed
@@ -76,6 +83,9 @@ def Put(self, t):
         self.boxed = t
 
 class Lock:
+    def ctor__(self):
+        pass
+
     def __init__(self) -> None:
         self.lock = threading.Lock()
 

Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go

@@ -1,4 +1,4 @@
-package DafnyStdLibs_Concurrent
+package Std_Concurrent
 
 import (
   _dafny "dafny"
@@ -56,7 +56,7 @@ func (_this *MutableMap) ParentTraits_() []*_dafny.TraitID {
 }
 var _ _dafny.TraitOffspring = &MutableMap{}
 
-func (_this *MutableMap) Ctor__(inv func (interface{}, interface{}) bool) {
+func (_this *MutableMap) Ctor__() {
   {
   }
 }
@@ -188,7 +188,7 @@ func (_this *AtomicBox) ParentTraits_() []*_dafny.TraitID {
 }
 var _ _dafny.TraitOffspring = &AtomicBox{}
 
-func (_this *AtomicBox) Ctor__(inv func (interface{}) bool, t interface{}) {
+func (_this *AtomicBox) Ctor__(t interface{}) {
   {
     _this.mu.Lock()
     _this.Boxed = t

Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go

@@ -1,4 +1,4 @@
-package DafnyStdLibs_FileIOInternalExterns
+package Std_FileIOInternalExterns
 
 import (
 	_dafny "dafny"
@@ -8,7 +8,12 @@ import (
 
 type Dummy__ struct{}
 
-func INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) {
+type CompanionStruct_Default___ struct {
+}
+var Companion_Default___ = CompanionStruct_Default___ {
+}
+
+func (_static *CompanionStruct_Default___) INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) {
 	p := _dafny.SequenceVerbatimString(path, false)
 	dat, err := os.ReadFile(p)
 	if err != nil {
@@ -19,7 +24,7 @@ func INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead
 	return false, datAsSequence, _dafny.EmptySeq
 }
 
-func INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) {
+func (_static *CompanionStruct_Default___) INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (isError bool, errorMsg _dafny.Sequence) {
 	p := _dafny.SequenceVerbatimString(path, false)
 
 	// Create directories
@@ -32,4 +37,4 @@ func INTERNAL__WriteBytesToFile(path _dafny.Sequence, bytes _dafny.Sequence) (is
 		return true, errAsSequence
 	}
 	return false, _dafny.EmptySeq
-}
+}