--- a/src/Tools/Haskell/Haskell.thy Sat Jul 31 11:40:37 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Sat Jul 31 12:14:45 2021 +0200
@@ -25,7 +25,8 @@
Bytes,
make, unmake, pack, unpack,
empty, null, length, index, all, any,
- head, last, take, drop, concat, trim_line
+ head, last, take, drop, concat, trim_line,
+ singleton
)
where
@@ -33,9 +34,11 @@
import qualified Data.ByteString.Short as ShortByteString
import Data.ByteString.Short (ShortByteString)
+import qualified Data.ByteString as ByteString
import Data.ByteString (ByteString)
import qualified Data.List as List
import Data.Word (Word8)
+import Data.Array (Array, array, (!))
type Bytes = ShortByteString
@@ -85,6 +88,14 @@
concat :: [Bytes] -> Bytes
concat = mconcat
+singletons :: Array Word8 Bytes
+singletons =
+ array (minBound, maxBound) $!
+ [(i, make (ByteString.singleton i)) | i <- [minBound .. maxBound]]
+
+singleton :: Word8 -> Bytes
+singleton b = singletons ! b
+
trim_line :: Bytes -> Bytes
trim_line s =
if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then take (n - 2) s
--- a/src/Tools/Haskell/Test.thy Sat Jul 31 11:40:37 2021 +0200
+++ b/src/Tools/Haskell/Test.thy Sat Jul 31 12:14:45 2021 +0200
@@ -18,7 +18,7 @@
GHC.new_project dir
{name = "isabelle",
depends =
- ["bytestring", "containers", "network", "split", "text", "threads", "uuid"],
+ ["array", "bytestring", "containers", "network", "split", "text", "threads", "uuid"],
modules = modules};
in
writeln (Generated_Files.execute dir \<open>Build\<close> "mv Isabelle src && isabelle ghc_stack build")