Rename DafnyStdLibs -> Std, make collections modules not plural

Source/DafnyStandardLibraries/CONTRIBUTING.md

@@ -142,7 +142,7 @@ There are a couple of things to watch out for when importing libraries from the
   and one under `src/dafny`. The latter is a copy refactored to nest all modules under a top-level
   `Dafny` module to reduce the risk of naming conflicts. This is a great idea,
   but it turns out that using "Dafny" conflicts with some Dafny runtime symbols,
-  so these libraries use `DafnyStdLib` instead. You will probably find you have to adjust
+  so these libraries use `Std` instead. You will probably find you have to adjust
   documentation examples accordingly.
 
   When the latter copy exists, prefer to use it along with its the Markdown documentation,

Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticExamples.dfy

@@ -1,7 +1,7 @@
 module ArithmeticExamples {
-  import opened DafnyStdLibs.Arithmetic.Logarithm
-  import opened DafnyStdLibs.Arithmetic.Power
-  import opened DafnyStdLibs.Arithmetic.Mul
+  import opened Std.Arithmetic.Logarithm
+  import opened Std.Arithmetic.Power
+  import opened Std.Arithmetic.Mul
 
   /* log_b(m * n) = log_b(m) + log_b(n) if m and n are also powers of b */
   lemma LogProductRule(b: nat, x: nat, y: nat)
@@ -19,7 +19,7 @@ module ArithmeticExamples {
     LemmaLogPow(b, y);
   }
 
-  module DecimalLittleEndian refines DafnyStdLibs.Arithmetic.LittleEndianNat {
+  module DecimalLittleEndian refines Std.Arithmetic.LittleEndianNat {
     function BASE(): nat {
       10
     }

Source/DafnyStandardLibraries/examples/Arithmetic/ArithmeticTests.dfy

@@ -1,11 +1,11 @@
 module ArithmeticTests {
-  import opened DafnyStdLibs.Arithmetic.Logarithm
-  import opened DafnyStdLibs.Arithmetic.Power
-  import opened DafnyStdLibs.Arithmetic.Mul
-  import opened DafnyStdLibs.Arithmetic.Power2
-  import opened DafnyStdLibs.Arithmetic.MulInternals
-  import opened DafnyStdLibs.Arithmetic.ModInternals
-  import opened DafnyStdLibs.Arithmetic.DivInternals
+  import opened Std.Arithmetic.Logarithm
+  import opened Std.Arithmetic.Power
+  import opened Std.Arithmetic.Mul
+  import opened Std.Arithmetic.Power2
+  import opened Std.Arithmetic.MulInternals
+  import opened Std.Arithmetic.ModInternals
+  import opened Std.Arithmetic.DivInternals
 
   method {:test} TestMul() {
     for i := -10 to 10 {

Source/DafnyStandardLibraries/examples/Base64Examples.dfy

@@ -1,7 +1,7 @@
 module Base64Examples {
-  import opened DafnyStdLibs.Base64
-  import opened DafnyStdLibs.BoundedInts
-  import opened DafnyStdLibs.Wrappers
+  import opened Std.Base64
+  import opened Std.BoundedInts
+  import opened Std.Wrappers
 
   method CheckEncodeDecode(uints: seq<uint8>, bytes: seq<bv8>) {
     expect Decode(Encode(uints)) == Success(uints);

Source/DafnyStandardLibraries/examples/BoundedIntExamples.dfy

@@ -1,4 +1,4 @@
-import opened DafnyStdLibs.BoundedInts
+import opened Std.BoundedInts
 
 lemma BoundedIntUser(x: uint32, z: nat16)
   ensures TWO_TO_THE_15 * 2 == TWO_TO_THE_16
@@ -15,7 +15,7 @@ method {:test} UseExterns() {
 }
 
 module {:extern} {:dummyImportMember "NonDefault", true} Externs {
-  import opened DafnyStdLibs.BoundedInts
+  import opened Std.BoundedInts
   class {:extern} NonDefault {
     static method {:extern} SquareNativeInt(i: int32) returns (r: int32)
   }

Source/DafnyStandardLibraries/examples/CollectionsExamples.dfy

@@ -17,8 +17,8 @@ module CollectionsExamples {
 
   module SeqExamples {
 
-    import opened DafnyStdLibs.Wrappers
-    import opened DafnyStdLibs.Collections.Seqs
+    import opened Std.Wrappers
+    import opened Std.Collections.Seq
     import opened Helpers
 
     // A sequence that's long enough to be non-trivial
@@ -116,8 +116,8 @@ module CollectionsExamples {
 
   module SetExamples {
 
-    import opened DafnyStdLibs.Wrappers
-    import opened DafnyStdLibs.Collections.Sets
+    import opened Std.Wrappers
+    import opened Std.Collections.Set
     import opened Helpers
 
     method {:test} TestSetRange() {
@@ -137,8 +137,8 @@ module CollectionsExamples {
 
   module MapsExamples {
 
-    import opened DafnyStdLibs.Wrappers
-    import opened DafnyStdLibs.Collections.Maps
+    import opened Std.Wrappers
+    import opened Std.Collections.Map
     import opened Helpers
 
     const m := map[1 := 10, 2 := 20, 3 := 30]
@@ -160,8 +160,8 @@ module CollectionsExamples {
 
   module ImapsExamples {
 
-    import opened DafnyStdLibs.Wrappers
-    import opened DafnyStdLibs.Collections.Imaps
+    import opened Std.Wrappers
+    import opened Std.Collections.Imap
     import opened Helpers
 
     const m := imap[1 := 10, 2 := 20, 3 := 30]
@@ -175,9 +175,9 @@ module CollectionsExamples {
 
   module ArraysExamples {
 
-    import opened DafnyStdLibs.Wrappers
-    import opened DafnyStdLibs.Relations
-    import opened DafnyStdLibs.Collections.Arrays
+    import opened Std.Wrappers
+    import opened Std.Relations
+    import opened Std.Collections.Array
     import opened Helpers
 
     method {:test} TestBinarySearch() {

Source/DafnyStandardLibraries/examples/DynamicArrayExamples.dfy

@@ -1,6 +1,6 @@
 module DynamicArrayExamples {
-  import opened DafnyStdLibs.DynamicArray
-  import opened DafnyStdLibs.BoundedInts
+  import opened Std.DynamicArray
+  import opened Std.BoundedInts
 
   method {:test} Ensure() {
     var arr := new DynamicArray<int>();

Source/DafnyStandardLibraries/examples/FileIO/ReadBytesFromFile.dfy

@@ -4,7 +4,7 @@
  *******************************************************************************/
 
 module ReadBytesFromFile {
-  import DafnyStdLibs.FileIO
+  import Std.FileIO
 
   method {:test} Test() {
     // TODO: extern function for the expected error prefix

Source/DafnyStandardLibraries/examples/FileIO/WriteBytesToFile.dfy

@@ -4,7 +4,7 @@
  *******************************************************************************/
 
 module WriteBytesToFile {
-  import DafnyStdLibs.FileIO
+  import Std.FileIO
 
   method {:test} Test() {
     // TODO: extern function for the expected error prefix

Source/DafnyStandardLibraries/examples/FunctionsExamples.dfy

@@ -1,6 +1,6 @@
 module FunctionExamples {
 
-  import opened DafnyStdLibs.Functions
+  import opened Std.Functions
 
   const square := (x: int) => x * x
   lemma TestInjective()

Source/DafnyStandardLibraries/examples/Helpers.dfy

@@ -4,7 +4,7 @@
  *******************************************************************************/
 
 module Helpers {
-  import opened DafnyStdLibs.Wrappers
+  import opened Std.Wrappers
     // TODO: consider tweaking /testContracts to support this use case better.
   method AssertAndExpect(p: bool, maybeMsg: Option<string> := None) requires p {
     match maybeMsg {

Source/DafnyStandardLibraries/examples/RelationExamples.dfy

@@ -1,6 +1,6 @@
 module RelationExamples {
 
-  import opened DafnyStdLibs.Relations
+  import opened Std.Relations
 
   const partialOrdering := (a: int, b: int) => !(a == 9 && b == 10) && a <= b
   lemma TestRelationProperties()

Source/DafnyStandardLibraries/examples/StringsExamples.dfy

@@ -1,6 +1,6 @@
 module StringsExamples {
-  import opened DafnyStdLibs.Strings
-  import opened DafnyStdLibs.Wrappers
+  import opened Std.Strings
+  import opened Std.Wrappers
 
   method {:test} TestOfInt() {
     expect OfInt(0) == "0";

Source/DafnyStandardLibraries/examples/UnicodeExamples.dfy

@@ -6,7 +6,7 @@
 
 module UnicodeExamples {
   module BaseExamples {
-    import opened DafnyStdLibs.Unicode.Base
+    import opened Std.Unicode.Base
     import opened Helpers
 
     const TEST_ASSIGNED_PLANE_CODE_POINTS: set<CodePoint> := {
@@ -32,9 +32,9 @@ module UnicodeExamples {
   }
 
   module Utf8EncodingFormExamples {
-    import opened DafnyStdLibs.Unicode.Base
-    import opened DafnyStdLibs.Unicode.Utf8EncodingForm
-    import opened DafnyStdLibs.Wrappers
+    import opened Std.Unicode.Base
+    import opened Std.Unicode.Utf8EncodingForm
+    import opened Std.Wrappers
     import opened Helpers
 
     method {:test} TestEmptySequenceIsWellFormed() {
@@ -89,9 +89,9 @@ module UnicodeExamples {
   }
 
   module Utf16EncodingFormExamples {
-    import opened DafnyStdLibs.Unicode.Base
-    import opened DafnyStdLibs.Unicode.Utf16EncodingForm
-    import opened DafnyStdLibs.Wrappers
+    import opened Std.Unicode.Base
+    import opened Std.Unicode.Utf16EncodingForm
+    import opened Std.Wrappers
     import opened Helpers
 
     method {:test} TestEmptySequenceIsWellFormed() {
@@ -142,12 +142,12 @@ module UnicodeExamples {
   }
 
   module UnicodeStringsWithUnicodeCharExamples {
-    import opened DafnyStdLibs.BoundedInts
-    import opened DafnyStdLibs.Unicode.Base
-    import opened DafnyStdLibs.Wrappers
+    import opened Std.BoundedInts
+    import opened Std.Unicode.Base
+    import opened Std.Wrappers
     import opened Helpers
 
-    import UnicodeStrings = DafnyStdLibs.Unicode.UnicodeStringsWithUnicodeChar
+    import UnicodeStrings = Std.Unicode.UnicodeStringsWithUnicodeChar
 
     const currenciesStr := "\U{24}\U{A3}\U{20AC}\U{1F4B0}"
     const currenciesUtf8: seq<uint8> := [0x24] + [0xC2, 0xA3] + [0xE2, 0x82, 0xAC] + [0xF0, 0x9F, 0x92, 0xB0]
@@ -178,10 +178,10 @@ module UnicodeExamples {
   }
 
   module Utf8EncodingSchemeExamples {
-    import opened DafnyStdLibs.Unicode.Base
-    import opened DafnyStdLibs.Unicode.Utf8EncodingForm
-    import EncodingScheme = DafnyStdLibs.Unicode.Utf8EncodingScheme
-    import opened DafnyStdLibs.Wrappers
+    import opened Std.Unicode.Base
+    import opened Std.Unicode.Utf8EncodingForm
+    import EncodingScheme = Std.Unicode.Utf8EncodingScheme
+    import opened Std.Wrappers
     import opened Helpers
 
     const currenciesUtf8: CodeUnitSeq := [0x24] + [0xC2, 0xA3] + [0xE2, 0x82, 0xAC] + [0xF0, 0x9F, 0x92, 0xB0]

Source/DafnyStandardLibraries/examples/WrappersExamples.dfy

@@ -1,4 +1,4 @@
-import opened DafnyStdLibs.Wrappers
+import opened Std.Wrappers
 
 // ------ Demo for Option ----------------------------
 // We use Option when we don't need to pass around a reason for the failure,

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/DivMod.dfy

@@ -10,7 +10,7 @@
 former takes arguments and may be more stable and less reliant on Z3
 heuristics. The latter includes automation and its use requires less effort*/
 
-module DafnyStdLibs.Arithmetic.DivMod {
+module Std.Arithmetic.DivMod {
 
   import opened DivInternals
   import DivINL = DivInternalsNonlinear

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/DivInternals.dfy

@@ -16,7 +16,7 @@ This may produce "surprising" results for negative values.
 For example, -3 div 5 is -1 and -3 mod 5 is 2.
 Note this is consistent: -3 * -1 + 2 == 5 */
 
-module DafnyStdLibs.Arithmetic.DivInternals {
+module Std.Arithmetic.DivInternals {
 
   import opened GeneralInternals
   import opened ModInternals

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/GeneralInternals.dfy

@@ -6,7 +6,7 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module DafnyStdLibs.Arithmetic.GeneralInternals {
+module Std.Arithmetic.GeneralInternals {
 
   /* this predicate is primarily used as a trigger */
   ghost predicate IsLe(x: int, y: int)

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/ModInternals.dfy

@@ -16,7 +16,7 @@ This may produce "surprising" results for negative values.
 For example, -3 div 5 is -1 and -3 mod 5 is 2.
 Note this is consistent: -3 * -1 + 2 == 5 */
 
-module DafnyStdLibs.Arithmetic.ModInternals {
+module Std.Arithmetic.ModInternals {
 
   import opened GeneralInternals
   import opened Mul

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Internal/MulInternals.dfy

@@ -8,7 +8,7 @@
 
 /* lemmas and functions in this file are used in the proofs in Mul.dfy */
 
-module DafnyStdLibs.Arithmetic.MulInternals {
+module Std.Arithmetic.MulInternals {
 
   import opened GeneralInternals
   import opened MulInternalsNonlinear

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/LittleEndianNat.dfy

@@ -11,12 +11,12 @@ Little endian interpretation of a sequence of numbers with a given base. The
 first element of a sequence is the least significant position; the last
 element is the most significant position.
  */
-abstract module DafnyStdLibs.Arithmetic.LittleEndianNat {
+abstract module Std.Arithmetic.LittleEndianNat {
 
   import opened DivMod
   import opened Mul
   import opened Power
-  import opened Collections.Seqs
+  import opened Collections.Seq
   import opened Logarithm
 
   function BASE(): nat

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Logarithm.dfy

@@ -1,4 +1,4 @@
-module DafnyStdLibs.Arithmetic.Logarithm {
+module Std.Arithmetic.Logarithm {
   import opened Mul
   import opened DivMod
   import opened Power

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Mul.dfy

@@ -10,7 +10,7 @@
 former takes arguments and may be more stable and less reliant on Z3
 heuristics. The latter includes automation and its use requires less effort */
 
-module DafnyStdLibs.Arithmetic.Mul {
+module Std.Arithmetic.Mul {
 
   import MulINL = MulInternalsNonlinear
   import opened MulInternals

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power.dfy

@@ -10,7 +10,7 @@
 former takes arguments and may be more stable and less reliant on Z3
 heuristics. The latter includes automation and its use requires less effort */
 
-module DafnyStdLibs.Arithmetic.Power {
+module Std.Arithmetic.Power {
   import opened DivMod
   import opened GeneralInternals
   import opened Mul

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Arithmetic/Power2.dfy

@@ -10,7 +10,7 @@
 former takes arguments and may be more stable and less reliant on Z3
 heuristics. The latter includes automation and its use requires less effort */
 
-module DafnyStdLibs.Arithmetic.Power2 {
+module Std.Arithmetic.Power2 {
   import opened GeneralInternals
   import opened MulInternals
   import opened Power

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/Strings.dfy

@@ -1,7 +1,7 @@
 /**
 The Strings module enables converting between numbers such as nat and int, and String
  */
-module DafnyStdLibs.Strings {
+module Std.Strings {
   import opened Wrappers
   import opened Arithmetic.Power
   import opened Arithmetic.Logarithm

Source/DafnyStandardLibraries/src/DafnyStdLibs/DisableNonLinearArithmetic/dfyconfig.toml

@@ -8,7 +8,7 @@ library = [
   "../EnableNonLinearArithmetic/Arithmetic/Internals/DivInternalsNonlinear.dfy",
   "../EnableNonLinearArithmetic/Arithmetic/Internals/ModInternalsNonlinear.dfy",
   "../EnableNonLinearArithmetic/Arithmetic/Internals/MulInternalsNonlinear.dfy",
-  "../EnableNonLinearArithmetic/Collections/Seqs.dfy",
+  "../EnableNonLinearArithmetic/Collections/Seq.dfy",
   "../EnableNonLinearArithmetic/Wrappers.dfy",
   "../EnableNonLinearArithmetic/Relations.dfy",
   "../EnableNonLinearArithmetic/Math.dfy",

Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/DivInternalsNonlinear.dfy

@@ -6,7 +6,7 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module DafnyStdLibs.Arithmetic.DivInternalsNonlinear {
+module Std.Arithmetic.DivInternalsNonlinear {
 
   /* WARNING: Think three times before adding to this file, as nonlinear
   verification is highly unstable! */

Source/DafnyStandardLibraries/src/DafnyStdLibs/EnableNonLinearArithmetic/Arithmetic/Internals/ModInternalsNonlinear.dfy

@@ -6,7 +6,7 @@
  *  SPDX-License-Identifier: MIT 
  *******************************************************************************/
 
-module DafnyStdLibs.Arithmetic.ModInternalsNonlinear {
+module Std.Arithmetic.ModInternalsNonlinear {
 
   /* WARNING: Think three times before adding to this file, as nonlinear
   verification is highly unstable! */