src/Pure/General/xml_data.ML
changeset 38266 492d377ecfe2
child 38267 e50c283dd125
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/xml_data.ML	Tue Aug 10 22:26:23 2010 +0200
     1.3 @@ -0,0 +1,125 @@
     1.4 +(*  Title:      Pure/General/xml_data.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +XML as basic data representation language.
     1.8 +*)
     1.9 +
    1.10 +signature XML_DATA =
    1.11 +sig
    1.12 +  exception XML_ATOM of string
    1.13 +  exception XML_BODY of XML.body
    1.14 +  val make_properties: Properties.T -> XML.body
    1.15 +  val dest_properties: XML.body -> Properties.T
    1.16 +  val make_string: string -> XML.body
    1.17 +  val dest_string : XML.body -> string
    1.18 +  val make_int: int -> XML.body
    1.19 +  val dest_int : XML.body -> int
    1.20 +  val make_bool: bool -> XML.body
    1.21 +  val dest_bool: XML.body -> bool
    1.22 +  val make_unit: unit -> XML.body
    1.23 +  val dest_unit: XML.body -> unit
    1.24 +  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
    1.25 +  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
    1.26 +  val make_triple:
    1.27 +    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
    1.28 +  val dest_triple:
    1.29 +    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
    1.30 +  val make_list: ('a -> XML.body) -> 'a list -> XML.body
    1.31 +  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
    1.32 +  val make_option: ('a -> XML.body) -> 'a option -> XML.body
    1.33 +  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
    1.34 +end;
    1.35 +
    1.36 +structure XML_Data: XML_DATA =
    1.37 +struct
    1.38 +
    1.39 +(* basic values *)
    1.40 +
    1.41 +exception XML_ATOM of string;
    1.42 +
    1.43 +
    1.44 +fun make_int_atom i = signed_string_of_int i;
    1.45 +
    1.46 +fun dest_int_atom s =
    1.47 +  (case Int.fromString s of
    1.48 +    SOME i => i
    1.49 +  | NONE => raise XML_ATOM s);
    1.50 +
    1.51 +
    1.52 +fun make_bool_atom false = "0"
    1.53 +  | make_bool_atom true = "1";
    1.54 +
    1.55 +fun dest_bool_atom "0" = false
    1.56 +  | dest_bool_atom "1" = true
    1.57 +  | dest_bool_atom s = raise XML_ATOM s;
    1.58 +
    1.59 +fun make_unit_atom () = "";
    1.60 +
    1.61 +fun dest_unit_atom "" = ()
    1.62 +  | dest_unit_atom s = raise XML_ATOM s;
    1.63 +
    1.64 +
    1.65 +(* structural nodes *)
    1.66 +
    1.67 +exception XML_BODY of XML.tree list;
    1.68 +
    1.69 +fun make_node ts = XML.Elem ((":", []), ts);
    1.70 +
    1.71 +fun dest_node (XML.Elem ((":", []), ts)) = ts
    1.72 +  | dest_node t = raise XML_BODY [t];
    1.73 +
    1.74 +
    1.75 +(* representation of standard types *)
    1.76 +
    1.77 +fun make_properties props = [XML.Elem ((":", props), [])];
    1.78 +
    1.79 +fun dest_properties [XML.Elem ((":", props), [])] = props
    1.80 +  | dest_properties ts = raise XML_BODY ts;
    1.81 +
    1.82 +
    1.83 +fun make_string s = [XML.Text s];
    1.84 +
    1.85 +fun dest_string [XML.Text s] = s
    1.86 +  | dest_string ts = raise XML_BODY ts;
    1.87 +
    1.88 +
    1.89 +val make_int = make_string o make_int_atom;
    1.90 +val dest_int = dest_int_atom o dest_string;
    1.91 +
    1.92 +val make_bool = make_string o make_bool_atom;
    1.93 +val dest_bool = dest_bool_atom o dest_string;
    1.94 +
    1.95 +val make_unit = make_string o make_unit_atom;
    1.96 +val dest_unit = dest_unit_atom o dest_string;
    1.97 +
    1.98 +
    1.99 +fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
   1.100 +
   1.101 +fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
   1.102 +  | dest_pair _ _ ts = raise XML_BODY ts;
   1.103 +
   1.104 +
   1.105 +fun make_triple make1 make2 make3 (x, y, z) =
   1.106 +  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
   1.107 +
   1.108 +fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
   1.109 +      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
   1.110 +  | dest_triple _ _ _ ts = raise XML_BODY ts;
   1.111 +
   1.112 +
   1.113 +fun make_list make xs = map (make_node o make) xs;
   1.114 +
   1.115 +fun dest_list dest ts = map (dest o dest_node) ts;
   1.116 +
   1.117 +
   1.118 +fun make_option make NONE = make_list make []
   1.119 +  | make_option make (SOME x) = make_list make [x];
   1.120 +
   1.121 +fun dest_option dest ts =
   1.122 +  (case dest_list dest ts of
   1.123 +    [] => NONE
   1.124 +  | [x] => SOME x
   1.125 +  | _ => raise XML_BODY ts);
   1.126 +
   1.127 +end;
   1.128 +