{- generated by Isabelle -}
{- Title: Tools/Haskell/XML/Decode.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
XML as data representation language.
See also "$ISABELLE_HOME/src/Pure/PIDE/xml.ML".
-}
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