diff --git a/src/Tools/Haskell/Haskell.thy b/src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy +++ b/src/Tools/Haskell/Haskell.thy @@ -1,2269 +1,2275 @@ (* Title: Tools/Haskell/Haskell.thy Author: Makarius Support for Isabelle tools in Haskell. *) theory Haskell 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 LICENSE: BSD 3-clause (Isabelle) Variations on UTF-8. See \<^file>\$ISABELLE_HOME/src/Pure/General/utf8.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/General/utf8.scala\. -} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE InstanceSigs #-} module Isabelle.UTF8 ( Recode (..) ) where import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Text.Encoding as Encoding import qualified Data.Text.Encoding.Error as Error import Data.ByteString (ByteString) import qualified Isabelle.Bytes as Bytes import Isabelle.Bytes (Bytes) class Recode a b where encode :: a -> b decode :: b -> a instance Recode Text ByteString where encode :: Text -> ByteString encode = Encoding.encodeUtf8 decode :: ByteString -> Text decode = Encoding.decodeUtf8With Error.lenientDecode 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 encode = encode . Text.pack decode :: ByteString -> String decode = Text.unpack . decode instance Recode String Bytes where encode :: String -> Bytes encode = encode . Text.pack decode :: Bytes -> String decode = Text.unpack . decode \ generate_file "Isabelle/Symbol.hs" = \ {- Title: Isabelle/Symbols.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Isabelle text symbols. -} module Isabelle.Symbol where {- ASCII characters -} is_ascii_letter :: Char -> Bool is_ascii_letter c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' is_ascii_digit :: Char -> Bool is_ascii_digit c = '0' <= c && c <= '9' is_ascii_hex :: Char -> Bool is_ascii_hex c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f' is_ascii_quasi :: Char -> Bool is_ascii_quasi c = c == '_' || c == '\'' is_ascii_blank :: Char -> Bool is_ascii_blank c = c `elem` " \t\n\11\f\r" is_ascii_line_terminator :: Char -> Bool is_ascii_line_terminator c = c == '\r' || c == '\n' is_ascii_letdig :: Char -> Bool is_ascii_letdig c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c is_ascii_identifier :: String -> Bool is_ascii_identifier s = not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s \ generate_file "Isabelle/Library.hs" = \ {- Title: Isabelle/Library.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Basic library of Isabelle idioms. See also \<^file>\$ISABELLE_HOME/src/Pure/General/basics.ML\, \<^file>\$ISABELLE_HOME/src/Pure/library.ML\. -} +{-# LANGUAGE OverloadedStrings #-} + module Isabelle.Library ( (|>), (|->), (#>), (#->), the, the_default, fold, fold_rev, single, map_index, get_index, proper_string, quote, space_implode, commas, commas_quote, cat_lines, space_explode, split_lines, trim_line, clean_name) where -import qualified Data.List as List +import Data.String (IsString) import qualified Data.List.Split as Split import qualified Isabelle.Symbol as Symbol {- functions -} (|>) :: a -> (a -> b) -> b x |> f = f x (|->) :: (a, b) -> (a -> b -> c) -> c (x, y) |-> f = f x y (#>) :: (a -> b) -> (b -> c) -> a -> c (f #> g) x = x |> f |> g (#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d (f #-> g) x = x |> f |-> g {- options -} the :: Maybe a -> a the (Just x) = x the Nothing = error "the Nothing" the_default :: a -> Maybe a -> a the_default x Nothing = x the_default _ (Just y) = y {- lists -} fold :: (a -> b -> b) -> [a] -> b -> b fold _ [] y = y fold f (x : xs) y = fold f xs (f x y) fold_rev :: (a -> b -> b) -> [a] -> b -> b fold_rev _ [] y = y fold_rev f (x : xs) y = f x (fold_rev f xs y) single :: a -> [a] single x = [x] map_index :: ((Int, a) -> b) -> [a] -> [b] map_index f = map_aux 0 where map_aux _ [] = [] map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b) get_index f = get_aux 0 where get_aux _ [] = Nothing get_aux i (x : xs) = case f x of Nothing -> get_aux (i + 1) xs Just y -> Just (i, y) +separate :: a -> [a] -> [a] +separate s (x : (xs @ (_ : _))) = x : s : separate s xs +separate _ xs = xs; + {- strings -} -proper_string :: String -> Maybe String -proper_string s = if null s then Nothing else Just s - -quote :: String -> String +proper_string :: (IsString a, Eq a) => a -> Maybe a +proper_string s = if s == "" then Nothing else Just s + +quote :: (IsString a, Semigroup a) => a -> a quote s = "\"" <> s <> "\"" -space_implode :: String -> [String] -> String -space_implode = List.intercalate - -commas, commas_quote :: [String] -> String +space_implode :: (IsString a, Monoid a) => a -> [a] -> a +space_implode s = mconcat . separate s + +commas, commas_quote :: (IsString a, Monoid a) => [a] -> a commas = space_implode ", " commas_quote = commas . map quote -cat_lines :: [String] -> String +cat_lines :: (IsString a, Monoid 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 case reverse line of '\n' : '\r' : rest -> reverse rest '\r' : rest -> reverse rest '\n' : rest -> reverse rest _ -> line else line clean_name :: String -> String clean_name = reverse #> dropWhile (== '_') #> reverse \ generate_file "Isabelle/Value.hs" = \ {- Title: Isabelle/Value.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Plain values, represented as string. See also \<^file>\$ISABELLE_HOME/src/Pure/General/value.ML\. -} module Isabelle.Value (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real) where import qualified Data.List as List import qualified Text.Read as Read {- bool -} print_bool :: Bool -> String print_bool True = "true" print_bool False = "false" parse_bool :: String -> Maybe Bool parse_bool "true" = Just True parse_bool "false" = Just False parse_bool _ = Nothing {- nat -} parse_nat :: String -> Maybe Int parse_nat s = case Read.readMaybe s of Just n | n >= 0 -> Just n _ -> Nothing {- int -} print_int :: Int -> String print_int = show parse_int :: String -> Maybe Int parse_int = Read.readMaybe {- real -} print_real :: Double -> String print_real x = let s = show x in case span (/= '.') s of (a, '.' : b) | List.all (== '0') b -> a _ -> s parse_real :: String -> Maybe Double parse_real = Read.readMaybe \ generate_file "Isabelle/Buffer.hs" = \ {- Title: Isabelle/Buffer.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Efficient text buffers. See also \<^file>\$ISABELLE_HOME/src/Pure/General/buffer.ML\. -} module Isabelle.Buffer (T, empty, add, content) where import Isabelle.Library newtype T = Buffer [Char] empty :: T empty = Buffer [] add :: String -> T -> T add s (Buffer cs) = Buffer (fold (:) s cs) content :: T -> String content (Buffer cs) = reverse cs \ generate_file "Isabelle/Properties.hs" = \ {- Title: Isabelle/Properties.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Property lists. See also \<^file>\$ISABELLE_HOME/src/Pure/General/properties.ML\. -} module Isabelle.Properties (Entry, T, defined, get, get_value, put, remove) where import qualified Data.List as List type Entry = (String, String) type T = [Entry] defined :: T -> String -> Bool defined props name = any (\(a, _) -> a == name) props get :: T -> String -> Maybe String get props name = List.lookup name props get_value :: (String -> Maybe a) -> T -> String -> Maybe a get_value parse props name = case get props name of Nothing -> Nothing Just s -> parse s put :: Entry -> T -> T put entry props = entry : remove (fst entry) props remove :: String -> T -> T remove name props = if defined props name then filter (\(a, _) -> a /= name) props else props \ generate_file "Isabelle/Markup.hs" = \ {- Title: Isabelle/Markup.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Quasi-abstract markup elements. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/markup.ML\. -} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.Markup ( T, empty, is_empty, properties, nameN, name, xnameN, xname, kindN, bindingN, binding, entityN, entity, defN, refN, completionN, completion, no_completionN, no_completion, lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position, expressionN, expression, citationN, citation, pathN, path, urlN, url, docN, doc, markupN, consistentN, unbreakableN, indentN, widthN, blockN, block, breakN, break, fbreakN, fbreak, itemN, item, wordsN, words, tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var, numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string, inner_cartoucheN, inner_cartouche, token_rangeN, token_range, sortingN, sorting, typingN, typing, class_parameterN, class_parameter, antiquotedN, antiquoted, antiquoteN, antiquote, paragraphN, paragraph, text_foldN, text_fold, keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword, improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string, verbatimN, verbatim, cartoucheN, cartouche, commentN, comment, comment1N, comment1, comment2N, comment2, comment3N, comment3, forkedN, forked, joinedN, joined, runningN, running, finishedN, finished, failedN, failed, canceledN, canceled, initializedN, initialized, finalizedN, finalized, consolidatedN, consolidated, writelnN, writeln, stateN, state, informationN, information, tracingN, tracing, warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report, intensifyN, intensify, Output, no_output) where import Prelude hiding (words, error, break) import Isabelle.Library import qualified Isabelle.Properties as Properties import qualified Isabelle.Value as Value {- basic markup -} type T = (String, Properties.T) empty :: T empty = ("", []) is_empty :: T -> Bool is_empty ("", _) = True is_empty _ = False properties :: Properties.T -> T -> T properties more_props (elem, props) = (elem, fold_rev Properties.put more_props props) markup_elem :: String -> T markup_elem name = (name, []) markup_string :: String -> String -> String -> T markup_string name prop = \s -> (name, [(prop, s)]) {- misc properties -} nameN :: String nameN = \Markup.nameN\ name :: String -> T -> T name a = properties [(nameN, a)] xnameN :: String xnameN = \Markup.xnameN\ xname :: String -> T -> T xname a = properties [(xnameN, a)] kindN :: String kindN = \Markup.kindN\ {- formal entities -} bindingN :: String bindingN = \Markup.bindingN\ binding :: T binding = markup_elem bindingN entityN :: String entityN = \Markup.entityN\ entity :: String -> String -> T entity kind name = (entityN, (if null name then [] else [(nameN, name)]) <> (if null kind then [] else [(kindN, kind)])) defN :: String defN = \Markup.defN\ refN :: String refN = \Markup.refN\ {- completion -} completionN :: String completionN = \Markup.completionN\ completion :: T completion = markup_elem completionN no_completionN :: String no_completionN = \Markup.no_completionN\ no_completion :: T no_completion = markup_elem no_completionN {- position -} lineN, end_lineN :: String lineN = \Markup.lineN\ end_lineN = \Markup.end_lineN\ offsetN, end_offsetN :: String offsetN = \Markup.offsetN\ end_offsetN = \Markup.end_offsetN\ fileN, idN :: String fileN = \Markup.fileN\ idN = \Markup.idN\ positionN :: String positionN = \Markup.positionN\ position :: T position = markup_elem positionN {- expression -} expressionN :: String expressionN = \Markup.expressionN\ expression :: String -> T expression kind = (expressionN, if kind == "" then [] else [(kindN, kind)]) {- citation -} citationN :: String citationN = \Markup.citationN\ citation :: String -> T citation = markup_string nameN citationN {- external resources -} pathN :: String pathN = \Markup.pathN\ path :: String -> T path = markup_string pathN nameN urlN :: String urlN = \Markup.urlN\ url :: String -> T url = markup_string urlN nameN docN :: String docN = \Markup.docN\ doc :: String -> T doc = markup_string docN nameN {- pretty printing -} markupN, consistentN, unbreakableN, indentN :: String markupN = \Markup.markupN\ consistentN = \Markup.consistentN\ unbreakableN = \Markup.unbreakableN\ indentN = \Markup.indentN\ widthN :: String widthN = \Markup.widthN\ blockN :: String blockN = \Markup.blockN\ block :: Bool -> Int -> T block c i = (blockN, (if c then [(consistentN, Value.print_bool c)] else []) <> (if i /= 0 then [(indentN, Value.print_int i)] else [])) breakN :: String breakN = \Markup.breakN\ break :: Int -> Int -> T break w i = (breakN, (if w /= 0 then [(widthN, Value.print_int w)] else []) <> (if i /= 0 then [(indentN, Value.print_int i)] else [])) fbreakN :: String fbreakN = \Markup.fbreakN\ fbreak :: T fbreak = markup_elem fbreakN itemN :: String itemN = \Markup.itemN\ item :: T item = markup_elem itemN {- text properties -} wordsN :: String wordsN = \Markup.wordsN\ words :: T words = markup_elem wordsN {- inner syntax -} tfreeN :: String tfreeN = \Markup.tfreeN\ tfree :: T tfree = markup_elem tfreeN tvarN :: String tvarN = \Markup.tvarN\ tvar :: T tvar = markup_elem tvarN freeN :: String freeN = \Markup.freeN\ free :: T free = markup_elem freeN skolemN :: String skolemN = \Markup.skolemN\ skolem :: T skolem = markup_elem skolemN boundN :: String boundN = \Markup.boundN\ bound :: T bound = markup_elem boundN varN :: String varN = \Markup.varN\ var :: T var = markup_elem varN numeralN :: String numeralN = \Markup.numeralN\ numeral :: T numeral = markup_elem numeralN literalN :: String literalN = \Markup.literalN\ literal :: T literal = markup_elem literalN delimiterN :: String delimiterN = \Markup.delimiterN\ delimiter :: T delimiter = markup_elem delimiterN inner_stringN :: String inner_stringN = \Markup.inner_stringN\ inner_string :: T inner_string = markup_elem inner_stringN inner_cartoucheN :: String inner_cartoucheN = \Markup.inner_cartoucheN\ inner_cartouche :: T inner_cartouche = markup_elem inner_cartoucheN token_rangeN :: String token_rangeN = \Markup.token_rangeN\ token_range :: T token_range = markup_elem token_rangeN sortingN :: String sortingN = \Markup.sortingN\ sorting :: T sorting = markup_elem sortingN typingN :: String typingN = \Markup.typingN\ typing :: T typing = markup_elem typingN class_parameterN :: String class_parameterN = \Markup.class_parameterN\ class_parameter :: T class_parameter = markup_elem class_parameterN {- antiquotations -} antiquotedN :: String antiquotedN = \Markup.antiquotedN\ antiquoted :: T antiquoted = markup_elem antiquotedN antiquoteN :: String antiquoteN = \Markup.antiquoteN\ antiquote :: T antiquote = markup_elem antiquoteN {- text structure -} paragraphN :: String paragraphN = \Markup.paragraphN\ paragraph :: T paragraph = markup_elem paragraphN text_foldN :: String text_foldN = \Markup.text_foldN\ text_fold :: T text_fold = markup_elem text_foldN {- outer syntax -} keyword1N :: String keyword1N = \Markup.keyword1N\ keyword1 :: T keyword1 = markup_elem keyword1N keyword2N :: String keyword2N = \Markup.keyword2N\ keyword2 :: T keyword2 = markup_elem keyword2N keyword3N :: String keyword3N = \Markup.keyword3N\ keyword3 :: T keyword3 = markup_elem keyword3N quasi_keywordN :: String quasi_keywordN = \Markup.quasi_keywordN\ quasi_keyword :: T quasi_keyword = markup_elem quasi_keywordN improperN :: String improperN = \Markup.improperN\ improper :: T improper = markup_elem improperN operatorN :: String operatorN = \Markup.operatorN\ operator :: T operator = markup_elem operatorN stringN :: String stringN = \Markup.stringN\ string :: T string = markup_elem stringN alt_stringN :: String alt_stringN = \Markup.alt_stringN\ alt_string :: T alt_string = markup_elem alt_stringN verbatimN :: String verbatimN = \Markup.verbatimN\ verbatim :: T verbatim = markup_elem verbatimN cartoucheN :: String cartoucheN = \Markup.cartoucheN\ cartouche :: T cartouche = markup_elem cartoucheN commentN :: String commentN = \Markup.commentN\ comment :: T comment = markup_elem commentN {- comments -} comment1N :: String comment1N = \Markup.comment1N\ comment1 :: T comment1 = markup_elem comment1N comment2N :: String comment2N = \Markup.comment2N\ comment2 :: T comment2 = markup_elem comment2N comment3N :: String comment3N = \Markup.comment3N\ comment3 :: T comment3 = markup_elem comment3N {- command status -} forkedN, joinedN, runningN, finishedN, failedN, canceledN, initializedN, finalizedN, consolidatedN :: String forkedN = \Markup.forkedN\ joinedN = \Markup.joinedN\ runningN = \Markup.runningN\ finishedN = \Markup.finishedN\ failedN = \Markup.failedN\ canceledN = \Markup.canceledN\ initializedN = \Markup.initializedN\ finalizedN = \Markup.finalizedN\ consolidatedN = \Markup.consolidatedN\ forked, joined, running, finished, failed, canceled, initialized, finalized, consolidated :: T forked = markup_elem forkedN joined = markup_elem joinedN running = markup_elem runningN finished = markup_elem finishedN failed = markup_elem failedN canceled = markup_elem canceledN initialized = markup_elem initializedN finalized = markup_elem finalizedN consolidated = markup_elem consolidatedN {- messages -} writelnN :: String writelnN = \Markup.writelnN\ writeln :: T writeln = markup_elem writelnN stateN :: String stateN = \Markup.stateN\ state :: T state = markup_elem stateN informationN :: String informationN = \Markup.informationN\ information :: T information = markup_elem informationN tracingN :: String tracingN = \Markup.tracingN\ tracing :: T tracing = markup_elem tracingN warningN :: String warningN = \Markup.warningN\ warning :: T warning = markup_elem warningN legacyN :: String legacyN = \Markup.legacyN\ legacy :: T legacy = markup_elem legacyN errorN :: String errorN = \Markup.errorN\ error :: T error = markup_elem errorN reportN :: String reportN = \Markup.reportN\ report :: T report = markup_elem reportN no_reportN :: String no_reportN = \Markup.no_reportN\ no_report :: T no_report = markup_elem no_reportN intensifyN :: String intensifyN = \Markup.intensifyN\ intensify :: T intensify = markup_elem intensifyN {- output -} type Output = (String, String) no_output :: Output no_output = ("", "") \ generate_file "Isabelle/Completion.hs" = \ {- Title: Isabelle/Completion.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Completion of names. See also \<^file>\$ISABELLE_HOME/src/Pure/General/completion.ML\. -} module Isabelle.Completion ( Name, T, names, none, make, markup_element, markup_report, make_report ) where import qualified Data.List as List import Isabelle.Library import qualified Isabelle.Properties as Properties import qualified Isabelle.Markup as Markup import qualified Isabelle.XML.Encode as Encode import qualified Isabelle.XML as XML import qualified Isabelle.YXML as YXML type Name = (String, (String, String)) -- external name, kind, internal name data T = Completion Properties.T Int [Name] -- position, total length, names names :: Int -> Properties.T -> [Name] -> T names limit props names = Completion props (length names) (take limit names) none :: T none = names 0 [] [] make :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> T make limit (name, props) make_names = if name /= "" && name /= "_" then names limit props (make_names $ List.isPrefixOf $ clean_name name) else none 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) else (Markup.empty, []) markup_report :: [T] -> String markup_report [] = "" markup_report elems = YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems) make_report :: Int -> (String, Properties.T) -> ((String -> Bool) -> [Name]) -> String make_report limit name_props make_names = markup_report [make limit name_props make_names] \ generate_file "Isabelle/File.hs" = \ {- Title: Isabelle/File.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) File-system operations. See also \<^file>\$ISABELLE_HOME/src/Pure/General/file.ML\. -} module Isabelle.File (setup, read, write, append) where import Prelude hiding (read) import qualified System.IO as IO setup :: IO.Handle -> IO () setup h = do IO.hSetEncoding h IO.utf8 IO.hSetNewlineMode h IO.noNewlineTranslation read :: IO.FilePath -> IO String read path = IO.withFile path IO.ReadMode (\h -> do setup h; IO.hGetContents h >>= \s -> length s `seq` return s) write :: IO.FilePath -> String -> IO () write path s = IO.withFile path IO.WriteMode (\h -> do setup h; IO.hPutStr h s) append :: IO.FilePath -> String -> IO () append path s = IO.withFile path IO.AppendMode (\h -> do setup h; IO.hPutStr h s) \ generate_file "Isabelle/XML.hs" = \ {- Title: Isabelle/XML.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Untyped XML trees and representation of ML values. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of) where import Isabelle.Library import qualified Isabelle.Properties as Properties import qualified Isabelle.Markup as Markup import qualified Isabelle.Buffer as Buffer {- types -} type Attributes = Properties.T type Body = [Tree] data Tree = Elem (Markup.T, Body) | Text String {- wrapped elements -} wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree wrap_elem (((a, atts), body1), body2) = Elem ((\XML.xml_elemN\, (\XML.xml_nameN\, a) : atts), Elem ((\XML.xml_bodyN\, []), body1) : body2) unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree]) unwrap_elem (Elem ((\XML.xml_elemN\, (\XML.xml_nameN\, a) : atts), Elem ((\XML.xml_bodyN\, []), body1) : body2)) = Just (((a, atts), body1), body2) unwrap_elem _ = Nothing {- text content -} add_content :: Tree -> Buffer.T -> Buffer.T add_content tree = case unwrap_elem tree of Just (_, ts) -> fold add_content ts Nothing -> case tree of Elem (_, ts) -> fold add_content ts Text s -> Buffer.add s content_of :: Body -> String content_of body = Buffer.empty |> fold add_content body |> Buffer.content {- string representation -} encode '<' = "<" encode '>' = ">" encode '&' = "&" encode '\'' = "'" encode '\"' = """ encode c = [c] instance Show Tree where show tree = Buffer.empty |> show_tree tree |> Buffer.content where show_tree (Elem ((name, atts), [])) = Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>" show_tree (Elem ((name, atts), ts)) = Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #> fold show_tree ts #> Buffer.add " Buffer.add name #> Buffer.add ">" show_tree (Text s) = Buffer.add (show_text s) show_elem name atts = unwords (name : map (\(a, x) -> a <> "=\"" <> show_text x <> "\"") atts) show_text = concatMap encode \ generate_file "Isabelle/XML/Encode.hs" = \ {- Title: Isabelle/XML/Encode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML as data representation language. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.XML.Encode ( A, T, V, P, int_atom, bool_atom, unit_atom, tree, properties, string, int, bool, unit, pair, triple, list, option, variant ) where import Isabelle.Library import qualified Isabelle.Value as Value import qualified Isabelle.Properties as Properties import qualified Isabelle.XML as XML type A a = a -> String type T a = a -> XML.Body type V a = a -> Maybe ([String], XML.Body) type P a = a -> [String] -- atomic values int_atom :: A Int int_atom = Value.print_int bool_atom :: A Bool bool_atom False = "0" bool_atom True = "1" unit_atom :: A () unit_atom () = "" -- structural nodes node ts = XML.Elem ((":", []), ts) vector = map_index (\(i, x) -> (int_atom i, x)) tagged (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts) -- representation of standard types tree :: T XML.Tree tree t = [t] properties :: T Properties.T properties props = [XML.Elem ((":", props), [])] string :: T String string "" = [] string s = [XML.Text s] int :: T Int int = string . int_atom bool :: T Bool bool = string . bool_atom unit :: T () unit = string . unit_atom pair :: T a -> T b -> T (a, b) pair f g (x, y) = [node (f x), node (g y)] triple :: T a -> T b -> T c -> T (a, b, c) triple f g h (x, y, z) = [node (f x), node (g y), node (h z)] list :: T a -> T [a] list f xs = map (node . f) xs option :: T a -> T (Maybe a) option _ Nothing = [] option f (Just x) = [node (f x)] variant :: [V a] -> T a variant fs x = [tagged (the (get_index (\f -> f x) fs))] \ generate_file "Isabelle/XML/Decode.hs" = \ {- Title: Isabelle/XML/Decode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML as data representation language. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.XML.Decode ( A, T, V, P, int_atom, bool_atom, unit_atom, tree, properties, string, int, bool, unit, pair, triple, list, option, variant ) where import Isabelle.Library import qualified Isabelle.Value as Value import qualified Isabelle.Properties as Properties import qualified Isabelle.XML as XML type A a = String -> a type T a = XML.Body -> a type V a = ([String], XML.Body) -> a type P a = [String] -> a err_atom = error "Malformed XML atom" err_body = error "Malformed XML body" {- atomic values -} int_atom :: A Int int_atom s = case Value.parse_int s of Just i -> i Nothing -> err_atom bool_atom :: A Bool bool_atom "0" = False bool_atom "1" = True bool_atom _ = err_atom unit_atom :: A () unit_atom "" = () unit_atom _ = err_atom {- structural nodes -} node (XML.Elem ((":", []), ts)) = ts node _ = err_body vector atts = map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts tagged (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts)) tagged _ = err_body {- representation of standard types -} tree :: T XML.Tree tree [t] = t tree _ = err_body properties :: T Properties.T properties [XML.Elem ((":", props), [])] = props properties _ = err_body string :: T String string [] = "" string [XML.Text s] = s string _ = err_body int :: T Int int = int_atom . string bool :: T Bool bool = bool_atom . string unit :: T () unit = unit_atom . string pair :: T a -> T b -> T (a, b) pair f g [t1, t2] = (f (node t1), g (node t2)) pair _ _ _ = err_body triple :: T a -> T b -> T c -> T (a, b, c) triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3)) triple _ _ _ _ = err_body list :: T a -> T [a] list f ts = map (f . node) ts option :: T a -> T (Maybe a) option _ [] = Nothing option f [t] = Just (f (node t)) option _ _ = err_body variant :: [V a] -> T a variant fs [t] = (fs !! tag) (xs, ts) where (tag, (xs, ts)) = tagged t variant _ _ = err_body \ generate_file "Isabelle/YXML.hs" = \ {- Title: Isabelle/YXML.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Efficient text representation of XML trees. Suitable for direct inlining into plain text. See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\. -} {-# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-incomplete-patterns #-} module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup, buffer_body, buffer, string_of_body, string_of, parse_body, parse) where import qualified Data.Char as Char import qualified Data.List as List import Isabelle.Library import qualified Isabelle.Markup as Markup import qualified Isabelle.XML as XML import qualified Isabelle.Buffer as Buffer {- markers -} charX, charY :: Char charX = Char.chr 5 charY = Char.chr 6 strX, strY, strXY, strXYX :: String strX = [charX] strY = [charY] strXY = strX <> strY strXYX = strXY <> strX detect :: String -> Bool detect = any (\c -> c == charX || c == charY) {- output -} output_markup :: Markup.T -> Markup.Output output_markup markup@(name, atts) = if Markup.is_empty markup then Markup.no_output else (strXY <> name <> concatMap (\(a, x) -> strY <> a <> "=" <> x) atts <> strX, strXYX) buffer_attrib (a, x) = Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x buffer_body :: XML.Body -> Buffer.T -> Buffer.T buffer_body = fold buffer buffer :: XML.Tree -> Buffer.T -> Buffer.T buffer (XML.Elem ((name, atts), ts)) = Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #> buffer_body ts #> Buffer.add strXYX buffer (XML.Text s) = Buffer.add s string_of_body :: XML.Body -> String string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content string_of :: XML.Tree -> String string_of = string_of_body . single {- parse -} -- split: fields or non-empty tokens split :: Bool -> Char -> String -> [String] split _ _ [] = [] split fields sep str = splitting str where splitting rest = case span (/= sep) rest of (_, []) -> cons rest [] (prfx, _ : rest') -> cons prfx (splitting rest') cons item = if fields || not (null item) then (:) item else id -- structural errors err msg = error ("Malformed YXML: " <> msg) err_attribute = err "bad attribute" err_element = err "bad element" err_unbalanced "" = err "unbalanced element" err_unbalanced name = err ("unbalanced element " <> quote name) -- stack operations add x ((elem, body) : pending) = (elem, x : body) : pending push "" _ _ = err_element push name atts pending = ((name, atts), []) : pending pop ((("", _), _) : _) = err_unbalanced "" pop ((markup, body) : pending) = add (XML.Elem (markup, reverse body)) pending -- parsing parse_attrib s = case List.elemIndex '=' s of Just i | i > 0 -> (take i s, drop (i + 1) s) _ -> err_attribute parse_chunk ["", ""] = pop parse_chunk ("" : name : atts) = push name (map parse_attrib atts) parse_chunk txts = fold (add . XML.Text) txts parse_body :: String -> XML.Body parse_body source = case fold parse_chunk chunks [(("", []), [])] of [(("", _), result)] -> reverse result ((name, _), _) : _ -> err_unbalanced name where chunks = split False charX source |> map (split True charY) parse :: String -> XML.Tree parse source = case parse_body source of [result] -> result [] -> XML.Text "" _ -> err "multiple results" \ generate_file "Isabelle/Pretty.hs" = \ {- Title: Isabelle/Pretty.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Generic pretty printing module. See also \<^file>\$ISABELLE_HOME/src/Pure/General/pretty.ML\. -} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Isabelle.Pretty ( T, symbolic, formatted, unformatted, str, brk_indent, brk, fbrk, breaks, fbreaks, blk, block, strs, markup, mark, mark_str, marks_str, item, text_fold, keyword1, keyword2, text, paragraph, para, quote, cartouche, separate, commas, enclose, enum, list, str_list, big_list) where import Isabelle.Library hiding (quote, commas) import qualified Data.List as List import qualified Isabelle.Buffer as Buffer import qualified Isabelle.Markup as Markup import qualified Isabelle.XML as XML import qualified Isabelle.YXML as YXML data T = Block Markup.T Bool Int [T] | Break Int Int | Str String {- output -} output_spaces n = replicate n ' ' symbolic_text "" = [] symbolic_text s = [XML.Text s] symbolic_markup markup body = if Markup.is_empty markup then body else [XML.Elem (markup, body)] symbolic :: T -> XML.Body symbolic (Block markup consistent indent prts) = concatMap symbolic prts |> symbolic_markup block_markup |> symbolic_markup markup where block_markup = if null prts then Markup.empty else Markup.block consistent indent symbolic (Break wd ind) = [XML.Elem (Markup.break wd ind, symbolic_text (output_spaces wd))] symbolic (Str s) = symbolic_text s formatted :: T -> String formatted = YXML.string_of_body . symbolic unformatted :: T -> String unformatted prt = Buffer.empty |> out prt |> Buffer.content where out (Block markup _ _ prts) = let (bg, en) = YXML.output_markup markup in Buffer.add bg #> fold out prts #> Buffer.add en out (Break _ wd) = Buffer.add (output_spaces wd) out (Str s) = Buffer.add s {- derived operations to create formatting expressions -} force_nat n | n < 0 = 0 force_nat n = n str :: String -> T str = Str brk_indent :: Int -> Int -> T brk_indent wd ind = Break (force_nat wd) ind brk :: Int -> T brk wd = brk_indent wd 0 fbrk :: T fbrk = str "\n" breaks, fbreaks :: [T] -> [T] breaks = List.intersperse (brk 1) fbreaks = List.intersperse fbrk blk :: (Int, [T]) -> T blk (indent, es) = Block Markup.empty False (force_nat indent) es block :: [T] -> T block prts = blk (2, prts) strs :: [String] -> T strs = block . breaks . map str markup :: Markup.T -> [T] -> T markup m = Block m False 0 mark :: Markup.T -> T -> T mark m prt = if m == Markup.empty then prt else markup m [prt] mark_str :: (Markup.T, String) -> T mark_str (m, s) = mark m (str s) marks_str :: ([Markup.T], String) -> T marks_str (ms, s) = fold_rev mark ms (str s) item :: [T] -> T item = markup Markup.item text_fold :: [T] -> T text_fold = markup Markup.text_fold keyword1, keyword2 :: String -> T keyword1 name = mark_str (Markup.keyword1, name) keyword2 name = mark_str (Markup.keyword2, name) text :: String -> [T] text = breaks . map str . words paragraph :: [T] -> T paragraph = markup Markup.paragraph para :: String -> T para = paragraph . text quote :: T -> T quote prt = blk (1, [str "\"", prt, str "\""]) cartouche :: T -> T cartouche prt = blk (1, [str "\92", prt, str "\92"]) separate :: String -> [T] -> [T] separate sep = List.intercalate [str sep, brk 1] . map single commas :: [T] -> [T] commas = separate "," enclose :: String -> String -> [T] -> T enclose lpar rpar prts = block (str lpar : prts <> [str rpar]) enum :: String -> String -> String -> [T] -> T enum sep lpar rpar = enclose lpar rpar . separate sep list :: String -> String -> [T] -> T list = enum "," str_list :: String -> String -> [String] -> T str_list lpar rpar = list lpar rpar . map str big_list :: String -> [T] -> T big_list name prts = block (fbreaks (str name : prts)) \ generate_file "Isabelle/Term.hs" = \ {- Title: Isabelle/Term.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Lambda terms, types, sorts. See also \<^file>\$ISABELLE_HOME/src/Pure/term.scala\. -} module Isabelle.Term ( Indexname, Sort, dummyS, Typ(..), dummyT, is_dummyT, Term(..)) where type Indexname = (String, Int) type Sort = [String] dummyS :: Sort dummyS = [""] data Typ = Type (String, [Typ]) | TFree (String, Sort) | TVar (Indexname, Sort) deriving Show dummyT :: Typ dummyT = Type (\\<^type_name>\dummy\\, []) is_dummyT :: Typ -> Bool is_dummyT (Type (\\<^type_name>\dummy\\, [])) = True is_dummyT _ = False data Term = Const (String, [Typ]) | Free (String, Typ) | Var (Indexname, Typ) | Bound Int | Abs (String, Typ, Term) | App (Term, Term) deriving Show \ generate_file "Isabelle/Term_XML/Encode.hs" = \ {- Title: Isabelle/Term_XML/Encode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. See also \<^file>\$ISABELLE_HOME/src/Pure/term_xml.ML\. -} {-# LANGUAGE LambdaCase #-} module Isabelle.Term_XML.Encode (indexname, sort, typ, typ_body, term) where import Isabelle.Library import Isabelle.XML.Encode import Isabelle.Term indexname :: P Indexname indexname (a, b) = if b == 0 then [a] else [a, int_atom b] sort :: T Sort sort = list string typ :: T Typ typ ty = ty |> variant [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing }, \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing }, \case { TVar (a, b) -> Just (indexname a, sort b); _ -> Nothing }] typ_body :: T Typ typ_body ty = if is_dummyT ty then [] else typ ty term :: T Term term t = t |> variant [\case { Const (a, b) -> Just ([a], list typ b); _ -> Nothing }, \case { Free (a, b) -> Just ([a], typ_body b); _ -> Nothing }, \case { Var (a, b) -> Just (indexname a, typ_body b); _ -> Nothing }, \case { Bound a -> Just ([], int a); _ -> Nothing }, \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing }, \case { App a -> Just ([], pair term term a); _ -> Nothing }] \ generate_file "Isabelle/Term_XML/Decode.hs" = \ {- Title: Isabelle/Term_XML/Decode.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. See also \<^file>\$ISABELLE_HOME/src/Pure/term_xml.ML\. -} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} module Isabelle.Term_XML.Decode (indexname, sort, typ, typ_body, term) where import Isabelle.Library import Isabelle.XML.Decode import Isabelle.Term indexname :: P Indexname indexname [a] = (a, 0) indexname [a, b] = (a, int_atom b) sort :: T Sort sort = list string typ :: T Typ typ ty = ty |> variant [\([a], b) -> Type (a, list typ b), \([a], b) -> TFree (a, sort b), \(a, b) -> TVar (indexname a, sort b)] typ_body :: T Typ typ_body [] = dummyT typ_body body = typ body term :: T Term term t = t |> variant [\([a], b) -> Const (a, list typ b), \([a], b) -> Free (a, typ_body b), \(a, b) -> Var (indexname a, typ_body b), \([], a) -> Bound (int a), \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d), \([], a) -> App (pair term term a)] \ generate_file "Isabelle/UUID.hs" = \ {- Title: Isabelle/UUID.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Universally unique identifiers. See \<^file>\$ISABELLE_HOME/src/Pure/General/uuid.scala\. -} module Isabelle.UUID ( T, parse_string, parse_bytes, string, bytes, random, random_string, random_bytes ) where 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 {- parse -} parse_string :: String -> Maybe T parse_string = UUID.fromString parse_bytes :: Bytes -> Maybe T parse_bytes = UUID.fromASCIIBytes . Bytes.unmake {- print -} string :: T -> String string = UUID.toString bytes :: T -> Bytes bytes = Bytes.make . UUID.toASCIIBytes {- random id -} random :: IO T random = nextRandom random_string :: IO String random_string = string <$> random random_bytes :: IO Bytes random_bytes = bytes <$> random \ generate_file "Isabelle/Byte_Message.hs" = \ {- Title: Isabelle/Byte_Message.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Byte-oriented messages. See \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\. -} {-# LANGUAGE OverloadedStrings #-} {-# OPTIONS_GHC -fno-warn-incomplete-patterns #-} module Isabelle.Byte_Message ( write, write_line, read, read_block, trim_line, read_line, make_message, write_message, read_message, make_line_message, write_line_message, read_line_message, read_yxml, write_yxml ) where import Prelude hiding (read) import Data.Maybe 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 import Network.Socket (Socket) import qualified Network.Socket.ByteString as Socket import Isabelle.Library hiding (trim_line) import qualified Isabelle.Value as Value {- output operations -} 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 Bytes read socket n = read_body 0 [] where result = Bytes.concat . reverse read_body len ss = if len >= n then return (result ss) else (do s <- Socket.recv socket (min (n - len) 8192) case ByteString.length s of 0 -> return (result ss) 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 = Bytes.length msg return (if len == n then Just msg else Nothing, len) trim_line :: Bytes -> Bytes trim_line 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 = Bytes.length s at = Bytes.index s read_line :: Socket -> IO (Maybe Bytes) read_line socket = read_body [] where result = trim_line . Bytes.pack . reverse read_body bs = do s <- Socket.recv socket 1 case ByteString.length s of 0 -> return (if null bs then Nothing else Just (result bs)) 1 -> case ByteString.head s of 10 -> return (Just (result bs)) b -> read_body (b : bs) {- messages with multiple chunks (arbitrary content) -} make_header :: [Int] -> [Bytes] make_header ns = [UTF8.encode (space_implode "," (map Value.print_int ns)), "\n"] 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 :: Bytes -> [Int] parse_header line = let res = map Value.parse_nat (space_explode ',' (UTF8.decode line)) in if all isJust res then map fromJust res else error ("Malformed message header: " <> quote (UTF8.decode line)) read_chunk :: Socket -> Int -> IO Bytes read_chunk socket n = do res <- read_block socket n return $ case res of (Just chunk, _) -> chunk (Nothing, len) -> error ("Malformed message chunk: unexpected EOF after " <> show len <> " of " <> show n <> " bytes") read_message :: Socket -> IO (Maybe [Bytes]) read_message socket = do res <- read_line socket case res of Just line -> Just <$> mapM (read_chunk socket) (parse_header line) Nothing -> return Nothing -- hybrid messages: line or length+block (with content restriction) is_length :: Bytes -> Bool is_length msg = not (Bytes.null msg) && Bytes.all (\b -> 48 <= b && b <= 57) msg is_terminated :: Bytes -> Bool is_terminated msg = not (Bytes.null msg) && (Bytes.last msg == 13 || Bytes.last msg == 10) make_line_message :: Bytes -> [Bytes] make_line_message msg = 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 || 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 Bytes) read_line_message socket = do opt_line <- read_line socket case opt_line of Nothing -> return Nothing Just line -> case Value.parse_nat (UTF8.decode line) of Nothing -> return $ Just line Just n -> fmap trim_line . fst <$> read_block socket n read_yxml :: Socket -> IO (Maybe XML.Body) read_yxml socket = do res <- read_line_message socket return (YXML.parse_body . UTF8.decode <$> res) write_yxml :: Socket -> XML.Body -> IO () write_yxml socket body = write_line_message socket (UTF8.encode (YXML.string_of_body body)) \ generate_file "Isabelle/Isabelle_Thread.hs" = \ {- Title: Isabelle/Isabelle_Thread.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) Isabelle-specific thread management. See \<^file>\$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.ML\ and \<^file>\$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.scala\. -} {-# LANGUAGE NamedFieldPuns #-} module Isabelle.Isabelle_Thread ( ThreadId, Result, find_id, properties, change_properties, add_resource, del_resource, bracket_resource, is_stopped, expose_stopped, stop, my_uuid, stop_uuid, Fork, fork_finally, fork) where import Data.Unique import Data.IORef import System.IO.Unsafe import qualified Data.List as List import Control.Monad (when, forM_) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Control.Exception as Exception import Control.Concurrent (ThreadId) import qualified Control.Concurrent as Concurrent import Control.Concurrent.Thread (Result) import qualified Control.Concurrent.Thread as Thread import qualified Isabelle.UUID as UUID import qualified Isabelle.Properties as Properties {- thread info -} type Resources = Map Unique (IO ()) data Info = Info {uuid :: UUID.T, props :: Properties.T, stopped :: Bool, resources :: Resources} type Infos = Map ThreadId Info lookup_info :: Infos -> ThreadId -> Maybe Info lookup_info infos id = Map.lookup id infos init_info :: ThreadId -> UUID.T -> Infos -> (Infos, ()) init_info id uuid infos = (Map.insert id (Info uuid [] False Map.empty) infos, ()) {- global state -} {-# NOINLINE global_state #-} global_state :: IORef Infos global_state = unsafePerformIO (newIORef Map.empty) find_id :: UUID.T -> IO (Maybe ThreadId) find_id uuid = do state <- readIORef global_state return $ fst <$> List.find (\(_, Info{uuid = uuid'}) -> uuid == uuid') (Map.assocs state) get_info :: ThreadId -> IO (Maybe Info) get_info id = do state <- readIORef global_state return $ lookup_info state id map_info :: ThreadId -> (Info -> Info) -> IO (Maybe Info) map_info id f = atomicModifyIORef' global_state (\infos -> case lookup_info infos id of Nothing -> (infos, Nothing) Just info -> let info' = f info in (Map.insert id info' infos, Just info')) delete_info :: ThreadId -> IO () delete_info id = atomicModifyIORef' global_state (\infos -> (Map.delete id infos, ())) {- thread properties -} my_info :: IO (Maybe Info) my_info = do id <- Concurrent.myThreadId get_info id properties :: IO Properties.T properties = maybe [] props <$> my_info change_properties :: (Properties.T -> Properties.T) -> IO () change_properties f = do id <- Concurrent.myThreadId map_info id (\info -> info {props = f (props info)}) return () {- managed resources -} add_resource :: IO () -> IO Unique add_resource resource = do id <- Concurrent.myThreadId u <- newUnique map_info id (\info -> info {resources = Map.insert u resource (resources info)}) return u del_resource :: Unique -> IO () del_resource u = do id <- Concurrent.myThreadId map_info id (\info -> info {resources = Map.delete u (resources info)}) return () bracket_resource :: IO () -> IO a -> IO a bracket_resource resource body = Exception.bracket (add_resource resource) del_resource (const body) {- stop -} is_stopped :: IO Bool is_stopped = maybe False stopped <$> my_info expose_stopped :: IO () expose_stopped = do stopped <- is_stopped when stopped $ throw ThreadKilled stop :: ThreadId -> IO () stop id = do info <- map_info id (\info -> info {stopped = True}) let ops = case info of Nothing -> []; Just Info{resources} -> map snd (Map.toDescList resources) sequence_ ops {- UUID -} my_uuid :: IO (Maybe UUID.T) my_uuid = fmap uuid <$> my_info stop_uuid :: UUID.T -> IO () stop_uuid uuid = do id <- find_id uuid forM_ id stop {- fork -} type Fork a = (ThreadId, UUID.T, IO (Result a)) fork_finally :: IO a -> (Either SomeException a -> IO b) -> IO (Fork b) fork_finally body finally = do uuid <- UUID.random (id, result) <- Exception.mask (\restore -> Thread.forkIO (Exception.try (do id <- Concurrent.myThreadId atomicModifyIORef' global_state (init_info id uuid) restore body) >>= (\res -> do id <- Concurrent.myThreadId; delete_info id; finally res))) return (id, uuid, result) fork :: IO a -> IO (Fork a) fork body = fork_finally body Thread.result \ generate_file "Isabelle/Server.hs" = \ {- Title: Isabelle/Server.hs Author: Makarius LICENSE: BSD 3-clause (Isabelle) TCP server on localhost. -} module Isabelle.Server ( localhost_name, localhost, publish_text, publish_stdout, server, connection ) where import Control.Monad (forever, when) import qualified Control.Exception as Exception import Network.Socket (Socket) import qualified Network.Socket as Socket 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 import qualified Isabelle.UTF8 as UTF8 {- server address -} localhost_name :: String 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 name address password = "server " <> quote name <> " = " <> address <> " (password " <> quote (show password) <> ")" publish_stdout :: String -> String -> UUID.T -> IO () publish_stdout name address password = putStrLn (publish_text name address password) {- server -} server :: (String -> UUID.T -> IO ()) -> (Socket -> IO ()) -> IO () server publish handle = Socket.withSocketsDo $ Exception.bracket open (Socket.close . fst) (uncurry loop) where 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) Socket.listen server_socket 50 port <- Socket.socketPort server_socket let address = localhost_name <> ":" <> show port password <- UUID.random publish address password return (server_socket, UUID.bytes password) loop :: Socket -> Bytes -> IO () loop server_socket password = forever $ do (connection, _) <- Socket.accept server_socket Isabelle_Thread.fork_finally (do line <- Byte_Message.read_line connection when (line == Just password) $ handle connection) (\finally -> do Socket.close connection case finally of Left exn -> IO.hPutStrLn IO.stderr $ Exception.displayException exn Right () -> return ()) return () {- client connection -} connection :: String -> String -> (Socket -> IO a) -> IO a connection port password client = Socket.withSocketsDo $ do addr <- resolve Exception.bracket (open addr) Socket.close body where resolve = do let hints = Socket.defaultHints { Socket.addrFlags = [Socket.AI_NUMERICHOST, Socket.AI_NUMERICSERV], Socket.addrSocketType = Socket.Stream } head <$> Socket.getAddrInfo (Just hints) (Just "127.0.0.1") (Just port) open addr = do socket <- Socket.socket (Socket.addrFamily addr) (Socket.addrSocketType addr) (Socket.addrProtocol addr) Socket.connect socket $ Socket.addrAddress addr return socket body socket = do Byte_Message.write_line socket (UTF8.encode password) client socket \ export_generated_files _ end