Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/Isabelle/Tools/Haskell/ (Eine funktionale Sprache ^©) Datei vom 16.11.2025 mit Größe 101 kB

Quellcode-Bibliothek Haskell.thy Sprache: Isabelle

(*  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" = \<open>
{-  Title:      Isabelle/Bytes.hs
    Author:     Makarius
    LICENSE:    BSD 3-clause (Isabelle)

Compact byte strings.

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

{-# LANGUAGE TypeApplications #-}

module 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
)
where

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

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

type Bytes = ShortByteString

make :: ByteString -> Bytes
make = ShortByteString.toShort

unmake :: Bytes -> ByteString
unmake = ShortByteString.fromShort

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

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

empty :: Bytes
empty = ShortByteString.empty

null :: Bytes -> Bool
null = ShortByteString.null

length :: Bytes -> Int
length = ShortByteString.length

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

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

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

head :: Bytes -> Word8
head bytes = index bytes 0

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

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

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

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

isSuffixOf :: Bytes -> Bytes -> Bool
isSuffixOf 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

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

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

concat :: [Bytes] -> Bytes
concat = mconcat

space :: Word8
space = 32

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

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

char :: Word8 -> Char
char = toEnum . fromEnum

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

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

byte :: Char -> Word8
byte = toEnum . fromEnum

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

singleton :: Word8 -> Bytes
singleton b = singletons ! b
\<close>

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

Variations on UTF-8.

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

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

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

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

import Data.ByteString (ByteString)

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

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

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

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

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

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

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

instance Recode String Bytes where
  encode :: String -> Bytes
  encode = encode . Text.pack
  decode :: Bytes -> String
  decode = Text.unpack . decode
\<close>

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

Basic library of Isabelle idioms.

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

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

module 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)
where

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

{- functions -}

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

(|->) :: (a, b) -> (a -> b -> c) -> c
(x, y) |-> f = f x y

(#>) :: (a -> b) -> (b -> c) -> a -> c
(f #> g) x = x |> f |> g

(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
(f #-> g) x  = x |> f |-> g

{- lists -}

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

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

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

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

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

singletonM :: Monad m => ([a] -> m [b]) -> a -> m b
singletonM f x = the_single <$> f [x]

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

get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
get_index f = get_aux 0
  where
    get_aux _ [] = Nothing
    get_aux i (x : xs) =
      case f x of
        Nothing -> get_aux (i + 1) xs
        Just y -> Just (i, y)

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

{- string-like interfaces -}

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

gen_trim_line :: Int -> (Int -> Char) -> (Int -> a -> a) -> a -> a
gen_trim_line 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

instance 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

instance 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

instance 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

instance 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

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

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

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

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

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

{- strings -}

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

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

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

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

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

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

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

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

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

{- getenv -}

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

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

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

Isabelle text symbols.

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

{-# LANGUAGE OverloadedStrings #-}

module 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
)
where

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

{- type -}

type Symbol = Bytes

eof :: Symbol
eof = ""

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

{- ASCII characters -}

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

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

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

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

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

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

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

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

{- explode symbols: ASCII, UTF8, named -}

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

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

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

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

explode :: Bytes -> [Symbol]
explode 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 []
\<close>

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

Efficient buffer of byte strings.

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

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

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

newtype T = Buffer [Bytes]

empty :: T
empty = Buffer []

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

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

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

build_content :: (T -> T) -> Bytes
build_content f = build f |> content
\<close>

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

Plain values, represented as string.

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

{-# LANGUAGE OverloadedStrings #-}

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

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

{- bool -}

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

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

{- nat -}

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

{- int -}

print_int :: Int -> Bytes
print_int = show_bytes

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

{- real -}

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

parse_real :: Bytes -> Maybe Double
parse_real = Read.readMaybe . make_string
\<close>

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

Property lists.

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

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

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

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

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

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

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

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

remove :: Bytes -> T -> T
remove name props =
  if defined props name then filter (\(a, _) -> a /= name) props
  else props
\<close>

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

Quasi-abstract markup elements.

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

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

module Isabelle.Markup (
  T, empty, is_empty, properties,

  nameN, name, xnameN, xname, kindN,

  bindingN, binding, entityN, entity, defN, refN,

  completionN, completion, no_completionN, no_completion,

  lineN, end_lineN, offsetN, end_offsetN, 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)
where

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

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

{- basic markup -}

type T = (Bytes, Properties.T)

empty :: T
empty = ("", [])

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

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

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

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

{- misc properties -}

nameN :: Bytes
nameN = \<open>Markup.nameN\<close>

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

xnameN :: Bytes
xnameN = \<open>Markup.xnameN\<close>

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

kindN :: Bytes
kindN = \<open>Markup.kindN\<close>

{- formal entities -}

bindingN :: Bytes
bindingN = \<open>Markup.bindingN\<close>
binding :: T
binding = markup_elem bindingN

entityN :: Bytes
entityN = \<open>Markup.entityN\<close>
entity :: Bytes -> Bytes -> T
entity kind name =
  (entityN,
    (if Bytes.null name then [] else [(nameN, name)]) <>
    (if Bytes.null kind then [] else [(kindN, kind)]))

defN :: Bytes
defN = \<open>Markup.defN\<close>

refN :: Bytes
refN = \<open>Markup.refN\<close>

{- completion -}

completionN :: Bytes
completionN = \<open>Markup.completionN\<close>
completion :: T
completion = markup_elem completionN

no_completionN :: Bytes
no_completionN = \<open>Markup.no_completionN\<close>
no_completion :: T
no_completion = markup_elem no_completionN

{- position -}

lineN, end_lineN :: Bytes
lineN = \<open>Markup.lineN\<close>
end_lineN = \<open>Markup.end_lineN\<close>

offsetN, end_offsetN :: Bytes
offsetN = \<open>Markup.offsetN\<close>
end_offsetN = \<open>Markup.end_offsetN\<close>

labelN, fileN, idN :: Bytes
labelN = \<open>Markup.labelN\<close>
fileN = \<open>Markup.fileN\<close>
idN = \<open>Markup.idN\<close>

positionN :: Bytes
positionN = \<open>Markup.positionN\<close>
position :: T
position = markup_elem positionN

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

{- position "def" names -}

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

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

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

{- expression -}

expressionN :: Bytes
expressionN = \<open>Markup.expressionN\<close>

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

{- external resources -}

pathN :: Bytes
pathN = \<open>Markup.pathN\<close>
path :: Bytes -> T
path = markup_string pathN nameN

urlN :: Bytes
urlN = \<open>Markup.urlN\<close>
url :: Bytes -> T
url = markup_string urlN nameN

docN :: Bytes
docN = \<open>Markup.docN\<close>
doc :: Bytes -> T
doc = markup_string docN nameN

{- pretty printing -}

markupN, consistentN, unbreakableN, indentN :: Bytes
markupN = \<open>Markup.markupN\<close>
consistentN = \<open>Markup.consistentN\<close>
unbreakableN = \<open>Markup.unbreakableN\<close>
indentN = \<open>Markup.indentN\<close>

widthN :: Bytes
widthN = \<open>Markup.widthN\<close>

blockN :: Bytes
blockN = \<open>Markup.blockN\<close>
block :: Bool -> Int -> T
block c i =
  (blockN,
    (if c then [(consistentN, Value.print_bool c)] else []) <>
    (if i /= 0 then [(indentN, Value.print_int i)] else []))

breakN :: Bytes
breakN = \<open>Markup.breakN\<close>
break :: Int -> Int -> T
break w i =
  (breakN,
    (if w /= 0 then [(widthN, Value.print_int w)] else []) <>
    (if i /= 0 then [(indentN, Value.print_int i)] else []))

fbreakN :: Bytes
fbreakN = \<open>Markup.fbreakN\<close>
fbreak :: T
fbreak = markup_elem fbreakN

itemN :: Bytes
itemN = \<open>Markup.itemN\<close>
item :: T
item = markup_elem itemN

{- text properties -}

wordsN :: Bytes
wordsN = \<open>Markup.wordsN\<close>
words :: T
words = markup_elem wordsN

{- inner syntax -}

tfreeN :: Bytes
tfreeN = \<open>Markup.tfreeN\<close>
tfree :: T
tfree = markup_elem tfreeN

tvarN :: Bytes
tvarN = \<open>Markup.tvarN\<close>
tvar :: T
tvar = markup_elem tvarN

freeN :: Bytes
freeN = \<open>Markup.freeN\<close>
free :: T
free = markup_elem freeN

skolemN :: Bytes
skolemN = \<open>Markup.skolemN\<close>
skolem :: T
skolem = markup_elem skolemN

boundN :: Bytes
boundN = \<open>Markup.boundN\<close>
bound :: T
bound = markup_elem boundN

varN :: Bytes
varN = \<open>Markup.varN\<close>
var :: T
var = markup_elem varN

numeralN :: Bytes
numeralN = \<open>Markup.numeralN\<close>
numeral :: T
numeral = markup_elem numeralN

literalN :: Bytes
literalN = \<open>Markup.literalN\<close>
literal :: T
literal = markup_elem literalN

delimiterN :: Bytes
delimiterN = \<open>Markup.delimiterN\<close>
delimiter :: T
delimiter = markup_elem delimiterN

inner_stringN :: Bytes
inner_stringN = \<open>Markup.inner_stringN\<close>
inner_string :: T
inner_string = markup_elem inner_stringN

inner_cartoucheN :: Bytes
inner_cartoucheN = \<open>Markup.inner_cartoucheN\<close>
inner_cartouche :: T
inner_cartouche = markup_elem inner_cartoucheN

token_rangeN :: Bytes
token_rangeN = \<open>Markup.token_rangeN\<close>
token_range :: T
token_range = markup_elem token_rangeN

sortingN :: Bytes
sortingN = \<open>Markup.sortingN\<close>
sorting :: T
sorting = markup_elem sortingN

typingN :: Bytes
typingN = \<open>Markup.typingN\<close>
typing :: T
typing = markup_elem typingN

class_parameterN :: Bytes
class_parameterN = \<open>Markup.class_parameterN\<close>
class_parameter :: T
class_parameter = markup_elem class_parameterN

{- antiquotations -}

antiquotedN :: Bytes
antiquotedN = \<open>Markup.antiquotedN\<close>
antiquoted :: T
antiquoted = markup_elem antiquotedN

antiquoteN :: Bytes
antiquoteN = \<open>Markup.antiquoteN\<close>
antiquote :: T
antiquote = markup_elem antiquoteN

{- text structure -}

paragraphN :: Bytes
paragraphN = \<open>Markup.paragraphN\<close>
paragraph :: T
paragraph = markup_elem paragraphN

text_foldN :: Bytes
text_foldN = \<open>Markup.text_foldN\<close>
text_fold :: T
text_fold = markup_elem text_foldN

{- outer syntax -}

keyword1N :: Bytes
keyword1N = \<open>Markup.keyword1N\<close>
keyword1 :: T
keyword1 = markup_elem keyword1N

keyword2N :: Bytes
keyword2N = \<open>Markup.keyword2N\<close>
keyword2 :: T
keyword2 = markup_elem keyword2N

keyword3N :: Bytes
keyword3N = \<open>Markup.keyword3N\<close>
keyword3 :: T
keyword3 = markup_elem keyword3N

quasi_keywordN :: Bytes
quasi_keywordN = \<open>Markup.quasi_keywordN\<close>
quasi_keyword :: T
quasi_keyword = markup_elem quasi_keywordN

improperN :: Bytes
improperN = \<open>Markup.improperN\<close>
improper :: T
improper = markup_elem improperN

operatorN :: Bytes
operatorN = \<open>Markup.operatorN\<close>
operator :: T
operator = markup_elem operatorN

stringN :: Bytes
stringN = \<open>Markup.stringN\<close>
string :: T
string = markup_elem stringN

alt_stringN :: Bytes
alt_stringN = \<open>Markup.alt_stringN\<close>
alt_string :: T
alt_string = markup_elem alt_stringN

verbatimN :: Bytes
verbatimN = \<open>Markup.verbatimN\<close>
verbatim :: T
verbatim = markup_elem verbatimN

cartoucheN :: Bytes
cartoucheN = \<open>Markup.cartoucheN\<close>
cartouche :: T
cartouche = markup_elem cartoucheN

commentN :: Bytes
commentN = \<open>Markup.commentN\<close>
comment :: T
comment = markup_elem commentN

{- comments -}

comment1N :: Bytes
comment1N = \<open>Markup.comment1N\<close>
comment1 :: T
comment1 = markup_elem comment1N

comment2N :: Bytes
comment2N = \<open>Markup.comment2N\<close>
comment2 :: T
comment2 = markup_elem comment2N

comment3N :: Bytes
comment3N = \<open>Markup.comment3N\<close>
comment3 :: T
comment3 = markup_elem comment3N

{- command status -}

forkedN, joinedN, runningN, finishedN, failedN, canceledN,
  initializedN, finalizedN, consolidatingN, consolidatedN :: Bytes
forkedN = \<open>Markup.forkedN\<close>
joinedN = \<open>Markup.joinedN\<close>
runningN = \<open>Markup.runningN\<close>
finishedN = \<open>Markup.finishedN\<close>
failedN = \<open>Markup.failedN\<close>
canceledN = \<open>Markup.canceledN\<close>
initializedN = \<open>Markup.initializedN\<close>
finalizedN = \<open>Markup.finalizedN\<close>
consolidatingN = \<open>Markup.consolidatingN\<close>
consolidatedN = \<open>Markup.consolidatedN\<close>

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

{- messages -}

writelnN :: Bytes
writelnN = \<open>Markup.writelnN\<close>
writeln :: T
writeln = markup_elem writelnN

stateN :: Bytes
stateN = \<open>Markup.stateN\<close>
state :: T
state = markup_elem stateN

informationN :: Bytes
informationN = \<open>Markup.informationN\<close>
information :: T
information = markup_elem informationN

tracingN :: Bytes
tracingN = \<open>Markup.tracingN\<close>
tracing :: T
tracing = markup_elem tracingN

warningN :: Bytes
warningN = \<open>Markup.warningN\<close>
warning :: T
warning = markup_elem warningN

legacyN :: Bytes
legacyN = \<open>Markup.legacyN\<close>
legacy :: T
legacy = markup_elem legacyN

errorN :: Bytes
errorN = \<open>Markup.errorN\<close>
error :: T
error = markup_elem errorN

reportN :: Bytes
reportN = \<open>Markup.reportN\<close>
report :: T
report = markup_elem reportN

no_reportN :: Bytes
no_reportN = \<open>Markup.no_reportN\<close>
no_report :: T
no_report = markup_elem no_reportN

intensifyN :: Bytes
intensifyN = \<open>Markup.intensifyN\<close>
intensify :: T
intensify = markup_elem intensifyN

{- output -}

type Output = (Bytes, Bytes)

no_output :: Output
no_output = ("", "")
\<close>

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

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

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

{-# LANGUAGE OverloadedStrings #-}

module 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
)
where

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

{- position -}

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

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

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

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

{- fields -}

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

label_of :: T -> Maybe Bytes
label_of = proper_string . _label

file_of :: T -> Maybe Bytes
file_of = proper_string . _file

id_of :: T -> Maybe Bytes
id_of = proper_string . _id

{- make position -}

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

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

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

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

file :: Bytes -> T
file file = put_file file start

file_only :: Bytes -> T
file_only file = put_file file none

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

id :: Bytes -> T
id id = put_id id start

id_only :: Bytes -> T
id_only id = put_id id none

{- count position -}

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

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

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

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

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

symbol_explode_string :: String -> T -> T
symbol_explode_string = symbol_explode

{- shift offsets -}

shift_offsets :: Int -> T -> T
shift_offsets 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 -}

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

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

of_properties :: Properties.T -> T
of_properties 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 }

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

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

properties_of :: T -> Properties.T
properties_of 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)

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

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

make_entity_markup :: Bool -> Int -> Bytes -> (Bytes, T) -> Markup.T
make_entity_markup 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 -}

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

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

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

{- here: user output -}

here :: T -> Bytes
here 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<^here>") else ("", "")

{- range -}

type Range = (T, T)

no_range :: Range
no_range = (none, none)

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

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

range :: Range -> Range
range (pos, pos') = (range_position (pos, pos'), no_range_position pos')
\<close>

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

Untyped XML trees and representation of ML values.

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

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

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

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

{- types -}

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

{- wrapped elements -}

wrap_elem :: ((Markup.T, Body), [Tree]) -> Tree
wrap_elem (((a, atts), body1), body2) =
  Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)

unwrap_elem :: Tree -> Maybe ((Markup.T, Body), [Tree])
unwrap_elem
  (Elem ((\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts), Elem ((\<open>XML.xml_bodyN\<close>, []), body1) : body2)) =
  Just (((a, atts), body1), body2)
unwrap_elem _ = Nothing

{- text content -}

add_content :: Tree -> Buffer.T -> Buffer.T
add_content tree =
  case unwrap_elem tree of
    Just (_, ts) -> fold add_content ts
    Nothing ->
      case tree of
        Elem (_, ts) -> fold add_content ts
        Text s -> Buffer.add s

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

{- string representation -}

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

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

instance 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)
\<close>

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

XML as data representation language.

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

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

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

  int_atom, bool_atom, unit_atom,

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

import Data.Maybe (fromJust)

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

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

-- atomic values

int_atom :: A Int
int_atom = Value.print_int

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

unit_atom :: A ()
unit_atom () = ""

-- structural nodes

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

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

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

-- representation of standard types

tree :: T XML.Tree
tree t = [t]

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

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

int :: T Int
int = string . int_atom

bool :: T Bool
bool = string . bool_atom

unit :: T ()
unit = string . unit_atom

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

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

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

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

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

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

XML as data representation language.

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

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

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

  int_atom, bool_atom, unit_atom,

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

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

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

err_atom = error "Malformed XML atom"
err_body = error "Malformed XML body"

{- atomic values -}

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

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

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

{- structural nodes -}

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

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

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

{- representation of standard types -}

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

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

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

int :: T Int
int = int_atom . string

bool :: T Bool
bool = bool_atom . string

unit :: T ()
unit = unit_atom . string

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

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

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

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

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

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

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

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

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

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

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

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

{- markers -}

charX, charY :: Word8
charX = 5
charY = 6

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

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

{- output -}

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

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

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

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

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

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

{- parse -}

-- split: fields or non-empty tokens

split :: Bool -> Word8 -> [Word8] -> [[Word8]]
split _ _ [] = []
split fields sep str = splitting str
  where
    splitting rest =
      case span (/= sep) rest of
        (_, []) -> cons rest []
        (prfx, _ : rest') -> cons prfx (splitting rest')
    cons item = if fields || not (null item) then (:) item else id

-- structural errors

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

err_attribute = err "bad attribute"
err_element = err "bad element"

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

-- stack operations

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

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

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

-- parsing

parse_attrib 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

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

parse_body :: Bytes -> XML.Body
parse_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)

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

generate_file "Isabelle/Completion.hs" = \<open>
{-  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", prt, Str "\92"])

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)
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.32Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.