src/Pure/General/xml_data.ML
author wenzelm
Tue Aug 10 22:26:23 2010 +0200 (2010-08-10)
changeset 38266 492d377ecfe2
child 38267 e50c283dd125
permissions -rw-r--r--
type XML.body as basic data representation language;
tuned;
wenzelm@38266
     1
(*  Title:      Pure/General/xml_data.ML
wenzelm@38266
     2
    Author:     Makarius
wenzelm@38266
     3
wenzelm@38266
     4
XML as basic data representation language.
wenzelm@38266
     5
*)
wenzelm@38266
     6
wenzelm@38266
     7
signature XML_DATA =
wenzelm@38266
     8
sig
wenzelm@38266
     9
  exception XML_ATOM of string
wenzelm@38266
    10
  exception XML_BODY of XML.body
wenzelm@38266
    11
  val make_properties: Properties.T -> XML.body
wenzelm@38266
    12
  val dest_properties: XML.body -> Properties.T
wenzelm@38266
    13
  val make_string: string -> XML.body
wenzelm@38266
    14
  val dest_string : XML.body -> string
wenzelm@38266
    15
  val make_int: int -> XML.body
wenzelm@38266
    16
  val dest_int : XML.body -> int
wenzelm@38266
    17
  val make_bool: bool -> XML.body
wenzelm@38266
    18
  val dest_bool: XML.body -> bool
wenzelm@38266
    19
  val make_unit: unit -> XML.body
wenzelm@38266
    20
  val dest_unit: XML.body -> unit
wenzelm@38266
    21
  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
wenzelm@38266
    22
  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
wenzelm@38266
    23
  val make_triple:
wenzelm@38266
    24
    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
wenzelm@38266
    25
  val dest_triple:
wenzelm@38266
    26
    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
wenzelm@38266
    27
  val make_list: ('a -> XML.body) -> 'a list -> XML.body
wenzelm@38266
    28
  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
wenzelm@38266
    29
  val make_option: ('a -> XML.body) -> 'a option -> XML.body
wenzelm@38266
    30
  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
wenzelm@38266
    31
end;
wenzelm@38266
    32
wenzelm@38266
    33
structure XML_Data: XML_DATA =
wenzelm@38266
    34
struct
wenzelm@38266
    35
wenzelm@38266
    36
(* basic values *)
wenzelm@38266
    37
wenzelm@38266
    38
exception XML_ATOM of string;
wenzelm@38266
    39
wenzelm@38266
    40
wenzelm@38266
    41
fun make_int_atom i = signed_string_of_int i;
wenzelm@38266
    42
wenzelm@38266
    43
fun dest_int_atom s =
wenzelm@38266
    44
  (case Int.fromString s of
wenzelm@38266
    45
    SOME i => i
wenzelm@38266
    46
  | NONE => raise XML_ATOM s);
wenzelm@38266
    47
wenzelm@38266
    48
wenzelm@38266
    49
fun make_bool_atom false = "0"
wenzelm@38266
    50
  | make_bool_atom true = "1";
wenzelm@38266
    51
wenzelm@38266
    52
fun dest_bool_atom "0" = false
wenzelm@38266
    53
  | dest_bool_atom "1" = true
wenzelm@38266
    54
  | dest_bool_atom s = raise XML_ATOM s;
wenzelm@38266
    55
wenzelm@38266
    56
fun make_unit_atom () = "";
wenzelm@38266
    57
wenzelm@38266
    58
fun dest_unit_atom "" = ()
wenzelm@38266
    59
  | dest_unit_atom s = raise XML_ATOM s;
wenzelm@38266
    60
wenzelm@38266
    61
wenzelm@38266
    62
(* structural nodes *)
wenzelm@38266
    63
wenzelm@38266
    64
exception XML_BODY of XML.tree list;
wenzelm@38266
    65
wenzelm@38266
    66
fun make_node ts = XML.Elem ((":", []), ts);
wenzelm@38266
    67
wenzelm@38266
    68
fun dest_node (XML.Elem ((":", []), ts)) = ts
wenzelm@38266
    69
  | dest_node t = raise XML_BODY [t];
wenzelm@38266
    70
wenzelm@38266
    71
wenzelm@38266
    72
(* representation of standard types *)
wenzelm@38266
    73
wenzelm@38266
    74
fun make_properties props = [XML.Elem ((":", props), [])];
wenzelm@38266
    75
wenzelm@38266
    76
fun dest_properties [XML.Elem ((":", props), [])] = props
wenzelm@38266
    77
  | dest_properties ts = raise XML_BODY ts;
wenzelm@38266
    78
wenzelm@38266
    79
wenzelm@38266
    80
fun make_string s = [XML.Text s];
wenzelm@38266
    81
wenzelm@38266
    82
fun dest_string [XML.Text s] = s
wenzelm@38266
    83
  | dest_string ts = raise XML_BODY ts;
wenzelm@38266
    84
wenzelm@38266
    85
wenzelm@38266
    86
val make_int = make_string o make_int_atom;
wenzelm@38266
    87
val dest_int = dest_int_atom o dest_string;
wenzelm@38266
    88
wenzelm@38266
    89
val make_bool = make_string o make_bool_atom;
wenzelm@38266
    90
val dest_bool = dest_bool_atom o dest_string;
wenzelm@38266
    91
wenzelm@38266
    92
val make_unit = make_string o make_unit_atom;
wenzelm@38266
    93
val dest_unit = dest_unit_atom o dest_string;
wenzelm@38266
    94
wenzelm@38266
    95
wenzelm@38266
    96
fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
wenzelm@38266
    97
wenzelm@38266
    98
fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
wenzelm@38266
    99
  | dest_pair _ _ ts = raise XML_BODY ts;
wenzelm@38266
   100
wenzelm@38266
   101
wenzelm@38266
   102
fun make_triple make1 make2 make3 (x, y, z) =
wenzelm@38266
   103
  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
wenzelm@38266
   104
wenzelm@38266
   105
fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
wenzelm@38266
   106
      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
wenzelm@38266
   107
  | dest_triple _ _ _ ts = raise XML_BODY ts;
wenzelm@38266
   108
wenzelm@38266
   109
wenzelm@38266
   110
fun make_list make xs = map (make_node o make) xs;
wenzelm@38266
   111
wenzelm@38266
   112
fun dest_list dest ts = map (dest o dest_node) ts;
wenzelm@38266
   113
wenzelm@38266
   114
wenzelm@38266
   115
fun make_option make NONE = make_list make []
wenzelm@38266
   116
  | make_option make (SOME x) = make_list make [x];
wenzelm@38266
   117
wenzelm@38266
   118
fun dest_option dest ts =
wenzelm@38266
   119
  (case dest_list dest ts of
wenzelm@38266
   120
    [] => NONE
wenzelm@38266
   121
  | [x] => SOME x
wenzelm@38266
   122
  | _ => raise XML_BODY ts);
wenzelm@38266
   123
wenzelm@38266
   124
end;
wenzelm@38266
   125