# HG changeset patch
# User wenzelm
# Date 1628189874 -7200
# Node ID e4575152b525c7c6e1368702be8f6ec2dbcd1573
# Parent  5fc39193887352f4b955bc78f42f5f022053735e# Parent  54a108beed3edbfb7f838f926d8328357edb3a2b
merged

diff -r 5fc391938873 -r e4575152b525 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Thu Aug 05 20:27:31 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Thu Aug 05 20:57:54 2021 +0200
@@ -25,7 +25,7 @@
   empty, null, length, index, all, any,
   head, last, take, drop, isPrefixOf, isSuffixOf,
   concat, space, spaces, singleton, char, byte,
-  trim_line, space_explode, split_lines
+  trim_line
 )
 where
 
@@ -130,20 +130,6 @@
   where
     n = length s
     at = char . index s
-
-space_explode :: Word8 -> Bytes -> [Bytes]
-space_explode sep str =
-  if null str then []
-  else if all (/= sep) str then [str]
-  else explode (unpack str)
-  where
-    explode rest =
-      case span (/= sep) rest of
-        (_, []) -> [pack rest]
-        (prfx, _ : rest') -> pack prfx : explode rest'
-
-split_lines :: Bytes -> [Bytes]
-split_lines = space_explode (byte '\n')
 \<close>
 
 generate_file "Isabelle/UTF8.hs" = \<open>
@@ -241,6 +227,7 @@
   fold, fold_rev, single, map_index, get_index, separate,
 
   StringLike, STRING (..), TEXT (..), BYTES (..),
+  show_bytes, show_text,
 
   proper_string, quote, space_implode, commas, commas_quote, cat_lines,
   space_explode, split_lines, trim_line)
@@ -249,9 +236,11 @@
 import qualified Data.Text as Text
 import Data.Text (Text)
 import qualified Data.Text.Lazy as Lazy
+import GHC.Exts (IsList, Item)
 import Data.String (IsString)
 import qualified Data.List.Split as Split
 import qualified Isabelle.Symbol as Symbol
+import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.UTF8 as UTF8
 
@@ -317,11 +306,40 @@
 
 {- string-like interfaces -}
 
-class (IsString a, Monoid a, Eq a, Ord a) => StringLike a
-instance StringLike String
-instance StringLike Text
-instance StringLike Lazy.Text
-instance StringLike Bytes
+class (IsList a, IsString a, Monoid a, Eq a, Ord a) => StringLike a
+  where
+    space_explode :: Item a -> a -> [a]
+    split_lines :: a -> [a]
+
+instance StringLike String where
+  space_explode sep = Split.split (Split.dropDelims (Split.whenElt (== sep)))
+  split_lines = space_explode '\n'
+
+instance StringLike Text where
+  space_explode sep str =
+    if Text.null str then []
+    else if Text.all (/= sep) str then [str]
+    else map Text.pack $ space_explode sep $ Text.unpack str
+  split_lines = space_explode '\n'
+
+instance StringLike Lazy.Text where
+  space_explode sep str =
+    if Lazy.null str then []
+    else if Lazy.all (/= sep) str then [str]
+    else map Lazy.pack $ space_explode sep $ Lazy.unpack str
+  split_lines = space_explode '\n'
+
+instance StringLike Bytes where
+  space_explode sep str =
+    if Bytes.null str then []
+    else if Bytes.all (/= sep) str then [str]
+    else explode (Bytes.unpack str)
+    where
+      explode rest =
+        case span (/= sep) rest of
+          (_, []) -> [Bytes.pack rest]
+          (prfx, _ : rest') -> Bytes.pack prfx : explode rest'
+  split_lines = space_explode (Bytes.byte '\n')
 
 class StringLike a => STRING a where make_string :: a -> String
 instance STRING String where make_string = id
@@ -341,6 +359,12 @@
 instance BYTES Lazy.Text where make_bytes = UTF8.encode . Lazy.toStrict
 instance BYTES Bytes where make_bytes = id
 
+show_bytes :: Show a => a -> Bytes
+show_bytes = make_bytes . show
+
+show_text :: Show a => a -> Text
+show_text = make_text . show
+
 
 {- strings -}
 
@@ -360,13 +384,6 @@
 cat_lines :: StringLike a => [a] -> a
 cat_lines = space_implode "\n"
 
-
-space_explode :: Char -> String -> [String]
-space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
-
-split_lines :: String -> [String]
-split_lines = space_explode '\n'
-
 trim_line :: String -> String
 trim_line line =
   if not (null line) && Symbol.is_ascii_line_terminator (last line) then
@@ -492,7 +509,7 @@
 {- int -}
 
 print_int :: Int -> Bytes
-print_int = make_bytes . show
+print_int = show_bytes
 
 parse_int :: Bytes -> Maybe Int
 parse_int = Read.readMaybe . make_string
@@ -1526,7 +1543,7 @@
 import Isabelle.Name (Name)
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Markup as Markup
-import qualified Isabelle.XML.Encode as Encode
+import Isabelle.XML.Classes
 import qualified Isabelle.XML as XML
 import qualified Isabelle.YXML as YXML
 
@@ -1549,13 +1566,7 @@
 markup_element :: T -> (Markup.T, XML.Body)
 markup_element (Completion props total names) =
   if not (null names) then
-    let
-      markup = Markup.properties props Markup.completion
-      body =
-        Encode.pair Encode.int
-          (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
-          (total, names)
-    in (markup, body)
+    (Markup.properties props Markup.completion, encode (total, names))
   else (Markup.empty, [])
 
 markup_report :: [T] -> Name
@@ -1717,7 +1728,7 @@
 keyword2 name = mark_str (Markup.keyword2, name)
 
 text :: BYTES a => a -> [T]
-text = breaks . map str . filter (not . Bytes.null) . Bytes.space_explode Bytes.space . make_bytes
+text = breaks . map str . filter (not . Bytes.null) . space_explode Bytes.space . make_bytes
 
 paragraph :: [T] -> T
 paragraph = markup Markup.paragraph
@@ -2252,6 +2263,90 @@
     \([], a) -> App (pair term term a)]
 \<close>
 
+generate_file "Isabelle/XML/Classes.hs" = \<open>
+{- generated by Isabelle -}
+
+{-  Title:      Isabelle/XML/Classes.hs
+    Author:     Makarius
+    LICENSE:    BSD 3-clause (Isabelle)
+
+Type classes for XML data representation.
+-}
+
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
+
+module Isabelle.XML.Classes
+  (Encode_Atom(..), Decode_Atom(..), Encode (..), Decode (..))
+where
+
+import qualified Isabelle.XML as XML
+import qualified Isabelle.XML.Encode as Encode
+import qualified Isabelle.XML.Decode as Decode
+import qualified Isabelle.Term_XML.Encode as Encode
+import qualified Isabelle.Term_XML.Decode as Decode
+import qualified Isabelle.Properties as Properties
+import Isabelle.Bytes (Bytes)
+import Isabelle.Term (Typ, Term)
+
+
+class Encode_Atom a where encode_atom :: Encode.A a
+class Decode_Atom a where decode_atom :: Decode.A a
+
+instance Encode_Atom Int where encode_atom = Encode.int_atom
+instance Decode_Atom Int where decode_atom = Decode.int_atom
+
+instance Encode_Atom Bool where encode_atom = Encode.bool_atom
+instance Decode_Atom Bool where decode_atom = Decode.bool_atom
+
+instance Encode_Atom () where encode_atom = Encode.unit_atom
+instance Decode_Atom () where decode_atom = Decode.unit_atom
+
+
+class Encode a where encode :: Encode.T a
+class Decode a where decode :: Decode.T a
+
+instance Encode Bytes where encode = Encode.string
+instance Decode Bytes where decode = Decode.string
+
+instance Encode Int where encode = Encode.int
+instance Decode Int where decode = Decode.int
+
+instance Encode Bool where encode = Encode.bool
+instance Decode Bool where decode = Decode.bool
+
+instance Encode () where encode = Encode.unit
+instance Decode () where decode = Decode.unit
+
+instance (Encode a, Encode b) => Encode (a, b)
+  where encode = Encode.pair encode encode
+instance (Decode a, Decode b) => Decode (a, b)
+  where decode = Decode.pair decode decode
+
+instance (Encode a, Encode b, Encode c) => Encode (a, b, c)
+  where encode = Encode.triple encode encode encode
+instance (Decode a, Decode b, Decode c) => Decode (a, b, c)
+  where decode = Decode.triple decode decode decode
+
+instance Encode a => Encode [a] where encode = Encode.list encode
+instance Decode a => Decode [a] where decode = Decode.list decode
+
+instance Encode a => Encode (Maybe a) where encode = Encode.option encode
+instance Decode a => Decode (Maybe a) where decode = Decode.option decode
+
+instance Encode XML.Tree where encode = Encode.tree
+instance Decode XML.Tree where decode = Decode.tree
+
+instance Encode Properties.T where encode = Encode.properties
+instance Decode Properties.T where decode = Decode.properties
+
+instance Encode Typ where encode = Encode.typ
+instance Decode Typ where decode = Decode.typ
+
+instance Encode Term where encode = Encode.term
+instance Decode Term where decode = Decode.term
+\<close>
+
 generate_file "Isabelle/UUID.hs" = \<open>
 {-  Title:      Isabelle/UUID.hs
     Author:     Makarius
@@ -2384,7 +2479,7 @@
 parse_header :: Bytes -> [Int]
 parse_header line =
   let
-    res = map Value.parse_nat (Bytes.space_explode (Bytes.byte ',') line)
+    res = map Value.parse_nat (space_explode (Bytes.byte ',') line)
   in
     if all isJust res then map fromJust res
     else error ("Malformed message header: " <> quote (UTF8.decode line))
@@ -2628,6 +2723,8 @@
 TCP server on localhost.
 -}
 
+{-# LANGUAGE OverloadedStrings #-}
+
 module Isabelle.Server (
   localhost_name, localhost, publish_text, publish_stdout,
   server, connection
@@ -2639,8 +2736,10 @@
 import Network.Socket (Socket)
 import qualified Network.Socket as Socket
 import qualified System.IO as IO
+import qualified Data.ByteString.Char8 as Char8
 
 import Isabelle.Library
+import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
 import qualified Isabelle.UUID as UUID
 import qualified Isabelle.Byte_Message as Byte_Message
@@ -2649,24 +2748,25 @@
 
 {- server address -}
 
-localhost_name :: String
+localhost_name :: Bytes
 localhost_name = "127.0.0.1"
 
 localhost :: Socket.HostAddress
 localhost = Socket.tupleToHostAddress (127, 0, 0, 1)
 
-publish_text :: String -> String -> UUID.T -> String
+publish_text :: Bytes -> Bytes -> UUID.T -> Bytes
 publish_text name address password =
-  "server " <> quote name <> " = " <> address <> " (password " <> quote (show password) <> ")"
-
-publish_stdout :: String -> String -> UUID.T -> IO ()
+  "server " <> quote name <> " = " <> address <>
+    " (password " <> quote (show_bytes password) <> ")"
+
+publish_stdout :: Bytes -> Bytes -> UUID.T -> IO ()
 publish_stdout name address password =
-  putStrLn (publish_text name address password)
+  Char8.putStrLn (Bytes.unmake $ publish_text name address password)
 
 
 {- server -}
 
-server :: (String -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
+server :: (Bytes -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO ()
 server publish handle =
   Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop)
   where
@@ -2677,7 +2777,7 @@
       Socket.listen server_socket 50
 
       port <- Socket.socketPort server_socket
-      let address = localhost_name <> ":" <> show port
+      let address = localhost_name <> ":" <> show_bytes port
       password <- UUID.random
       publish address password