diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo index 815f253050..d5ef3edcaa 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo index 245f678b57..3f73a8610c 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo index 6059092c78..ac45478e52 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo index 48df095041..beab34ae3b 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo index f320bf2c8e..27523da94c 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo index a6de78d0e2..78945df6ba 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo differ diff --git a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo index 1044b55011..aba9385db4 100644 Binary files a/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo and b/Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo differ diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/AtomicBox.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java similarity index 88% rename from Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/AtomicBox.java rename to Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java index 3102dd56e8..33d38947d7 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/AtomicBox.java +++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/AtomicBox.java @@ -1,4 +1,4 @@ -package DafnyStdLibsExterns.Concurrent; +package Std.Concurrent; import dafny.*; diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/Concurrent.cs b/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs similarity index 98% rename from Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/Concurrent.cs rename to Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs index 28e3698ab2..becbb8d78c 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/Concurrent.cs +++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/Concurrent.cs @@ -1,4 +1,4 @@ -namespace Concurrent { +namespace Std.Concurrent { using System.Collections.Concurrent; using Std.Wrappers; diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/Lock.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java similarity index 85% rename from Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/Lock.java rename to Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java index fdc64e926d..a07168500c 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/Lock.java +++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/Lock.java @@ -1,4 +1,4 @@ -package DafnyStdLibsExterns.Concurrent; +package Std.Concurrent; import java.util.concurrent.locks.ReentrantLock; diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/MutableMap.java b/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java similarity index 97% rename from Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/MutableMap.java rename to Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java index 55f6641655..1fc171ec63 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/Concurrent/MutableMap.java +++ b/Source/DafnyStandardLibraries/src/Std/Concurrent/MutableMap.java @@ -1,4 +1,4 @@ -package DafnyStdLibsExterns.Concurrent; +package Std.Concurrent; import dafny.*; import Std.Wrappers.*; diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.cs b/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.cs similarity index 90% rename from Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.cs rename to Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.cs index d3b59d9710..1f420d70fa 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.cs +++ b/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 { /// /// Attempts to read all bytes from the file at the given path, and outputs the following values: /// @@ -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. /// - public static void INTERNAL_ReadBytesFromFile(ISequence path, out bool isError, out ISequence bytesRead, + public static void INTERNAL__ReadBytesFromFile(ISequence path, out bool isError, out ISequence bytesRead, out ISequence errorMsg) { isError = true; bytesRead = Sequence.Empty; @@ -70,7 +70,7 @@ public static void INTERNAL_ReadBytesFromFile(ISequence 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. /// - public static void INTERNAL_WriteBytesToFile(ISequence path, ISequence bytes, out bool isError, out ISequence errorMsg) { + public static void INTERNAL__WriteBytesToFile(ISequence path, ISequence bytes, out bool isError, out ISequence errorMsg) { isError = true; errorMsg = Sequence.Empty; try { diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.js b/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js similarity index 90% rename from Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.js rename to Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/FileIO.js index 3465ed0725..b327d81031 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.js +++ b/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) diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.java b/Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/__default.java similarity index 94% rename from Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.java rename to Source/DafnyStandardLibraries/src/Std/FileIOInternalExterns/__default.java index 60f0bb6292..00d5acf12f 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibsExterns/FileIO.java +++ b/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: *
@@ -34,7 +34,7 @@ public class FileIO { * It is the responsibility of library code to construct an equivalent {@code Result} value. */ public static Tuple3, DafnySequence> - INTERNAL_ReadBytesFromFile(DafnySequence path) { + INTERNAL__ReadBytesFromFile(DafnySequence path) { try { final Path pathObj = dafnyStringToPath(path); final DafnySequence 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> - INTERNAL_WriteBytesToFile(DafnySequence path, DafnySequence bytes) { + INTERNAL__WriteBytesToFile(DafnySequence path, DafnySequence bytes) { try { final Path pathObj = dafnyStringToPath(path); createParentDirs(pathObj); diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy index 33b63a73a1..0296e711b5 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-go.dfy +++ b/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 ... { diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy index 9591fa090a..5e7f5c6f1a 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-java.dfy +++ b/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 ... { + class {:extern} MutableMap ... { constructor {:extern} {:axiom} (ghost inv: (K, V) -> bool) ensures this.inv == inv diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy index ee3f86d01f..ca0355b00d 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-js.dfy +++ b/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 ... { @@ -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 diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy index 91fce33071..1079d09ffe 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-notarget-cs.dfy +++ b/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 ... { diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy index ac9d5edcdd..3b61ab9195 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/Concurrent-py.dfy +++ b/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 ... { diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy index d5e555a679..c7f69bd07d 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/ConcurrentInterface-notarget-java-cs-js-go-py.dfy +++ b/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 diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy index 83c73156c8..7f87ee27fe 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-go.dfy +++ b/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) diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy index 30ad3a2ea1..ed6d7a8d43 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-java-cs-js.dfy +++ b/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, errorMsg: string) - method - {:extern "DafnyStdLibsExterns.FileIO", "INTERNAL_WriteBytesToFile"} - INTERNAL_WriteBytesToFile(path: string, bytes: seq) + method {:extern} INTERNAL_WriteBytesToFile(path: string, bytes: seq) returns (isError: bool, errorMsg: string) } \ No newline at end of file diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-notarget.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-notarget-java-cs-js-go-py.dfy similarity index 92% rename from Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-notarget.dfy rename to Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-notarget-java-cs-js-go-py.dfy index 1069b18eb8..264a6c924c 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-notarget.dfy +++ b/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, errorMsg: string) diff --git a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-py.dfy b/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-py.dfy index a5582df662..8f74f02e7d 100644 --- a/Source/DafnyStandardLibraries/src/Std/TargetSpecific/FileIOInternalExterns-py.dfy +++ b/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, errorMsg: string) - method - {:extern} - INTERNAL_WriteBytesToFile(path: string, bytes: seq) + method {:extern} INTERNAL_WriteBytesToFile(path: string, bytes: seq) returns (isError: bool, errorMsg: string) } \ No newline at end of file diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs_Concurrent/DafnyStdLibs_Concurrent.go b/Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go similarity index 100% rename from Source/DafnyStandardLibraries/src/DafnyStdLibs_Concurrent/DafnyStdLibs_Concurrent.go rename to Source/DafnyStandardLibraries/src/Std_Concurrent/Std_Concurrent.go diff --git a/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns/DafnyStdLibs_FileIOInternalExterns.go b/Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go similarity index 97% rename from Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns/DafnyStdLibs_FileIOInternalExterns.go rename to Source/DafnyStandardLibraries/src/Std_FileIOInternalExterns/Std_FileIOInternalExterns.go index 11e794b3f4..a5c1e88b9e 100644 --- a/Source/DafnyStandardLibraries/src/DafnyStdLibs_FileIOInternalExterns/DafnyStdLibs_FileIOInternalExterns.go +++ b/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)