(*  Title:      Tools/Haskell/Haskell.thy
    Author:     Makarius
    UUID:       0e3ceb40-61a8-4f78-a6c7-ae4892dd80b3

Support for Isabelle tools in Haskell.
*)

theory Haskell
  imports Main
begin

generate_file "Isabelle/Bytes.hs" = ‹
 - Title: Isabelle/Bytes.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  byte strings.

  🚫‹$ISABELLE_HOME/src/Pure/General/bytes.ML›
  🚫‹$ISABELLE_HOME/src/Pure/General/bytes.scala›.
 }

 -# LANGUAGE TypeApplications #-}

  Isabelle.Bytes (
 Bytes,
 make, unmake, pack, unpack,
 empty, null, length, index, all, any,
 head, last, take, drop, isPrefixOf, isSuffixOf, try_unprefix, try_unsuffix,
 concat, space, spaces, char, all_char, any_char, byte, singleton
 
 

  Prelude hiding (null, length, all, any, head, last, take, drop, concat)

  qualified Data.ByteString.Short as ShortByteString
  Data.ByteString.Short (ShortByteString)
  qualified Data.ByteString as ByteString
  Data.ByteString (ByteString)
  qualified Data.List as List
  Data.Word (Word8)
  Data.Array (Array, array, (!))


  Bytes = ShortByteString

  :: ByteString -> Bytes
  = ShortByteString.toShort

  :: Bytes -> ByteString
  = ShortByteString.fromShort

  :: [Word8] -> Bytes
  = ShortByteString.pack

  :: Bytes -> [Word8]
  = ShortByteString.unpack

  :: Bytes
  = ShortByteString.empty

  :: Bytes -> Bool
  = ShortByteString.null

  :: Bytes -> Int
  = ShortByteString.length

  :: Bytes -> Int -> Word8
  = ShortByteString.index

  :: (Word8 -> Bool) -> Bytes -> Bool
  p = List.all p . unpack

  :: (Word8 -> Bool) -> Bytes -> Bool
  p = List.any p . unpack

  :: Bytes -> Word8
  bytes = index bytes 0

  :: Bytes -> Word8
  bytes = index bytes (length bytes - 1)

  :: Int -> Bytes -> Bytes
  n bs
 | n == 0 = empty
 | n >= length bs = bs
 | otherwise = pack (List.take n (unpack bs))

  :: Int -> Bytes -> Bytes
  n bs
 | n == 0 = bs
 | n >= length bs = empty
 | otherwise = pack (List.drop n (unpack bs))

  :: Bytes -> Bytes -> Bool
  bs1 bs2 =
 n1 <= n2 && List.all (\i -> index bs1 i == index bs2 i) [0 .. n1 - 1]
 where n1 = length bs1; n2 = length bs2

  :: Bytes -> Bytes -> Bool
  bs1 bs2 =
 n1 <= n2 && List.all (\i -> index bs1 i == index bs2 (i + k)) [0 .. n1 - 1]
 where n1 = length bs1; n2 = length bs2; k = n2 - n1

  :: Bytes -> Bytes -> Maybe Bytes
  bs1 bs2 =
 if isPrefixOf bs1 bs2 then Just (drop (length bs1) bs2)
 else Nothing

  :: Bytes -> Bytes -> Maybe Bytes
  bs1 bs2 =
 if isSuffixOf bs1 bs2 then Just (take (length bs2 - length bs1) bs2)
 else Nothing

  :: [Bytes] -> Bytes
  = mconcat

  :: Word8
  = 32

  :: Array Int Bytes
  = array (0, 64) [(i, pack (replicate i space)) | i <- [0 .. 64]]

  :: Int -> Bytes
  n =
 if n < 64 then small_spaces ! n
 else concat ((small_spaces ! (n `mod` 64)) : replicate (n `div` 64) (small_spaces ! 64))

  :: Word8 -> Char
  = toEnum . fromEnum

  :: (Char -> Bool) -> Bytes -> Bool
  pred = all (pred . char)

  :: (Char -> Bool) -> Bytes -> Bool
  pred = any (pred . char)

  :: Char -> Word8
  = toEnum . fromEnum

  :: Array Word8 Bytes
  =
 array (minBound, maxBound)
 [(i, make (ByteString.singleton i)) | i <- [minBound .. maxBound]]

  :: Word8 -> Bytes
  b = singletons ! b
 ›

generate_file "Isabelle/UTF8.hs" = ‹
 - Title: Isabelle/UTF8.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  on UTF-8.

  🚫‹$ISABELLE_HOME/src/Pure/General/utf8.ML›
  🚫‹$ISABELLE_HOME/src/Pure/General/utf8.scala›.
 }

 -# LANGUAGE MultiParamTypeClasses #-}
 -# LANGUAGE TypeSynonymInstances #-}
 -# LANGUAGE FlexibleInstances #-}
 -# LANGUAGE InstanceSigs #-}

  Isabelle.UTF8 (
 setup, setup3,
 Recode (..)
 
 

  qualified System.IO as IO
  Data.Text (Text)
  qualified Data.Text as Text
  qualified Data.Text.Encoding as Encoding
  qualified Data.Text.Encoding.Error as Error

  Data.ByteString (ByteString)

  qualified Isabelle.Bytes as Bytes
  Isabelle.Bytes (Bytes)

  :: IO.Handle -> IO ()
  h = do
 IO.hSetEncoding h IO.utf8
 IO.hSetNewlineMode h IO.noNewlineTranslation

  :: IO.Handle -> IO.Handle -> IO.Handle -> IO ()
  h1 h2 h3 = do
 setup h1
 setup h2
 setup h3

  Recode a b where
 encode :: a -> b
 decode :: b -> a

  Recode Text ByteString where
 encode :: Text -> ByteString
 encode = Encoding.encodeUtf8
 decode :: ByteString -> Text
 decode = Encoding.decodeUtf8With Error.lenientDecode

  Recode Text Bytes where
 encode :: Text -> Bytes
 encode = Bytes.make . encode
 decode :: Bytes -> Text
 decode = decode . Bytes.unmake

  Recode String ByteString where
 encode :: String -> ByteString
 encode = encode . Text.pack
 decode :: ByteString -> String
 decode = Text.unpack . decode

  Recode String Bytes where
 encode :: String -> Bytes
 encode = encode . Text.pack
 decode :: Bytes -> String
 decode = Text.unpack . decode
 ›

generate_file "Isabelle/Library.hs" = ‹
 - Title: Isabelle/Library.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  library of Isabelle idioms.

  🚫‹$ISABELLE_HOME/src/Pure/General/basics.ML›
  🚫‹$ISABELLE_HOME/src/Pure/library.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}
 -# LANGUAGE TypeSynonymInstances #-}
 -# LANGUAGE FlexibleInstances #-}
 -# LANGUAGE InstanceSigs #-}

  Isabelle.Library (
 (|>), (|->), (#>), (#->),

 fold, fold_rev, fold_map, single, the_single, singletonM,
 map_index, get_index, separate,

 StringLike, STRING (..), TEXT (..), BYTES (..),
 show_bytes, show_text,

 proper_string, enclose, quote, space_implode, implode_space, commas, commas_quote,
 cat_lines, space_explode, split_lines, trim_line, trim_split_lines,

 getenv, getenv_strict)
 

  System.Environment (lookupEnv)
  Data.Maybe (fromMaybe)
  qualified Data.Text as Text
  Data.Text (Text)
  qualified Data.Text.Lazy as Lazy
  Data.String (IsString)
  qualified Data.List.Split as Split
  qualified Isabelle.Symbol as Symbol
  qualified Isabelle.Bytes as Bytes
  Isabelle.Bytes (Bytes)
  qualified Isabelle.UTF8 as UTF8


 - functions -}

 |>) :: a -> (a -> b) -> b
  |> 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


 - lists -}

  :: (a -> b -> b) -> [a] -> b -> b
  _ [] y = y
  f (x : xs) y = fold f xs (f x y)

  :: (a -> b -> b) -> [a] -> b -> b
  _ [] y = y
  f (x : xs) y = f x (fold_rev f xs y)

  :: (a -> b -> (c, b)) -> [a] -> b -> ([c], b)
  _ [] y = ([], y)
  f (x : xs) y =
 let
 (x', y') = f x y
 (xs', y'') = fold_map f xs y'
 in (x' : xs', y'')

  :: a -> [a]
  x = [x]

  :: [a] -> a
  [x] = x
  _ = undefined

  :: Monad m => ([a] -> m [b]) -> a -> m b
  f x = the_single 🚫 f [x]

  :: ((Int, a) -> b) -> [a] -> [b]
  f = map_aux 0
 where
 map_aux _ [] = []
 map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs

  :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
  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)

  :: a -> [a] -> [a]
  s (x : xs@(_ : _)) = x : s : separate s xs
  _ xs = xs;


 - string-like interfaces -}

  (IsString a, Monoid a, Eq a, Ord a) => StringLike a where
 space_explode :: Char -> a -> [a]
 trim_line :: a -> a

  :: Int -> (Int -> Char) -> (Int -> a -> a) -> a -> a
  n at trim s =
 if n >= 2 && at (n - 2) == '\r' && at (n - 1) == '\n' then trim (n - 2) s
 else if n >= 1 && Symbol.is_ascii_line_terminator (at (n - 1)) then trim (n - 1) s
 else s

  StringLike String where
 space_explode :: Char -> String -> [String]
 space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
 trim_line :: String -> String
 trim_line s = gen_trim_line (length s) (s !!) take s

  StringLike Text where
 space_explode :: Char -> Text -> [Text]
 space_explode c str =
 if Text.null str then []
 else if Text.all (/= c) str then [str]
 else map Text.pack $ space_explode c $ Text.unpack str
 trim_line :: Text -> Text
 trim_line s = gen_trim_line (Text.length s) (Text.index s) Text.take s

  StringLike Lazy.Text where
 space_explode :: Char -> Lazy.Text -> [Lazy.Text]
 space_explode c str =
 if Lazy.null str then []
 else if Lazy.all (/= c) str then [str]
 else map Lazy.pack $ space_explode c $ Lazy.unpack str
 trim_line :: Lazy.Text -> Lazy.Text
 trim_line = Lazy.fromStrict . trim_line . Lazy.toStrict

  StringLike Bytes where
 space_explode :: Char -> Bytes -> [Bytes]
 space_explode c str =
 if Bytes.null str then []
 else if Bytes.all_char (/= c) str then [str]
 else
 explode (Bytes.unpack str)
 where
 explode rest =
 case span (/= (Bytes.byte c)) rest of
 (_, []) -> [Bytes.pack rest]
 (prfx, _ : rest') -> Bytes.pack prfx : explode rest'
 trim_line :: Bytes -> Bytes
 trim_line s = gen_trim_line (Bytes.length s) (Bytes.char . Bytes.index s) Bytes.take s

  StringLike a => STRING a where make_string :: a -> String
  STRING String where make_string = id
  STRING Text where make_string = Text.unpack
  STRING Lazy.Text where make_string = Lazy.unpack
  STRING Bytes where make_string = UTF8.decode

  StringLike a => TEXT a where make_text :: a -> Text
  TEXT String where make_text = Text.pack
  TEXT Text where make_text = id
  TEXT Lazy.Text where make_text = Lazy.toStrict
  TEXT Bytes where make_text = UTF8.decode

  StringLike a => BYTES a where make_bytes :: a -> Bytes
  BYTES String where make_bytes = UTF8.encode
  BYTES Text where make_bytes = UTF8.encode
  BYTES Lazy.Text where make_bytes = UTF8.encode . Lazy.toStrict
  BYTES Bytes where make_bytes = id

  :: Show a => a -> Bytes
  = make_bytes . show

  :: Show a => a -> Text
  = make_text . show


 - strings -}

  :: StringLike a => a -> Maybe a
  s = if s == "" then Nothing else Just s

  :: StringLike a => a -> a -> a -> a
  lpar rpar str = lpar <> str <> rpar

  :: StringLike a => a -> a
  = enclose "\"" "\""

  :: StringLike a => a -> [a] -> a
  s = mconcat . separate s

  :: StringLike a => [a] -> a
  = space_implode " "

 , commas_quote :: StringLike a => [a] -> a
  = space_implode ", "
  = commas . map quote

  :: StringLike a => a -> [a]
  = space_explode '\n'

  :: StringLike a => [a] -> a
  = space_implode "\n"

  :: StringLike a => a -> [a]
  = trim_line #> split_lines #> map trim_line


 - getenv -}

  :: Bytes -> IO Bytes
  x = do
 y <- lookupEnv (make_string x)
 return $ make_bytes $ fromMaybe "" y

  :: Bytes -> IO Bytes
  x = do
 y <- getenv x
 if Bytes.null y then
 errorWithoutStackTrace $ make_string ("Undefined Isabelle environment variable: " <> quote x)
 else return y
 ›


generate_file "Isabelle/Symbol.hs" = ‹
 - Title: Isabelle/Symbols.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  text symbols.

  🚫‹$ISABELLE_HOME/src/Pure/General/symbol.ML›
  🚫‹$ISABELLE_HOME/src/Pure/General/symbol_explode.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}

  Isabelle.Symbol (
 Symbol, eof, is_eof, not_eof,

 is_ascii_letter, is_ascii_digit, is_ascii_hex, is_ascii_quasi,
 is_ascii_blank, is_ascii_line_terminator, is_ascii_letdig,
 is_ascii_identifier,

 explode
 
 

  Data.Word (Word8)
  qualified Isabelle.Bytes as Bytes
  Isabelle.Bytes (Bytes)


 - type -}

  Symbol = Bytes

  :: Symbol
  = ""

 , not_eof :: Symbol -> Bool
  = Bytes.null
  = not . is_eof


 - ASCII characters -}

  :: Char -> Bool
  c = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z'

  :: Char -> Bool
  c = '0' <= c && c <= '9'

  :: Char -> Bool
  c = '0' <= c && c <= '9' || 'A' <= c && c <= 'F' || 'a' <= c && c <= 'f'

  :: Char -> Bool
  c = c == '_' || c == '\''

  :: Char -> Bool
  c = c `elem` (" \t\n\11\f\r" :: String)

  :: Char -> Bool
  c = c == '\r' || c == '\n'

  :: Char -> Bool
  c = is_ascii_letter c || is_ascii_digit c || is_ascii_quasi c

  :: String -> Bool
  s =
 not (null s) && is_ascii_letter (head s) && all is_ascii_letdig s


 - explode symbols: ASCII, UTF8, named -}

  :: Word8 -> Bool
  b = b >= 128

  :: Word8 -> Bool
  b = 128 <= b && b < 192

  :: Word8 -> Bool
  b = 128 <= b && b < 160

 |>) :: a -> (a -> b) -> b
  |> f = f x

  :: Bytes -> [Symbol]
  string = scan 0
 where
 byte = Bytes.index string
 substring i j =
 if i == j - 1 then Bytes.singleton (byte i)
 else Bytes.pack (map byte [i .. j - 1])

 n = Bytes.length string
 test pred i = i < n && pred (byte i)
 test_char pred i = i < n && pred (Bytes.char (byte i))
 many pred i = if test pred i then many pred (i + 1) else i
 maybe_char c i = if test_char (== c) i then i + 1 else i
 maybe_ascii_id i =
 if test_char is_ascii_letter i
 then many (is_ascii_letdig . Bytes.char) (i + 1)
 else i

 scan i =
 if i < n then
 let
 b = byte i
 c = Bytes.char b
 in
 {-encoded newline-}
 if c == '\r' then "\n" : scan (maybe_char '\n' (i + 1))
 {-pseudo utf8: encoded ascii control-}
 else if b == 192 && test is_utf8_control (i + 1) && not (test is_utf8 (i + 2))
 then Bytes.singleton (byte (i + 1) - 128) : scan (i + 2)
 {-utf8-}
 else if is_utf8 b then
 let j = many is_utf8_trailer (i + 1)
 in substring i j : scan j
 {-named symbol-}
 else if c == '\\' && test_char (== '<') (i + 1) then
 let j = (i + 2) |> maybe_char '^' |> maybe_ascii_id |> maybe_char '>'
 in substring i j : scan j
 {-single character-}
 else Bytes.singleton b : scan (i + 1)
 else []
 ›

generate_file "Isabelle/Buffer.hs" = ‹
 - Title: Isabelle/Buffer.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  buffer of byte strings.

  🚫‹$ISABELLE_HOME/src/Pure/General/buffer.ML›.
 }

  Isabelle.Buffer (T, empty, add, content, build, build_content)
 

  qualified Isabelle.Bytes as Bytes
  Isabelle.Bytes (Bytes)
  Isabelle.Library


  T = Buffer [Bytes]

  :: T
  = Buffer []

  :: Bytes -> T -> T
  b (Buffer bs) = Buffer (if Bytes.null b then bs else b : bs)

  :: T -> Bytes
  (Buffer bs) = Bytes.concat (reverse bs)

  :: (T -> T) -> T
  f = f empty

  :: (T -> T) -> Bytes
  f = build f |> content
 ›

generate_file "Isabelle/Value.hs" = ‹
 - Title: Isabelle/Value.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  values, represented as string.

  🚫‹$ISABELLE_HOME/src/Pure/General/value.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}

  Isabelle.Value
 (print_bool, parse_bool, parse_nat, print_int, parse_int, print_real, parse_real)
 

  qualified Data.List as List
  qualified Text.Read as Read
  Isabelle.Bytes (Bytes)
  Isabelle.Library


 - bool -}

  :: Bool -> Bytes
  True = "true"
  False = "false"

  :: Bytes -> Maybe Bool
  "true" = Just True
  "false" = Just False
  _ = Nothing


 - nat -}

  :: Bytes -> Maybe Int
  s =
 case Read.readMaybe (make_string s) of
 Just n | n >= 0 -> Just n
 _ -> Nothing


 - int -}

  :: Int -> Bytes
  = show_bytes

  :: Bytes -> Maybe Int
  = Read.readMaybe . make_string


 - real -}

  :: Double -> Bytes
  x =
 let s = show x in
 case span (/= '.') s of
 (a, '.' : b) | List.all (== '0') b -> make_bytes a
 _ -> make_bytes s

  :: Bytes -> Maybe Double
  = Read.readMaybe . make_string
 ›

generate_file "Isabelle/Properties.hs" = ‹
 - Title: Isabelle/Properties.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  lists.

  🚫‹$ISABELLE_HOME/src/Pure/General/properties.ML›.
 }

  Isabelle.Properties (Entry, T, defined, get, get_value, put, remove)
 

  qualified Data.List as List
  Isabelle.Bytes (Bytes)


  Entry = (Bytes, Bytes)
  T = [Entry]

  :: T -> Bytes -> Bool
  props name = any (\(a, _) -> a == name) props

  :: T -> Bytes -> Maybe Bytes
  props name = List.lookup name props

  :: (Bytes -> Maybe a) -> T -> Bytes -> Maybe a
  parse props name = maybe Nothing parse (get props name)

  :: Entry -> T -> T
  entry props = entry : remove (fst entry) props

  :: Bytes -> T -> T
  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)

 -abstract markup elements.

  🚫‹$ISABELLE_HOME/src/Pure/PIDE/markup.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}
 -# OPTIONS_GHC -fno-warn-missing-signatures #-}

  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, labelN, fileN, idN, positionN, position,
 position_properties, def_name,

 expressionN, expression,

 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,
 consolidatingN, consolidating, 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)
 

  Prelude hiding (words, error, break)
  Data.Map.Strict (Map)
  qualified Data.Map.Strict as Map

  Isabelle.Library
  qualified Isabelle.Properties as Properties
  qualified Isabelle.Value as Value
  qualified Isabelle.Bytes as Bytes
  Isabelle.Bytes (Bytes)


 - basic markup -}

  T = (Bytes, Properties.T)

  :: T
  = ("", [])

  :: T -> Bool
  ("", _) = True
  _ = False

  :: Properties.T -> T -> T
  more_props (elem, props) =
 (elem, fold_rev Properties.put more_props props)

  :: Bytes -> T
  name = (name, [])

  :: Bytes -> Bytes -> Bytes -> T
  name prop = \s -> (name, [(prop, s)])


 - misc properties -}

  :: Bytes
  = ‹Markup.nameN›

  :: Bytes -> T -> T
  a = properties [(nameN, a)]

  :: Bytes
  = ‹Markup.xnameN›

  :: Bytes -> T -> T
  a = properties [(xnameN, a)]

  :: Bytes
  = ‹Markup.kindN›


 - formal entities -}

  :: Bytes
  = ‹Markup.bindingN›
  :: T
  = markup_elem bindingN

  :: Bytes
  = ‹Markup.entityN›
  :: Bytes -> Bytes -> T
  kind name =
 (entityN,
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
 (if Bytes.null kind then [] else [(kindN, kind)]))

  :: Bytes
  = ‹Markup.defN›

  :: Bytes
  = ‹Markup.refN›


 - completion -}

  :: Bytes
  = ‹Markup.completionN›
  :: T
  = markup_elem completionN

  :: Bytes
  = ‹Markup.no_completionN›
  :: T
  = markup_elem no_completionN


 - position -}

 , end_lineN :: Bytes
  = ‹Markup.lineN›
  = ‹Markup.end_lineN›

 , end_offsetN :: Bytes
  = ‹Markup.offsetN›
  = ‹Markup.end_offsetN›

 , fileN, idN :: Bytes
  = ‹Markup.labelN›
  = ‹Markup.fileN›
  = ‹Markup.idN›

  :: Bytes
  = ‹Markup.positionN›
  :: T
  = markup_elem positionN

  :: [Bytes]
  = [lineN, offsetN, end_offsetN, labelN, fileN, idN]


 - position "def" names -}

  :: Bytes -> Bytes
  a = "def_" <> a

  :: Map Bytes Bytes
  = Map.fromList $ map (\a -> (a, make_def a)) position_properties

  :: Bytes -> Bytes
  a =
 case Map.lookup a def_names of
 Just b -> b
 Nothing -> make_def a


 - expression -}

  :: Bytes
  = ‹Markup.expressionN›

  :: Bytes -> T
  kind = (expressionN, if kind == "" then [] else [(kindN, kind)])


 - external resources -}

  :: Bytes
  = ‹Markup.pathN›
  :: Bytes -> T
  = markup_string pathN nameN

  :: Bytes
  = ‹Markup.urlN›
  :: Bytes -> T
  = markup_string urlN nameN

  :: Bytes
  = ‹Markup.docN›
  :: Bytes -> T
  = markup_string docN nameN


 - pretty printing -}

 , consistentN, unbreakableN, indentN :: Bytes
  = ‹Markup.markupN›
  = ‹Markup.consistentN›
  = ‹Markup.unbreakableN›
  = ‹Markup.indentN›

  :: Bytes
  = ‹Markup.widthN›

  :: Bytes
  = ‹Markup.blockN›
  :: Bool -> Int -> T
  c i =
 (blockN,
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
 (if i /= 0 then [(indentN, Value.print_int i)] else []))

  :: Bytes
  = ‹Markup.breakN›
  :: Int -> Int -> T
  w i =
 (breakN,
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "brackoff" is null
 (if i /= 0 then [(indentN, Value.print_int i)] else []))

  :: Bytes
  = ‹Markup.fbreakN›
  :: T
  = markup_elem fbreakN

  :: Bytes
  = ‹Markup.itemN›
  :: T
  = markup_elem itemN


 - text properties -}

  :: Bytes
  = ‹Markup.wordsN›
  :: T
  = markup_elem wordsN


 - inner syntax -}

  :: Bytes
  = ‹Markup.tfreeN›
  :: T
  = markup_elem tfreeN

  :: Bytes
  = ‹Markup.tvarN›
  :: T
  = markup_elem tvarN

  :: Bytes
  = ‹Markup.freeN›
  :: T
  = markup_elem freeN

  :: Bytes
  = ‹Markup.skolemN›
  :: T
  = markup_elem skolemN

  :: Bytes
  = ‹Markup.boundN›
  :: T
  = markup_elem boundN

  :: Bytes
  = ‹Markup.varN›
  :: T
  = markup_elem varN

  :: Bytes
  = ‹Markup.numeralN›
  :: T
  = markup_elem numeralN

  :: Bytes
  = ‹Markup.literalN›
  :: T
  = markup_elem literalN

  :: Bytes
  = ‹Markup.delimiterN›
  :: T
  = markup_elem delimiterN

  :: Bytes
  = ‹Markup.inner_stringN›
  :: T
  = markup_elem inner_stringN

  :: Bytes
  = ‹Markup.inner_cartoucheN›
  :: T
  = markup_elem inner_cartoucheN


  :: Bytes
  = ‹Markup.token_rangeN›
  :: T
  = markup_elem token_rangeN


  :: Bytes
  = ‹Markup.sortingN›
  :: T
  = markup_elem sortingN

  :: Bytes
  = ‹Markup.typingN›
  :: T
  = markup_elem typingN

  :: Bytes
  = ‹Markup.class_parameterN›
  :: T
  = markup_elem class_parameterN


 - antiquotations -}

  :: Bytes
  = ‹Markup.antiquotedN›
  :: T
  = markup_elem antiquotedN

  :: Bytes
  = ‹Markup.antiquoteN›
  :: T
  = markup_elem antiquoteN


 - text structure -}

  :: Bytes
  = ‹Markup.paragraphN›
  :: T
  = markup_elem paragraphN

  :: Bytes
  = ‹Markup.text_foldN›
  :: T
  = markup_elem text_foldN


 - outer syntax -}

  :: Bytes
  = ‹Markup.keyword1N›
  :: T
  = markup_elem keyword1N

  :: Bytes
  = ‹Markup.keyword2N›
  :: T
  = markup_elem keyword2N

  :: Bytes
  = ‹Markup.keyword3N›
  :: T
  = markup_elem keyword3N

  :: Bytes
  = ‹Markup.quasi_keywordN›
  :: T
  = markup_elem quasi_keywordN

  :: Bytes
  = ‹Markup.improperN›
  :: T
  = markup_elem improperN

  :: Bytes
  = ‹Markup.operatorN›
  :: T
  = markup_elem operatorN

  :: Bytes
  = ‹Markup.stringN›
  :: T
  = markup_elem stringN

  :: Bytes
  = ‹Markup.alt_stringN›
  :: T
  = markup_elem alt_stringN

  :: Bytes
  = ‹Markup.verbatimN›
  :: T
  = markup_elem verbatimN

  :: Bytes
  = ‹Markup.cartoucheN›
  :: T
  = markup_elem cartoucheN

  :: Bytes
  = ‹Markup.commentN›
  :: T
  = markup_elem commentN


 - comments -}

  :: Bytes
  = ‹Markup.comment1N›
  :: T
  = markup_elem comment1N

  :: Bytes
  = ‹Markup.comment2N›
  :: T
  = markup_elem comment2N

  :: Bytes
  = ‹Markup.comment3N›
  :: T
  = markup_elem comment3N


 - command status -}

 , joinedN, runningN, finishedN, failedN, canceledN,
 initializedN, finalizedN, consolidatingN, consolidatedN :: Bytes
  = ‹Markup.forkedN›
  = ‹Markup.joinedN›
  = ‹Markup.runningN›
  = ‹Markup.finishedN›
  = ‹Markup.failedN›
  = ‹Markup.canceledN›
  = ‹Markup.initializedN›
  = ‹Markup.finalizedN›
  = ‹Markup.consolidatingN›
  = ‹Markup.consolidatedN›

 , joined, running, finished, failed, canceled,
 initialized, finalized, consolidating, consolidated :: T
  = markup_elem forkedN
  = markup_elem joinedN
  = markup_elem runningN
  = markup_elem finishedN
  = markup_elem failedN
  = markup_elem canceledN
  = markup_elem initializedN
  = markup_elem finalizedN
  = markup_elem consolidatingN
  = markup_elem consolidatedN


 - messages -}

  :: Bytes
  = ‹Markup.writelnN›
  :: T
  = markup_elem writelnN

  :: Bytes
  = ‹Markup.stateN›
  :: T
  = markup_elem stateN

  :: Bytes
  = ‹Markup.informationN›
  :: T
  = markup_elem informationN

  :: Bytes
  = ‹Markup.tracingN›
  :: T
  = markup_elem tracingN

  :: Bytes
  = ‹Markup.warningN›
  :: T
  = markup_elem warningN

  :: Bytes
  = ‹Markup.legacyN›
  :: T
  = markup_elem legacyN

  :: Bytes
  = ‹Markup.errorN›
  :: T
  = markup_elem errorN

  :: Bytes
  = ‹Markup.reportN›
  :: T
  = markup_elem reportN

  :: Bytes
  = ‹Markup.no_reportN›
  :: T
  = markup_elem no_reportN

  :: Bytes
  = ‹Markup.intensifyN›
  :: T
  = markup_elem intensifyN


 - output -}

  Output = (Bytes, Bytes)

  :: Output
  = ("", "")
 ›

generate_file "Isabelle/Position.hs" = ‹
 - Title: Isabelle/Position.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  positions starting from 1; values <= 0 mean "absent". Count Isabelle
 , not UTF8 bytes nor UTF16 characters. Position range specifies a
 -open interval offset .. end_offset (exclusive).

  🚫‹$ISABELLE_HOME/src/Pure/General/position.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}

  Isabelle.Position (
 T, line_of, column_of, offset_of, end_offset_of, label_of, file_of, id_of,
 start, none, label, put_file, file, file_only, put_id, id, id_only,
 symbol, symbol_explode, symbol_explode_string, shift_offsets,
 of_properties, properties_of, def_properties_of, entity_markup, make_entity_markup,
 Report, Report_Text, is_reported, is_reported_range, here,
 Range, no_range, no_range_position, range_position, range
 
 

  Prelude hiding (id)
  Data.Maybe (isJust, fromMaybe)
  Data.Bifunctor (first)
  qualified Isabelle.Properties as Properties
  qualified Isabelle.Bytes as Bytes
  qualified Isabelle.Value as Value
  Isabelle.Bytes (Bytes)
  qualified Isabelle.Markup as Markup
  qualified Isabelle.YXML as YXML
  Isabelle.Library
  qualified Isabelle.Symbol as Symbol
  Isabelle.Symbol (Symbol)


 - position -}

  T =
 Position {
 _line :: Int,
 _column :: Int,
 _offset :: Int,
 _end_offset :: Int,
 _label :: Bytes,
 _file :: Bytes,
 _id :: Bytes }
 deriving (Eq, Ord)

 , invalid :: Int -> Bool
  i = i > 0
  = not . valid

  :: Int -> Maybe Int
  i = if valid i then Just i else Nothing

  :: Int -> Int -> Int
  i i' = if valid i then i' else i


 - fields -}

 , column_of, offset_of, end_offset_of :: T -> Maybe Int
  = maybe_valid . _line
  = maybe_valid . _column
  = maybe_valid . _offset
  = maybe_valid . _end_offset

  :: T -> Maybe Bytes
  = proper_string . _label

  :: T -> Maybe Bytes
  = proper_string . _file

  :: T -> Maybe Bytes
  = proper_string . _id


 - make position -}

  :: T
  = Position 1 1 1 0 Bytes.empty Bytes.empty Bytes.empty

  :: T
  = Position 0 0 0 0 Bytes.empty Bytes.empty Bytes.empty

  :: Bytes -> T -> T
  label pos = pos { _label = label }

  :: Bytes -> T -> T
  file pos = pos { _file = file }

  :: Bytes -> T
  file = put_file file start

  :: Bytes -> T
  file = put_file file none

  :: Bytes -> T -> T
  id pos = pos { _id = id }

  :: Bytes -> T
  id = put_id id start

  :: Bytes -> T
  id = put_id id none


 - count position -}

  :: Symbol -> Int -> Int
  "\n" line = if_valid line (line + 1)
  _ line = line

  :: Symbol -> Int -> Int
  "\n" column = if_valid column 1
  s column = if Symbol.not_eof s then if_valid column (column + 1) else column

  :: Symbol -> Int -> Int
  s offset = if Symbol.not_eof s then if_valid offset (offset + 1) else offset

  :: Symbol -> T -> T
  s pos =
 pos {
 _line = count_line s (_line pos),
 _column = count_column s (_column pos),
 _offset = count_offset s (_offset pos) }

  :: BYTES a => a -> T -> T
  = fold symbol . Symbol.explode . make_bytes

  :: String -> T -> T
  = symbol_explode


 - shift offsets -}

  :: Int -> T -> T
  shift pos = pos { _offset = offset', _end_offset = end_offset' }
 where
 offset = _offset pos
 end_offset = _end_offset pos
 offset' = if invalid offset || invalid shift then offset else offset + shift
 end_offset' = if invalid end_offset || invalid shift then end_offset else end_offset + shift


 - markup properties -}

  :: Properties.T -> Bytes -> Bytes
  props name = fromMaybe "" (Properties.get_value Just props name)

  :: Properties.T -> Bytes -> Int
  props name = fromMaybe 0 (Properties.get_value Value.parse_int props name)

  :: Properties.T -> T
  props =
 none {
 _line = get_int props Markup.lineN,
 _offset = get_int props Markup.offsetN,
 _end_offset = get_int props Markup.end_offsetN,
 _label = get_string props Markup.labelN,
 _file = get_string props Markup.fileN,
 _id = get_string props Markup.idN }

  :: Bytes -> Bytes -> Properties.T
  k s = if Bytes.null s then [] else [(k, s)]

  :: Bytes -> Int -> Properties.T
  k i = if invalid i then [] else [(k, Value.print_int i)]

  :: T -> Properties.T
  pos =
 int_entry Markup.lineN (_line pos) ++
 int_entry Markup.offsetN (_offset pos) ++
 int_entry Markup.end_offsetN (_end_offset pos) ++
 string_entry Markup.labelN (_label pos) ++
 string_entry Markup.fileN (_file pos) ++
 string_entry Markup.idN (_id pos)

  :: T -> Properties.T
  = properties_of #> map (first Markup.def_name)

  :: Bytes -> (Bytes, T) -> Markup.T
  kind (name, pos) =
 Markup.entity kind name |> Markup.properties (def_properties_of pos)

  :: Bool -> Int -> Bytes -> (Bytes, T) -> Markup.T
  def serial kind (name, pos) =
 let
 props =
 if def then (Markup.defN, Value.print_int serial) : properties_of pos
 else (Markup.refN, Value.print_int serial) : def_properties_of pos
 in Markup.entity kind name |> Markup.properties props


 - reports -}

  Report = (T, Markup.T)
  Report_Text = (Report, Bytes)

  :: T -> Bool
  pos = isJust (offset_of pos) && isJust (id_of pos)

  :: T -> Bool
  pos = is_reported pos && isJust (end_offset_of pos)


 - here: user output -}

  :: T -> Bytes
  pos = if Bytes.null s2 then "" else s1 <> m1 <> s2 <> m2
 where
 props = properties_of pos
 (m1, m2) = YXML.output_markup (Markup.properties props Markup.position)
 (s1, s2) =
 case (line_of pos, file_of pos) of
 (Just i, Nothing) -> (" ", "(line " <> Value.print_int i <> ")")
 (Just i, Just name) -> (" ", "(line " <> Value.print_int i <> " of " <> quote name <> ")")
 (Nothing, Just name) -> (" ", "(file " <> quote name <> ")")
 _ -> if is_reported pos then ("", "\092🚫") else ("", "")


 - range -}

  Range = (T, T)

  :: Range
  = (none, none)

  :: T -> T
  pos = pos { _end_offset = 0 }

  :: Range -> T
  (pos, pos') = pos { _end_offset = _offset pos' }

  :: Range -> Range
  (pos, pos') = (range_position (pos, pos'), no_range_position pos')
 ›

generate_file "Isabelle/XML.hs" = ‹
 - Title: Isabelle/XML.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  XML trees and representation of ML values.

  🚫‹$ISABELLE_HOME/src/Pure/PIDE/xml.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}
 -# OPTIONS_GHC -fno-warn-missing-signatures #-}

  Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
 

  Isabelle.Library
  qualified Isabelle.Properties as Properties
  qualified Isabelle.Markup as Markup
  qualified Isabelle.Buffer as Buffer
  qualified Isabelle.Bytes as Bytes
  Isabelle.Bytes (Bytes)


 - types -}

  Attributes = Properties.T
  Body = [Tree]
  Tree = Elem (Markup.T, Body) | Text Bytes


 - wrapped elements -}

  :: ((Markup.T, Body), [Tree]) -> Tree
  (((a, atts), body1), body2) =
 Elem ((‹XML.xml_elemN›, (‹XML.xml_nameN›, a) : atts), Elem ((‹XML.xml_bodyN›, []), body1) : body2)

  :: Tree -> Maybe ((Markup.T, Body), [Tree])
 
 (Elem ((‹XML.xml_elemN›, (‹XML.xml_nameN›, a) : atts), Elem ((‹XML.xml_bodyN›, []), body1) : body2)) =
 Just (((a, atts), body1), body2)
  _ = Nothing


 - text content -}

  :: Tree -> Buffer.T -> Buffer.T
  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

  :: Body -> Bytes
  = Buffer.build_content . fold add_content


 - string representation -}

  :: Char -> String
  '<' = "<"
  '>' = ">"
  '&' = "&"
  '\'' = "'"
  '\"' = """
  c = [c]

  :: Bytes -> Bytes
  = make_bytes . concatMap (encode_char . Bytes.char) . Bytes.unpack

  Show Tree where
 show tree =
 make_string $ Buffer.build_content (show_tree tree)
 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 (encode_text s)

 show_elem name atts =
 implode_space (name : map (\(a, x) -> a <> "=\"" <> encode_text x <> "\"") atts)
 ›

generate_file "Isabelle/XML/Encode.hs" = ‹
 - Title: Isabelle/XML/Encode.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  as data representation language.

  🚫‹$ISABELLE_HOME/src/Pure/PIDE/xml.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}
 -# OPTIONS_GHC -fno-warn-missing-signatures #-}

  Isabelle.XML.Encode (
 A, T, V, P,

 int_atom, bool_atom, unit_atom,

 tree, properties, string, int, bool, unit, pair, triple, list, option, variant
 
 

  Data.Maybe (fromJust)

  Isabelle.Library
  Isabelle.Bytes (Bytes)
  qualified Isabelle.Value as Value
  qualified Isabelle.Properties as Properties
  qualified Isabelle.XML as XML


  A a = a -> Bytes
  T a = a -> XML.Body
  V a = a -> Maybe ([Bytes], XML.Body)
  P a = a -> [Bytes]


 - atomic values

  :: A Int
  = Value.print_int

  :: A Bool
  False = "0"
  True = "1"

  :: A ()
  () = ""


 - structural nodes

  ts = XML.Elem ((":", []), ts)

  = map_index (\(i, x) -> (int_atom i, x))

  (tag, (xs, ts)) = XML.Elem ((int_atom tag, vector xs), ts)


 - representation of standard types

  :: T XML.Tree
  t = [t]

  :: T Properties.T
  props = [XML.Elem ((":", props), [])]

  :: T Bytes
  "" = []
  s = [XML.Text s]

  :: T Int
  = string . int_atom

  :: T Bool
  = string . bool_atom

  :: T ()
  = string . unit_atom

  :: T a -> T b -> T (a, b)
  f g (x, y) = [node (f x), node (g y)]

  :: T a -> T b -> T c -> T (a, b, c)
  f g h (x, y, z) = [node (f x), node (g y), node (h z)]

  :: T a -> T [a]
  f xs = map (node . f) xs

  :: T a -> T (Maybe a)
  _ Nothing = []
  f (Just x) = [node (f x)]

  :: [V a] -> T a
  fs x = [tagged (fromJust (get_index (\f -> f x) fs))]
 ›

generate_file "Isabelle/XML/Decode.hs" = ‹
 - Title: Isabelle/XML/Decode.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  as data representation language.

  🚫‹$ISABELLE_HOME/src/Pure/PIDE/xml.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}
 -# OPTIONS_GHC -fno-warn-missing-signatures #-}

  Isabelle.XML.Decode (
 A, T, V, P,

 int_atom, bool_atom, unit_atom,

 tree, properties, string, int, bool, unit, pair, triple, list, option, variant
 
 

  Isabelle.Library
  Isabelle.Bytes (Bytes)
  qualified Isabelle.Value as Value
  qualified Isabelle.Properties as Properties
  qualified Isabelle.XML as XML


  A a = Bytes -> a
  T a = XML.Body -> a
  V a = ([Bytes], XML.Body) -> a
  P a = [Bytes] -> a

  = error "Malformed XML atom"
  = error "Malformed XML body"


 - atomic values -}

  :: A Int
  s =
 case Value.parse_int s of
 Just i -> i
 Nothing -> err_atom

  :: A Bool
  "0" = False
  "1" = True
  _ = err_atom

  :: A ()
  "" = ()
  _ = err_atom


 - structural nodes -}

  (XML.Elem ((":", []), ts)) = ts
  _ = err_body

  atts =
 map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts

  (XML.Elem ((name, atts), ts)) = (int_atom name, (vector atts, ts))
  _ = err_body


 - representation of standard types -}

  :: T XML.Tree
  [t] = t
  _ = err_body

  :: T Properties.T
  [XML.Elem ((":", props), [])] = props
  _ = err_body

  :: T Bytes
  [] = ""
  [XML.Text s] = s
  _ = err_body

  :: T Int
  = int_atom . string

  :: T Bool
  = bool_atom . string

  :: T ()
  = unit_atom . string

  :: T a -> T b -> T (a, b)
  f g [t1, t2] = (f (node t1), g (node t2))
  _ _ _ = err_body

  :: T a -> T b -> T c -> T (a, b, c)
  f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
  _ _ _ _ = err_body

  :: T a -> T [a]
  f ts = map (f . node) ts

  :: T a -> T (Maybe a)
  _ [] = Nothing
  f [t] = Just (f (node t))
  _ _ = err_body

  :: [V a] -> T a
  fs [t] = (fs !! tag) (xs, ts)
 where (tag, (xs, ts)) = tagged t
  _ _ = err_body
 ›

generate_file "Isabelle/YXML.hs" = ‹
 - Title: Isabelle/YXML.hs
 Author: Makarius
 LICENSE: BSD 3-clause (Isabelle)

  text representation of XML trees. Suitable for direct
  into plain text.

  🚫‹$ISABELLE_HOME/src/Pure/PIDE/yxml.ML›.
 }

 -# LANGUAGE OverloadedStrings #-}
 -# OPTIONS_GHC -fno-warn-missing-signatures -fno-warn-incomplete-patterns #-}

  Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,
 buffer_body, buffer, string_of_body, string_of, parse_body, parse)
 

  qualified Data.List as List
  Data.Word (Word8)

  Isabelle.Library
  qualified Isabelle.Bytes as Bytes
  Isabelle.Bytes (Bytes)
  qualified Isabelle.Markup as Markup
  qualified Isabelle.XML as XML
  qualified Isabelle.Buffer as Buffer


 - markers -}

 , charY :: Word8
  = 5
  = 6

 , strY, strXY, strXYX :: Bytes
  = Bytes.singleton charX
  = Bytes.singleton charY
  = strX <> strY
  = strXY <> strX

  :: Bytes -> Bool
  = Bytes.any (\c -> c == charX || c == charY)


 - output -}

  :: Markup.T -> Markup.Output
  markup@(name, atts) =
 if Markup.is_empty markup then Markup.no_output
 else (strXY <> name <> Bytes.concat (map (\(a, x) -> strY <> a <> "=" <> x) atts) <> strX, strXYX)

  (a, x) =
 Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x

  :: XML.Body -> Buffer.T -> Buffer.T
  = fold buffer

  :: XML.Tree -> Buffer.T -> Buffer.T
  (XML.Elem ((name, atts), ts)) =
 Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
 buffer_body ts #>
 Buffer.add strXYX
  (XML.Text s) = Buffer.add s

  :: XML.Body -> Bytes
  = Buffer.build_content . buffer_body

  :: XML.Tree -> Bytes
  = string_of_body . single


 - parse -}

 - split: fields or non-empty tokens

  :: Bool -> Word8 -> [Word8] -> [[Word8]]
  _ _ [] = []
  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

  :: Bytes -> a
  msg = error (make_string ("Malformed YXML: " <> msg))

  = err "bad attribute"
  = err "bad element"

  :: Bytes -> a
  name =
 if Bytes.null name then err "unbalanced element"
 else err ("unbalanced element " <> quote name)


 - stack operations

  x ((elem, body) : pending) = (elem, x : body) : pending

  name atts pending =
 if Bytes.null name then err_element
 else ((name, atts), []) : pending

  (((name, atts), body) : pending) =
 if Bytes.null name then err_unbalanced name
 else add (XML.Elem ((name, atts), reverse body)) pending


 - parsing

  s =
 case List.elemIndex (Bytes.byte '=') s of
 Just i | i > 0 -> (Bytes.pack $ take i s, Bytes.pack $ drop (i + 1) s)
 _ -> err_attribute

  [[], []] = pop
  ([] : name : atts) = push (Bytes.pack name) (map parse_attrib atts)
  txts = fold (add . XML.Text . Bytes.pack) txts

  :: Bytes -> XML.Body
  source =
 case fold parse_chunk chunks [((Bytes.empty, []), [])] of
 [((name, _), result)] | Bytes.null name -> reverse result
 ((name, _), _) : _ -> err_unbalanced name
 where chunks = source |> Bytes.unpack |> split False charX |> map (split True charY)

  :: Bytes -> XML.Tree
  source =
 case parse_body source of
 [result] -> result
 [] -> XML.Text ""
 _ -> err "multiple results"
 ›

generate_file "Isabelle/Completion.hs" = ‹
{-  Title:      Isabelle/Completion.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Completion of names.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/completion.ML\<close>.
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Completion (
    Name, T, names, none, make, markup_element, markup_report, make_report
  ) where

import qualified Isabelle.Bytes as Bytes
import qualified Isabelle.Name as Name
import Isabelle.Name (Name)
import qualified Isabelle.Properties as Properties
import qualified Isabelle.Markup as Markup
import Isabelle.XML.Classes
import qualified Isabelle.XML as XML
import qualified Isabelle.YXML as YXML


type Names = [(Name, (Name, Name))]  -- external name, kind, internal name
data T = Completion Properties.T Int Names  -- position, total length, names

names :: Int -> Properties.T -> Names -> T
names limit props names = Completion props (length names) (take limit names)

none :: T
none = names 0 [] []

make :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> T
make limit (name, props) make_names =
  if name /= "" && name /= "_" then
    names limit props (make_names (Bytes.isPrefixOf (Name.clean name)))
  else none

markup_element :: T -> (Markup.T, XML.Body)
markup_element (Completion props total names) =
  if not (null names) then
    (Markup.properties props Markup.completion, encode (total, names))
  else (Markup.empty, [])

markup_report :: [T] -> Name
markup_report [] = Bytes.empty
markup_report elems =
  YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)

make_report :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> Name
make_report limit name_props make_names =
  markup_report [make limit name_props make_names]
\<close>

generate_file "Isabelle/File.hs" = \<open>
{-  Title:      Isabelle/File.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

File-system operations.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/file.ML\<close>.
-}

module Isabelle.File (read, write, append) where

import Prelude hiding (read)
import qualified System.IO as IO
import qualified Data.ByteString as ByteString
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)

read :: IO.FilePath -> IO Bytes
read path = Bytes.make <$> IO.withFile path IO.ReadMode ByteString.hGetContents

write :: IO.FilePath -> Bytes -> IO ()
write path bs = IO.withFile path IO.WriteMode (\h -> ByteString.hPut h (Bytes.unmake bs))

append :: IO.FilePath -> Bytes -> IO ()
append path bs = IO.withFile path IO.AppendMode (\h -> ByteString.hPut h (Bytes.unmake bs))
\<close>

generate_file "Isabelle/Pretty.hs" = \<open>
{-  Title:      Isabelle/Pretty.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Generic pretty printing module.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/pretty.ML\<close>.
-}

{-# LANGUAGE OverloadedStrings #-}
{-# 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 qualified Data.List as List

import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
import Isabelle.Library hiding (enclose, quote, separate, commas)
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 Bytes


{- output -}

symbolic_text s = if Bytes.null s then [] else [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 (Bytes.spaces wd))]
symbolic (Str s) = symbolic_text s

formatted :: T -> Bytes
formatted = YXML.string_of_body . symbolic

unformatted :: T -> Bytes
unformatted = Buffer.build_content . out
  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 (Bytes.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 :: BYTES a => a -> T
str = Str . make_bytes

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 :: BYTES a => [a] -> 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 :: BYTES a => (Markup.T, a) -> T
mark_str (m, s) = mark m (str s)

marks_str :: BYTES a => ([Markup.T], a) -> 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 :: BYTES a => a -> T
keyword1 name = mark_str (Markup.keyword1, name)
keyword2 name = mark_str (Markup.keyword2, name)

text :: BYTES a => a -> [T]
text = breaks . map str . filter (not . Bytes.null) . space_explode ' ' . make_bytes

paragraph :: [T] -> T
paragraph = markup Markup.paragraph

para :: BYTES a => a -> T
para = paragraph . text

quote :: T -> T
quote prt = blk (1, [Str "\"", prt, Str "\""])

cartouche :: T -> T
cartouche prt = blk (1, [Str "\92<open>", prt, Str "\92<close>"])

separate :: BYTES a => a -> [T] -> [T]
separate sep = List.intercalate [str sep, brk 1] . map single

commas :: [T] -> [T]
commas = separate ("," :: Bytes)

enclose :: BYTES a => a -> a -> [T] -> T
enclose lpar rpar prts = block (str lpar : prts <> [str rpar])

enum :: BYTES a => a -> a -> a -> [T] -> T
enum sep lpar rpar = enclose lpar rpar . separate sep

list :: BYTES a => a -> a -> [T] -> T
list = enum ","

str_list :: BYTES a => a -> a -> [a] -> T
str_list lpar rpar = list lpar rpar . map str

big_list :: BYTES a => a -> [T] -> T
big_list name prts = block (fbreaks (str name : prts))
\<close>

generate_file "Isabelle/Name.hs" = \<open>
{-  Title:      Isabelle/Name.hs
    Author:     Makarius

Names of basic logical entities (variables etc.).

See \<^file>\<open>$ISABELLE_HOME/src/Pure/name.ML\<close>.
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Name (
  Name,
  uu, uu_, aT,
  clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
  Context, declare, declare_renamed, is_declared, declared, context, make_context,
  variant, variant_list
)
where

import Data.Maybe (fromMaybe)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Word (Word8)
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Symbol as Symbol
import Isabelle.Library


type Name = Bytes


{- common defaults -}

uu, uu_, aT :: Name
uu = "uu"
uu_ = "uu_"
aT = "'a"


{- internal names -- NB: internal subsumes skolem -}

underscore :: Word8
underscore = Bytes.byte '_'

internal, skolem :: Name -> Name
internal x = x <> "_"
skolem x = x <> "__"

is_internal, is_skolem :: Name -> Bool
is_internal = Bytes.isSuffixOf "_"
is_skolem = Bytes.isSuffixOf "__"

dest_internal, dest_skolem :: Name -> Maybe Name
dest_internal = Bytes.try_unsuffix "_"
dest_skolem = Bytes.try_unsuffix "__"

clean_index :: (Name, Int) -> (Name, Int)
clean_index (x, i) =
  case dest_internal x of
    Nothing -> (x, i)
    Just x' -> clean_index (x', i + 1)

clean :: Name -> Name
clean x = fst (clean_index (x, 0))


{- context for used names -}

newtype Context = Context (Map Name (Maybe Name))  {-declared names with latest renaming-}

declare :: Name -> Context -> Context
declare x (Context names) =
  Context (
    let a = clean x
    in if Map.member a names then names else Map.insert a Nothing names)

declare_renaming :: (Name, Name) -> Context -> Context
declare_renaming (x, x') (Context names) =
  Context (Map.insert (clean x) (Just (clean x')) names)

declare_renamed :: (Name, Name) -> Context -> Context
declare_renamed (x, x') =
  (if clean x /= clean x' then declare_renaming (x, x') else id) #> declare x'

is_declared :: Context -> Name -> Bool
is_declared (Context names) x = Map.member x names

declared :: Context -> Name -> Maybe (Maybe Name)
declared (Context names) a = Map.lookup a names

context :: Context
context = Context Map.empty |> fold declare ["", "'"]

make_context :: [Name] -> Context
make_context used = fold declare used context


{- generating fresh names -}

bump_init :: Name -> Name
bump_init str = str <> "a"

bump_string :: Name -> Name
bump_string str =
  let
    a = Bytes.byte 'a'
    z = Bytes.byte 'z'
    bump (b : bs) | b == z = a : bump bs
    bump (b : bs) | a <= b && b < z = b + 1 : bs
    bump bs = a : bs

    rev = reverse (Bytes.unpack str)
    part2 = reverse (takeWhile (Symbol.is_ascii_quasi . Bytes.char) rev)
    part1 = reverse (bump (drop (length part2) rev))
  in Bytes.pack (part1 <> part2)

variant :: Name -> Context -> (Name, Context)
variant name ctxt =
  let
    vary x =
      case declared ctxt x of
        Nothing -> x
        Just x' -> vary (bump_string (fromMaybe x x'))

    (x, n) = clean_index (name, 0)
    (x', ctxt') =
      if not (is_declared ctxt x) then (x, declare x ctxt)
      else
        let
          x0 = bump_init x
          x' = vary x0
          ctxt' = ctxt |> declare_renamed (x0, x')
        in (x', ctxt')
  in (x' <> Bytes.pack (replicate n underscore), ctxt')

variant_list :: [Name] -> [Name] -> [Name]
variant_list used names = fst (make_context used |> fold_map variant names)
\<close>

generate_file "Isabelle/Term.hs" = \<open>
{-  Title:      Isabelle/Term.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Lambda terms, types, sorts.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/term.scala\<close>.
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Term (
  Indexname, Sort, Typ(..), Term(..),
  Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_lambda, strip_lambda,
  type_op0, type_op1, op0, op1, op2, typed_op0, typed_op1, typed_op2, binder,
  dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
  aconv, list_comb, strip_comb, head_of
)
where

import Isabelle.Library
import qualified Isabelle.Name as Name
import Isabelle.Name (Name)

infixr 5 -->
infixr --->


{- types and terms -}

type Indexname = (Name, Int)

type Sort = [Name]

data Typ =
    Type (Name, [Typ])
  | TFree (Name, Sort)
  | TVar (Indexname, Sort)
  deriving (Show, Eq, Ord)

data Term =
    Const (Name, [Typ])
  | Free (Name, Typ)
  | Var (Indexname, Typ)
  | Bound Int
  | Abs (Name, Typ, Term)
  | App (Term, Term)
  | OFCLASS (Typ, Name)
  deriving (Show, Eq, Ord)


{- free and bound variables -}

type Free = (Name, Typ)

lambda :: Free -> Term -> Term
lambda (name, typ) body = Abs (name, typ, abstract 0 body)
  where
    abstract lev (Free (x, ty)) | name == x && typ == ty = Bound lev
    abstract lev (Abs (a, ty, t)) = Abs (a, ty, abstract (lev + 1) t)
    abstract lev (App (t, u)) = App (abstract lev t, abstract lev u)
    abstract _ t = t

declare_frees :: Term -> Name.Context -> Name.Context
declare_frees (Free (x, _)) = Name.declare x
declare_frees (Abs (_, _, b)) = declare_frees b
declare_frees (App (t, u)) = declare_frees t #> declare_frees u
declare_frees _ = id

incr_boundvars :: Int -> Term -> Term
incr_boundvars inc = if inc == 0 then id else incr 0
  where
    incr lev (Bound i) = if i >= lev then Bound (i + inc) else Bound i
    incr lev (Abs (a, ty, b)) = Abs (a, ty, incr (lev + 1) b)
    incr lev (App (t, u)) = App (incr lev t, incr lev u)
    incr _ t = t

subst_bound :: Term -> Term -> Term
subst_bound arg = subst 0
  where
    subst lev (Bound i) =
      if i < lev then Bound i
      else if i == lev then incr_boundvars lev arg
      else Bound (i - 1)
    subst lev (Abs (a, ty, b)) = Abs (a, ty, subst (lev + 1) b)
    subst lev (App (t, u)) = App (subst lev t, subst lev u)
    subst _ t = t

dest_lambda :: Name.Context -> Term -> Maybe (Free, Term)
dest_lambda names (Abs (x, ty, b)) =
  let
    (x', _) = Name.variant x (declare_frees b names)
    v = (x', ty)
  in Just (v, subst_bound (Free v) b)
dest_lambda _ _ = Nothing

strip_lambda :: Name.Context -> Term -> ([Free], Term)
strip_lambda names tm =
  case dest_lambda names tm of
    Just (v, t) ->
      let (vs, t') = strip_lambda names t'
      in (v : vs, t')
    Nothing -> ([], tm)


{- type and term operators -}

type_op0 :: Name -> (Typ, Typ -> Bool)
type_op0 name = (mk, is)
  where
    mk = Type (name, [])
    is (Type (c, _)) = c == name
    is _ = False

type_op1 :: Name -> (Typ -> Typ, Typ -> Maybe Typ)
type_op1 name = (mk, dest)
  where
    mk ty = Type (name, [ty])
    dest (Type (c, [ty])) | c == name = Just ty
    dest _ = Nothing

type_op2 :: Name -> (Typ -> Typ -> Typ, Typ -> Maybe (Typ, Typ))
type_op2 name = (mk, dest)
  where
    mk ty1 ty2 = Type (name, [ty1, ty2])
    dest (Type (c, [ty1, ty2])) | c == name = Just (ty1, ty2)
    dest _ = Nothing

op0 :: Name -> (Term, Term -> Bool)
op0 name = (mk, is)
  where
    mk = Const (name, [])
    is (Const (c, _)) = c == name
    is _ = False

op1 :: Name -> (Term -> Term, Term -> Maybe Term)
op1 name = (mk, dest)
  where
    mk t = App (Const (name, []), t)
    dest (App (Const (c, _), t)) | c == name = Just t
    dest _ = Nothing

op2 :: Name -> (Term -> Term -> Term, Term -> Maybe (Term, Term))
op2 name = (mk, dest)
  where
    mk t u = App (App (Const (name, []), t), u)
    dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
    dest _ = Nothing

typed_op0 :: Name -> (Typ -> Term, Term -> Maybe Typ)
typed_op0 name = (mk, dest)
  where
    mk ty = Const (name, [ty])
    dest (Const (c, [ty])) | c == name = Just ty
    dest _ = Nothing

typed_op1 :: Name -> (Typ -> Term -> Term, Term -> Maybe (Typ, Term))
typed_op1 name = (mk, dest)
  where
    mk ty t = App (Const (name, [ty]), t)
    dest (App (Const (c, [ty]), t)) | c == name = Just (ty, t)
    dest _ = Nothing

typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term))
typed_op2 name = (mk, dest)
  where
    mk ty t u = App (App (Const (name, [ty]), t), u)
    dest (App (App (Const (c, [ty]), t), u)) | c == name = Just (ty, t, u)
    dest _ = Nothing

binder :: Name -> (Free -> Term -> Term, Name.Context -> Term -> Maybe (Free, Term))
binder name = (mk, dest)
  where
    mk (a, ty) b = App (Const (name, [ty]), lambda (a, ty) b)
    dest names (App (Const (c, _), t)) | c == name = dest_lambda names t
    dest _ _ = Nothing


{- type operations -}

dummyS :: Sort
dummyS = [""]

dummyT :: Typ; is_dummyT :: Typ -> Bool
(dummyT, is_dummyT) = type_op0 \<open>\<^type_name>\<open>dummy\<close>\<close>

propT :: Typ; is_propT :: Typ -> Bool
(propT, is_propT) = type_op0 \<open>\<^type_name>\<open>prop\<close>\<close>

(-->) :: Typ -> Typ -> Typ; dest_funT :: Typ -> Maybe (Typ, Typ)
((-->), dest_funT) = type_op2 \<open>\<^type_name>\<open>fun\<close>\<close>

(--->) :: [Typ] -> Typ -> Typ
[] ---> b = b
(a : as) ---> b = a --> (as ---> b)


{- term operations -}

aconv :: Term -> Term -> Bool
aconv (App (t1, u1)) (App (t2, u2)) = aconv t1 t2 && aconv u1 u2
aconv (Abs (_, ty1, t1)) (Abs (_, ty2, t2)) = aconv t1 t2 && ty1 == ty2
aconv a1 a2 = a1 == a2

list_comb :: Term -> [Term] -> Term
list_comb f [] = f
list_comb f (t : ts) = list_comb (App (f, t)) ts

strip_comb :: Term -> (Term, [Term])
strip_comb tm = strip (tm, [])
  where
    strip (App (f, t), ts) = strip (f, t : ts)
    strip x = x

head_of :: Term -> Term
head_of (App (f, _)) = head_of f
head_of u = u
\<close>

generate_file "Isabelle/Pure.hs" = \<open>
{-  Title:      Isabelle/Term.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Support for Isabelle/Pure logic.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/logic.ML\<close>.
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Pure (
  mk_forall_op, dest_forall_op, mk_forall, dest_forall,
  mk_equals, dest_equals, mk_implies, dest_implies
)
where

import qualified Isabelle.Name as Name
import Isabelle.Term

mk_forall_op :: Typ -> Term -> Term; dest_forall_op :: Term -> Maybe (Typ, Term)
(mk_forall_op, dest_forall_op) = typed_op1 \<open>\<^const_name>\<open>Pure.all\<close>\<close>

mk_forall :: Free -> Term -> Term; dest_forall :: Name.Context -> Term -> Maybe (Free, Term)
(mk_forall, dest_forall) = binder \<open>\<^const_name>\<open>Pure.all\<close>\<close>

mk_equals :: Typ -> Term -> Term -> Term; dest_equals :: Term -> Maybe (Typ, Term, Term)
(mk_equals, dest_equals) = typed_op2 \<open>\<^const_name>\<open>Pure.eq\<close>\<close>

mk_implies :: Term -> Term -> Term; dest_implies :: Term -> Maybe (Term, Term)
(mk_implies, dest_implies) = op2 \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
\<close>

generate_file "Isabelle/HOL.hs" = \<open>
{-  Title:      Isabelle/Term.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Support for Isabelle/HOL logic.

See \<^file>\<open>$ISABELLE_HOME/src/HOL/Tools/hologic.ML\<close>.
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.HOL (
  boolT, is_boolT, mk_trueprop, dest_trueprop,
  mk_setT, dest_setT, mk_mem, dest_mem,
  mk_eq, dest_eq, true, is_true, false, is_false,
  mk_not, dest_not, mk_conj, dest_conj, mk_disj, dest_disj,
  mk_imp, dest_imp, mk_iff, dest_iff,
  mk_all_op, dest_all_op, mk_ex_op, dest_ex_op,
  mk_all, dest_all, mk_ex, dest_ex,
  mk_undefined, dest_undefined
)
where

import qualified Isabelle.Name as Name
import Isabelle.Term


boolT :: Typ; is_boolT :: Typ -> Bool
(boolT, is_boolT) = type_op0 \<open>\<^type_name>\<open>bool\<close>\<close>

mk_trueprop :: Term -> Term; dest_trueprop :: Term -> Maybe Term
(mk_trueprop, dest_trueprop) = op1 \<open>\<^const_name>\<open>Trueprop\<close>\<close>

mk_setT :: Typ -> Typ; dest_setT :: Typ -> Maybe Typ
(mk_setT, dest_setT) = type_op1 \<open>\<^type_name>\<open>set\<close>\<close>

mk_mem :: Typ -> Term -> Term -> Term; dest_mem :: Term -> Maybe (Typ, Term, Term)
(mk_mem, dest_mem) = typed_op2 \<open>\<^const_name>\<open>Set.member\<close>\<close>

mk_eq :: Typ -> Term -> Term -> Term; dest_eq :: Term -> Maybe (Typ, Term, Term)
(mk_eq, dest_eq) = typed_op2 \<open>\<^const_name>\<open>HOL.eq\<close>\<close>

true :: Term; is_true :: Term -> Bool
(true, is_true) = op0 \<open>\<^const_name>\<open>True\<close>\<close>

false :: Term; is_false :: Term -> Bool
(false, is_false) = op0 \<open>\<^const_name>\<open>False\<close>\<close>

mk_not :: Term -> Term; dest_not :: Term -> Maybe Term
(mk_not, dest_not) = op1 \<open>\<^const_name>\<open>Not\<close>\<close>

mk_conj :: Term -> Term -> Term; dest_conj :: Term -> Maybe (Term, Term)
(mk_conj, dest_conj) = op2 \<open>\<^const_name>\<open>conj\<close>\<close>

mk_disj :: Term -> Term -> Term; dest_disj :: Term -> Maybe (Term, Term)
(mk_disj, dest_disj) = op2 \<open>\<^const_name>\<open>disj\<close>\<close>

mk_imp :: Term -> Term -> Term; dest_imp :: Term -> Maybe (Term, Term)
(mk_imp, dest_imp) = op2 \<open>\<^const_name>\<open>implies\<close>\<close>

mk_iff :: Term -> Term -> Term
mk_iff = mk_eq boolT

dest_iff :: Term -> Maybe (Term, Term)
dest_iff tm =
  case dest_eq tm of
    Just (ty, t, u) | ty == boolT -> Just (t, u)
    _ -> Nothing

mk_all_op :: Typ -> Term -> Term; dest_all_op :: Term -> Maybe (Typ, Term)
(mk_all_op, dest_all_op) = typed_op1 \<open>\<^const_name>\<open>All\<close>\<close>

mk_ex_op :: Typ -> Term -> Term; dest_ex_op :: Term -> Maybe (Typ, Term)
(mk_ex_op, dest_ex_op) = typed_op1 \<open>\<^const_name>\<open>Ex\<close>\<close>

mk_all :: Free -> Term -> Term; dest_all :: Name.Context -> Term -> Maybe (Free, Term)
(mk_all, dest_all) = binder \<open>\<^const_name>\<open>All\<close>\<close>

mk_ex :: Free -> Term -> Term; dest_ex :: Name.Context -> Term -> Maybe (Free, Term)
(mk_ex, dest_ex) = binder \<open>\<^const_name>\<open>Ex\<close>\<close>

mk_undefined :: Typ -> Term; dest_undefined :: Term -> Maybe Typ
(mk_undefined, dest_undefined) = typed_op0 \<open>\<^const_name>\<open>undefined\<close>\<close>
\<close>

generate_file "Isabelle/Term_XML/Encode.hs" = \<open>
{-  Title:      Isabelle/Term_XML/Encode.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

XML data representation of lambda terms.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
-}

{-# LANGUAGE LambdaCase #-}

module Isabelle.Term_XML.Encode (indexname, sort, typ, 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 }]

var_type :: T Typ
var_type 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], var_type b); _ -> Nothing },
    \case { Var (a, b) -> Just (indexname a, var_type 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 },
    \case { OFCLASS (a, b) -> Just ([b], typ a); _ -> Nothing }]
\<close>

generate_file "Isabelle/Term_XML/Decode.hs" = \<open>
{-  Title:      Isabelle/Term_XML/Decode.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

XML data representation of lambda terms.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/term_xml.ML\<close>.
-}

{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}

module Isabelle.Term_XML.Decode (indexname, sort, typ, 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)]

var_type :: T Typ
var_type [] = dummyT
var_type body = typ body

term :: T Term
term t =
  t |> variant
   [\([a], b) -> Const (a, list typ b),
    \([a], b) -> Free (a, var_type b),
    \(a, b) -> Var (indexname a, var_type 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),
    \([a], b) -> OFCLASS (typ b, 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 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
    LICENSE:    BSD 3-clause (Isabelle)

Universally unique identifiers.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/General/uuid.scala\<close>.
-}

module Isabelle.UUID (T, random, print, parse)
where

import Prelude hiding (print)

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

random :: IO T
random = nextRandom

print :: T -> Bytes
print = Bytes.make . UUID.toASCIIBytes

parse :: Bytes -> Maybe T
parse = UUID.fromASCIIBytes . Bytes.unmake
\<close>

generate_file "Isabelle/Byte_Message.hs" = \<open>
{-  Title:      Isabelle/Byte_Message.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Byte-oriented messages.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.ML\<close>
and \<^file>\<open>$ISABELLE_HOME/src/Pure/PIDE/byte_message.scala\<close>.
-}

{-# LANGUAGE OverloadedStrings #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}

module Isabelle.Byte_Message (
    write, write_line,
    read, read_block, read_line,
    make_message, write_message, read_message,
    exchange_message, exchange_message0,
    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.Symbol as Symbol
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
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)

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 = [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 ',' 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

exchange_message :: Socket -> [Bytes] -> IO (Maybe [Bytes])
exchange_message socket msg = do
  write_message socket msg
  read_message socket

exchange_message0 :: Socket -> [Bytes] -> IO ()
exchange_message0 socket msg = do
  _ <- exchange_message socket msg
  return ()


-- hybrid messages: line or length+block (with content restriction)

is_length :: Bytes -> Bool
is_length msg =
  not (Bytes.null msg) && Bytes.all_char (\c -> '0' <= c && c <= '9') msg

is_terminated :: Bytes -> Bool
is_terminated msg =
  not (Bytes.null msg) && Symbol.is_ascii_line_terminator (Bytes.char $ Bytes.last msg)

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_char (== '\n') 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 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 <$> res)

write_yxml :: Socket -> XML.Body -> IO ()
write_yxml socket body =
  write_line_message socket (YXML.string_of_body body)
\<close>

generate_file "Isabelle/Isabelle_Thread.hs" = \<open>
{-  Title:      Isabelle/Isabelle_Thread.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Isabelle-specific thread management.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.ML\<close>
and \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.scala\<close>.
-}

{-# 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
\<close>

generate_file "Isabelle/Server.hs" = \<open>
{-  Title:      Isabelle/Server.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

TCP server on localhost.
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Server (
  localhost_name, localhost_prefix, 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 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
import qualified Isabelle.Isabelle_Thread as Isabelle_Thread


{- server address -}

localhost_name :: Bytes
localhost_name = "127.0.0.1"

localhost_prefix :: Bytes
localhost_prefix = localhost_name <> ":"

localhost :: Socket.HostAddress
localhost = Socket.tupleToHostAddress (127, 0, 0, 1)

publish_text :: Bytes -> Bytes -> UUID.T -> Bytes
publish_text name address password =
  "server " <> quote name <> " = " <> address <>
    " (password " <> quote (show_bytes password) <> ")"

publish_stdout :: Bytes -> Bytes -> UUID.T -> IO ()
publish_stdout name address password =
  Char8.putStrLn (Bytes.unmake $ publish_text name address password)


{- server -}

server :: (Bytes -> 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_bytes port
      password <- UUID.random
      publish address password

      return (server_socket, UUID.print 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 -> Bytes -> (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 $ make_string localhost_name) (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 password
      client socket
\<close>

generate_file "Isabelle/Time.hs" = \<open>
{-  Title:      Isabelle/Time.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Time based on milliseconds.

See \<^file>\<open>~~/src/Pure/General/time.scala\<close>
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Time (
  Time, seconds, minutes, ms, zero, is_zero, is_relevant,
  get_seconds, get_minutes, get_ms, message, now
)
where

import Text.Printf (printf)
import Data.Time.Clock.POSIX (getPOSIXTime)
import Isabelle.Bytes (Bytes)
import Isabelle.Library


newtype Time = Time Int

instance Eq Time where Time a == Time b = a == b
instance Ord Time where compare (Time a) (Time b) = compare a b
instance Num Time where
  fromInteger = Time . fromInteger
  Time a + Time b = Time (a + b)
  Time a - Time b = Time (a - b)
  Time a * Time b = Time (a * b)
  abs (Time a) = Time (abs a)
  signum (Time a) = Time (signum a)

seconds :: Double -> Time
seconds s = Time (round (s * 1000.0))

minutes :: Double -> Time
minutes m = Time (round (m * 60000.0))

ms :: Int -> Time
ms = Time

zero :: Time
zero = ms 0

is_zero :: Time -> Bool
is_zero (Time ms) = ms == 0

is_relevant :: Time -> Bool
is_relevant (Time ms) = ms >= 1

get_seconds :: Time -> Double
get_seconds (Time ms) = fromIntegral ms / 1000.0

get_minutes :: Time -> Double
get_minutes (Time ms) = fromIntegral ms / 60000.0

get_ms :: Time -> Int
get_ms (Time ms) = ms

instance Show Time where
  show t = printf "%.3f" (get_seconds t)

message :: Time -> Bytes
message t = make_bytes (show t) <> "s"

now :: IO Time
now = do
  t <- getPOSIXTime
  return $ Time (round (realToFrac t * 1000.0 :: Double))
\<close>

generate_file "Isabelle/Timing.hs" = \<open>
{-  Title:      Isabelle/Timing.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Support for time measurement.

See \<^file>\<open>~~/src/Pure/General/timing.ML\<close>
and \<^file>\<open>~~/src/Pure/General/timing.scala\<close>
-}

module Isabelle.Timing (
  Timing (..), zero, is_zero, is_relevant
)
where

import qualified Isabelle.Time as Time
import Isabelle.Time (Time)

data Timing = Timing {elapsed :: Time, cpu :: Time, gc :: Time}
  deriving (Show, Eq)

zero :: Timing
zero = Timing Time.zero Time.zero Time.zero

is_zero :: Timing -> Bool
is_zero t = Time.is_zero (elapsed t) && Time.is_zero (cpu t) && Time.is_zero (gc t)

is_relevant :: Timing -> Bool
is_relevant t = Time.is_relevant (elapsed t) || Time.is_relevant (cpu t) || Time.is_relevant (gc t)
\<close>

generate_file "Isabelle/Bash.hs" = \<open>
{-  Title:      Isabelle/Bash.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Support for GNU bash.

See \<^file>\<open>$ISABELLE_HOME/src/Pure/System/bash.ML\<close>
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Bash (
  string, strings,

  Params,
  get_script, get_input, get_cwd, get_putenv, get_redirect,
  get_timeout, get_description,
  script, input, cwd, putenv, redirect, timeout, description,
  server_run, server_kill,
  server_uuid, server_interrupt, server_failure, server_result
)
where

import Text.Printf (printf)
import qualified Isabelle.Symbol as Symbol
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Time as Time
import Isabelle.Time (Time)
import Isabelle.Library


{- concrete syntax -}

string :: Bytes -> Bytes
string str =
  if Bytes.null str then "\"\""
  else str |> Bytes.unpack |> map trans |> Bytes.concat
    where
      trans b =
        case Bytes.char b of
          '\t' -> "$'\\t'"
          '\n' -> "$'\\n'"
          '\f' -> "$'\\f'"
          '\r' -> "$'\\r'"
          c ->
            if Symbol.is_ascii_letter c || Symbol.is_ascii_digit c || c `elem` ("+,-./:_" :: String)
            then Bytes.singleton b
            else if b < 32 || b >= 127 then make_bytes (printf "$'\\x%02x'" b :: String)
            else "\\" <> Bytes.singleton b

strings :: [Bytes] -> Bytes
strings = implode_space . map string


{- server parameters -}

data Params = Params {
    _script :: Bytes,
    _input :: Bytes,
    _cwd :: Maybe Bytes,
    _putenv :: [(Bytes, Bytes)],
    _redirect :: Bool,
    _timeout :: Time,
    _description :: Bytes}
  deriving (Show, Eq)

get_script :: Params -> Bytes
get_script = _script

get_input :: Params -> Bytes
get_input = _input

get_cwd :: Params -> Maybe Bytes
get_cwd = _cwd

get_putenv :: Params -> [(Bytes, Bytes)]
get_putenv = _putenv

get_redirect :: Params -> Bool
get_redirect = _redirect

get_timeout :: Params -> Time
get_timeout = _timeout

get_description :: Params -> Bytes
get_description = _description

script :: Bytes -> Params
script script = Params script "" Nothing [] False Time.zero ""

input :: Bytes -> Params -> Params
input input params = params { _input = input }

cwd :: Bytes -> Params -> Params
cwd cwd params = params { _cwd = Just cwd }

putenv :: [(Bytes, Bytes)] -> Params -> Params
putenv putenv params = params { _putenv = putenv }

redirect :: Params -> Params
redirect params = params { _redirect = True }

timeout :: Time -> Params -> Params
timeout timeout params = params { _timeout = timeout }

description :: Bytes -> Params -> Params
description description params = params { _description = description }


{- server messages -}

server_run, server_kill :: Bytes
server_run = \<open>Bash.server_run\<close>;
server_kill = \<open>Bash.server_kill\<close>;

server_uuid, server_interrupt, server_failure, server_result :: Bytes
server_uuid = \<open>Bash.server_uuid\<close>;
server_interrupt = \<open>Bash.server_interrupt\<close>;
server_failure = \<open>Bash.server_failure\<close>;
server_result = \<open>Bash.server_result\<close>;
\<close>

generate_file "Isabelle/Process_Result.hs" = \<open>
{-  Title:      Isabelle/Process_Result.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Result of system process.

See \<^file>\<open>~~/src/Pure/System/process_result.ML\<close>
and \<^file>\<open>~~/src/Pure/System/process_result.scala\<close>
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Process_Result (
  ok_rc, error_rc, failure_rc, interrupt_rc , timeout_rc,

  T, make, rc, out_lines, err_lines, timing, timing_elapsed, out, err, ok, check
)
where

import Isabelle.Time (Time)
import qualified Isabelle.Timing as Timing
import Isabelle.Timing (Timing)
import Isabelle.Bytes (Bytes)
import Isabelle.Library


ok_rc, error_rc, failure_rc, interrupt_rc , timeout_rc :: Int
ok_rc = 0
error_rc = 1
failure_rc = 2
interrupt_rc = 130
timeout_rc = 142

data T =
  Process_Result {
    _rc :: Int,
    _out_lines :: [Bytes],
    _err_lines :: [Bytes],
    _timing :: Timing}
  deriving (Show, Eq)

make :: Int -> [Bytes] -> [Bytes] -> Timing -> T
make = Process_Result

rc :: T -> Int
rc = _rc

out_lines :: T -> [Bytes]
out_lines = _out_lines

err_lines :: T -> [Bytes]
err_lines = _err_lines

timing :: T -> Timing
timing = _timing

timing_elapsed :: T -> Time
timing_elapsed = Timing.elapsed . timing

out :: T -> Bytes
out = trim_line . cat_lines . out_lines

err :: T -> Bytes
err = trim_line . cat_lines . err_lines

ok :: T -> Bool
ok result = rc result == ok_rc

check :: T -> T
check result = if ok result then result else error (make_string $ err result)
\<close>

generate_file "Isabelle/Options.hs" = \<open>
{-  Title:      Isabelle/Options.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

System options with external string representation.

See \<^file>\<open>~~/src/Pure/System/options.ML\<close>
and \<^file>\<open>~~/src/Pure/System/options.scala\<close>
-}

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE InstanceSigs #-}

module Isabelle.Options (
  boolT, intT, realT, stringT, unknownT,

  T, typ, bool, int, real, seconds, string,
  decode
)
where

import qualified Data.Map.Strict as Map
import Data.Map.Strict (Map)
import qualified Isabelle.Properties as Properties
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Value as Value
import qualified Isabelle.Time as Time
import Isabelle.Time (Time)
import Isabelle.Library
import qualified Isabelle.XML.Decode as Decode
import Isabelle.XML.Classes (Decode (..))


{- representation -}

boolT :: Bytes
boolT = "bool"

intT :: Bytes
intT = "int"

realT :: Bytes
realT = "real"

stringT :: Bytes
stringT = "string"

unknownT :: Bytes
unknownT = "unknown"

data Opt = Opt {
  _pos :: Properties.T,
  _name :: Bytes,
  _typ :: Bytes,
  _value :: Bytes }

newtype T = Options (Map Bytes Opt)


{- check -}

check_name :: T -> Bytes -> Opt
check_name (Options map) name =
  case Map.lookup name map of
    Just opt | _typ opt /= unknownT -> opt
    _ -> error (make_string ("Unknown system option " <> quote name))

check_type :: T -> Bytes -> Bytes -> Opt
check_type options name typ =
  let
    opt = check_name options name
    t = _typ opt
  in
    if t == typ then opt
    else error (make_string ("Ill-typed system option " <> quote name <> " : " <> t <> " vs. " <> typ))


{- get typ -}

typ :: T -> Bytes -> Bytes
typ options name = _typ (check_name options name)


{- get value -}

get :: Bytes -> (Bytes -> Maybe a) -> T -> Bytes -> a
get typ parse options name =
  let opt = check_type options name typ in
    case parse (_value opt) of
      Just x -> x
      Nothing ->
        error (make_string ("Malformed value for system option " <> quote name <>
          " : " <> typ <> " =\n" <> quote (_value opt)))

bool :: T -> Bytes -> Bool
bool = get boolT Value.parse_bool

int :: T -> Bytes -> Int
int = get intT Value.parse_int

real :: T -> Bytes -> Double
real = get realT Value.parse_real

seconds :: T -> Bytes -> Time
seconds options = Time.seconds . real options

string :: T -> Bytes -> Bytes
string = get stringT Just


{- decode -}

instance Decode T where
  decode :: Decode.T T
  decode =
    let
      decode_entry :: Decode.T (Bytes, Opt)
      decode_entry body =
        let
          (pos, (name, (typ, value))) =
            Decode.pair Decode.properties (Decode.pair Decode.string (Decode.pair Decode.string Decode.string)) body
        in (name, Opt { _pos = pos, _name = name, _typ = typ, _value = value })
    in Options . Map.fromList . Decode.list decode_entry
\<close>

generate_file "Isabelle/Isabelle_System.hs" = \<open>
{-  Title:      Isabelle/Isabelle_System.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Isabelle system support.

See \<^file>\<open>~~/src/Pure/System/isabelle_system.ML\<close>
and \<^file>\<open>~~/src/Pure/System/isabelle_system.scala\<close>
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Isabelle_System (
  bash_process, bash_process0
)
where

import Data.Maybe (fromMaybe)
import Control.Exception (throw, AsyncException (UserInterrupt))
import Network.Socket (Socket)
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Byte_Message as Byte_Message
import qualified Isabelle.Time as Time
import Isabelle.Timing (Timing (..))
import qualified Isabelle.Options as Options
import qualified Isabelle.Bash as Bash
import qualified Isabelle.Process_Result as Process_Result
import qualified Isabelle.XML.Encode as Encode
import qualified Isabelle.YXML as YXML
import qualified Isabelle.Value as Value
import qualified Isabelle.Server as Server
import qualified Isabelle.Isabelle_Thread as Isabelle_Thread
import Isabelle.Library


{- bash_process -}

absolute_path :: Bytes -> Bytes  -- FIXME dummy
absolute_path = id

bash_process :: Options.T -> Bash.Params -> IO Process_Result.T
bash_process options = bash_process0 address password
  where
    address = Options.string options "bash_process_address"
    password = Options.string options "bash_process_password"

bash_process0 :: Bytes -> Bytes -> Bash.Params -> IO Process_Result.T
bash_process0 address password params = do
  Server.connection port password
    (\socket -> do
        isabelle_tmp <- getenv "ISABELLE_TMP"
        Byte_Message.write_message socket (run isabelle_tmp)
        loop Nothing socket)
  where
    port =
      case Bytes.try_unprefix Server.localhost_prefix address of
        Just port -> make_string port
        Nothing -> errorWithoutStackTrace "Bad bash_process server address"

    script = Bash.get_script params
    input = Bash.get_input params
    cwd = Bash.get_cwd params
    putenv = Bash.get_putenv params
    redirect = Bash.get_redirect params
    timeout = Bash.get_timeout params
    description = Bash.get_description params

    run :: Bytes -> [Bytes]
    run isabelle_tmp =
     [Bash.server_run, script, input,
      YXML.string_of_body (Encode.option (Encode.string . absolute_path) cwd),
      YXML.string_of_body
      (Encode.list (Encode.pair Encode.string Encode.string)
        (("ISABELLE_TMP", isabelle_tmp) : putenv)),
      Value.print_bool redirect,
      Value.print_real (Time.get_seconds timeout),
      description]

    kill :: Maybe Bytes -> IO ()
    kill maybe_uuid = do
      case maybe_uuid of
        Just uuid ->
          Server.connection port password (\socket ->
            Byte_Message.write_message socket [Bash.server_kill, uuid])
        Nothing -> return ()

    err = errorWithoutStackTrace "Malformed result from bash_process server"
    the = fromMaybe err

    loop :: Maybe Bytes -> Socket -> IO Process_Result.T
    loop maybe_uuid socket = do
      result <- Isabelle_Thread.bracket_resource (kill maybe_uuid) (Byte_Message.read_message socket)
      case result of
        Just [head, uuid] | head == Bash.server_uuid -> loop (Just uuid) socket
        Just [head] | head == Bash.server_interrupt -> throw UserInterrupt
        Just [head, msg] | head == Bash.server_failure -> errorWithoutStackTrace $ make_string msg
        Just (head : a : b : c : d : lines) | head == Bash.server_result ->
          let
            rc = the $ Value.parse_int a
            elapsed = Time.ms $ the $ Value.parse_int b
            cpu = Time.ms $ the $ Value.parse_int c
            timing = Timing elapsed cpu Time.zero
            n = the $ Value.parse_int d
            out_lines = take n lines
            err_lines = drop n lines
          in return $ Process_Result.make rc out_lines err_lines timing
        _ -> err
\<close>

generate_file "Isabelle/Cache.hs" = \<open>
{-  Title:      Isabelle/Cache.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Cache for slow computations.
-}

module Isabelle.Cache (
  T, init, apply, prune
)
where

import Prelude hiding (init)
import Data.IORef
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import qualified Data.List as List

import Isabelle.Time (Time)
import qualified Isabelle.Time as Time


data Entry v = Entry {_value :: v, _access :: Time, _timing :: Time}

newtype T k v = Cache (IORef (Map k (Entry v)))

init :: IO (T k v)
init = Cache <$> newIORef Map.empty

commit :: Ord k => T k v -> k -> Entry v -> IO v
commit (Cache ref) x e = do
  atomicModifyIORef' ref (\entries ->
    let
      entry =
        case Map.lookup x entries of
          Just e' | _access e' > _access e -> e'
          _ -> e
    in (Map.insert x entry entries, _value entry))

apply :: Ord k => T k v -> k -> IO v -> IO v
apply cache@(Cache ref) x body = do
  start <- Time.now
  entries <- readIORef ref
  case Map.lookup x entries of
    Just entry -> do
      commit cache x (entry {_access = start})
    Nothing -> do
      y <- body
      stop <- Time.now
      commit cache x (Entry y start (stop - start))

prune :: Ord k => T k v -> Int -> Time -> IO ()
prune (Cache ref) max_size min_timing = do
  atomicModifyIORef' ref (\entries ->
    let
      sort = List.sortBy (\(_, e1) (_, e2) -> compare (_access e2) (_access e1))
      entries1 = Map.filter (\e -> _timing e >= min_timing) entries
      entries2 =
        if Map.size entries1 <= max_size then entries1
        else Map.fromList $ List.take max_size $ sort $ Map.toList entries1
    in (entries2, ()))
\<close>

export_generated_files _

end