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