[ refactor ] Remove Data.Strings module (#1607)

.github/workflows/ci-ubuntu-combined.yml

@@ -12,7 +12,7 @@ on:
       - main
 
 env:
-  IDRIS2_VERSION: 0.3.0 # For previous-version build
+  IDRIS2_VERSION: 0.4.0 # For previous-version build
   SCHEME: scheme
 
 jobs:
@@ -86,7 +86,7 @@ jobs:
           wget https://www.idris-lang.org/idris2-src/idris2-$IDRIS2_VERSION.tgz
           tar zxvf idris2-$IDRIS2_VERSION.tgz
           cd Idris2-$IDRIS2_VERSION
-          make bootstrap-build
+          make bootstrap
           cd ..
       - name: Install previous version
         run: |

CHANGELOG.md

@@ -17,6 +17,14 @@
   and reverts to whole program compilation. Incremental compilation is currently
   supported only by the Chez Scheme back end.
 
+### Library Changes
+
+#### Prelude
+
+Changed
+
+- Removed `Data.Strings`.  Use `Data.String` instead.
+
 ## v0.4.0
 
 ### Syntax changes

benchmark/benchmarks/mergeStr/mergeStr.idr

@@ -1,5 +1,5 @@
 import System.File
-import Data.Strings
+import Data.String
 import Data.List
 
 -- read in a dictionary, shuffle and then resort

benchmark/benchmarks/spellcheck/spellcheck.idr

@@ -1,5 +1,5 @@
 import System.File
-import Data.Strings
+import Data.String
 import Data.List
 
 main : IO ()

docs/source/tutorial/interfaces.rst

@@ -350,7 +350,7 @@ which reads a number from the console, returning a value of the form
 
 .. code-block:: idris
 
-    import Data.Strings
+    import Data.String
 
     readNumber : IO (Maybe Nat)
     readNumber = do

docs/source/typedd/typedd.rst

@@ -31,7 +31,7 @@ In ``Average.idr``, add:
 
 .. code-block:: idris
 
-    import Data.Strings -- for `words`
+    import Data.String -- for `words`
     import Data.List -- for `length` on lists
 
 In ``AveMain.idr`` and ``Reverse.idr`` add:
@@ -58,7 +58,7 @@ Chapter 4
 
 For the reasons described above:
 
-+ In ``DataStore.idr``, add ``import System.REPL`` and ``import Data.Strings``
++ In ``DataStore.idr``, add ``import System.REPL`` and ``import Data.String``
 + In ``SumInputs.idr``, add ``import System.REPL``
 + In ``TryIndex.idr``, add an implicit argument:
 
@@ -78,9 +78,9 @@ Chapter 5
 There is no longer a ``Cast`` instance from ``String`` to ``Nat``, because its
 behaviour of returing Z if the ``String`` wasn't numeric was thought to be
 confusing and potentially error prone. Instead, there is ``stringToNatOrZ`` in
-``Data.Strings`` which at least has a clearer name. So:
+``Data.String`` which at least has a clearer name. So:
 
-In ``Loops.idr`` and ``ReadNum.idr`` add ``import Data.Strings`` and change ``cast`` to
+In ``Loops.idr`` and ``ReadNum.idr`` add ``import Data.String`` and change ``cast`` to
 ``stringToNatOrZ``
 
 In ``ReadNum.idr``, since functions must now be ``covering`` by default, add
@@ -89,15 +89,15 @@ a ``partial`` annotation to ``readNumber_v2``.
 Chapter 6
 ---------
 
-In ``DataStore.idr`` and ``DataStoreHoles.idr``, add ``import Data.Strings`` and
+In ``DataStore.idr`` and ``DataStoreHoles.idr``, add ``import Data.String`` and
 ``import System.REPL``. Also in ``DataStore.idr``, the ``schema`` argument to
 ``display`` is required for matching, so change the type to:
 
 .. code-block:: idris
 
     display : {schema : _} -> SchemaType schema -> String
 
-In ``TypeFuns.idr`` add ``import Data.Strings``
+In ``TypeFuns.idr`` add ``import Data.String``
 
 Chapter 7
 ---------
@@ -158,7 +158,7 @@ Chapter 9
 
 In ``Hangman.idr``:
 
-+ Add ``import Data.Strings``, ``import Data.Vect.Elem`` and ``import Decidable.Equality``
++ Add ``import Data.String``, ``import Data.Vect.Elem`` and ``import Decidable.Equality``
 + ``removeElem`` pattern matches on ``n``, so it needs to be written in its
   type:
 
@@ -335,12 +335,12 @@ now uses a safer type for the number of shifts:
 
 
 In ``ArithCmd.idr``, update ``DivBy``, ``randoms``, and ``import Data.Bits``
-as above. Also add ``import Data.Strings`` for ``Strings.toLower``.
+as above. Also add ``import Data.String`` for ``String.toLower``.
 
-In ``ArithCmd.idr``, update ``DivBy``, ``randoms``, ``import Data.Bits``
-and ``import Data.Strings`` as above. Also,
-since export rules are per-namespace now, rather than per-file, you need to
-export ``(>>=)`` from the namespaces ``CommandDo`` and ``ConsoleDo``.
+In ``ArithCmd.idr``, update ``DivBy``, ``randoms``, ``import Data.Bits`` and
+``import Data.String`` as above.  Also, since export rules are per-namespace
+now, rather than per-file, you need to export ``(>>=)`` from the namespaces
+``CommandDo`` and ``ConsoleDo``.
 
 In ``ArithCmdDo.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO``
 also have to be ``export``. Also, update ``randoms`` and ``import Data.Bits`` as above.
@@ -350,11 +350,11 @@ In ``StreamFail.idr``, add a ``partial`` annotation to ``labelWith``.
 Chapter 12
 ----------
 
-For reasons described above: In ``ArithState.idr``, add ``import Data.Strings``
-and ``import Data.Bits`` and update ``randoms``.
-Also the ``(>>=)`` operators need to be set as ``export`` since they are in their
-own namespaces, and in ``getRandom``, ``DivBy`` needs to take additional
-arguments ``div`` and ``rem``.
+For reasons described above: In ``ArithState.idr``, add ``import Data.String``
+and ``import Data.Bits`` and update ``randoms``.  Also the ``(>>=)`` operators
+need to be set as ``export`` since they are in their own namespaces, and in
+``getRandom``, ``DivBy`` needs to take additional arguments ``div`` and
+``rem``.
 
 In ``ArithState.idr``, since ``(>>=)`` is ``export``, ``Command`` and ``ConsoleIO``
 also have to be ``export``.
@@ -392,7 +392,7 @@ In ``StackIO.idr``:
 
 In ``Vending.idr``:
 
-+ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``strToInput``
++ Add ``import Data.String`` and change ``cast`` to ``stringToNatOrZ`` in ``strToInput``
 + In ``MachineCmd`` type, add an implicit argument to ``(>>=)`` data constructor:
 
 .. code-block:: idris
@@ -449,14 +449,14 @@ Chapter 14
 
 In ``ATM.idr``:
 
-+ Add ``import Data.Strings`` and change ``cast`` to ``stringToNatOrZ`` in ``runATM``
++ Add ``import Data.String`` and change ``cast`` to ``stringToNatOrZ`` in ``runATM``
 
 In ``Hangman.idr``, add:
 
 .. code-block:: idris
 
     import Data.Vect.Elem -- `Elem` now has its own submodule
-    import Data.Strings -- for `toUpper`
+    import Data.String -- for `toUpper`
     import Data.List -- for `nub`
 
 + In ``Loop`` namespace, export ``GameLoop`` type and its data constructors:

libs/base/Control/App/FileIO.idr

@@ -3,7 +3,7 @@ module Control.App.FileIO
 import Control.App
 
 import Data.List
-import Data.Strings
+import Data.String
 import System.File
 
 %default covering

libs/base/System.idr

@@ -2,7 +2,7 @@ module System
 
 import public Data.So
 import Data.List
-import Data.Strings
+import Data.String
 
 %default total
 

libs/base/System/File.idr

@@ -3,7 +3,7 @@ module System.File
 import public Data.Fuel
 
 import Data.List
-import Data.Strings
+import Data.String
 import System.Info
 
 %default total

libs/base/base.ipkg

@@ -64,7 +64,6 @@ modules = Control.App,
           Data.So,
           Data.Stream,
           Data.String,
-          Data.Strings,
           Data.These,
           Data.Vect,
           Data.Vect.Elem,

libs/contrib/Control/Validation.idr

@@ -13,7 +13,7 @@ module Control.Validation
 import Control.Monad.Identity
 import Control.Monad.Error.Either
 import Data.Nat
-import Data.Strings
+import Data.String
 import Data.Vect
 import Decidable.Equality
 

libs/contrib/Data/String/Extra.idr

@@ -3,7 +3,7 @@ module Data.String.Extra
 import Data.List
 import Data.List1
 import Data.Nat
-import Data.Strings
+import Data.String
 
 %default total
 

libs/contrib/Data/String/Interpolation.idr

@@ -2,7 +2,7 @@
 ||| Not as fancy
 module Data.String.Interpolation
 
-import Data.Strings
+import Data.String
 
 namespace Data.String.Interpolation.Basic
   %inline

libs/contrib/Data/String/Parser.idr

@@ -3,7 +3,7 @@ module Data.String.Parser
 import public Control.Monad.Identity
 import Control.Monad.Trans
 
-import Data.Strings
+import Data.String
 import Data.Fin
 import Data.List
 import Data.List1

libs/contrib/Language/JSON/Data.idr

@@ -4,7 +4,7 @@ import Data.Bits
 import Data.List
 import Data.Nat
 import Data.String.Extra
-import Data.Strings
+import Data.String
 
 %default total
 

libs/contrib/System/Console/GetOpt.idr

@@ -10,7 +10,7 @@ import Control.Monad.State
 import Data.List
 import Data.List1
 import Data.Maybe
-import Data.Strings
+import Data.String
 
 %default total
 

libs/contrib/System/Directory/Tree.idr

@@ -3,7 +3,7 @@ module System.Directory.Tree
 import Data.DPair
 import Data.List
 import Data.Nat
-import Data.Strings
+import Data.String
 import System.Directory
 import System.Path
 

libs/contrib/System/Path.idr

@@ -4,7 +4,7 @@ import Data.List
 import Data.List1
 import Data.Maybe
 import Data.Nat
-import Data.Strings
+import Data.String
 import Data.String.Extra
 
 import Text.Token
@@ -108,14 +108,14 @@ Show Body where
 export
 Show Volume where
   show (UNC server share) = "\\\\" ++ server ++ "\\" ++ share
-  show (Disk disk) = Strings.singleton disk ++ ":"
+  show (Disk disk) = String.singleton disk ++ ":"
 
 ||| Displays the path in the format of this platform.
 export
 Show Path where
   show path =
     let
-      sep = Strings.singleton dirSeparator
+      sep = String.singleton dirSeparator
       showVol = maybe "" show path.volume
       showRoot = if path.hasRoot then sep else ""
       showBody = join sep $ map show path.body

libs/contrib/Text/Lexer/Core.idr

@@ -4,7 +4,7 @@ import public Control.Delayed
 import Data.Bool
 import Data.List
 import Data.Nat
-import Data.Strings
+import Data.String
 
 ||| A language of token recognisers.
 ||| @ consumes If `True`, this recogniser is guaranteed to consume at

libs/contrib/Text/PrettyPrint/Prettyprinter/Doc.idr

@@ -3,7 +3,7 @@ module Text.PrettyPrint.Prettyprinter.Doc
 import Data.List
 import public Data.List1
 import Data.Maybe
-import Data.Strings
+import Data.String
 import public Data.String.Extra
 
 %default total

libs/contrib/Text/PrettyPrint/Prettyprinter/Render/HTML.idr

@@ -1,7 +1,7 @@
 module Text.PrettyPrint.Prettyprinter.Render.HTML
 
 import Data.List
-import Data.Strings
+import Data.String
 
 export
 htmlEscape : String -> String

libs/contrib/Text/PrettyPrint/Prettyprinter/Render/String.idr

@@ -1,6 +1,6 @@
 module Text.PrettyPrint.Prettyprinter.Render.String
 
-import Data.Strings
+import Data.String
 import Data.String.Extra
 import Text.PrettyPrint.Prettyprinter.Doc
 

libs/contrib/Text/PrettyPrint/Prettyprinter/Render/Terminal.idr

@@ -1,7 +1,7 @@
 module Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 import Data.Maybe
-import Data.Strings
+import Data.String
 import public Control.ANSI
 import Control.Monad.ST
 import Text.PrettyPrint.Prettyprinter.Doc

libs/contrib/Text/PrettyPrint/Prettyprinter/Util.idr

@@ -1,7 +1,7 @@
 module Text.PrettyPrint.Prettyprinter.Util
 
 import Data.List
-import Data.Strings
+import Data.String
 import Text.PrettyPrint.Prettyprinter.Doc
 import Text.PrettyPrint.Prettyprinter.Render.String
 

libs/network/Network/Socket/Data.idr

@@ -7,7 +7,7 @@ module Network.Socket.Data
 
 import Data.List
 import Data.List1
-import Data.Strings
+import Data.String
 
 -- ------------------------------------------------------------ [ Type Aliases ]
 

src/Compiler/Common.idr

@@ -20,7 +20,7 @@ import Data.IOArray
 import Data.List
 import Data.List1
 import Libraries.Data.NameMap
-import Data.Strings as String
+import Data.String as String
 
 import Idris.Env