# HG changeset patch
# User wenzelm
# Date 1627726485 -7200
# Node ID c26f4ec59835d895b2aaaba82d4c6f6ec6d00f33
# Parent  be6b813926d187a496324614a473335c08daf590
more operations;

diff -r be6b813926d1 -r c26f4ec59835 src/Tools/Haskell/Haskell.thy
--- 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
diff -r be6b813926d1 -r c26f4ec59835 src/Tools/Haskell/Test.thy
--- 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")