# HG changeset patch # User wenzelm # Date 1627486218 -7200 # Node ID a8bbeb26665189cc029252e4d75b16ff75380fdb # Parent e249650504f3061e360ca10bcdf6b6065b5e64aa prefer Isabelle.Bytes, based on ShortByteString; diff -r e249650504f3 -r a8bbeb266651 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Wed Jul 28 15:39:19 2021 +0200 +++ b/src/Tools/Haskell/Haskell.thy Wed Jul 28 17:30:18 2021 +0200 @@ -8,6 +8,82 @@ imports Pure begin +generate_file "Isabelle/Bytes.hs" = \ +{- Title: Isabelle/Bytes.hs + Author: Makarius + LICENSE: BSD 3-clause (Isabelle) + +Compact byte strings. + +See \<^file>\$ISABELLE_HOME/src/Pure/General/bytes.ML\ +and \<^file>\$ISABELLE_HOME/src/Pure/General/bytes.scala\. +-} + +module Isabelle.Bytes ( + Bytes, + make, unmake, pack, unpack, + empty, null, length, index, all, any, + head, last, take, drop, concat, +) +where + +import Prelude hiding (null, length, all, any, head, last, take, drop, concat) + +import qualified Data.ByteString.Short as ShortByteString +import Data.ByteString.Short (ShortByteString) +import Data.ByteString (ByteString) +import qualified Data.List as List +import Data.Word (Word8) + + +type Bytes = ShortByteString + +make :: ByteString -> Bytes +make = ShortByteString.toShort + +unmake :: Bytes -> ByteString +unmake = ShortByteString.fromShort + +pack :: [Word8] -> Bytes +pack = ShortByteString.pack + +unpack :: Bytes -> [Word8] +unpack = ShortByteString.unpack + +empty :: Bytes +empty = ShortByteString.empty + +null :: Bytes -> Bool +null = ShortByteString.null + +length :: Bytes -> Int +length = ShortByteString.length + +index :: Bytes -> Int -> Word8 +index = ShortByteString.index + +all :: (Word8 -> Bool) -> Bytes -> Bool +all p = List.all p . unpack + +any :: (Word8 -> Bool) -> Bytes -> Bool +any p = List.any p . unpack + +head :: Bytes -> Word8 +head bytes = index bytes 0 + +last :: Bytes -> Word8 +last bytes = index bytes (length bytes - 1) + +take :: Int -> Bytes -> Bytes +take n = pack . List.take n . unpack + +drop :: Int -> Bytes -> Bytes +drop n = pack . List.drop n . unpack + +concat :: [Bytes] -> Bytes +concat = mconcat +\ + generate_file "Isabelle/UTF8.hs" = \ {- Title: Isabelle/UTF8.hs Author: Makarius @@ -35,7 +111,9 @@ import qualified Data.Text.Encoding.Error as Error import Data.ByteString (ByteString) -import Data.ByteString.Short (ShortByteString, toShort, fromShort) + +import qualified Isabelle.Bytes as Bytes +import Isabelle.Bytes (Bytes) class Recode a b where @@ -48,11 +126,11 @@ decode :: ByteString -> Text decode = Encoding.decodeUtf8With Error.lenientDecode -instance Recode Text ShortByteString where - encode :: Text -> ShortByteString - encode = toShort . encode - decode :: ShortByteString -> Text - decode = decode . fromShort +instance Recode Text Bytes where + encode :: Text -> Bytes + encode = Bytes.make . encode + decode :: Bytes -> Text + decode = decode . Bytes.unmake instance Recode String ByteString where encode :: String -> ByteString @@ -60,10 +138,10 @@ decode :: ByteString -> String decode = Text.unpack . decode -instance Recode String ShortByteString where - encode :: String -> ShortByteString +instance Recode String Bytes where + encode :: String -> Bytes encode = encode . Text.pack - decode :: ShortByteString -> String + decode :: Bytes -> String decode = Text.unpack . decode \ @@ -1699,11 +1777,13 @@ ) where -import Data.ByteString (ByteString) import Data.UUID (UUID) import qualified Data.UUID as UUID import Data.UUID.V4 (nextRandom) +import qualified Isabelle.Bytes as Bytes +import Isabelle.Bytes (Bytes) + type T = UUID @@ -1713,8 +1793,8 @@ parse_string :: String -> Maybe T parse_string = UUID.fromString -parse_bytes :: ByteString -> Maybe T -parse_bytes = UUID.fromASCIIBytes +parse_bytes :: Bytes -> Maybe T +parse_bytes = UUID.fromASCIIBytes . Bytes.unmake {- print -} @@ -1722,8 +1802,8 @@ string :: T -> String string = UUID.toString -bytes :: T -> ByteString -bytes = UUID.toASCIIBytes +bytes :: T -> Bytes +bytes = Bytes.make . UUID.toASCIIBytes {- random id -} @@ -1734,7 +1814,7 @@ random_string :: IO String random_string = string <$> random -random_bytes :: IO ByteString +random_bytes :: IO Bytes random_bytes = bytes <$> random \ @@ -1763,8 +1843,9 @@ import Prelude hiding (read) import Data.Maybe -import Data.ByteString (ByteString) import qualified Data.ByteString as ByteString +import qualified Isabelle.Bytes as Bytes +import Isabelle.Bytes (Bytes) import qualified Isabelle.UTF8 as UTF8 import qualified Isabelle.XML as XML import qualified Isabelle.YXML as YXML @@ -1778,19 +1859,19 @@ {- output operations -} -write :: Socket -> [ByteString] -> IO () -write = Socket.sendMany - -write_line :: Socket -> ByteString -> IO () +write :: Socket -> [Bytes] -> IO () +write socket = Socket.sendMany socket . map Bytes.unmake + +write_line :: Socket -> Bytes -> IO () write_line socket s = write socket [s, "\n"] {- input operations -} -read :: Socket -> Int -> IO ByteString +read :: Socket -> Int -> IO Bytes read socket n = read_body 0 [] where - result = ByteString.concat . reverse + result = Bytes.concat . reverse read_body len ss = if len >= n then return (result ss) else @@ -1798,27 +1879,27 @@ s <- Socket.recv socket (min (n - len) 8192) case ByteString.length s of 0 -> return (result ss) - m -> read_body (len + m) (s : ss)) - -read_block :: Socket -> Int -> IO (Maybe ByteString, Int) + m -> read_body (len + m) (Bytes.make s : ss)) + +read_block :: Socket -> Int -> IO (Maybe Bytes, Int) read_block socket n = do msg <- read socket n - let len = ByteString.length msg + let len = Bytes.length msg return (if len == n then Just msg else Nothing, len) -trim_line :: ByteString -> ByteString +trim_line :: Bytes -> Bytes trim_line s = - if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then ByteString.take (n - 2) s - else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then ByteString.take (n - 1) s + if n >= 2 && at (n - 2) == 13 && at (n - 1) == 10 then Bytes.take (n - 2) s + else if n >= 1 && (at (n - 1) == 13 || at (n - 1) == 10) then Bytes.take (n - 1) s else s where - n = ByteString.length s - at = ByteString.index s - -read_line :: Socket -> IO (Maybe ByteString) + n = Bytes.length s + at = Bytes.index s + +read_line :: Socket -> IO (Maybe Bytes) read_line socket = read_body [] where - result = trim_line . ByteString.pack . reverse + result = trim_line . Bytes.pack . reverse read_body bs = do s <- Socket.recv socket 1 case ByteString.length s of @@ -1831,16 +1912,16 @@ {- messages with multiple chunks (arbitrary content) -} -make_header :: [Int] -> [ByteString] +make_header :: [Int] -> [Bytes] make_header ns = [UTF8.encode (space_implode "," (map Value.print_int ns)), "\n"] -make_message :: [ByteString] -> [ByteString] -make_message chunks = make_header (map ByteString.length chunks) <> chunks - -write_message :: Socket -> [ByteString] -> IO () +make_message :: [Bytes] -> [Bytes] +make_message chunks = make_header (map Bytes.length chunks) <> chunks + +write_message :: Socket -> [Bytes] -> IO () write_message socket = write socket . make_message -parse_header :: ByteString -> [Int] +parse_header :: Bytes -> [Int] parse_header line = let res = map Value.parse_nat (space_explode ',' (UTF8.decode line)) @@ -1848,7 +1929,7 @@ if all isJust res then map fromJust res else error ("Malformed message header: " <> quote (UTF8.decode line)) -read_chunk :: Socket -> Int -> IO ByteString +read_chunk :: Socket -> Int -> IO Bytes read_chunk socket n = do res <- read_block socket n return $ @@ -1858,7 +1939,7 @@ error ("Malformed message chunk: unexpected EOF after " <> show len <> " of " <> show n <> " bytes") -read_message :: Socket -> IO (Maybe [ByteString]) +read_message :: Socket -> IO (Maybe [Bytes]) read_message socket = do res <- read_line socket case res of @@ -1868,27 +1949,26 @@ -- hybrid messages: line or length+block (with content restriction) -is_length :: ByteString -> Bool +is_length :: Bytes -> Bool is_length msg = - not (ByteString.null msg) && ByteString.all (\b -> 48 <= b && b <= 57) msg - -is_terminated :: ByteString -> Bool + not (Bytes.null msg) && Bytes.all (\b -> 48 <= b && b <= 57) msg + +is_terminated :: Bytes -> Bool is_terminated msg = - not (ByteString.null msg) && (ByteString.last msg == 13 || ByteString.last msg == 10) - -make_line_message :: ByteString -> [ByteString] + not (Bytes.null msg) && (Bytes.last msg == 13 || Bytes.last msg == 10) + +make_line_message :: Bytes -> [Bytes] make_line_message msg = - let n = ByteString.length msg in + let n = Bytes.length msg in if is_length msg || is_terminated msg then error ("Bad content for line message:\n" <> take 100 (UTF8.decode msg)) else - (if n > 100 || ByteString.any (== 10) msg then make_header [n + 1] else []) <> - [msg, "\n"] - -write_line_message :: Socket -> ByteString -> IO () + (if n > 100 || Bytes.any (== 10) msg then make_header [n + 1] else []) <> [msg, "\n"] + +write_line_message :: Socket -> Bytes -> IO () write_line_message socket = write socket . make_line_message -read_line_message :: Socket -> IO (Maybe ByteString) +read_line_message :: Socket -> IO (Maybe Bytes) read_line_message socket = do opt_line <- read_line socket case opt_line of @@ -2094,7 +2174,6 @@ ) where -import Data.ByteString (ByteString) import Control.Monad (forever, when) import qualified Control.Exception as Exception import Network.Socket (Socket) @@ -2102,6 +2181,7 @@ import qualified System.IO as IO import Isabelle.Library +import Isabelle.Bytes (Bytes) import qualified Isabelle.UUID as UUID import qualified Isabelle.Byte_Message as Byte_Message import qualified Isabelle.Isabelle_Thread as Isabelle_Thread @@ -2130,7 +2210,7 @@ server publish handle = Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop) where - open :: IO (Socket, ByteString) + open :: IO (Socket, Bytes) open = do server_socket <- Socket.socket Socket.AF_INET Socket.Stream Socket.defaultProtocol Socket.bind server_socket (Socket.SockAddrInet 0 localhost) @@ -2143,7 +2223,7 @@ return (server_socket, UUID.bytes password) - loop :: Socket -> ByteString -> IO () + loop :: Socket -> Bytes -> IO () loop server_socket password = forever $ do (connection, _) <- Socket.accept server_socket Isabelle_Thread.fork_finally