From f3984fff46bb887542d651d17999d7f5fdb37221 Mon Sep 17 00:00:00 2001
From: Matus Tejiscak <ziman@functor.sk>
Date: Sat, 19 Sep 2020 14:57:45 +0200
Subject: [PATCH] Remove more redundancy.

---
 src/Data/String/Iterator.idr | 45 ------------------------------------
 src/Text/Lexer/Core.idr      |  9 ++------
 2 files changed, 2 insertions(+), 52 deletions(-)
 delete mode 100644 src/Data/String/Iterator.idr

diff --git a/src/Data/String/Iterator.idr b/src/Data/String/Iterator.idr
deleted file mode 100644
index 75dc8f8f7..000000000
--- a/src/Data/String/Iterator.idr
+++ /dev/null
@@ -1,45 +0,0 @@
--- This is a copy of the module in contrib.
--- We can't use that module because it would break bootstrapping.
-module Data.String.Iterator
-
-export
-record StringIterator where
-  constructor MkSI
-  string : String
-
-  -- backend-dependent offset into the string
-  -- see prim__readChar below
-  offset : Int
-
-export
-fromString : String -> StringIterator
-fromString s = MkSI s 0
-
-private
-data ReadResult
-  = EOF
-  | Character Char Int  -- character, width
-
--- takes a backend-dependent offset into the string
--- on ML-based backends, this is in bytes
--- in Scheme, this is in codepoints
-private
-%foreign "scheme:read-string-char"
-prim__readChar : Int -> String -> ReadResult
-
-export
-uncons : StringIterator -> Maybe (Char, StringIterator)
-uncons (MkSI s ofs) =
-  case prim__readChar ofs s of
-    EOF => Nothing
-    Character ch width => Just (ch, MkSI s (ofs + width))
-
-export
-foldl : (a -> Char -> a) -> a -> String -> a
-foldl f acc s = loop 0 acc
-  where
-    loop : Int -> a -> a
-    loop ofs acc =
-      case prim__readChar ofs s of
-        EOF => acc
-        Character ch width => loop (ofs + width) (f acc ch)
diff --git a/src/Text/Lexer/Core.idr b/src/Text/Lexer/Core.idr
index fe51bf71d..15c007520 100644
--- a/src/Text/Lexer/Core.idr
+++ b/src/Text/Lexer/Core.idr
@@ -164,11 +164,6 @@ tokenise pred line col acc tmap str
                            line', col', rest)
                Nothing => getFirstToken ts str
 
--- to avoid breaking the bootstrap,
--- we can't depend on the stdlib version of fastUnpack here
-%foreign "scheme:string-unpack"
-fastUnpack : String -> List Char
-
 ||| Given a mapping from lexers to token generating functions (the
 ||| TokenMap a) and an input string, return a list of recognised tokens,
 ||| and the line, column, and remainder of the input at the first point in the
@@ -176,12 +171,12 @@ fastUnpack : String -> List Char
 export
 lex : TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lex tmap str
-    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (Lexer.Core.fastUnpack str) in
+    = let (ts, (l, c, str')) = tokenise (const False) 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, fastPack str'))
 
 export
 lexTo : (WithBounds a -> Bool) ->
         TokenMap a -> String -> (List (WithBounds a), (Int, Int, String))
 lexTo pred tmap str
-    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (Lexer.Core.fastUnpack str) in
+    = let (ts, (l, c, str')) = tokenise pred 0 0 [] tmap (fastUnpack str) in
           (ts, (l, c, fastPack str'))