(*  Title:      Pure/General/xml_data.ML

    Author:     Makarius

XML as basic data representation language.

*)

signature XML_DATA =

sig

  exception XML_ATOM of string

  exception XML_BODY of XML.body

  val make_properties: Properties.T -> XML.body

  val dest_properties: XML.body -> Properties.T

  val make_string: string -> XML.body

  val dest_string : XML.body -> string

  val make_int: int -> XML.body

  val dest_int : XML.body -> int

  val make_bool: bool -> XML.body

  val dest_bool: XML.body -> bool

  val make_unit: unit -> XML.body

  val dest_unit: XML.body -> unit

  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body

  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b

  val make_triple:

    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body

  val dest_triple:

    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c

  val make_list: ('a -> XML.body) -> 'a list -> XML.body

  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list

  val make_option: ('a -> XML.body) -> 'a option -> XML.body

  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option

end;

structure XML_Data: XML_DATA =

struct

(* basic values *)

exception XML_ATOM of string;

fun make_int_atom i = signed_string_of_int i;

fun dest_int_atom s =

  (case Int.fromString s of

    SOME i => i

  | NONE => raise XML_ATOM s);

fun make_bool_atom false = "0"

  | make_bool_atom true = "1";

fun dest_bool_atom "0" = false

  | dest_bool_atom "1" = true

  | dest_bool_atom s = raise XML_ATOM s;

fun make_unit_atom () = "";

fun dest_unit_atom "" = ()

  | dest_unit_atom s = raise XML_ATOM s;

(* structural nodes *)

exception XML_BODY of XML.tree list;

fun make_node ts = XML.Elem ((":", []), ts);

fun dest_node (XML.Elem ((":", []), ts)) = ts

  | dest_node t = raise XML_BODY [t];

(* representation of standard types *)

fun make_properties props = [XML.Elem ((":", props), [])];

fun dest_properties [XML.Elem ((":", props), [])] = props

  | dest_properties ts = raise XML_BODY ts;

fun make_string s = [XML.Text s];

fun dest_string [XML.Text s] = s

  | dest_string ts = raise XML_BODY ts;

val make_int = make_string o make_int_atom;

val dest_int = dest_int_atom o dest_string;

val make_bool = make_string o make_bool_atom;

val dest_bool = dest_bool_atom o dest_string;

val make_unit = make_string o make_unit_atom;

val dest_unit = dest_unit_atom o dest_string;

fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];

fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))

  | dest_pair _ _ ts = raise XML_BODY ts;

fun make_triple make1 make2 make3 (x, y, z) =

  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];

fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =

      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))

  | dest_triple _ _ _ ts = raise XML_BODY ts;

fun make_list make xs = map (make_node o make) xs;

fun dest_list dest ts = map (dest o dest_node) ts;

fun make_option make NONE = make_list make []

  | make_option make (SOME x) = make_list make [x];

fun dest_option dest ts =

  (case dest_list dest ts of

    [] => NONE

  | [x] => SOME x

  | _ => raise XML_BODY ts);

end;