src/Tools/Haskell/Haskell.thy
author wenzelm
Mon Nov 05 11:29:11 2018 +0100 (7 months ago)
changeset 69236 a75aab6d785b
parent 69234 2dec32c7313f
child 69240 16ca270090b6
permissions -rw-r--r--
tuned;
wenzelm@69222
     1
(*  Title:      Tools/Haskell/Haskell.thy
wenzelm@69222
     2
    Author:     Makarius
wenzelm@69225
     3
wenzelm@69225
     4
Support for Isabelle tools in Haskell.
wenzelm@69222
     5
*)
wenzelm@69222
     6
wenzelm@69222
     7
theory Haskell
wenzelm@69222
     8
  imports Pure
wenzelm@69222
     9
  keywords "generate_haskell_file" "export_haskell_file" :: thy_decl
wenzelm@69222
    10
begin
wenzelm@69222
    11
wenzelm@69225
    12
ML_file "haskell.ML"
wenzelm@69225
    13
wenzelm@69225
    14
wenzelm@69225
    15
section \<open>Commands\<close>
wenzelm@69225
    16
wenzelm@69222
    17
ML \<open>
wenzelm@69222
    18
  Outer_Syntax.command \<^command_keyword>\<open>generate_haskell_file\<close> "generate Haskell file"
wenzelm@69225
    19
    (Parse.position Parse.path -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
wenzelm@69225
    20
      >> Haskell.generate_file_cmd);
wenzelm@69225
    21
wenzelm@69225
    22
  Outer_Syntax.command \<^command_keyword>\<open>export_haskell_file\<close> "export Haskell file"
wenzelm@69225
    23
    (Parse.name -- (\<^keyword>\<open>=\<close> |-- Parse.input Parse.embedded)
wenzelm@69225
    24
      >> Haskell.export_file_cmd);
wenzelm@69225
    25
\<close>
wenzelm@69225
    26
wenzelm@69225
    27
wenzelm@69225
    28
section \<open>Source modules\<close>
wenzelm@69225
    29
wenzelm@69226
    30
generate_haskell_file Library.hs = \<open>
wenzelm@69226
    31
{-  Title:      Tools/Haskell/Library.hs
wenzelm@69225
    32
    Author:     Makarius
wenzelm@69225
    33
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
    34
wenzelm@69225
    35
Basic library of Isabelle idioms.
wenzelm@69225
    36
-}
wenzelm@69225
    37
wenzelm@69225
    38
module Isabelle.Library
wenzelm@69234
    39
  ((|>), (|->), (#>), (#->), the_default, fold, fold_rev, single, quote, trim_line)
wenzelm@69225
    40
where
wenzelm@69225
    41
wenzelm@69234
    42
import Data.Maybe
wenzelm@69234
    43
wenzelm@69234
    44
wenzelm@69225
    45
{- functions -}
wenzelm@69225
    46
wenzelm@69225
    47
(|>) :: a -> (a -> b) -> b
wenzelm@69225
    48
x |> f = f x
wenzelm@69225
    49
wenzelm@69225
    50
(|->) :: (a, b) -> (a -> b -> c) -> c
wenzelm@69225
    51
(x, y) |-> f = f x y
wenzelm@69225
    52
wenzelm@69225
    53
(#>) :: (a -> b) -> (b -> c) -> a -> c
wenzelm@69225
    54
(f #> g) x = x |> f |> g
wenzelm@69225
    55
wenzelm@69225
    56
(#->) :: (a -> (c, b)) -> (c -> b -> d) -> a -> d
wenzelm@69225
    57
(f #-> g) x  = x |> f |-> g
wenzelm@69225
    58
wenzelm@69225
    59
wenzelm@69234
    60
{- options -}
wenzelm@69234
    61
wenzelm@69234
    62
the_default :: a -> Maybe a -> a
wenzelm@69234
    63
the_default x Nothing = x
wenzelm@69234
    64
the_default _ (Just y) = y
wenzelm@69234
    65
wenzelm@69234
    66
wenzelm@69225
    67
{- lists -}
wenzelm@69225
    68
wenzelm@69225
    69
fold :: (a -> b -> b) -> [a] -> b -> b
wenzelm@69225
    70
fold _ [] y = y
wenzelm@69225
    71
fold f (x : xs) y = fold f xs (f x y)
wenzelm@69225
    72
wenzelm@69225
    73
fold_rev :: (a -> b -> b) -> [a] -> b -> b
wenzelm@69225
    74
fold_rev _ [] y = y
wenzelm@69225
    75
fold_rev f (x : xs) y = f x (fold_rev f xs y)
wenzelm@69225
    76
wenzelm@69225
    77
single :: a -> [a]
wenzelm@69225
    78
single x = [x]
wenzelm@69225
    79
wenzelm@69225
    80
wenzelm@69225
    81
{- strings -}
wenzelm@69225
    82
wenzelm@69225
    83
quote :: String -> String
wenzelm@69225
    84
quote s = "\"" ++ s ++ "\""
wenzelm@69225
    85
wenzelm@69225
    86
trim_line :: String -> String
wenzelm@69225
    87
trim_line line =
wenzelm@69225
    88
  case reverse line of
wenzelm@69225
    89
    '\n' : '\r' : rest -> reverse rest
wenzelm@69225
    90
    '\n' : rest -> reverse rest
wenzelm@69225
    91
    _ -> line
wenzelm@69225
    92
\<close>
wenzelm@69225
    93
wenzelm@69233
    94
generate_haskell_file Value.hs = \<open>
wenzelm@69233
    95
{-  Title:      Haskell/Tools/Value.hs
wenzelm@69233
    96
    Author:     Makarius
wenzelm@69233
    97
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69233
    98
wenzelm@69233
    99
Plain values, represented as string.
wenzelm@69233
   100
-}
wenzelm@69233
   101
wenzelm@69233
   102
module Isabelle.Value
wenzelm@69233
   103
  (print_bool, parse_bool, print_int, parse_int, print_real, parse_real)
wenzelm@69233
   104
where
wenzelm@69233
   105
wenzelm@69233
   106
import Data.Maybe
wenzelm@69233
   107
import qualified Data.List as List
wenzelm@69233
   108
import qualified Text.Read as Read
wenzelm@69233
   109
wenzelm@69233
   110
wenzelm@69233
   111
{- bool -}
wenzelm@69233
   112
wenzelm@69233
   113
print_bool :: Bool -> String
wenzelm@69233
   114
print_bool True = "true"
wenzelm@69233
   115
print_bool False = "false"
wenzelm@69233
   116
wenzelm@69233
   117
parse_bool :: String -> Maybe Bool
wenzelm@69233
   118
parse_bool "true" = Just True
wenzelm@69233
   119
parse_bool "false" = Just False
wenzelm@69233
   120
parse_bool _ = Nothing
wenzelm@69233
   121
wenzelm@69233
   122
wenzelm@69233
   123
{- int -}
wenzelm@69233
   124
wenzelm@69233
   125
print_int :: Int -> String
wenzelm@69233
   126
print_int = show
wenzelm@69233
   127
wenzelm@69233
   128
parse_int :: String -> Maybe Int
wenzelm@69233
   129
parse_int = Read.readMaybe
wenzelm@69233
   130
wenzelm@69233
   131
wenzelm@69233
   132
{- real -}
wenzelm@69233
   133
wenzelm@69233
   134
print_real :: Double -> String
wenzelm@69233
   135
print_real x =
wenzelm@69233
   136
  let s = show x in
wenzelm@69233
   137
    case span (/= '.') s of
wenzelm@69233
   138
      (a, '.' : b) | List.all (== '0') b -> a
wenzelm@69233
   139
      _ -> s
wenzelm@69233
   140
wenzelm@69233
   141
parse_real :: String -> Maybe Double
wenzelm@69233
   142
parse_real = Read.readMaybe
wenzelm@69233
   143
\<close>
wenzelm@69233
   144
wenzelm@69226
   145
generate_haskell_file Buffer.hs = \<open>
wenzelm@69226
   146
{-  Title:      Tools/Haskell/Buffer.hs
wenzelm@69225
   147
    Author:     Makarius
wenzelm@69225
   148
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   149
wenzelm@69225
   150
Efficient text buffers.
wenzelm@69225
   151
-}
wenzelm@69222
   152
wenzelm@69225
   153
module Isabelle.Buffer (T, empty, add, content)
wenzelm@69225
   154
where
wenzelm@69225
   155
wenzelm@69225
   156
newtype T = Buffer [String]
wenzelm@69225
   157
wenzelm@69225
   158
empty :: T
wenzelm@69225
   159
empty = Buffer []
wenzelm@69225
   160
wenzelm@69225
   161
add :: String -> T -> T
wenzelm@69225
   162
add "" buf = buf
wenzelm@69225
   163
add x (Buffer xs) = Buffer (x : xs)
wenzelm@69225
   164
wenzelm@69225
   165
content :: T -> String
wenzelm@69225
   166
content (Buffer xs) = concat (reverse xs)
wenzelm@69225
   167
\<close>
wenzelm@69225
   168
wenzelm@69226
   169
generate_haskell_file Properties.hs = \<open>
wenzelm@69226
   170
{-  Title:      Tools/Haskell/Properties.hs
wenzelm@69225
   171
    Author:     Makarius
wenzelm@69225
   172
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   173
wenzelm@69225
   174
Property lists.
wenzelm@69225
   175
-}
wenzelm@69225
   176
wenzelm@69225
   177
module Isabelle.Properties (Entry, T, defined, get, put, remove)
wenzelm@69225
   178
where
wenzelm@69225
   179
wenzelm@69225
   180
import qualified Data.List as List
wenzelm@69225
   181
wenzelm@69225
   182
wenzelm@69225
   183
type Entry = (String, String)
wenzelm@69225
   184
type T = [Entry]
wenzelm@69225
   185
wenzelm@69225
   186
defined :: T -> String -> Bool
wenzelm@69225
   187
defined props name = any (\(a, _) -> a == name) props
wenzelm@69225
   188
wenzelm@69225
   189
get :: T -> String -> Maybe String
wenzelm@69225
   190
get props name = List.lookup name props
wenzelm@69225
   191
wenzelm@69225
   192
put :: Entry -> T -> T
wenzelm@69225
   193
put entry props = entry : remove (fst entry) props
wenzelm@69225
   194
wenzelm@69225
   195
remove :: String -> T -> T
wenzelm@69225
   196
remove name props =
wenzelm@69225
   197
  if defined props name then filter (\(a, _) -> a /= name) props
wenzelm@69225
   198
  else props
wenzelm@69225
   199
\<close>
wenzelm@69225
   200
wenzelm@69226
   201
generate_haskell_file Markup.hs = \<open>
wenzelm@69226
   202
{-  Title:      Haskell/Tools/Markup.hs
wenzelm@69225
   203
    Author:     Makarius
wenzelm@69225
   204
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   205
wenzelm@69225
   206
Quasi-abstract markup elements.
wenzelm@69225
   207
-}
wenzelm@69225
   208
wenzelm@69234
   209
module Isabelle.Markup (
wenzelm@69234
   210
  T, empty, is_empty, properties,
wenzelm@69234
   211
wenzelm@69234
   212
  nameN, name, xnameN, xname, kindN,
wenzelm@69234
   213
wenzelm@69234
   214
  lineN, end_lineN, offsetN, end_offsetN, fileN, idN, positionN, position,
wenzelm@69234
   215
wenzelm@69234
   216
  wordsN, words, no_wordsN, no_words,
wenzelm@69234
   217
wenzelm@69234
   218
  tfreeN, tfree, tvarN, tvar, freeN, free, skolemN, skolem, boundN, bound, varN, var,
wenzelm@69234
   219
  numeralN, numeral, literalN, literal, delimiterN, delimiter, inner_stringN, inner_string,
wenzelm@69234
   220
  inner_cartoucheN, inner_cartouche, inner_commentN, inner_comment,
wenzelm@69234
   221
  token_rangeN, token_range,
wenzelm@69234
   222
  sortingN, sorting, typingN, typing, class_parameterN, class_parameter,
wenzelm@69234
   223
wenzelm@69234
   224
  antiquotedN, antiquoted, antiquoteN, antiquote,
wenzelm@69234
   225
wenzelm@69234
   226
  paragraphN, paragraph, text_foldN, text_fold,
wenzelm@69234
   227
wenzelm@69234
   228
  keyword1N, keyword1, keyword2N, keyword2, keyword3N, keyword3, quasi_keywordN, quasi_keyword,
wenzelm@69234
   229
  improperN, improper, operatorN, operator, stringN, string, alt_stringN, alt_string,
wenzelm@69234
   230
  verbatimN, verbatim, cartoucheN, cartouche, commentN, comment,
wenzelm@69234
   231
wenzelm@69234
   232
  writelnN, writeln, stateN, state, informationN, information, tracingN, tracing,
wenzelm@69234
   233
  warningN, warning, legacyN, legacy, errorN, error, reportN, report, no_reportN, no_report,
wenzelm@69234
   234
wenzelm@69234
   235
  intensifyN, intensify,
wenzelm@69234
   236
  Output, no_output)
wenzelm@69225
   237
where
wenzelm@69225
   238
wenzelm@69234
   239
import Prelude hiding (words, error)
wenzelm@69234
   240
wenzelm@69234
   241
import Isabelle.Library
wenzelm@69225
   242
import qualified Isabelle.Properties as Properties
wenzelm@69225
   243
wenzelm@69225
   244
wenzelm@69234
   245
{- basic markup -}
wenzelm@69234
   246
wenzelm@69225
   247
type T = (String, Properties.T)
wenzelm@69225
   248
wenzelm@69225
   249
empty :: T
wenzelm@69225
   250
empty = ("", [])
wenzelm@69225
   251
wenzelm@69225
   252
is_empty :: T -> Bool
wenzelm@69225
   253
is_empty ("", _) = True
wenzelm@69225
   254
is_empty _ = False
wenzelm@69225
   255
wenzelm@69234
   256
properties :: Properties.T -> T -> T
wenzelm@69234
   257
properties more_props (elem, props) =
wenzelm@69234
   258
  (elem, fold_rev Properties.put more_props props)
wenzelm@69234
   259
wenzelm@69234
   260
markup_elem name = (name, (name, []) :: T)
wenzelm@69234
   261
wenzelm@69234
   262
wenzelm@69234
   263
{- misc properties -}
wenzelm@69234
   264
wenzelm@69234
   265
nameN :: String
wenzelm@69234
   266
nameN = \<open>Markup.nameN\<close>
wenzelm@69234
   267
wenzelm@69234
   268
name :: String -> T -> T
wenzelm@69234
   269
name a = properties [(nameN, a)]
wenzelm@69234
   270
wenzelm@69234
   271
xnameN :: String
wenzelm@69234
   272
xnameN = \<open>Markup.xnameN\<close>
wenzelm@69234
   273
wenzelm@69234
   274
xname :: String -> T -> T
wenzelm@69234
   275
xname a = properties [(xnameN, a)]
wenzelm@69234
   276
wenzelm@69234
   277
kindN :: String
wenzelm@69234
   278
kindN = \<open>Markup.kindN\<close>
wenzelm@69234
   279
wenzelm@69234
   280
wenzelm@69234
   281
{- position -}
wenzelm@69234
   282
wenzelm@69234
   283
lineN, end_lineN :: String
wenzelm@69234
   284
lineN = \<open>Markup.lineN\<close>
wenzelm@69234
   285
end_lineN = \<open>Markup.end_lineN\<close>
wenzelm@69234
   286
wenzelm@69234
   287
offsetN, end_offsetN :: String
wenzelm@69234
   288
offsetN = \<open>Markup.offsetN\<close>
wenzelm@69234
   289
end_offsetN = \<open>Markup.end_offsetN\<close>
wenzelm@69234
   290
wenzelm@69234
   291
fileN, idN :: String
wenzelm@69234
   292
fileN = \<open>Markup.fileN\<close>
wenzelm@69234
   293
idN = \<open>Markup.idN\<close>
wenzelm@69234
   294
wenzelm@69234
   295
positionN :: String; position :: T
wenzelm@69234
   296
(positionN, position) = markup_elem \<open>Markup.positionN\<close>
wenzelm@69234
   297
wenzelm@69234
   298
wenzelm@69234
   299
{- text properties -}
wenzelm@69234
   300
wenzelm@69234
   301
wordsN :: String; words :: T
wenzelm@69234
   302
(wordsN, words) = markup_elem \<open>Markup.wordsN\<close>
wenzelm@69234
   303
wenzelm@69234
   304
no_wordsN :: String; no_words :: T
wenzelm@69234
   305
(no_wordsN, no_words) = markup_elem \<open>Markup.no_wordsN\<close>
wenzelm@69234
   306
wenzelm@69234
   307
wenzelm@69234
   308
{- inner syntax -}
wenzelm@69234
   309
wenzelm@69234
   310
tfreeN :: String; tfree :: T
wenzelm@69234
   311
(tfreeN, tfree) = markup_elem \<open>Markup.tfreeN\<close>
wenzelm@69234
   312
wenzelm@69234
   313
tvarN :: String; tvar :: T
wenzelm@69234
   314
(tvarN, tvar) = markup_elem \<open>Markup.tvarN\<close>
wenzelm@69234
   315
wenzelm@69234
   316
freeN :: String; free :: T
wenzelm@69234
   317
(freeN, free) = markup_elem \<open>Markup.freeN\<close>
wenzelm@69234
   318
wenzelm@69234
   319
skolemN :: String; skolem :: T
wenzelm@69234
   320
(skolemN, skolem) = markup_elem \<open>Markup.skolemN\<close>
wenzelm@69234
   321
wenzelm@69234
   322
boundN :: String; bound :: T
wenzelm@69234
   323
(boundN, bound) = markup_elem \<open>Markup.boundN\<close>
wenzelm@69234
   324
wenzelm@69234
   325
varN :: String; var :: T
wenzelm@69234
   326
(varN, var) = markup_elem \<open>Markup.varN\<close>
wenzelm@69234
   327
wenzelm@69234
   328
numeralN :: String; numeral :: T
wenzelm@69234
   329
(numeralN, numeral) = markup_elem \<open>Markup.numeralN\<close>
wenzelm@69234
   330
wenzelm@69234
   331
literalN :: String; literal :: T
wenzelm@69234
   332
(literalN, literal) = markup_elem \<open>Markup.literalN\<close>
wenzelm@69234
   333
wenzelm@69234
   334
delimiterN :: String; delimiter :: T
wenzelm@69234
   335
(delimiterN, delimiter) = markup_elem \<open>Markup.delimiterN\<close>
wenzelm@69234
   336
wenzelm@69234
   337
inner_stringN :: String; inner_string :: T
wenzelm@69234
   338
(inner_stringN, inner_string) = markup_elem \<open>Markup.inner_stringN\<close>
wenzelm@69234
   339
wenzelm@69234
   340
inner_cartoucheN :: String; inner_cartouche :: T
wenzelm@69234
   341
(inner_cartoucheN, inner_cartouche) = markup_elem \<open>Markup.inner_cartoucheN\<close>
wenzelm@69234
   342
wenzelm@69234
   343
inner_commentN :: String; inner_comment :: T
wenzelm@69234
   344
(inner_commentN, inner_comment) = markup_elem \<open>Markup.inner_commentN\<close>
wenzelm@69234
   345
wenzelm@69234
   346
wenzelm@69234
   347
token_rangeN :: String; token_range :: T
wenzelm@69234
   348
(token_rangeN, token_range) = markup_elem \<open>Markup.token_rangeN\<close>
wenzelm@69234
   349
wenzelm@69234
   350
wenzelm@69234
   351
sortingN :: String; sorting :: T
wenzelm@69234
   352
(sortingN, sorting) = markup_elem \<open>Markup.sortingN\<close>
wenzelm@69234
   353
wenzelm@69234
   354
typingN :: String; typing :: T
wenzelm@69234
   355
(typingN, typing) = markup_elem \<open>Markup.typingN\<close>
wenzelm@69234
   356
wenzelm@69234
   357
class_parameterN :: String; class_parameter :: T
wenzelm@69234
   358
(class_parameterN, class_parameter) = markup_elem \<open>Markup.class_parameterN\<close>
wenzelm@69234
   359
wenzelm@69234
   360
wenzelm@69234
   361
{- antiquotations -}
wenzelm@69234
   362
wenzelm@69234
   363
antiquotedN :: String; antiquoted :: T
wenzelm@69234
   364
(antiquotedN, antiquoted) = markup_elem \<open>Markup.antiquotedN\<close>
wenzelm@69234
   365
wenzelm@69234
   366
antiquoteN :: String; antiquote :: T
wenzelm@69234
   367
(antiquoteN, antiquote) = markup_elem \<open>Markup.antiquoteN\<close>
wenzelm@69234
   368
wenzelm@69234
   369
wenzelm@69234
   370
{- text structure -}
wenzelm@69234
   371
wenzelm@69234
   372
paragraphN :: String; paragraph :: T
wenzelm@69234
   373
(paragraphN, paragraph) = markup_elem \<open>Markup.paragraphN\<close>
wenzelm@69234
   374
wenzelm@69234
   375
text_foldN :: String; text_fold :: T
wenzelm@69234
   376
(text_foldN, text_fold) = markup_elem \<open>Markup.text_foldN\<close>
wenzelm@69234
   377
wenzelm@69234
   378
wenzelm@69234
   379
{- outer syntax -}
wenzelm@69234
   380
wenzelm@69234
   381
keyword1N :: String; keyword1 :: T
wenzelm@69234
   382
(keyword1N, keyword1) = markup_elem \<open>Markup.keyword1N\<close>
wenzelm@69234
   383
wenzelm@69234
   384
keyword2N :: String; keyword2 :: T
wenzelm@69234
   385
(keyword2N, keyword2) = markup_elem \<open>Markup.keyword2N\<close>
wenzelm@69234
   386
wenzelm@69234
   387
keyword3N :: String; keyword3 :: T
wenzelm@69234
   388
(keyword3N, keyword3) = markup_elem \<open>Markup.keyword3N\<close>
wenzelm@69234
   389
wenzelm@69234
   390
quasi_keywordN :: String; quasi_keyword :: T
wenzelm@69234
   391
(quasi_keywordN, quasi_keyword) = markup_elem \<open>Markup.quasi_keywordN\<close>
wenzelm@69234
   392
wenzelm@69234
   393
improperN :: String; improper :: T
wenzelm@69234
   394
(improperN, improper) = markup_elem \<open>Markup.improperN\<close>
wenzelm@69234
   395
wenzelm@69234
   396
operatorN :: String; operator :: T
wenzelm@69234
   397
(operatorN, operator) = markup_elem \<open>Markup.operatorN\<close>
wenzelm@69234
   398
wenzelm@69234
   399
stringN :: String; string :: T
wenzelm@69234
   400
(stringN, string) = markup_elem \<open>Markup.stringN\<close>
wenzelm@69234
   401
wenzelm@69234
   402
alt_stringN :: String; alt_string :: T
wenzelm@69234
   403
(alt_stringN, alt_string) = markup_elem \<open>Markup.alt_stringN\<close>
wenzelm@69234
   404
wenzelm@69234
   405
verbatimN :: String; verbatim :: T
wenzelm@69234
   406
(verbatimN, verbatim) = markup_elem \<open>Markup.verbatimN\<close>
wenzelm@69234
   407
wenzelm@69234
   408
cartoucheN :: String; cartouche :: T
wenzelm@69234
   409
(cartoucheN, cartouche) = markup_elem \<open>Markup.cartoucheN\<close>
wenzelm@69234
   410
wenzelm@69234
   411
commentN :: String; comment :: T
wenzelm@69234
   412
(commentN, comment) = markup_elem \<open>Markup.commentN\<close>
wenzelm@69234
   413
wenzelm@69234
   414
wenzelm@69234
   415
{- messages -}
wenzelm@69234
   416
wenzelm@69234
   417
writelnN :: String; writeln :: T
wenzelm@69234
   418
(writelnN, writeln) = markup_elem \<open>Markup.writelnN\<close>
wenzelm@69234
   419
wenzelm@69234
   420
stateN :: String; state :: T
wenzelm@69234
   421
(stateN, state) = markup_elem \<open>Markup.stateN\<close>
wenzelm@69234
   422
wenzelm@69234
   423
informationN :: String; information :: T
wenzelm@69234
   424
(informationN, information) = markup_elem \<open>Markup.informationN\<close>
wenzelm@69234
   425
wenzelm@69234
   426
tracingN :: String; tracing :: T
wenzelm@69234
   427
(tracingN, tracing) = markup_elem \<open>Markup.tracingN\<close>
wenzelm@69234
   428
wenzelm@69234
   429
warningN :: String; warning :: T
wenzelm@69234
   430
(warningN, warning) = markup_elem \<open>Markup.warningN\<close>
wenzelm@69234
   431
wenzelm@69234
   432
legacyN :: String; legacy :: T
wenzelm@69234
   433
(legacyN, legacy) = markup_elem \<open>Markup.legacyN\<close>
wenzelm@69234
   434
wenzelm@69234
   435
errorN :: String; error :: T
wenzelm@69234
   436
(errorN, error) = markup_elem \<open>Markup.errorN\<close>
wenzelm@69234
   437
wenzelm@69234
   438
reportN :: String; report :: T
wenzelm@69234
   439
(reportN, report) = markup_elem \<open>Markup.reportN\<close>
wenzelm@69234
   440
wenzelm@69234
   441
no_reportN :: String; no_report :: T
wenzelm@69234
   442
(no_reportN, no_report) = markup_elem \<open>Markup.no_reportN\<close>
wenzelm@69234
   443
wenzelm@69234
   444
intensifyN :: String; intensify :: T
wenzelm@69234
   445
(intensifyN, intensify) = markup_elem \<open>Markup.intensifyN\<close>
wenzelm@69234
   446
wenzelm@69234
   447
wenzelm@69234
   448
{- output -}
wenzelm@69225
   449
wenzelm@69225
   450
type Output = (String, String)
wenzelm@69225
   451
wenzelm@69225
   452
no_output :: Output
wenzelm@69225
   453
no_output = ("", "")
wenzelm@69222
   454
\<close>
wenzelm@69222
   455
wenzelm@69226
   456
generate_haskell_file XML.hs = \<open>
wenzelm@69226
   457
{-  Title:      Tools/Haskell/XML.hs
wenzelm@69225
   458
    Author:     Makarius
wenzelm@69225
   459
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   460
wenzelm@69225
   461
Untyped XML trees and representation of ML values.
wenzelm@69225
   462
-}
wenzelm@69225
   463
wenzelm@69225
   464
module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of)
wenzelm@69225
   465
where
wenzelm@69225
   466
wenzelm@69225
   467
import qualified Data.List as List
wenzelm@69225
   468
wenzelm@69225
   469
import Isabelle.Library
wenzelm@69225
   470
import qualified Isabelle.Properties as Properties
wenzelm@69225
   471
import qualified Isabelle.Markup as Markup
wenzelm@69225
   472
import qualified Isabelle.Buffer as Buffer
wenzelm@69225
   473
wenzelm@69225
   474
wenzelm@69225
   475
{- types -}
wenzelm@69225
   476
wenzelm@69225
   477
type Attributes = Properties.T
wenzelm@69225
   478
type Body = [Tree]
wenzelm@69225
   479
data Tree = Elem Markup.T Body | Text String
wenzelm@69225
   480
wenzelm@69225
   481
wenzelm@69225
   482
{- wrapped elements -}
wenzelm@69225
   483
wenzelm@69236
   484
wrap_elem (((a, atts), body1), body2) =
wenzelm@69236
   485
  Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)
wenzelm@69225
   486
wenzelm@69236
   487
unwrap_elem
wenzelm@69236
   488
  (Elem (\<open>XML.xml_elemN\<close>, (\<open>XML.xml_nameN\<close>, a) : atts) (Elem (\<open>XML.xml_bodyN\<close>, []) body1 : body2)) =
wenzelm@69236
   489
  Just (((a, atts), body1), body2)
wenzelm@69225
   490
unwrap_elem _ = Nothing
wenzelm@69225
   491
wenzelm@69225
   492
wenzelm@69225
   493
{- text content -}
wenzelm@69225
   494
wenzelm@69225
   495
add_content tree =
wenzelm@69225
   496
  case unwrap_elem tree of
wenzelm@69225
   497
    Just (_, ts) -> fold add_content ts
wenzelm@69225
   498
    Nothing ->
wenzelm@69225
   499
      case tree of
wenzelm@69225
   500
        Elem _ ts -> fold add_content ts
wenzelm@69225
   501
        Text s -> Buffer.add s
wenzelm@69225
   502
wenzelm@69225
   503
content_of body = Buffer.empty |> fold add_content body |> Buffer.content
wenzelm@69225
   504
wenzelm@69225
   505
wenzelm@69225
   506
{- string representation -}
wenzelm@69225
   507
wenzelm@69225
   508
encode '<' = "&lt;"
wenzelm@69225
   509
encode '>' = "&gt;"
wenzelm@69225
   510
encode '&' = "&amp;"
wenzelm@69225
   511
encode '\'' = "&apos;"
wenzelm@69225
   512
encode '\"' = "&quot;"
wenzelm@69225
   513
encode c = [c]
wenzelm@69225
   514
wenzelm@69225
   515
instance Show Tree where
wenzelm@69225
   516
  show tree =
wenzelm@69225
   517
    Buffer.empty |> show_tree tree |> Buffer.content
wenzelm@69225
   518
    where
wenzelm@69225
   519
      show_tree (Elem (name, atts) []) =
wenzelm@69225
   520
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add "/>"
wenzelm@69225
   521
      show_tree (Elem (name, atts) ts) =
wenzelm@69225
   522
        Buffer.add "<" #> Buffer.add (show_elem name atts) #> Buffer.add ">" #>
wenzelm@69225
   523
        fold show_tree ts #>
wenzelm@69225
   524
        Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
wenzelm@69225
   525
      show_tree (Text s) = Buffer.add (show_text s)
wenzelm@69225
   526
wenzelm@69225
   527
      show_elem name atts =
wenzelm@69225
   528
        unwords (name : map (\(a, x) -> a ++ "=\"" ++ show_text x ++ "\"") atts)
wenzelm@69225
   529
wenzelm@69225
   530
      show_text = concatMap encode
wenzelm@69225
   531
\<close>
wenzelm@69225
   532
wenzelm@69226
   533
generate_haskell_file YXML.hs = \<open>
wenzelm@69226
   534
{-  Title:      Tools/Haskell/YXML.hs
wenzelm@69225
   535
    Author:     Makarius
wenzelm@69225
   536
    LICENSE:    BSD 3-clause (Isabelle)
wenzelm@69225
   537
wenzelm@69225
   538
Efficient text representation of XML trees.  Suitable for direct
wenzelm@69225
   539
inlining into plain text.
wenzelm@69225
   540
-}
wenzelm@69225
   541
wenzelm@69225
   542
module Isabelle.YXML (charX, charY, strX, strY, detect,
wenzelm@69225
   543
  buffer_body, buffer, string_of_body, string_of, parse_body, parse)
wenzelm@69225
   544
where
wenzelm@69225
   545
wenzelm@69225
   546
import qualified Data.Char as Char
wenzelm@69225
   547
import qualified Data.List as List
wenzelm@69222
   548
wenzelm@69225
   549
import Isabelle.Library
wenzelm@69225
   550
import qualified Isabelle.Markup as Markup
wenzelm@69225
   551
import qualified Isabelle.XML as XML
wenzelm@69225
   552
import qualified Isabelle.Buffer as Buffer
wenzelm@69225
   553
wenzelm@69225
   554
wenzelm@69225
   555
{- markers -}
wenzelm@69225
   556
wenzelm@69225
   557
charX, charY :: Char
wenzelm@69225
   558
charX = Char.chr 5
wenzelm@69225
   559
charY = Char.chr 6
wenzelm@69225
   560
wenzelm@69225
   561
strX, strY, strXY, strXYX :: String
wenzelm@69225
   562
strX = [charX]
wenzelm@69225
   563
strY = [charY]
wenzelm@69225
   564
strXY = strX ++ strY
wenzelm@69225
   565
strXYX = strXY ++ strX
wenzelm@69225
   566
wenzelm@69225
   567
detect :: String -> Bool
wenzelm@69225
   568
detect = any (\c -> c == charX || c == charY)
wenzelm@69225
   569
wenzelm@69225
   570
wenzelm@69225
   571
{- output -}
wenzelm@69225
   572
wenzelm@69225
   573
buffer_attrib (a, x) =
wenzelm@69225
   574
  Buffer.add strY #> Buffer.add a #> Buffer.add "=" #> Buffer.add x
wenzelm@69225
   575
wenzelm@69225
   576
buffer_body :: XML.Body -> Buffer.T -> Buffer.T
wenzelm@69225
   577
buffer_body = fold buffer
wenzelm@69225
   578
wenzelm@69225
   579
buffer :: XML.Tree -> Buffer.T -> Buffer.T
wenzelm@69225
   580
buffer (XML.Elem (name, atts) ts) =
wenzelm@69225
   581
  Buffer.add strXY #> Buffer.add name #> fold buffer_attrib atts #> Buffer.add strX #>
wenzelm@69225
   582
  buffer_body ts #>
wenzelm@69225
   583
  Buffer.add strXYX
wenzelm@69225
   584
buffer (XML.Text s) = Buffer.add s
wenzelm@69225
   585
wenzelm@69225
   586
string_of_body :: XML.Body -> String
wenzelm@69225
   587
string_of_body body = Buffer.empty |> buffer_body body |> Buffer.content
wenzelm@69225
   588
wenzelm@69225
   589
string_of :: XML.Tree -> String
wenzelm@69225
   590
string_of = string_of_body . single
wenzelm@69225
   591
wenzelm@69225
   592
wenzelm@69225
   593
{- parse -}
wenzelm@69225
   594
wenzelm@69225
   595
-- split: fields or non-empty tokens
wenzelm@69225
   596
wenzelm@69225
   597
split :: Bool -> Char -> String -> [String]
wenzelm@69225
   598
split _ _ [] = []
wenzelm@69225
   599
split fields sep str = splitting str
wenzelm@69225
   600
  where
wenzelm@69225
   601
    splitting rest =
wenzelm@69225
   602
      case span (/= sep) rest of
wenzelm@69225
   603
        (_, []) -> cons rest []
wenzelm@69225
   604
        (prfx, _ : rest') -> cons prfx (splitting rest')
wenzelm@69225
   605
    cons item = if fields || not (null item) then (:) item else id
wenzelm@69225
   606
wenzelm@69225
   607
wenzelm@69225
   608
-- structural errors
wenzelm@69225
   609
wenzelm@69225
   610
err msg = error ("Malformed YXML: " ++ msg)
wenzelm@69225
   611
err_attribute = err "bad attribute"
wenzelm@69225
   612
err_element = err "bad element"
wenzelm@69225
   613
err_unbalanced "" = err "unbalanced element"
wenzelm@69225
   614
err_unbalanced name = err ("unbalanced element " ++ quote name)
wenzelm@69225
   615
wenzelm@69225
   616
wenzelm@69225
   617
-- stack operations
wenzelm@69225
   618
wenzelm@69225
   619
add x ((elem, body) : pending) = (elem, x : body) : pending
wenzelm@69225
   620
wenzelm@69225
   621
push "" _ _ = err_element
wenzelm@69225
   622
push name atts pending = ((name, atts), []) : pending
wenzelm@69225
   623
wenzelm@69225
   624
pop ((("", _), _) : _) = err_unbalanced ""
wenzelm@69225
   625
pop ((markup, body) : pending) = add (XML.Elem markup (reverse body)) pending
wenzelm@69225
   626
wenzelm@69225
   627
wenzelm@69225
   628
-- parsing
wenzelm@69225
   629
wenzelm@69225
   630
parse_attrib s =
wenzelm@69225
   631
  case List.elemIndex '=' s of
wenzelm@69225
   632
    Just i | i > 0 -> (take i s, drop (i + 1) s)
wenzelm@69225
   633
    _ -> err_attribute
wenzelm@69225
   634
wenzelm@69225
   635
parse_chunk ["", ""] = pop
wenzelm@69225
   636
parse_chunk ("" : name : atts) = push name (map parse_attrib atts)
wenzelm@69225
   637
parse_chunk txts = fold (add . XML.Text) txts
wenzelm@69225
   638
wenzelm@69225
   639
parse_body :: String -> XML.Body
wenzelm@69225
   640
parse_body source =
wenzelm@69225
   641
  case fold parse_chunk chunks [(("", []), [])] of
wenzelm@69225
   642
    [(("", _), result)] -> reverse result
wenzelm@69225
   643
    ((name, _), _) : _ -> err_unbalanced name
wenzelm@69225
   644
  where chunks = split False charX source |> map (split True charY)
wenzelm@69225
   645
wenzelm@69225
   646
parse :: String -> XML.Tree
wenzelm@69225
   647
parse source =
wenzelm@69225
   648
  case parse_body source of
wenzelm@69225
   649
    [result] -> result
wenzelm@69225
   650
    [] -> XML.Text ""
wenzelm@69225
   651
    _ -> err "multiple results"
wenzelm@69222
   652
\<close>
wenzelm@69222
   653
wenzelm@69222
   654
end