(* Title: Tools/Haskell/Haskell.thy
Author: Makarius
Support for Isabelle tools in Haskell.
*)
theory Haskell
imports Pure
keywords "generate_haskell_file" "export_haskell_file" :: thy_decl
begin
ML_file "haskell.ML"
section \<open>Commands\<close>
ML \<open>
Outer_Syntax.command \<^command_keyword>\<open>generate_haskell_file\<close> "generate Haskell file"
(Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
>> Haskell.generate_file_cmd);
Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
(Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
>> Haskell.export_file_cmd);
\<close>
section \<open>Source modules\<close>
generate_haskell_file "Library.hs" = \<open>
{- Title: Tools/Haskell/Library.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Basic library of Isabelle idioms.
-}
module Isabelle.Library (
(|>), (|->), (#>), (#->),
the, the_default,
fold, fold_rev, single, map_index, get_index,
quote, trim_line)
where
import Data.Maybe
{- functions -}
(|>) :: a -> (a -> b) -> b
x |> f = f x
(|->) :: (a, b) -> (a -> b -> c) -> c
(x, y) |-> f = f x y
(#>) :: (a -> b) -> (b -> c) -> a -> c
(f #> g) x = x |> f |> g
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
(f #-> g) x = x |> f |-> g
{- options -}
the :: Maybe a -> a
the (Just x) = x
the Nothing = error "the Nothing"
the_default :: a -> Maybe a -> a
the_default x Nothing = x
the_default _ (Just y) = y
{- lists -}
fold :: (a -> b -> b) -> [a] -> b -> b
fold _ [] y = y
fold f (x : xs) y = fold f xs (f x y)
fold_rev :: (a -> b -> b) -> [a] -> b -> b
fold_rev _ [] y = y
fold_rev f (x : xs) y = f x (fold_rev f xs y)
single :: a -> [a]
single x = [x]
map_index :: ((Int, a) -> b) -> [a] -> [b]
map_index f = map_aux 0
where
map_aux _ [] = []
map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
get_index f = get_aux 0
where
get_aux _ [] = Nothing
get_aux i (x : xs) =
case f x of
Nothing -> get_aux (i + 1) xs
Just y -> Just (i, y)
{- strings -}
quote :: String -> String
quote s = "\"" ++ s ++ "\""
trim_line :: String -> String
trim_line line =
case reverse line of
'\n' : '\r' : rest -> reverse rest
'\n' : rest -> reverse rest
_ -> line
\<close>
generate_haskell_file "Value.hs" = \<open>
{- Title: Haskell/Tools/Value.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Plain values, represented as string.
-}
module Isabelle.Value
(print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
where
import Data.Maybe
import qualified Data.List as List
import qualified Text.Read as Read
{- bool -}
print_bool :: Bool -> String
print_bool True = "true"
print_bool False = "false"
parse_bool :: String -> Maybe Bool
parse_bool "true" = Just True
parse_bool "false" = Just False
parse_bool _ = Nothing
{- int -}
print_int :: Int -> String
print_int = show
parse_int :: String -> Maybe Int
parse_int = Read.readMaybe
{- real -}
print_real :: Double -> String
print_real x =
let s = show x in
case span (/= '.') s of
(a, '.' : b) | List.all (== '0') b -> a
_ -> s
parse_real :: String -> Maybe Double
parse_real = Read.readMaybe
\<close>
generate_haskell_file "Buffer.hs" = \<open>
{- Title: Tools/Haskell/Buffer.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Efficient text buffers.
-}
module Isabelle.Buffer (T, empty, add, content)
where
newtype T = Buffer [String]
empty :: T
empty = Buffer []
add :: String -> T -> T
add "" buf = buf
add x (Buffer xs) = Buffer (x : xs)
content :: T -> String
content (Buffer xs) = concat (reverse xs)
\<close>
generate_haskell_file "Properties.hs" = \<open>
{- Title: Tools/Haskell/Properties.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Property lists.
-}
module Isabelle.Properties (Entry, T, defined, get, put, remove)
where
import qualified Data.List as List
type Entry = (String, String)
type T = [Entry]
defined :: T -> String -> Bool
defined props name = any (\(a, _) -> a == name) props
get :: T -> String -> Maybe String
get props name = List.lookup name props
put :: Entry -> T -> T
put entry props = entry : remove (fst entry) props
remove :: String -> T -> T
remove name props =
if defined props name then filter (\(a, _) -> a /= name) props
else props
\<close>
generate_haskell_file "Markup.hs" = \<open>
{- Title: Haskell/Tools/Markup.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Quasi-abstract markup elements.
-}
module Isabelle.Markup (
T, empty, is_empty, properties,
nameN, name, xnameN, xname, kindN,
lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
wordsN, words, no_wordsN, no_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, inner_commentN, inner_comment,
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,
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)
import Isabelle.Library
import qualified Isabelle.Properties as Properties
{- basic markup -}
type T = (String, Properties.T)
empty :: T
empty = ("", [])
is_empty :: T -> Bool
is_empty ("", _) = True
is_empty _ = False
properties :: Properties.T -> T -> T
properties more_props (elem, props) =
(elem, fold_rev Properties.put more_props props)
markup_elem name = (name, (name, []) :: T)
{- misc properties -}
nameN :: String
nameN = \<open>Markup.nameN\<close>
name :: String -> T -> T
name a = properties [(nameN, a)]
xnameN :: String
xnameN = \<open>Markup.xnameN\<close>
xname :: String -> T -> T
xname a = properties [(xnameN, a)]
kindN :: String
kindN = \<open>Markup.kindN\<close>
{- position -}
lineN, end_lineN :: String
lineN = \<open>Markup.lineN\<close>
end_lineN = \<open>Markup.end_lineN\<close>
offsetN, end_offsetN :: String
offsetN = \<open>Markup.offsetN\<close>
end_offsetN = \<open>Markup.end_offsetN\<close>
fileN, idN :: String
fileN = \<open>Markup.fileN\<close>
idN = \<open>Markup.idN\<close>
positionN :: String; position :: T
(positionN, position) = markup_elem \<open>Markup.positionN\<close>
{- text properties -}
wordsN :: String; words :: T
(wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
no_wordsN :: String; no_words :: T
(no_wordsN, no_words) = markup_elem \<open>Markup.no_wordsN\<close>
{- inner syntax -}
tfreeN :: String; tfree :: T
(tfreeN, tfree) = markup_elem \<open>Markup.tfreeN\<close>
tvarN :: String; tvar :: T
(tvarN, tvar) = markup_elem \<open>Markup.tvarN\<close>
freeN :: String; free :: T
(freeN, free) = markup_elem \<open>Markup.freeN\<close>
skolemN :: String; skolem :: T
(skolemN, skolem) = markup_elem \<open>Markup.skolemN\<close>
boundN :: String; bound :: T
(boundN, bound) = markup_elem \<open>Markup.boundN\<close>
varN :: String; var :: T
(varN, var) = markup_elem \<open>Markup.varN\<close>
numeralN :: String; numeral :: T
(numeralN, numeral) = markup_elem \<open>Markup.numeralN\<close>
literalN :: String; literal :: T
(literalN, literal) = markup_elem \<open>Markup.literalN\<close>
delimiterN :: String; delimiter :: T
(delimiterN, delimiter) = markup_elem \<open>Markup.delimiterN\<close>
inner_stringN :: String; inner_string :: T
(inner_stringN, inner_string) = markup_elem \<open>Markup.inner_stringN\<close>
inner_cartoucheN :: String; inner_cartouche :: T
(inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
inner_commentN :: String; inner_comment :: T
(inner_commentN, inner_comment) = markup_elem \<open>Markup.inner_commentN\<close>
token_rangeN :: String; token_range :: T
(token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
sortingN :: String; sorting :: T
(sortingN, sorting) = markup_elem \<open>Markup.sortingN\<close>
typingN :: String; typing :: T
(typingN, typing) = markup_elem \<open>Markup.typingN\<close>
class_parameterN :: String; class_parameter :: T
(class_parameterN, class_parameter) = markup_elem \<open>Markup.class_parameterN\<close>
{- antiquotations -}
antiquotedN :: String; antiquoted :: T
(antiquotedN, antiquoted) = markup_elem \<open>Markup.antiquotedN\<close>
antiquoteN :: String; antiquote :: T
(antiquoteN, antiquote) = markup_elem \<open>Markup.antiquoteN\<close>
{- text structure -}
paragraphN :: String; paragraph :: T
(paragraphN, paragraph) = markup_elem \<open>Markup.paragraphN\<close>
text_foldN :: String; text_fold :: T
(text_foldN, text_fold) = markup_elem \<open>Markup.text_foldN\<close>
{- outer syntax -}
keyword1N :: String; keyword1 :: T
(keyword1N, keyword1) = markup_elem \<open>Markup.keyword1N\<close>
keyword2N :: String; keyword2 :: T
(keyword2N, keyword2) = markup_elem \<open>Markup.keyword2N\<close>
keyword3N :: String; keyword3 :: T
(keyword3N, keyword3) = markup_elem \<open>Markup.keyword3N\<close>
quasi_keywordN :: String; quasi_keyword :: T
(quasi_keywordN, quasi_keyword) = markup_elem \<open>Markup.quasi_keywordN\<close>
improperN :: String; improper :: T
(improperN, improper) = markup_elem \<open>Markup.improperN\<close>
operatorN :: String; operator :: T
(operatorN, operator) = markup_elem \<open>Markup.operatorN\<close>
stringN :: String; string :: T
(stringN, string) = markup_elem \<open>Markup.stringN\<close>
alt_stringN :: String; alt_string :: T
(alt_stringN, alt_string) = markup_elem \<open>Markup.alt_stringN\<close>
verbatimN :: String; verbatim :: T
(verbatimN, verbatim) = markup_elem \<open>Markup.verbatimN\<close>
cartoucheN :: String; cartouche :: T
(cartoucheN, cartouche) = markup_elem \<open>Markup.cartoucheN\<close>
commentN :: String; comment :: T
(commentN, comment) = markup_elem \<open>Markup.commentN\<close>
{- messages -}
writelnN :: String; writeln :: T
(writelnN, writeln) = markup_elem \<open>Markup.writelnN\<close>
stateN :: String; state :: T
(stateN, state) = markup_elem \<open>Markup.stateN\<close>
informationN :: String; information :: T
(informationN, information) = markup_elem \<open>Markup.informationN\<close>
tracingN :: String; tracing :: T
(tracingN, tracing) = markup_elem \<open>Markup.tracingN\<close>
warningN :: String; warning :: T
(warningN, warning) = markup_elem \<open>Markup.warningN\<close>
legacyN :: String; legacy :: T
(legacyN, legacy) = markup_elem \<open>Markup.legacyN\<close>
errorN :: String; error :: T
(errorN, error) = markup_elem \<open>Markup.errorN\<close>
reportN :: String; report :: T
(reportN, report) = markup_elem \<open>Markup.reportN\<close>
no_reportN :: String; no_report :: T
(no_reportN, no_report) = markup_elem \<open>Markup.no_reportN\<close>
intensifyN :: String; intensify :: T
(intensifyN, intensify) = markup_elem \<open>Markup.intensifyN\<close>
{- output -}
type Output = (String, String)
no_output :: Output
no_output = ("", "")
\<close>
generate_haskell_file "XML.hs" = \<open>
{- Title: Tools/Haskell/XML.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Untyped XML trees and representation of ML values.
-}
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
where
import qualified Data.List as List
import Isabelle.Library
import qualified Isabelle.Properties as Properties
import qualified Isabelle.Markup as Markup
import qualified Isabelle.Buffer as Buffer
{- types -}
type Attributes = Properties.T
type Body = [Tree]
data Tree = Elem Markup.T Body | Text String
{- wrapped elements -}
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
(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 =
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 = Buffer.empty |> fold add_content body |> Buffer.content
{- string representation -}
encode '<' = "<"
encode '>' = ">"
encode '&' = "&"
encode '\'' = "'"
encode '\"' = """
encode c = [c]
instance Show Tree where
show tree =
Buffer.empty |> show_tree tree |> Buffer.content
where
show_tree (Elem (name, atts) []) =
Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
show_tree (Elem (name, atts) ts) =
Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
fold show_tree ts #>
Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
show_tree (Text s) = Buffer.add (show_text s)
show_elem name atts =
unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
show_text = concatMap encode
\<close>
generate_haskell_file "XML/Encode.hs" = \<open>
{- Title: Tools/Haskell/XML/Encode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
XML as data representation language.
-}
module Isabelle.XML.Encode (
A, T, V,
int_atom, bool_atom, unit_atom,
tree, properties, string, init, bool, unit, pair, triple, list, variant
)
where
import Isabelle.Library
import qualified Isabelle.Value as Value
import qualified Isabelle.Properties as Properties
import qualified Isabelle.XML as XML
type A a = a -> String
type T a = a -> XML.Body
type V a = a -> Maybe ([String], XML.Body)
-- 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 = XML.Elem (":", [])
vector = map_index (\(i, x) -> (int_atom i, x))
tagged (tag, (xs, ts)) = XML.Elem (int_atom tag, vector xs) ts
-- representation of standard types
tree :: T XML.Tree
tree t = [t]
properties :: T Properties.T
properties props = [XML.Elem (":", props) []]
string :: T String
string "" = []
string s = [XML.Text s]
int :: T Int
int = string . int_atom
bool :: T Bool
bool = string . bool_atom
unit :: T ()
unit = string . unit_atom
pair :: T a -> T b -> T (a, b)
pair f g (x, y) = [node (f x), node (g y)]
triple :: T a -> T b -> T c -> T (a, b, c)
triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
list :: T a -> T [a]
list f xs = map (node . f) xs
variant :: [V a] -> T a
variant fs x = [tagged (the (get_index (\f -> f x) fs))]
\<close>
generate_haskell_file "XML/Decode.hs" = \<open>
{- Title: Tools/Haskell/XML/Decode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
XML as data representation language.
-}
module Isabelle.XML.Decode (
A, T, V,
int_atom, bool_atom, unit_atom,
tree, properties, string, init, bool, unit, pair, triple, list, variant
)
where
import Data.List ((!!))
import Isabelle.Library
import qualified Isabelle.Value as Value
import qualified Isabelle.Properties as Properties
import qualified Isabelle.XML as XML
type A a = String -> a
type T a = XML.Body -> a
type V a = ([String], XML.Body) -> a
err_atom = error "Malformed XML atom"
err_body = error "Malformed XML body"
{- atomic values -}
int_atom :: A Int
int_atom s =
case Value.parse_int s of
Just i -> i
Nothing -> err_atom
bool_atom :: A Bool
bool_atom "0" = False
bool_atom "1" = True
bool_atom _ = err_atom
unit_atom :: A ()
unit_atom "" = ()
unit_atom _ = err_atom
{- structural nodes -}
node (XML.Elem (":", []) ts) = ts
node _ = err_body
vector atts =
map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
tagged (XML.Elem (name, atts) ts) = (int_atom name, (vector atts, ts))
tagged _ = err_body
{- representation of standard types -}
tree :: T XML.Tree
tree [t] = t
tree _ = err_body
properties :: T Properties.T
properties [XML.Elem (":", props) []] = props
properties _ = err_body
string :: T String
string [] = ""
string [XML.Text s] = s
string _ = err_body
int :: T Int
int = int_atom . string
bool :: T Bool
bool = bool_atom . string
unit :: T ()
unit = unit_atom . string
pair :: T a -> T b -> T (a, b)
pair f g [t1, t2] = (f (node t1), g (node t2))
pair _ _ _ = err_body
triple :: T a -> T b -> T c -> T (a, b, c)
triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
triple _ _ _ _ = err_body
list :: T a -> T [a]
list f ts = map (f . node) ts
option :: T a -> T (Maybe a)
option _ [] = Nothing
option f [t] = Just (f (node t))
option _ _ = err_body
variant :: [V a] -> T a
variant fs [t] = (fs !! tag) (xs, ts)
where (tag, (xs, ts)) = tagged t
variant _ _ = err_body
\<close>
generate_haskell_file "YXML.hs" = \<open>
{- Title: Tools/Haskell/YXML.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Efficient text representation of XML trees. Suitable for direct
inlining into plain text.
-}
module Isabelle.YXML (charX, charY, strX, strY, detect,
buffer_body, buffer, string_of_body, string_of, parse_body, parse)
where
import qualified Data.Char as Char
import qualified Data.List as List
import Isabelle.Library
import qualified Isabelle.Markup as Markup
import qualified Isabelle.XML as XML
import qualified Isabelle.Buffer as Buffer
{- markers -}
charX, charY :: Char
charX = Char.chr 5
charY = Char.chr 6
strX, strY, strXY, strXYX :: String
strX = [charX]
strY = [charY]
strXY = strX ++ strY
strXYX = strXY ++ strX
detect :: String -> Bool
detect = any (\c -> c == charX || c == charY)
{- output -}
buffer_attrib (a, x) =
Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
buffer_body :: XML.Body -> Buffer.T -> Buffer.T
buffer_body = fold buffer
buffer :: XML.Tree -> Buffer.T -> Buffer.T
buffer (XML.Elem (name, atts) ts) =
Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
buffer_body ts #>
Buffer.add strXYX
buffer (XML.Text s) = Buffer.add s
string_of_body :: XML.Body -> String
string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
string_of :: XML.Tree -> String
string_of = string_of_body . single
{- parse -}
-- split: fields or non-empty tokens
split :: Bool -> Char -> String -> [String]
split _ _ [] = []
split fields sep str = splitting str
where
splitting rest =
case span (/= sep) rest of
(_, []) -> cons rest []
(prfx, _ : rest') -> cons prfx (splitting rest')
cons item = if fields || not (null item) then (:) item else id
-- structural errors
err msg = error ("Malformed YXML: " ++ msg)
err_attribute = err "bad attribute"
err_element = err "bad element"
err_unbalanced "" = err "unbalanced element"
err_unbalanced name = err ("unbalanced element " ++ quote name)
-- stack operations
add x ((elem, body) : pending) = (elem, x : body) : pending
push "" _ _ = err_element
push name atts pending = ((name, atts), []) : pending
pop ((("", _), _) : _) = err_unbalanced ""
pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
-- parsing
parse_attrib s =
case List.elemIndex '=' s of
Just i | i > 0 -> (take i s, drop (i + 1) s)
_ -> err_attribute
parse_chunk ["", ""] = pop
parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
parse_chunk txts = fold (add . XML.Text) txts
parse_body :: String -> XML.Body
parse_body source =
case fold parse_chunk chunks [(("", []), [])] of
[(("", _), result)] -> reverse result
((name, _), _) : _ -> err_unbalanced name
where chunks = split False charX source |> map (split True charY)
parse :: String -> XML.Tree
parse source =
case parse_body source of
[result] -> result
[] -> XML.Text ""
_ -> err "multiple results"
\<close>
generate_haskell_file "Term.hs" = \<open>
{- Title: Tools/Haskell/Term.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
Lambda terms, types, sorts.
-}
module Isabelle.Term (
Indexname,
Sort, dummyS,
Typ(..), dummyT, Term(..))
where
type Indexname = (String, Int)
type Sort = [String]
dummyS :: Sort
dummyS = [""]
data Typ =
Type (String, [Typ])
| TFree (String, Sort)
| TVar (Indexname, Sort)
deriving Show
dummyT :: Typ
dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
data Term =
Const (String, Typ)
| Free (String, Typ)
| Var (Indexname, Typ)
| Bound Int
| Abs (String, Typ, Term)
| App (Term, Term)
deriving Show
\<close>
generate_haskell_file "Term_XML/Encode.hs" = \<open>
{- Title: Tools/Haskell/Term_XML/Encode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
XML data representation of lambda terms.
-}
{-# LANGUAGE LambdaCase #-}
module Isabelle.Term_XML.Encode (sort, typ, term)
where
import Isabelle.Library
import qualified Isabelle.XML as XML
import Isabelle.XML.Encode
import Isabelle.Term
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), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
term :: T Term
term t =
t |> variant
[\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
\case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
\case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
\case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
\case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
\case { App a -> Just ([], pair term term a); _ -> Nothing }]
\<close>
generate_haskell_file "Term_XML/Decode.hs" = \<open>
{- Title: Tools/Haskell/Term_XML/Decode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
XML data representation of lambda terms.
-}
module Isabelle.Term_XML.Decode (sort, typ, term)
where
import Isabelle.Library
import qualified Isabelle.XML as XML
import Isabelle.XML.Decode
import Isabelle.Term
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], c) -> TVar ((a, int_atom b), sort c)]
term :: T Term
term t =
t |> variant
[\([a], b) -> Const (a, typ b),
\([a], b) -> Free (a, typ b),
\([a, b], c) -> Var ((a, int_atom b), typ c),
\([a], []) -> Bound (int_atom a),
\([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
\([], a) -> App (pair term term a)]
\<close>
end