src/Tools/Haskell/Haskell.thy
author wenzelm
Mon, 05 Nov 2018 17:06:50 +0100
changeset 69240 16ca270090b6
parent 69236 a75aab6d785b
child 69248 9f21381600e3
permissions -rw-r--r--
more Haskell operations; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     1
(*  Title:      Tools/Haskell/Haskell.thy
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
     3
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
     4
Support for Isabelle tools in Haskell.
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     5
*)
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     6
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     7
theory Haskell
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     8
  imports Pure
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
     9
  keywords "generate_haskell_file" "export_haskell_file" :: thy_decl
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
    10
begin
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
    11
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    12
ML_file "haskell.ML"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    13
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    14
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    15
section \<open>Commands\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    16
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
    17
ML \<open>
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
    18
  Outer_Syntax.command \<^command_keyword>\<open>generate_haskell_file\<close> "generate Haskell file"
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    19
    (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    20
      >> Haskell.generate_file_cmd);
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    21
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    22
  Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    23
    (Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    24
      >> Haskell.export_file_cmd);
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    25
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    26
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    27
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    28
section \<open>Source modules\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    29
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    30
generate_haskell_file "Library.hs" = \<open>
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
    31
{-  Title:      Tools/Haskell/Library.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    32
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    33
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    34
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    35
Basic library of Isabelle idioms.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    36
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    37
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    38
module Isabelle.Library (
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    39
  (|>), (|->), (#>), (#->),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    40
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    41
  the, the_default,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    42
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    43
  fold, fold_rev, single, map_index, get_index,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    44
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    45
  quote, trim_line)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    46
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    47
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    48
import Data.Maybe
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    49
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    50
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    51
{- functions -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    52
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    53
(|>) :: a -> (a -> b) -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    54
x |> f = f x
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    55
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    56
(|->) :: (a, b) -> (a -> b -> c) -> c
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    57
(x, y) |-> f = f x y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    58
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    59
(#>) :: (a -> b) -> (b -> c) -> a -> c
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    60
(f #> g) x = x |> f |> g
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    61
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    62
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    63
(f #-> g) x  = x |> f |-> g
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    64
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    65
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    66
{- options -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    67
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    68
the :: Maybe a -> a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    69
the (Just x) = x
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    70
the Nothing = error "the Nothing"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    71
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    72
the_default :: a -> Maybe a -> a
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    73
the_default x Nothing = x
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    74
the_default _ (Just y) = y
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    75
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
    76
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    77
{- lists -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    78
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    79
fold :: (a -> b -> b) -> [a] -> b -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    80
fold _ [] y = y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    81
fold f (x : xs) y = fold f xs (f x y)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    82
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    83
fold_rev :: (a -> b -> b) -> [a] -> b -> b
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    84
fold_rev _ [] y = y
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    85
fold_rev f (x : xs) y = f x (fold_rev f xs y)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    86
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    87
single :: a -> [a]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    88
single x = [x]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
    89
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    90
map_index :: ((Int, a) -> b) -> [a] -> [b]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    91
map_index f = map_aux 0
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    92
  where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    93
    map_aux _ [] = []
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    94
    map_aux i (x : xs) = f (i, x) : map_aux (i + 1) xs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    95
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    96
get_index :: (a -> Maybe b) -> [a] -> Maybe (Int, b)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    97
get_index f = get_aux 0
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    98
  where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
    99
    get_aux _ [] = Nothing
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   100
    get_aux i (x : xs) =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   101
      case f x of
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   102
        Nothing -> get_aux (i + 1) xs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   103
        Just y -> Just (i, y)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   104
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   105
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   106
{- strings -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   107
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   108
quote :: String -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   109
quote s = "\"" ++ s ++ "\""
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   110
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   111
trim_line :: String -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   112
trim_line line =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   113
  case reverse line of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   114
    '\n' : '\r' : rest -> reverse rest
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   115
    '\n' : rest -> reverse rest
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   116
    _ -> line
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   117
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   118
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   119
generate_haskell_file "Value.hs" = \<open>
69233
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   120
{-  Title:      Haskell/Tools/Value.hs
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   121
    Author:     Makarius
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   122
    LICENSE:    BSD 3-clause (Isabelle)
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   123
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   124
Plain values, represented as string.
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   125
-}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   126
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   127
module Isabelle.Value
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   128
  (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   129
where
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   130
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   131
import Data.Maybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   132
import qualified Data.List as List
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   133
import qualified Text.Read as Read
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   134
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   135
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   136
{- bool -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   137
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   138
print_bool :: Bool -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   139
print_bool True = "true"
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   140
print_bool False = "false"
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   141
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   142
parse_bool :: String -> Maybe Bool
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   143
parse_bool "true" = Just True
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   144
parse_bool "false" = Just False
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   145
parse_bool _ = Nothing
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   146
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   147
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   148
{- int -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   149
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   150
print_int :: Int -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   151
print_int = show
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   152
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   153
parse_int :: String -> Maybe Int
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   154
parse_int = Read.readMaybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   155
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   156
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   157
{- real -}
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   158
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   159
print_real :: Double -> String
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   160
print_real x =
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   161
  let s = show x in
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   162
    case span (/= '.') s of
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   163
      (a, '.' : b) | List.all (== '0') b -> a
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   164
      _ -> s
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   165
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   166
parse_real :: String -> Maybe Double
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   167
parse_real = Read.readMaybe
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   168
\<close>
560263485988 ported from src/Pure/General/value.ML;
wenzelm
parents: 69228
diff changeset
   169
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   170
generate_haskell_file "Buffer.hs" = \<open>
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
   171
{-  Title:      Tools/Haskell/Buffer.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   172
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   173
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   174
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   175
Efficient text buffers.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   176
-}
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   177
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   178
module Isabelle.Buffer (T, empty, add, content)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   179
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   180
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   181
newtype T = Buffer [String]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   182
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   183
empty :: T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   184
empty = Buffer []
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   185
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   186
add :: String -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   187
add "" buf = buf
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   188
add x (Buffer xs) = Buffer (x : xs)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   189
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   190
content :: T -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   191
content (Buffer xs) = concat (reverse xs)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   192
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   193
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   194
generate_haskell_file "Properties.hs" = \<open>
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
   195
{-  Title:      Tools/Haskell/Properties.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   196
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   197
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   198
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   199
Property lists.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   200
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   201
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   202
module Isabelle.Properties (Entry, T, defined, get, put, remove)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   203
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   204
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   205
import qualified Data.List as List
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   206
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   207
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   208
type Entry = (String, String)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   209
type T = [Entry]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   210
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   211
defined :: T -> String -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   212
defined props name = any (\(a, _) -> a == name) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   213
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   214
get :: T -> String -> Maybe String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   215
get props name = List.lookup name props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   216
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   217
put :: Entry -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   218
put entry props = entry : remove (fst entry) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   219
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   220
remove :: String -> T -> T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   221
remove name props =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   222
  if defined props name then filter (\(a, _) -> a /= name) props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   223
  else props
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   224
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   225
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   226
generate_haskell_file "Markup.hs" = \<open>
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
   227
{-  Title:      Haskell/Tools/Markup.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   228
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   229
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   230
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   231
Quasi-abstract markup elements.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   232
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   233
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   234
module Isabelle.Markup (
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   235
  T, empty, is_empty, properties,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   236
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   237
  nameN, name, xnameN, xname, kindN,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   238
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   239
  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   240
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   241
  wordsN, words, no_wordsN, no_words,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   242
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   243
  tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   244
  numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   245
  inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   246
  token_rangeN, token_range,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   247
  sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   248
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   249
  antiquotedN, antiquoted, antiquoteN, antiquote,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   250
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   251
  paragraphN, paragraph, text_foldN, text_fold,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   252
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   253
  keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   254
  improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   255
  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   256
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   257
  writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   258
  warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   259
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   260
  intensifyN, intensify,
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   261
  Output, no_output)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   262
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   263
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   264
import Prelude hiding (words, error)
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   265
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   266
import Isabelle.Library
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   267
import qualified Isabelle.Properties as Properties
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   268
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   269
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   270
{- basic markup -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   271
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   272
type T = (String, Properties.T)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   273
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   274
empty :: T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   275
empty = ("", [])
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   276
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   277
is_empty :: T -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   278
is_empty ("", _) = True
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   279
is_empty _ = False
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   280
69234
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   281
properties :: Properties.T -> T -> T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   282
properties more_props (elem, props) =
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   283
  (elem, fold_rev Properties.put more_props props)
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   284
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   285
markup_elem name = (name, (name, []) :: T)
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   286
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   287
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   288
{- misc properties -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   289
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   290
nameN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   291
nameN = \<open>Markup.nameN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   292
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   293
name :: String -> T -> T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   294
name a = properties [(nameN, a)]
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   295
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   296
xnameN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   297
xnameN = \<open>Markup.xnameN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   298
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   299
xname :: String -> T -> T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   300
xname a = properties [(xnameN, a)]
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   301
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   302
kindN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   303
kindN = \<open>Markup.kindN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   304
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   305
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   306
{- position -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   307
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   308
lineN, end_lineN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   309
lineN = \<open>Markup.lineN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   310
end_lineN = \<open>Markup.end_lineN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   311
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   312
offsetN, end_offsetN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   313
offsetN = \<open>Markup.offsetN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   314
end_offsetN = \<open>Markup.end_offsetN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   315
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   316
fileN, idN :: String
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   317
fileN = \<open>Markup.fileN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   318
idN = \<open>Markup.idN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   319
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   320
positionN :: String; position :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   321
(positionN, position) = markup_elem \<open>Markup.positionN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   322
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   323
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   324
{- text properties -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   325
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   326
wordsN :: String; words :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   327
(wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   328
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   329
no_wordsN :: String; no_words :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   330
(no_wordsN, no_words) = markup_elem \<open>Markup.no_wordsN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   331
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   332
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   333
{- inner syntax -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   334
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   335
tfreeN :: String; tfree :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   336
(tfreeN, tfree) = markup_elem \<open>Markup.tfreeN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   337
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   338
tvarN :: String; tvar :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   339
(tvarN, tvar) = markup_elem \<open>Markup.tvarN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   340
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   341
freeN :: String; free :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   342
(freeN, free) = markup_elem \<open>Markup.freeN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   343
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   344
skolemN :: String; skolem :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   345
(skolemN, skolem) = markup_elem \<open>Markup.skolemN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   346
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   347
boundN :: String; bound :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   348
(boundN, bound) = markup_elem \<open>Markup.boundN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   349
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   350
varN :: String; var :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   351
(varN, var) = markup_elem \<open>Markup.varN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   352
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   353
numeralN :: String; numeral :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   354
(numeralN, numeral) = markup_elem \<open>Markup.numeralN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   355
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   356
literalN :: String; literal :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   357
(literalN, literal) = markup_elem \<open>Markup.literalN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   358
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   359
delimiterN :: String; delimiter :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   360
(delimiterN, delimiter) = markup_elem \<open>Markup.delimiterN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   361
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   362
inner_stringN :: String; inner_string :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   363
(inner_stringN, inner_string) = markup_elem \<open>Markup.inner_stringN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   364
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   365
inner_cartoucheN :: String; inner_cartouche :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   366
(inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   367
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   368
inner_commentN :: String; inner_comment :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   369
(inner_commentN, inner_comment) = markup_elem \<open>Markup.inner_commentN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   370
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   371
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   372
token_rangeN :: String; token_range :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   373
(token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   374
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   375
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   376
sortingN :: String; sorting :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   377
(sortingN, sorting) = markup_elem \<open>Markup.sortingN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   378
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   379
typingN :: String; typing :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   380
(typingN, typing) = markup_elem \<open>Markup.typingN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   381
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   382
class_parameterN :: String; class_parameter :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   383
(class_parameterN, class_parameter) = markup_elem \<open>Markup.class_parameterN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   384
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   385
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   386
{- antiquotations -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   387
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   388
antiquotedN :: String; antiquoted :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   389
(antiquotedN, antiquoted) = markup_elem \<open>Markup.antiquotedN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   390
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   391
antiquoteN :: String; antiquote :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   392
(antiquoteN, antiquote) = markup_elem \<open>Markup.antiquoteN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   393
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   394
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   395
{- text structure -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   396
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   397
paragraphN :: String; paragraph :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   398
(paragraphN, paragraph) = markup_elem \<open>Markup.paragraphN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   399
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   400
text_foldN :: String; text_fold :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   401
(text_foldN, text_fold) = markup_elem \<open>Markup.text_foldN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   402
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   403
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   404
{- outer syntax -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   405
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   406
keyword1N :: String; keyword1 :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   407
(keyword1N, keyword1) = markup_elem \<open>Markup.keyword1N\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   408
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   409
keyword2N :: String; keyword2 :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   410
(keyword2N, keyword2) = markup_elem \<open>Markup.keyword2N\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   411
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   412
keyword3N :: String; keyword3 :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   413
(keyword3N, keyword3) = markup_elem \<open>Markup.keyword3N\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   414
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   415
quasi_keywordN :: String; quasi_keyword :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   416
(quasi_keywordN, quasi_keyword) = markup_elem \<open>Markup.quasi_keywordN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   417
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   418
improperN :: String; improper :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   419
(improperN, improper) = markup_elem \<open>Markup.improperN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   420
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   421
operatorN :: String; operator :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   422
(operatorN, operator) = markup_elem \<open>Markup.operatorN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   423
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   424
stringN :: String; string :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   425
(stringN, string) = markup_elem \<open>Markup.stringN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   426
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   427
alt_stringN :: String; alt_string :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   428
(alt_stringN, alt_string) = markup_elem \<open>Markup.alt_stringN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   429
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   430
verbatimN :: String; verbatim :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   431
(verbatimN, verbatim) = markup_elem \<open>Markup.verbatimN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   432
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   433
cartoucheN :: String; cartouche :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   434
(cartoucheN, cartouche) = markup_elem \<open>Markup.cartoucheN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   435
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   436
commentN :: String; comment :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   437
(commentN, comment) = markup_elem \<open>Markup.commentN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   438
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   439
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   440
{- messages -}
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   441
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   442
writelnN :: String; writeln :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   443
(writelnN, writeln) = markup_elem \<open>Markup.writelnN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   444
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   445
stateN :: String; state :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   446
(stateN, state) = markup_elem \<open>Markup.stateN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   447
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   448
informationN :: String; information :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   449
(informationN, information) = markup_elem \<open>Markup.informationN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   450
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   451
tracingN :: String; tracing :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   452
(tracingN, tracing) = markup_elem \<open>Markup.tracingN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   453
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   454
warningN :: String; warning :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   455
(warningN, warning) = markup_elem \<open>Markup.warningN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   456
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   457
legacyN :: String; legacy :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   458
(legacyN, legacy) = markup_elem \<open>Markup.legacyN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   459
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   460
errorN :: String; error :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   461
(errorN, error) = markup_elem \<open>Markup.errorN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   462
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   463
reportN :: String; report :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   464
(reportN, report) = markup_elem \<open>Markup.reportN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   465
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   466
no_reportN :: String; no_report :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   467
(no_reportN, no_report) = markup_elem \<open>Markup.no_reportN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   468
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   469
intensifyN :: String; intensify :: T
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   470
(intensifyN, intensify) = markup_elem \<open>Markup.intensifyN\<close>
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   471
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   472
2dec32c7313f more Haskell operations;
wenzelm
parents: 69233
diff changeset
   473
{- output -}
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   474
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   475
type Output = (String, String)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   476
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   477
no_output :: Output
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   478
no_output = ("", "")
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   479
\<close>
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   480
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   481
generate_haskell_file "XML.hs" = \<open>
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
   482
{-  Title:      Tools/Haskell/XML.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   483
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   484
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   485
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   486
Untyped XML trees and representation of ML values.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   487
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   488
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   489
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   490
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   491
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   492
import qualified Data.List as List
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   493
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   494
import Isabelle.Library
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   495
import qualified Isabelle.Properties as Properties
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   496
import qualified Isabelle.Markup as Markup
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   497
import qualified Isabelle.Buffer as Buffer
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   498
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   499
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   500
{- types -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   501
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   502
type Attributes = Properties.T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   503
type Body = [Tree]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   504
data Tree = Elem Markup.T Body | Text String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   505
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   506
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   507
{- wrapped elements -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   508
69236
wenzelm
parents: 69234
diff changeset
   509
wrap_elem (((a, atts), body1), body2) =
wenzelm
parents: 69234
diff changeset
   510
  Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   511
69236
wenzelm
parents: 69234
diff changeset
   512
unwrap_elem
wenzelm
parents: 69234
diff changeset
   513
  (Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)) =
wenzelm
parents: 69234
diff changeset
   514
  Just (((a, atts), body1), body2)
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   515
unwrap_elem _ = Nothing
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   516
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   517
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   518
{- text content -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   519
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   520
add_content tree =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   521
  case unwrap_elem tree of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   522
    Just (_, ts) -> fold add_content ts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   523
    Nothing ->
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   524
      case tree of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   525
        Elem _ ts -> fold add_content ts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   526
        Text s -> Buffer.add s
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   527
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   528
content_of body = Buffer.empty |> fold add_content body |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   529
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   530
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   531
{- string representation -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   532
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   533
encode '<' = "&lt;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   534
encode '>' = "&gt;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   535
encode '&' = "&amp;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   536
encode '\'' = "&apos;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   537
encode '\"' = "&quot;"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   538
encode c = [c]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   539
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   540
instance Show Tree where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   541
  show tree =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   542
    Buffer.empty |> show_tree tree |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   543
    where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   544
      show_tree (Elem (name, atts) []) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   545
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   546
      show_tree (Elem (name, atts) ts) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   547
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   548
        fold show_tree ts #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   549
        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   550
      show_tree (Text s) = Buffer.add (show_text s)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   551
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   552
      show_elem name atts =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   553
        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   554
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   555
      show_text = concatMap encode
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   556
\<close>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   557
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   558
generate_haskell_file "XML/Encode.hs" = \<open>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   559
{-  Title:      Tools/Haskell/XML/Encode.hs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   560
    Author:     Makarius
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   561
    LICENSE:    BSD 3-clause (Isabelle)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   562
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   563
XML as data representation language.
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   564
-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   565
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   566
module Isabelle.XML.Encode (
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   567
  A, T, V,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   568
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   569
  int_atom, bool_atom, unit_atom,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   570
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   571
  tree, properties, string, init, bool, unit, pair, triple, list, variant
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   572
)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   573
where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   574
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   575
import Isabelle.Library
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   576
import qualified Isabelle.Value as Value
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   577
import qualified Isabelle.Properties as Properties
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   578
import qualified Isabelle.XML as XML
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   579
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   580
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   581
type A a = a -> String
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   582
type T a = a -> XML.Body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   583
type V a = a -> Maybe ([String], XML.Body)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   584
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   585
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   586
-- atomic values
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   587
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   588
int_atom :: A Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   589
int_atom = Value.print_int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   590
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   591
bool_atom :: A Bool
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   592
bool_atom False = "0"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   593
bool_atom True = "1"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   594
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   595
unit_atom :: A ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   596
unit_atom () = ""
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   597
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   598
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   599
-- structural nodes
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   600
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   601
node = XML.Elem (":", [])
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   602
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   603
vector = map_index (\(i, x) -> (int_atom i, x))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   604
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   605
tagged (tag, (xs, ts)) = XML.Elem (int_atom tag, vector xs) ts
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   606
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   607
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   608
-- representation of standard types
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   609
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   610
tree :: T XML.Tree
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   611
tree t = [t]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   612
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   613
properties :: T Properties.T
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   614
properties props = [XML.Elem (":", props) []]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   615
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   616
string :: T String
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   617
string "" = []
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   618
string s = [XML.Text s]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   619
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   620
int :: T Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   621
int = string . int_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   622
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   623
bool :: T Bool
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   624
bool = string . bool_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   625
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   626
unit :: T ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   627
unit = string . unit_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   628
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   629
pair :: T a -> T b -> T (a, b)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   630
pair f g (x, y) = [node (f x), node (g y)]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   631
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   632
triple :: T a -> T b -> T c -> T (a, b, c)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   633
triple f g h (x, y, z) = [node (f x), node (g y), node (h z)]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   634
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   635
list :: T a -> T [a]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   636
list f xs = map (node . f) xs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   637
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   638
variant :: [V a] -> T a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   639
variant fs x = [tagged (the (get_index (\f -> f x) fs))]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   640
\<close>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   641
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   642
generate_haskell_file "XML/Decode.hs" = \<open>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   643
{-  Title:      Tools/Haskell/XML/Decode.hs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   644
    Author:     Makarius
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   645
    LICENSE:    BSD 3-clause (Isabelle)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   646
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   647
XML as data representation language.
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   648
-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   649
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   650
module Isabelle.XML.Decode (
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   651
  A, T, V,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   652
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   653
  int_atom, bool_atom, unit_atom,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   654
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   655
  tree, properties, string, init, bool, unit, pair, triple, list, variant
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   656
)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   657
where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   658
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   659
import Data.List ((!!))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   660
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   661
import Isabelle.Library
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   662
import qualified Isabelle.Value as Value
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   663
import qualified Isabelle.Properties as Properties
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   664
import qualified Isabelle.XML as XML
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   665
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   666
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   667
type A a = String -> a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   668
type T a = XML.Body -> a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   669
type V a = ([String], XML.Body) -> a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   670
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   671
err_atom = error "Malformed XML atom"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   672
err_body = error "Malformed XML body"
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   673
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   674
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   675
{- atomic values -}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   676
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   677
int_atom :: A Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   678
int_atom s =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   679
  case Value.parse_int s of
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   680
    Just i -> i
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   681
    Nothing -> err_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   682
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   683
bool_atom :: A Bool
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   684
bool_atom "0" = False
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   685
bool_atom "1" = True
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   686
bool_atom _ = err_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   687
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   688
unit_atom :: A ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   689
unit_atom "" = ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   690
unit_atom _ = err_atom
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   691
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   692
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   693
{- structural nodes -}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   694
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   695
node (XML.Elem (":", []) ts) = ts
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   696
node _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   697
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   698
vector atts =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   699
  map_index (\(i, (a, x)) -> if int_atom a == i then x else err_atom) atts
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   700
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   701
tagged (XML.Elem (name, atts) ts) = (int_atom name, (vector atts, ts))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   702
tagged _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   703
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   704
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   705
{- representation of standard types -}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   706
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   707
tree :: T XML.Tree
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   708
tree [t] = t
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   709
tree _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   710
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   711
properties :: T Properties.T
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   712
properties [XML.Elem (":", props) []] = props
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   713
properties _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   714
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   715
string :: T String
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   716
string [] = ""
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   717
string [XML.Text s] = s
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   718
string _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   719
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   720
int :: T Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   721
int = int_atom . string
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   722
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   723
bool :: T Bool
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   724
bool = bool_atom . string
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   725
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   726
unit :: T ()
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   727
unit = unit_atom . string
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   728
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   729
pair :: T a -> T b -> T (a, b)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   730
pair f g [t1, t2] = (f (node t1), g (node t2))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   731
pair _ _ _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   732
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   733
triple :: T a -> T b -> T c -> T (a, b, c)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   734
triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   735
triple _ _ _ _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   736
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   737
list :: T a -> T [a]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   738
list f ts = map (f . node) ts
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   739
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   740
option :: T a -> T (Maybe a)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   741
option _ [] = Nothing
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   742
option f [t] = Just (f (node t))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   743
option _ _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   744
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   745
variant :: [V a] -> T a
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   746
variant fs [t] = (fs !! tag) (xs, ts)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   747
  where (tag, (xs, ts)) = tagged t
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   748
variant _ _ = err_body
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   749
\<close>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   750
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   751
generate_haskell_file "YXML.hs" = \<open>
69226
68f5dc2275ac tuned whitespace;
wenzelm
parents: 69225
diff changeset
   752
{-  Title:      Tools/Haskell/YXML.hs
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   753
    Author:     Makarius
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   754
    LICENSE:    BSD 3-clause (Isabelle)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   755
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   756
Efficient text representation of XML trees.  Suitable for direct
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   757
inlining into plain text.
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   758
-}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   759
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   760
module Isabelle.YXML (charX, charY, strX, strY, detect,
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   761
  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   762
where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   763
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   764
import qualified Data.Char as Char
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   765
import qualified Data.List as List
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   766
69225
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   767
import Isabelle.Library
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   768
import qualified Isabelle.Markup as Markup
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   769
import qualified Isabelle.XML as XML
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   770
import qualified Isabelle.Buffer as Buffer
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   771
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   772
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   773
{- markers -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   774
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   775
charX, charY :: Char
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   776
charX = Char.chr 5
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   777
charY = Char.chr 6
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   778
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   779
strX, strY, strXY, strXYX :: String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   780
strX = [charX]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   781
strY = [charY]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   782
strXY = strX ++ strY
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   783
strXYX = strXY ++ strX
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   784
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   785
detect :: String -> Bool
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   786
detect = any (\c -> c == charX || c == charY)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   787
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   788
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   789
{- output -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   790
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   791
buffer_attrib (a, x) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   792
  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   793
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   794
buffer_body :: XML.Body -> Buffer.T -> Buffer.T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   795
buffer_body = fold buffer
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   796
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   797
buffer :: XML.Tree -> Buffer.T -> Buffer.T
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   798
buffer (XML.Elem (name, atts) ts) =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   799
  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   800
  buffer_body ts #>
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   801
  Buffer.add strXYX
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   802
buffer (XML.Text s) = Buffer.add s
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   803
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   804
string_of_body :: XML.Body -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   805
string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   806
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   807
string_of :: XML.Tree -> String
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   808
string_of = string_of_body . single
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   809
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   810
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   811
{- parse -}
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   812
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   813
-- split: fields or non-empty tokens
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   814
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   815
split :: Bool -> Char -> String -> [String]
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   816
split _ _ [] = []
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   817
split fields sep str = splitting str
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   818
  where
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   819
    splitting rest =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   820
      case span (/= sep) rest of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   821
        (_, []) -> cons rest []
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   822
        (prfx, _ : rest') -> cons prfx (splitting rest')
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   823
    cons item = if fields || not (null item) then (:) item else id
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   824
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   825
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   826
-- structural errors
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   827
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   828
err msg = error ("Malformed YXML: " ++ msg)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   829
err_attribute = err "bad attribute"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   830
err_element = err "bad element"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   831
err_unbalanced "" = err "unbalanced element"
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   832
err_unbalanced name = err ("unbalanced element " ++ quote name)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   833
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   834
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   835
-- stack operations
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   836
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   837
add x ((elem, body) : pending) = (elem, x : body) : pending
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   838
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   839
push "" _ _ = err_element
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   840
push name atts pending = ((name, atts), []) : pending
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   841
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   842
pop ((("", _), _) : _) = err_unbalanced ""
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   843
pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   844
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   845
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   846
-- parsing
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   847
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   848
parse_attrib s =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   849
  case List.elemIndex '=' s of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   850
    Just i | i > 0 -> (take i s, drop (i + 1) s)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   851
    _ -> err_attribute
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   852
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   853
parse_chunk ["", ""] = pop
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   854
parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   855
parse_chunk txts = fold (add . XML.Text) txts
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   856
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   857
parse_body :: String -> XML.Body
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   858
parse_body source =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   859
  case fold parse_chunk chunks [(("", []), [])] of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   860
    [(("", _), result)] -> reverse result
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   861
    ((name, _), _) : _ -> err_unbalanced name
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   862
  where chunks = split False charX source |> map (split True charY)
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   863
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   864
parse :: String -> XML.Tree
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   865
parse source =
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   866
  case parse_body source of
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   867
    [result] -> result
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   868
    [] -> XML.Text ""
bf2fecda8383 support for Isabelle tools in Haskell;
wenzelm
parents: 69222
diff changeset
   869
    _ -> err "multiple results"
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   870
\<close>
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   871
69240
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   872
generate_haskell_file "Term.hs" = \<open>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   873
{-  Title:      Tools/Haskell/Term.hs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   874
    Author:     Makarius
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   875
    LICENSE:    BSD 3-clause (Isabelle)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   876
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   877
Lambda terms, types, sorts.
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   878
-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   879
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   880
module Isabelle.Term (
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   881
  Indexname,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   882
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   883
  Sort, dummyS,
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   884
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   885
  Typ(..), dummyT, Term(..))
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   886
where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   887
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   888
type Indexname = (String, Int)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   889
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   890
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   891
type Sort = [String]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   892
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   893
dummyS :: Sort
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   894
dummyS = [""]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   895
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   896
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   897
data Typ =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   898
    Type (String, [Typ])
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   899
  | TFree (String, Sort)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   900
  | TVar (Indexname, Sort)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   901
  deriving Show
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   902
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   903
dummyT :: Typ
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   904
dummyT = Type (\<open>\<^type_name>\<open>dummy\<close>\<close>, [])
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   905
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   906
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   907
data Term =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   908
    Const (String, Typ)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   909
  | Free (String, Typ)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   910
  | Var (Indexname, Typ)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   911
  | Bound Int
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   912
  | Abs (String, Typ, Term)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   913
  | App (Term, Term)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   914
  deriving Show
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   915
\<close>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   916
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   917
generate_haskell_file "Term_XML/Encode.hs" = \<open>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   918
{-  Title:      Tools/Haskell/Term_XML/Encode.hs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   919
    Author:     Makarius
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   920
    LICENSE:    BSD 3-clause (Isabelle)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   921
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   922
XML data representation of lambda terms.
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   923
-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   924
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   925
{-# LANGUAGE LambdaCase #-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   926
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   927
module Isabelle.Term_XML.Encode (sort, typ, term)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   928
where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   929
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   930
import Isabelle.Library
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   931
import qualified Isabelle.XML as XML
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   932
import Isabelle.XML.Encode
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   933
import Isabelle.Term
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   934
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   935
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   936
sort :: T Sort
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   937
sort = list string
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   938
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   939
typ :: T Typ
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   940
typ ty =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   941
  ty |> variant
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   942
   [\case { Type (a, b) -> Just ([a], list typ b); _ -> Nothing },
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   943
    \case { TFree (a, b) -> Just ([a], sort b); _ -> Nothing },
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   944
    \case { TVar ((a, b), c) -> Just ([a, int_atom b], sort c); _ -> Nothing }]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   945
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   946
term :: T Term
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   947
term t =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   948
  t |> variant
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   949
   [\case { Const (a, b) -> Just ([a], typ b); _ -> Nothing },
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   950
    \case { Free (a, b) -> Just ([a], typ b); _ -> Nothing },
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   951
    \case { Var ((a, b), c) -> Just ([a, int_atom b], typ c); _ -> Nothing },
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   952
    \case { Bound a -> Just ([int_atom a], []); _ -> Nothing },
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   953
    \case { Abs (a, b, c) -> Just ([a], pair typ term (b, c)); _ -> Nothing },
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   954
    \case { App a -> Just ([], pair term term a); _ -> Nothing }]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   955
\<close>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   956
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   957
generate_haskell_file "Term_XML/Decode.hs" = \<open>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   958
{-  Title:      Tools/Haskell/Term_XML/Decode.hs
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   959
    Author:     Makarius
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   960
    LICENSE:    BSD 3-clause (Isabelle)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   961
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   962
XML data representation of lambda terms.
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   963
-}
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   964
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   965
module Isabelle.Term_XML.Decode (sort, typ, term)
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   966
where
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   967
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   968
import Isabelle.Library
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   969
import qualified Isabelle.XML as XML
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   970
import Isabelle.XML.Decode
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   971
import Isabelle.Term
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   972
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   973
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   974
sort :: T Sort
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   975
sort = list string
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   976
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   977
typ :: T Typ
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   978
typ ty =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   979
  ty |> variant
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   980
  [\([a], b) -> Type (a, list typ b),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   981
   \([a], b) -> TFree (a, sort b),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   982
   \([a, b], c) -> TVar ((a, int_atom b), sort c)]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   983
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   984
term :: T Term
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   985
term t =
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   986
  t |> variant
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   987
   [\([a], b) -> Const (a, typ b),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   988
    \([a], b) -> Free (a, typ b),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   989
    \([a, b], c) -> Var ((a, int_atom b), typ c),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   990
    \([a], []) -> Bound (int_atom a),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   991
    \([a], b) -> let (c, d) = pair typ term b in Abs (a, c, d),
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   992
    \([], a) -> App (pair term term a)]
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   993
\<close>
16ca270090b6 more Haskell operations;
wenzelm
parents: 69236
diff changeset
   994
69222
8365124a86ae support for Isabelle tool development in Haskell;
wenzelm
parents:
diff changeset
   995
end