Using replaceable modules

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

@@ -1,4 +1,4 @@
-package DafnyStdLibsExterns.Concurrent;
+package Std.Concurrent;
 
 import dafny.*;
 

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

@@ -1,4 +1,4 @@
-namespace Concurrent {
+namespace Std.Concurrent {
     using System.Collections.Concurrent;
     using Std.Wrappers;
 

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

@@ -1,4 +1,4 @@
-package DafnyStdLibsExterns.Concurrent;
+package Std.Concurrent;
 
 import java.util.concurrent.locks.ReentrantLock;
 

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

@@ -1,4 +1,4 @@
-package DafnyStdLibsExterns.Concurrent;
+package Std.Concurrent;
 
 import dafny.*;
 import Std.Wrappers.*;

Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.cs → Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.cs

@@ -3,13 +3,13 @@
 *  SPDX-License-Identifier: MIT
 *******************************************************************************/
 
-namespace DafnyStdLibsExterns {
+namespace Std.FileIOInternalExterns {
   using System;
   using System.IO;
 
   using Dafny;
 
-  public class FileIO {
+  public class __default {
     /// <summary>
     /// Attempts to read all bytes from the file at the given path, and outputs the following values:
     /// <list>
@@ -36,7 +36,7 @@ public class FileIO {
     /// We output these values individually because Result is not defined in the runtime but instead in library code.
     /// It is the responsibility of library code to construct an equivalent Result value.
     /// </summary>
-    public static void INTERNAL_ReadBytesFromFile(ISequence<Dafny.Rune> path, out bool isError, out ISequence<byte> bytesRead,
+    public static void INTERNAL__ReadBytesFromFile(ISequence<Dafny.Rune> path, out bool isError, out ISequence<byte> bytesRead,
       out ISequence<Dafny.Rune> errorMsg) {
       isError = true;
       bytesRead = Sequence<byte>.Empty;
@@ -70,7 +70,7 @@ public static void INTERNAL_ReadBytesFromFile(ISequence<Dafny.Rune> path, out bo
     /// We output these values individually because Result is not defined in the runtime but instead in library code.
     /// It is the responsibility of library code to construct an equivalent Result value.
     /// </summary>
-    public static void INTERNAL_WriteBytesToFile(ISequence<Dafny.Rune> path, ISequence<byte> bytes, out bool isError, out ISequence<Dafny.Rune> errorMsg) {
+    public static void INTERNAL__WriteBytesToFile(ISequence<Dafny.Rune> path, ISequence<byte> bytes, out bool isError, out ISequence<Dafny.Rune> errorMsg) {
       isError = true;
       errorMsg = Sequence<Rune>.Empty;
       try {

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

@@ -3,8 +3,9 @@
 *  SPDX-License-Identifier: MIT
 *******************************************************************************/
 
-var DafnyStdLibsExterns = DafnyStdLibsExterns || {};
-DafnyStdLibsExterns.FileIO = (function() {
+var Std_ConcurrentInterface = Std_ConcurrentInterface || {};
+var FileIOInternalExterns = FileIOInternalExterns || {};
+FileIOInternalExterns.__default = (function() {
   const buffer = require("buffer");
   const fs = require("fs");
   const nodePath = require("path");
@@ -21,7 +22,7 @@ DafnyStdLibsExterns.FileIO = (function() {
    * We return these values individually because `Result` is not defined in the runtime but instead in library code.
    * It is the responsibility of library code to construct an equivalent `Result` value.
    */
-  $module.INTERNAL_ReadBytesFromFile = function(path) {
+  $module.INTERNAL__ReadBytesFromFile = function(path) {
     const emptySeq = _dafny.Seq.of();
     try {
       const readOpts = { encoding: null };  // read as buffer, not string
@@ -45,7 +46,7 @@ DafnyStdLibsExterns.FileIO = (function() {
    * We return these values individually because `Result` is not defined in the runtime but instead in library code.
    * It is the responsibility of library code to construct an equivalent `Result` value.
    */
-  $module.INTERNAL_WriteBytesToFile = function(path, bytes) {
+  $module.INTERNAL__WriteBytesToFile = function(path, bytes) {
     try {
       const buf = buffer.Buffer.from(bytes);
       const pathStr = path.toVerbatimString(false)

Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.java → Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/__default.java

@@ -3,7 +3,7 @@
 *  SPDX-License-Identifier: MIT
 *******************************************************************************/
 
-package DafnyStdLibsExterns;
+package Std.FileIOInternalExterns;
 
 import java.io.IOException;
 import java.io.PrintWriter;
@@ -18,7 +18,7 @@
 import dafny.Tuple3;
 import dafny.TypeDescriptor;
 
-public class FileIO {
+public class __default {
     /**
      * Attempts to read all bytes from the file at {@code path}, and returns a tuple of the following values:
      * <dl>
@@ -34,7 +34,7 @@ public class FileIO {
      * It is the responsibility of library code to construct an equivalent {@code Result} value.
      */
     public static Tuple3<Boolean, DafnySequence<? extends Byte>, DafnySequence<? extends CodePoint>>
-        INTERNAL_ReadBytesFromFile(DafnySequence<? extends CodePoint> path) {
+        INTERNAL__ReadBytesFromFile(DafnySequence<? extends CodePoint> path) {
         try {
             final Path pathObj = dafnyStringToPath(path);
             final DafnySequence<Byte> readBytes = DafnySequence.fromBytes(Files.readAllBytes(pathObj));
@@ -58,7 +58,7 @@ public class FileIO {
      * It is the responsibility of library code to construct an equivalent {@code Result} value.
      */
     public static Tuple2<Boolean, DafnySequence<? extends CodePoint>>
-        INTERNAL_WriteBytesToFile(DafnySequence<? extends CodePoint> path, DafnySequence<? extends Byte> bytes) {
+        INTERNAL__WriteBytesToFile(DafnySequence<? extends CodePoint> path, DafnySequence<? extends Byte> bytes) {
         try {
             final Path pathObj = dafnyStringToPath(path);
             createParentDirs(pathObj);

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

@@ -1,8 +1,7 @@
 module
   {:compile false}
-{:extern "DafnyStdLibs_Concurrent"}
 {:dummyImportMember "Dummy__", true}
-Std.Concurrent refines ConcurrentInterface {
+Std.GoConcurrent replaces Concurrent {
 
   class {:extern} MutableMap<K(==), V(==)> ... {
 

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

@@ -1,6 +1,6 @@
-module {:extern "DafnyStdLibsExterns.Concurrent"} Std.Concurrent refines ConcurrentInterface {
+module {:extern} Std.JavaConcurrent replaces Concurrent {
 
-  class {:extern "MutableMap"} MutableMap<K(==), V(==)> ... {
+  class {:extern} MutableMap<K(==), V(==)> ... {
 
     constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool)
       ensures this.inv == inv

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

@@ -1,5 +1,5 @@
 
-module  {:extern "Std_ConcurrentDafny"} {:compile false} Std.Concurrent refines ConcurrentInterface {
+module {:compile false} Std.JavaScriptConcurrent replaces Concurrent {
 
   class {:extern} MutableMap<K(==), V(==)> ... {
 
@@ -55,7 +55,7 @@ module  {:extern "Std_ConcurrentDafny"} {:compile false} Std.Concurrent refines
 }
 
 // Dafny-native implementation, used to generate the extern implementation
-module Std.ConcurrentDafny {
+module {:extern "Std_Concurrent"} Std.ConcurrentDafny {
 
   import opened Wrappers
 

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

@@ -1,4 +1,4 @@
-module {:extern} {:compile false} Std.Concurrent refines ConcurrentInterface {
+module {:extern} {:compile false} Std.CSharpConcurrent replaces Concurrent {
 
   class {:extern} MutableMap<K(==), V(==)> ... {
 

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

@@ -1,4 +1,4 @@
-module {:compile false} Std.Concurrent refines ConcurrentInterface {
+module {:compile false} Std.PythonConcurrent replaces Concurrent {
 
   class {:extern} MutableMap<K(==), V(==)> ... {
 

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

@@ -1,4 +1,4 @@
-abstract module Std.ConcurrentInterface {
+replaceable module Std.Concurrent {
 
   import opened Wrappers
 

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

@@ -12,9 +12,9 @@ module
   // across multiple Go files under the same path.
   // But it makes debugging the translated output a little clearer.
   {:compile false}
-{:extern "DafnyStdLibs_FileIOInternalExterns"}
-{:dummyImportMember "INTERNAL__ReadBytesFromFile", false}
-Std.FileIOInternalExterns {
+{:extern}
+{:dummyImportMember "Dummy_", true}
+Std.GoFileIOInternalExterns replaces FileIOInternalExterns {
   method
     {:extern}
   INTERNAL_ReadBytesFromFile(path: string)

Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy

@@ -6,14 +6,10 @@
 /*
  * Private API - these should not be used elsewhere
  */
-module Std.FileIOInternalExterns {
-  method
-    {:extern "DafnyStdLibsExterns.FileIO", "INTERNAL_ReadBytesFromFile"}
-  INTERNAL_ReadBytesFromFile(path: string)
+module {:extern} Std.JavaCsJsFileIOInternalExterns replaces FileIOInternalExterns {
+  method {:extern} INTERNAL_ReadBytesFromFile(path: string)
     returns (isError: bool, bytesRead: seq<bv8>, errorMsg: string)
 
-  method
-    {:extern "DafnyStdLibsExterns.FileIO", "INTERNAL_WriteBytesToFile"}
-  INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
+  method {:extern} INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
     returns (isError: bool, errorMsg: string)
 }

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

@@ -6,7 +6,7 @@
 /*
  * Private API - these should not be used elsewhere
  */
-module Std.FileIOInternalExterns {
+replaceable module Std.FileIOInternalExterns {
   method
     INTERNAL_ReadBytesFromFile(path: string)
     returns (isError: bool, bytesRead: seq<bv8>, errorMsg: string)

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

@@ -9,14 +9,10 @@
 // {:compile false} is necessary here since otherwise the translation to Python
 // will create a Std_FileIOInternalExterns.py source file as well,
 // which the embedded version can't easily override.
-module {:compile false} Std.FileIOInternalExterns {
-  method
-    {:extern}
-  INTERNAL_ReadBytesFromFile(path: string)
+module {:extern} {:compile false} Std.PythonFileIOInternalExterns replaces FileIOInternalExterns {
+  method {:extern} INTERNAL_ReadBytesFromFile(path: string)
     returns (isError: bool, bytesRead: seq<bv8>, errorMsg: string)
 
-  method
-    {:extern}
-  INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
+  method {:extern} INTERNAL_WriteBytesToFile(path: string, bytes: seq<bv8>)
     returns (isError: bool, errorMsg: string)
 }

Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns/DafnyStdLibs_FileIOInternalExterns.go → Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go

@@ -6,6 +6,8 @@ import (
 	filepath "path/filepath"
 )
 
+type Dummy__ struct{}
+
 func INTERNAL__ReadBytesFromFile(path _dafny.Sequence) (isError bool, bytesRead _dafny.Sequence, errorMsg _dafny.Sequence) {
 	p := _dafny.SequenceVerbatimString(path, false)
 	dat, err := os.ReadFile(p)