more Haskell operations;
authorwenzelm
Mon Nov 05 17:06:50 2018 +0100 (6 months ago)
changeset 6924016ca270090b6
parent 69239 6cd985a78d6e
child 69241 5426d266dcc5
more Haskell operations;
tuned;
src/Tools/Haskell/Haskell.thy
src/Tools/Haskell/Library.hs
src/Tools/Haskell/Term.hs
src/Tools/Haskell/Term_XML/Decode.hs
src/Tools/Haskell/Term_XML/Encode.hs
src/Tools/Haskell/XML/Decode.hs
src/Tools/Haskell/XML/Encode.hs
src/Tools/Haskell/haskell.ML
     1.1 --- a/src/Tools/Haskell/Haskell.thy	Mon Nov 05 15:04:31 2018 +0100
     1.2 +++ b/src/Tools/Haskell/Haskell.thy	Mon Nov 05 17:06:50 2018 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  section \<open>Source modules\<close>
     1.6  
     1.7 -generate_haskell_file Library.hs = \<open>
     1.8 +generate_haskell_file "Library.hs" = \<open>
     1.9  {-  Title:      Tools/Haskell/Library.hs
    1.10      Author:     Makarius
    1.11      LICENSE:    BSD 3-clause (Isabelle)
    1.12 @@ -35,8 +35,14 @@
    1.13  Basic library of Isabelle idioms.
    1.14  -}
    1.15  
    1.16 -module Isabelle.Library
    1.17 -  ((|>), (|->), (#>), (#->), the_default, fold, fold_rev, single, quote, trim_line)
    1.18 +module Isabelle.Library (
    1.19 +  (|>), (|->), (#>), (#->),
    1.20 +
    1.21 +  the, the_default,
    1.22 +
    1.23 +  fold, fold_rev, single, map_index, get_index,
    1.24 +
    1.25 +  quote, trim_line)
    1.26  where
    1.27  
    1.28  import Data.Maybe
    1.29 @@ -59,6 +65,10 @@
    1.30  
    1.31  {- options -}
    1.32  
    1.33 +the :: Maybe a -> a
    1.34 +the (Just x) = x
    1.35 +the Nothing = error "the Nothing"
    1.36 +
    1.37  the_default :: a -> Maybe a -> a
    1.38  the_default x Nothing = x
    1.39  the_default _ (Just y) = y
    1.40 @@ -77,6 +87,21 @@
    1.41  single :: a -> [a]
    1.42  single x = [x]
    1.43  
    1.44 +map_index :: ((Int, a) -> b) -> [a] -> [b]
    1.45 +map_index f = map_aux 0
    1.46 +  where
    1.47 +    map_aux _ [] = []
    1.48 +    map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
    1.49 +
    1.50 +get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
    1.51 +get_index f = get_aux 0
    1.52 +  where
    1.53 +    get_aux _ [] = Nothing
    1.54 +    get_aux i (x : xs) =
    1.55 +      case f x of
    1.56 +        Nothing -> get_aux (i + 1) xs
    1.57 +        Just y -> Just (i, y)
    1.58 +
    1.59  
    1.60  {- strings -}
    1.61  
    1.62 @@ -91,7 +116,7 @@
    1.63      _ -> line
    1.64  \<close>
    1.65  
    1.66 -generate_haskell_file Value.hs = \<open>
    1.67 +generate_haskell_file "Value.hs" = \<open>
    1.68  {-  Title:      Haskell/Tools/Value.hs
    1.69      Author:     Makarius
    1.70      LICENSE:    BSD 3-clause (Isabelle)
    1.71 @@ -142,7 +167,7 @@
    1.72  parse_real = Read.readMaybe
    1.73  \<close>
    1.74  
    1.75 -generate_haskell_file Buffer.hs = \<open>
    1.76 +generate_haskell_file "Buffer.hs" = \<open>
    1.77  {-  Title:      Tools/Haskell/Buffer.hs
    1.78      Author:     Makarius
    1.79      LICENSE:    BSD 3-clause (Isabelle)
    1.80 @@ -166,7 +191,7 @@
    1.81  content (Buffer xs) = concat (reverse xs)
    1.82  \<close>
    1.83  
    1.84 -generate_haskell_file Properties.hs = \<open>
    1.85 +generate_haskell_file "Properties.hs" = \<open>
    1.86  {-  Title:      Tools/Haskell/Properties.hs
    1.87      Author:     Makarius
    1.88      LICENSE:    BSD 3-clause (Isabelle)
    1.89 @@ -198,7 +223,7 @@
    1.90    else props
    1.91  \<close>
    1.92  
    1.93 -generate_haskell_file Markup.hs = \<open>
    1.94 +generate_haskell_file "Markup.hs" = \<open>
    1.95  {-  Title:      Haskell/Tools/Markup.hs
    1.96      Author:     Makarius
    1.97      LICENSE:    BSD 3-clause (Isabelle)
    1.98 @@ -453,7 +478,7 @@
    1.99  no_output = ("", "")
   1.100  \<close>
   1.101  
   1.102 -generate_haskell_file XML.hs = \<open>
   1.103 +generate_haskell_file "XML.hs" = \<open>
   1.104  {-  Title:      Tools/Haskell/XML.hs
   1.105      Author:     Makarius
   1.106      LICENSE:    BSD 3-clause (Isabelle)
   1.107 @@ -530,7 +555,200 @@
   1.108        show_text = concatMap encode
   1.109  \<close>
   1.110  
   1.111 -generate_haskell_file YXML.hs = \<open>
   1.112 +generate_haskell_file "XML/Encode.hs" = \<open>
   1.113 +{-  Title:      Tools/Haskell/XML/Encode.hs
   1.114 +    Author:     Makarius
   1.115 +    LICENSE:    BSD 3-clause (Isabelle)
   1.116 +
   1.117 +XML as data representation language.
   1.118 +-}
   1.119 +
   1.120 +module Isabelle.XML.Encode (
   1.121 +  A, T, V,
   1.122 +
   1.123 +  int_atom, bool_atom, unit_atom,
   1.124 +
   1.125 +  tree, properties, string, init, bool, unit, pair, triple, list, variant
   1.126 +)
   1.127 +where
   1.128 +
   1.129 +import Isabelle.Library
   1.130 +import qualified Isabelle.Value as Value
   1.131 +import qualified Isabelle.Properties as Properties
   1.132 +import qualified Isabelle.XML as XML
   1.133 +
   1.134 +
   1.135 +type A a = a -> String
   1.136 +type T a = a -> XML.Body
   1.137 +type V a = a -> Maybe ([String], XML.Body)
   1.138 +
   1.139 +
   1.140 +-- atomic values
   1.141 +
   1.142 +int_atom :: A Int
   1.143 +int_atom = Value.print_int
   1.144 +
   1.145 +bool_atom :: A Bool
   1.146 +bool_atom False = "0"
   1.147 +bool_atom True = "1"
   1.148 +
   1.149 +unit_atom :: A ()
   1.150 +unit_atom () = ""
   1.151 +
   1.152 +
   1.153 +-- structural nodes
   1.154 +
   1.155 +node = XML.Elem (":", [])
   1.156 +
   1.157 +vector = map_index (\(i, x) -> (int_atom i, x))
   1.158 +
   1.159 +tagged (tag, (xs, ts)) = XML.Elem (int_atom tag, vector xs) ts
   1.160 +
   1.161 +
   1.162 +-- representation of standard types
   1.163 +
   1.164 +tree :: T XML.Tree
   1.165 +tree t = [t]
   1.166 +
   1.167 +properties :: T Properties.T
   1.168 +properties props = [XML.Elem (":", props) []]
   1.169 +
   1.170 +string :: T String
   1.171 +string "" = []
   1.172 +string s = [XML.Text s]
   1.173 +
   1.174 +int :: T Int
   1.175 +int = string . int_atom
   1.176 +
   1.177 +bool :: T Bool
   1.178 +bool = string . bool_atom
   1.179 +
   1.180 +unit :: T ()
   1.181 +unit = string . unit_atom
   1.182 +
   1.183 +pair :: T a -> T b -> T (a, b)
   1.184 +pair f g (x, y) = [node (f x), node (g y)]
   1.185 +
   1.186 +triple :: T a -> T b -> T c -> T (a, b, c)
   1.187 +triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
   1.188 +
   1.189 +list :: T a -> T [a]
   1.190 +list f xs = map (node . f) xs
   1.191 +
   1.192 +variant :: [V a] -> T a
   1.193 +variant fs x = [tagged (the (get_index (\f -> f x) fs))]
   1.194 +\<close>
   1.195 +
   1.196 +generate_haskell_file "XML/Decode.hs" = \<open>
   1.197 +{-  Title:      Tools/Haskell/XML/Decode.hs
   1.198 +    Author:     Makarius
   1.199 +    LICENSE:    BSD 3-clause (Isabelle)
   1.200 +
   1.201 +XML as data representation language.
   1.202 +-}
   1.203 +
   1.204 +module Isabelle.XML.Decode (
   1.205 +  A, T, V,
   1.206 +
   1.207 +  int_atom, bool_atom, unit_atom,
   1.208 +
   1.209 +  tree, properties, string, init, bool, unit, pair, triple, list, variant
   1.210 +)
   1.211 +where
   1.212 +
   1.213 +import Data.List ((!!))
   1.214 +
   1.215 +import Isabelle.Library
   1.216 +import qualified Isabelle.Value as Value
   1.217 +import qualified Isabelle.Properties as Properties
   1.218 +import qualified Isabelle.XML as XML
   1.219 +
   1.220 +
   1.221 +type A a = String -> a
   1.222 +type T a = XML.Body -> a
   1.223 +type V a = ([String], XML.Body) -> a
   1.224 +
   1.225 +err_atom = error "Malformed XML atom"
   1.226 +err_body = error "Malformed XML body"
   1.227 +
   1.228 +
   1.229 +{- atomic values -}
   1.230 +
   1.231 +int_atom :: A Int
   1.232 +int_atom s =
   1.233 +  case Value.parse_int s of
   1.234 +    Just i -> i
   1.235 +    Nothing -> err_atom
   1.236 +
   1.237 +bool_atom :: A Bool
   1.238 +bool_atom "0" = False
   1.239 +bool_atom "1" = True
   1.240 +bool_atom _ = err_atom
   1.241 +
   1.242 +unit_atom :: A ()
   1.243 +unit_atom "" = ()
   1.244 +unit_atom _ = err_atom
   1.245 +
   1.246 +
   1.247 +{- structural nodes -}
   1.248 +
   1.249 +node (XML.Elem (":", []) ts) = ts
   1.250 +node _ = err_body
   1.251 +
   1.252 +vector atts =
   1.253 +  map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
   1.254 +
   1.255 +tagged (XML.Elem (name, atts) ts) = (int_atom name, (vector atts, ts))
   1.256 +tagged _ = err_body
   1.257 +
   1.258 +
   1.259 +{- representation of standard types -}
   1.260 +
   1.261 +tree :: T XML.Tree
   1.262 +tree [t] = t
   1.263 +tree _ = err_body
   1.264 +
   1.265 +properties :: T Properties.T
   1.266 +properties [XML.Elem (":", props) []] = props
   1.267 +properties _ = err_body
   1.268 +
   1.269 +string :: T String
   1.270 +string [] = ""
   1.271 +string [XML.Text s] = s
   1.272 +string _ = err_body
   1.273 +
   1.274 +int :: T Int
   1.275 +int = int_atom . string
   1.276 +
   1.277 +bool :: T Bool
   1.278 +bool = bool_atom . string
   1.279 +
   1.280 +unit :: T ()
   1.281 +unit = unit_atom . string
   1.282 +
   1.283 +pair :: T a -> T b -> T (a, b)
   1.284 +pair f g [t1, t2] = (f (node t1), g (node t2))
   1.285 +pair _ _ _ = err_body
   1.286 +
   1.287 +triple :: T a -> T b -> T c -> T (a, b, c)
   1.288 +triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
   1.289 +triple _ _ _ _ = err_body
   1.290 +
   1.291 +list :: T a -> T [a]
   1.292 +list f ts = map (f . node) ts
   1.293 +
   1.294 +option :: T a -> T (Maybe a)
   1.295 +option _ [] = Nothing
   1.296 +option f [t] = Just (f (node t))
   1.297 +option _ _ = err_body
   1.298 +
   1.299 +variant :: [V a] -> T a
   1.300 +variant fs [t] = (fs !! tag) (xs, ts)
   1.301 +  where (tag, (xs, ts)) = tagged t
   1.302 +variant _ _ = err_body
   1.303 +\<close>
   1.304 +
   1.305 +generate_haskell_file "YXML.hs" = \<open>
   1.306  {-  Title:      Tools/Haskell/YXML.hs
   1.307      Author:     Makarius
   1.308      LICENSE:    BSD 3-clause (Isabelle)
   1.309 @@ -651,4 +869,127 @@
   1.310      _ -> err "multiple results"
   1.311  \<close>
   1.312  
   1.313 +generate_haskell_file "Term.hs" = \<open>
   1.314 +{-  Title:      Tools/Haskell/Term.hs
   1.315 +    Author:     Makarius
   1.316 +    LICENSE:    BSD 3-clause (Isabelle)
   1.317 +
   1.318 +Lambda terms, types, sorts.
   1.319 +-}
   1.320 +
   1.321 +module Isabelle.Term (
   1.322 +  Indexname,
   1.323 +
   1.324 +  Sort, dummyS,
   1.325 +
   1.326 +  Typ(..), dummyT, Term(..))
   1.327 +where
   1.328 +
   1.329 +type Indexname = (String, Int)
   1.330 +
   1.331 +
   1.332 +type Sort = [String]
   1.333 +
   1.334 +dummyS :: Sort
   1.335 +dummyS = [""]
   1.336 +
   1.337 +
   1.338 +data Typ =
   1.339 +    Type (String, [Typ])
   1.340 +  | TFree (String, Sort)
   1.341 +  | TVar (Indexname, Sort)
   1.342 +  deriving Show
   1.343 +
   1.344 +dummyT :: Typ
   1.345 +dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
   1.346 +
   1.347 +
   1.348 +data Term =
   1.349 +    Const (String, Typ)
   1.350 +  | Free (String, Typ)
   1.351 +  | Var (Indexname, Typ)
   1.352 +  | Bound Int
   1.353 +  | Abs (String, Typ, Term)
   1.354 +  | App (Term, Term)
   1.355 +  deriving Show
   1.356 +\<close>
   1.357 +
   1.358 +generate_haskell_file "Term_XML/Encode.hs" = \<open>
   1.359 +{-  Title:      Tools/Haskell/Term_XML/Encode.hs
   1.360 +    Author:     Makarius
   1.361 +    LICENSE:    BSD 3-clause (Isabelle)
   1.362 +
   1.363 +XML data representation of lambda terms.
   1.364 +-}
   1.365 +
   1.366 +{-# LANGUAGE LambdaCase #-}
   1.367 +
   1.368 +module Isabelle.Term_XML.Encode (sort, typ, term)
   1.369 +where
   1.370 +
   1.371 +import Isabelle.Library
   1.372 +import qualified Isabelle.XML as XML
   1.373 +import Isabelle.XML.Encode
   1.374 +import Isabelle.Term
   1.375 +
   1.376 +
   1.377 +sort :: T Sort
   1.378 +sort = list string
   1.379 +
   1.380 +typ :: T Typ
   1.381 +typ ty =
   1.382 +  ty |> variant
   1.383 +   [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
   1.384 +    \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
   1.385 +    \case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
   1.386 +
   1.387 +term :: T Term
   1.388 +term t =
   1.389 +  t |> variant
   1.390 +   [\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
   1.391 +    \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
   1.392 +    \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
   1.393 +    \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
   1.394 +    \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
   1.395 +    \case { App a -> Just ([], pair term term a); _ -> Nothing }]
   1.396 +\<close>
   1.397 +
   1.398 +generate_haskell_file "Term_XML/Decode.hs" = \<open>
   1.399 +{-  Title:      Tools/Haskell/Term_XML/Decode.hs
   1.400 +    Author:     Makarius
   1.401 +    LICENSE:    BSD 3-clause (Isabelle)
   1.402 +
   1.403 +XML data representation of lambda terms.
   1.404 +-}
   1.405 +
   1.406 +module Isabelle.Term_XML.Decode (sort, typ, term)
   1.407 +where
   1.408 +
   1.409 +import Isabelle.Library
   1.410 +import qualified Isabelle.XML as XML
   1.411 +import Isabelle.XML.Decode
   1.412 +import Isabelle.Term
   1.413 +
   1.414 +
   1.415 +sort :: T Sort
   1.416 +sort = list string
   1.417 +
   1.418 +typ :: T Typ
   1.419 +typ ty =
   1.420 +  ty |> variant
   1.421 +  [\([a], b) -> Type (a, list typ b),
   1.422 +   \([a], b) -> TFree (a, sort b),
   1.423 +   \([a, b], c) -> TVar ((a, int_atom b), sort c)]
   1.424 +
   1.425 +term :: T Term
   1.426 +term t =
   1.427 +  t |> variant
   1.428 +   [\([a], b) -> Const (a, typ b),
   1.429 +    \([a], b) -> Free (a, typ b),
   1.430 +    \([a, b], c) -> Var ((a, int_atom b), typ c),
   1.431 +    \([a], []) -> Bound (int_atom a),
   1.432 +    \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
   1.433 +    \([], a) -> App (pair term term a)]
   1.434 +\<close>
   1.435 +
   1.436  end
     2.1 --- a/src/Tools/Haskell/Library.hs	Mon Nov 05 15:04:31 2018 +0100
     2.2 +++ b/src/Tools/Haskell/Library.hs	Mon Nov 05 17:06:50 2018 +0100
     2.3 @@ -7,8 +7,14 @@
     2.4  Basic library of Isabelle idioms.
     2.5  -}
     2.6  
     2.7 -module Isabelle.Library
     2.8 -  ((|>), (|->), (#>), (#->), the_default, fold, fold_rev, single, quote, trim_line)
     2.9 +module Isabelle.Library (
    2.10 +  (|>), (|->), (#>), (#->),
    2.11 +
    2.12 +  the, the_default,
    2.13 +
    2.14 +  fold, fold_rev, single, map_index, get_index,
    2.15 +
    2.16 +  quote, trim_line)
    2.17  where
    2.18  
    2.19  import Data.Maybe
    2.20 @@ -31,6 +37,10 @@
    2.21  
    2.22  {- options -}
    2.23  
    2.24 +the :: Maybe a -> a
    2.25 +the (Just x) = x
    2.26 +the Nothing = error "the Nothing"
    2.27 +
    2.28  the_default :: a -> Maybe a -> a
    2.29  the_default x Nothing = x
    2.30  the_default _ (Just y) = y
    2.31 @@ -49,6 +59,21 @@
    2.32  single :: a -> [a]
    2.33  single x = [x]
    2.34  
    2.35 +map_index :: ((Int, a) -> b) -> [a] -> [b]
    2.36 +map_index f = map_aux 0
    2.37 +  where
    2.38 +    map_aux _ [] = []
    2.39 +    map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
    2.40 +
    2.41 +get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
    2.42 +get_index f = get_aux 0
    2.43 +  where
    2.44 +    get_aux _ [] = Nothing
    2.45 +    get_aux i (x : xs) =
    2.46 +      case f x of
    2.47 +        Nothing -> get_aux (i + 1) xs
    2.48 +        Just y -> Just (i, y)
    2.49 +
    2.50  
    2.51  {- strings -}
    2.52  
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/Haskell/Term.hs	Mon Nov 05 17:06:50 2018 +0100
     3.3 @@ -0,0 +1,44 @@
     3.4 +{- generated by Isabelle -}
     3.5 +
     3.6 +{-  Title:      Tools/Haskell/Term.hs
     3.7 +    Author:     Makarius
     3.8 +    LICENSE:    BSD 3-clause (Isabelle)
     3.9 +
    3.10 +Lambda terms, types, sorts.
    3.11 +-}
    3.12 +
    3.13 +module Isabelle.Term (
    3.14 +  Indexname,
    3.15 +
    3.16 +  Sort, dummyS,
    3.17 +
    3.18 +  Typ(..), dummyT, Term(..))
    3.19 +where
    3.20 +
    3.21 +type Indexname = (String, Int)
    3.22 +
    3.23 +
    3.24 +type Sort = [String]
    3.25 +
    3.26 +dummyS :: Sort
    3.27 +dummyS = [""]
    3.28 +
    3.29 +
    3.30 +data Typ =
    3.31 +    Type (String, [Typ])
    3.32 +  | TFree (String, Sort)
    3.33 +  | TVar (Indexname, Sort)
    3.34 +  deriving Show
    3.35 +
    3.36 +dummyT :: Typ
    3.37 +dummyT = Type ("dummy", [])
    3.38 +
    3.39 +
    3.40 +data Term =
    3.41 +    Const (String, Typ)
    3.42 +  | Free (String, Typ)
    3.43 +  | Var (Indexname, Typ)
    3.44 +  | Bound Int
    3.45 +  | Abs (String, Typ, Term)
    3.46 +  | App (Term, Term)
    3.47 +  deriving Show
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/Haskell/Term_XML/Decode.hs	Mon Nov 05 17:06:50 2018 +0100
     4.3 @@ -0,0 +1,37 @@
     4.4 +{- generated by Isabelle -}
     4.5 +
     4.6 +{-  Title:      Tools/Haskell/Term_XML/Decode.hs
     4.7 +    Author:     Makarius
     4.8 +    LICENSE:    BSD 3-clause (Isabelle)
     4.9 +
    4.10 +XML data representation of lambda terms.
    4.11 +-}
    4.12 +
    4.13 +module Isabelle.Term_XML.Decode (sort, typ, term)
    4.14 +where
    4.15 +
    4.16 +import Isabelle.Library
    4.17 +import qualified Isabelle.XML as XML
    4.18 +import Isabelle.XML.Decode
    4.19 +import Isabelle.Term
    4.20 +
    4.21 +
    4.22 +sort :: T Sort
    4.23 +sort = list string
    4.24 +
    4.25 +typ :: T Typ
    4.26 +typ ty =
    4.27 +  ty |> variant
    4.28 +  [\([a], b) -> Type (a, list typ b),
    4.29 +   \([a], b) -> TFree (a, sort b),
    4.30 +   \([a, b], c) -> TVar ((a, int_atom b), sort c)]
    4.31 +
    4.32 +term :: T Term
    4.33 +term t =
    4.34 +  t |> variant
    4.35 +   [\([a], b) -> Const (a, typ b),
    4.36 +    \([a], b) -> Free (a, typ b),
    4.37 +    \([a, b], c) -> Var ((a, int_atom b), typ c),
    4.38 +    \([a], []) -> Bound (int_atom a),
    4.39 +    \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
    4.40 +    \([], a) -> App (pair term term a)]
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/Haskell/Term_XML/Encode.hs	Mon Nov 05 17:06:50 2018 +0100
     5.3 @@ -0,0 +1,39 @@
     5.4 +{- generated by Isabelle -}
     5.5 +
     5.6 +{-  Title:      Tools/Haskell/Term_XML/Encode.hs
     5.7 +    Author:     Makarius
     5.8 +    LICENSE:    BSD 3-clause (Isabelle)
     5.9 +
    5.10 +XML data representation of lambda terms.
    5.11 +-}
    5.12 +
    5.13 +{-# LANGUAGE LambdaCase #-}
    5.14 +
    5.15 +module Isabelle.Term_XML.Encode (sort, typ, term)
    5.16 +where
    5.17 +
    5.18 +import Isabelle.Library
    5.19 +import qualified Isabelle.XML as XML
    5.20 +import Isabelle.XML.Encode
    5.21 +import Isabelle.Term
    5.22 +
    5.23 +
    5.24 +sort :: T Sort
    5.25 +sort = list string
    5.26 +
    5.27 +typ :: T Typ
    5.28 +typ ty =
    5.29 +  ty |> variant
    5.30 +   [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
    5.31 +    \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
    5.32 +    \case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
    5.33 +
    5.34 +term :: T Term
    5.35 +term t =
    5.36 +  t |> variant
    5.37 +   [\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
    5.38 +    \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
    5.39 +    \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
    5.40 +    \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
    5.41 +    \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
    5.42 +    \case { App a -> Just ([], pair term term a); _ -> Nothing }]
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/Haskell/XML/Decode.hs	Mon Nov 05 17:06:50 2018 +0100
     6.3 @@ -0,0 +1,108 @@
     6.4 +{- generated by Isabelle -}
     6.5 +
     6.6 +{-  Title:      Tools/Haskell/XML/Decode.hs
     6.7 +    Author:     Makarius
     6.8 +    LICENSE:    BSD 3-clause (Isabelle)
     6.9 +
    6.10 +XML as data representation language.
    6.11 +-}
    6.12 +
    6.13 +module Isabelle.XML.Decode (
    6.14 +  A, T, V,
    6.15 +
    6.16 +  int_atom, bool_atom, unit_atom,
    6.17 +
    6.18 +  tree, properties, string, init, bool, unit, pair, triple, list, variant
    6.19 +)
    6.20 +where
    6.21 +
    6.22 +import Data.List ((!!))
    6.23 +
    6.24 +import Isabelle.Library
    6.25 +import qualified Isabelle.Value as Value
    6.26 +import qualified Isabelle.Properties as Properties
    6.27 +import qualified Isabelle.XML as XML
    6.28 +
    6.29 +
    6.30 +type A a = String -> a
    6.31 +type T a = XML.Body -> a
    6.32 +type V a = ([String], XML.Body) -> a
    6.33 +
    6.34 +err_atom = error "Malformed XML atom"
    6.35 +err_body = error "Malformed XML body"
    6.36 +
    6.37 +
    6.38 +{- atomic values -}
    6.39 +
    6.40 +int_atom :: A Int
    6.41 +int_atom s =
    6.42 +  case Value.parse_int s of
    6.43 +    Just i -> i
    6.44 +    Nothing -> err_atom
    6.45 +
    6.46 +bool_atom :: A Bool
    6.47 +bool_atom "0" = False
    6.48 +bool_atom "1" = True
    6.49 +bool_atom _ = err_atom
    6.50 +
    6.51 +unit_atom :: A ()
    6.52 +unit_atom "" = ()
    6.53 +unit_atom _ = err_atom
    6.54 +
    6.55 +
    6.56 +{- structural nodes -}
    6.57 +
    6.58 +node (XML.Elem (":", []) ts) = ts
    6.59 +node _ = err_body
    6.60 +
    6.61 +vector atts =
    6.62 +  map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
    6.63 +
    6.64 +tagged (XML.Elem (name, atts) ts) = (int_atom name, (vector atts, ts))
    6.65 +tagged _ = err_body
    6.66 +
    6.67 +
    6.68 +{- representation of standard types -}
    6.69 +
    6.70 +tree :: T XML.Tree
    6.71 +tree [t] = t
    6.72 +tree _ = err_body
    6.73 +
    6.74 +properties :: T Properties.T
    6.75 +properties [XML.Elem (":", props) []] = props
    6.76 +properties _ = err_body
    6.77 +
    6.78 +string :: T String
    6.79 +string [] = ""
    6.80 +string [XML.Text s] = s
    6.81 +string _ = err_body
    6.82 +
    6.83 +int :: T Int
    6.84 +int = int_atom . string
    6.85 +
    6.86 +bool :: T Bool
    6.87 +bool = bool_atom . string
    6.88 +
    6.89 +unit :: T ()
    6.90 +unit = unit_atom . string
    6.91 +
    6.92 +pair :: T a -> T b -> T (a, b)
    6.93 +pair f g [t1, t2] = (f (node t1), g (node t2))
    6.94 +pair _ _ _ = err_body
    6.95 +
    6.96 +triple :: T a -> T b -> T c -> T (a, b, c)
    6.97 +triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
    6.98 +triple _ _ _ _ = err_body
    6.99 +
   6.100 +list :: T a -> T [a]
   6.101 +list f ts = map (f . node) ts
   6.102 +
   6.103 +option :: T a -> T (Maybe a)
   6.104 +option _ [] = Nothing
   6.105 +option f [t] = Just (f (node t))
   6.106 +option _ _ = err_body
   6.107 +
   6.108 +variant :: [V a] -> T a
   6.109 +variant fs [t] = (fs !! tag) (xs, ts)
   6.110 +  where (tag, (xs, ts)) = tagged t
   6.111 +variant _ _ = err_body
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/Haskell/XML/Encode.hs	Mon Nov 05 17:06:50 2018 +0100
     7.3 @@ -0,0 +1,83 @@
     7.4 +{- generated by Isabelle -}
     7.5 +
     7.6 +{-  Title:      Tools/Haskell/XML/Encode.hs
     7.7 +    Author:     Makarius
     7.8 +    LICENSE:    BSD 3-clause (Isabelle)
     7.9 +
    7.10 +XML as data representation language.
    7.11 +-}
    7.12 +
    7.13 +module Isabelle.XML.Encode (
    7.14 +  A, T, V,
    7.15 +
    7.16 +  int_atom, bool_atom, unit_atom,
    7.17 +
    7.18 +  tree, properties, string, init, bool, unit, pair, triple, list, variant
    7.19 +)
    7.20 +where
    7.21 +
    7.22 +import Isabelle.Library
    7.23 +import qualified Isabelle.Value as Value
    7.24 +import qualified Isabelle.Properties as Properties
    7.25 +import qualified Isabelle.XML as XML
    7.26 +
    7.27 +
    7.28 +type A a = a -> String
    7.29 +type T a = a -> XML.Body
    7.30 +type V a = a -> Maybe ([String], XML.Body)
    7.31 +
    7.32 +
    7.33 +-- atomic values
    7.34 +
    7.35 +int_atom :: A Int
    7.36 +int_atom = Value.print_int
    7.37 +
    7.38 +bool_atom :: A Bool
    7.39 +bool_atom False = "0"
    7.40 +bool_atom True = "1"
    7.41 +
    7.42 +unit_atom :: A ()
    7.43 +unit_atom () = ""
    7.44 +
    7.45 +
    7.46 +-- structural nodes
    7.47 +
    7.48 +node = XML.Elem (":", [])
    7.49 +
    7.50 +vector = map_index (\(i, x) -> (int_atom i, x))
    7.51 +
    7.52 +tagged (tag, (xs, ts)) = XML.Elem (int_atom tag, vector xs) ts
    7.53 +
    7.54 +
    7.55 +-- representation of standard types
    7.56 +
    7.57 +tree :: T XML.Tree
    7.58 +tree t = [t]
    7.59 +
    7.60 +properties :: T Properties.T
    7.61 +properties props = [XML.Elem (":", props) []]
    7.62 +
    7.63 +string :: T String
    7.64 +string "" = []
    7.65 +string s = [XML.Text s]
    7.66 +
    7.67 +int :: T Int
    7.68 +int = string . int_atom
    7.69 +
    7.70 +bool :: T Bool
    7.71 +bool = string . bool_atom
    7.72 +
    7.73 +unit :: T ()
    7.74 +unit = string . unit_atom
    7.75 +
    7.76 +pair :: T a -> T b -> T (a, b)
    7.77 +pair f g (x, y) = [node (f x), node (g y)]
    7.78 +
    7.79 +triple :: T a -> T b -> T c -> T (a, b, c)
    7.80 +triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
    7.81 +
    7.82 +list :: T a -> T [a]
    7.83 +list f xs = map (node . f) xs
    7.84 +
    7.85 +variant :: [V a] -> T a
    7.86 +variant fs x = [tagged (the (get_index (\f -> f x) fs))]
     8.1 --- a/src/Tools/Haskell/haskell.ML	Mon Nov 05 15:04:31 2018 +0100
     8.2 +++ b/src/Tools/Haskell/haskell.ML	Mon Nov 05 17:06:50 2018 +0100
     8.3 @@ -53,7 +53,12 @@
     8.4    \<^path>\<open>Properties.hs\<close>,
     8.5    \<^path>\<open>Markup.hs\<close>,
     8.6    \<^path>\<open>XML.hs\<close>,
     8.7 -  \<^path>\<open>YXML.hs\<close>];
     8.8 +  \<^path>\<open>XML/Encode.hs\<close>,
     8.9 +  \<^path>\<open>XML/Decode.hs\<close>,
    8.10 +  \<^path>\<open>YXML.hs\<close>,
    8.11 +  \<^path>\<open>Term.hs\<close>,
    8.12 +  \<^path>\<open>Term_XML/Encode.hs\<close>,
    8.13 +  \<^path>\<open>Term_XML/Decode.hs\<close>];
    8.14  
    8.15  val master_dir = Resources.master_directory \<^theory>;
    8.16