# HG changeset patch # User wenzelm # Date 1310075715 -7200 # Node ID 91c4d7397f0ed6facf0bc3d4698bb49db0bf222c # Parent 77ce24aa1770fb21272324aa04b41bdd6b8fa930 simplified make_option/dest_option; added make_variant/dest_variant -- usual representation of datatypes; diff -r 77ce24aa1770 -r 91c4d7397f0e src/Pure/General/xml_data.ML --- a/src/Pure/General/xml_data.ML Thu Jul 07 22:04:30 2011 +0200 +++ b/src/Pure/General/xml_data.ML Thu Jul 07 23:55:15 2011 +0200 @@ -28,6 +28,8 @@ 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 + val make_variant: ('a -> XML.body) list -> 'a -> XML.body + val dest_variant: (XML.body -> 'a) list -> XML.body -> 'a end; structure XML_Data: XML_DATA = @@ -69,6 +71,11 @@ fun dest_node (XML.Elem ((":", []), ts)) = ts | dest_node t = raise XML_BODY [t]; +fun make_tagged (tag, ts) = XML.Elem ((make_int_atom tag, []), ts); + +fun dest_tagged (XML.Elem ((s, []), ts)) = (dest_int_atom s, ts) + | dest_tagged t = raise XML_BODY [t]; + (* representation of standard types *) @@ -115,14 +122,21 @@ 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 make_option _ NONE = [] + | make_option make (SOME x) = [make_node (make x)]; + +fun dest_option _ [] = NONE + | dest_option dest [t] = SOME (dest (dest_node t)) + | dest_option _ ts = raise XML_BODY ts; + -fun dest_option dest ts = - (case dest_list dest ts of - [] => NONE - | [x] => SOME x - | _ => raise XML_BODY ts); +fun make_variant makes x = + [make_tagged (the (get_index (fn make => try make x) makes))]; + +fun dest_variant dests [t] = + let val (tag, ts) = dest_tagged t + in nth dests tag ts end + | dest_variant _ ts = raise XML_BODY ts; end; diff -r 77ce24aa1770 -r 91c4d7397f0e src/Pure/General/xml_data.scala --- a/src/Pure/General/xml_data.scala Thu Jul 07 22:04:30 2011 +0200 +++ b/src/Pure/General/xml_data.scala Thu Jul 07 23:55:15 2011 +0200 @@ -55,6 +55,15 @@ case _ => throw new XML_Body(List(t)) } + private def make_tagged(tag: Int, ts: XML.Body): XML.Tree = + XML.Elem(Markup(make_int_atom(tag), Nil), ts) + + private def dest_tagged(t: XML.Tree): (Int, XML.Body) = + t match { + case XML.Elem(Markup(s, Nil), ts) => (dest_int_atom(s), ts) + case _ => throw new XML_Body(List(t)) + } + /* representation of standard types */ @@ -122,14 +131,29 @@ def make_option[A](make: A => XML.Body)(opt: Option[A]): XML.Body = opt match { - case None => make_list(make)(Nil) - case Some(x) => make_list(make)(List(x)) + case None => Nil + case Some(x) => List(make_node(make(x))) } def dest_option[A](dest: XML.Body => A)(ts: XML.Body): Option[A] = - dest_list(dest)(ts) match { + ts match { case Nil => None - case List(x) => Some(x) + case List(t) => Some(dest(dest_node(t))) + case _ => throw new XML_Body(ts) + } + + + def make_variant[A](makes: List[PartialFunction[A, XML.Body]])(x: A): XML.Body = + { + val (make, tag) = makes.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get + List(make_tagged(tag, make(x))) + } + + def dest_variant[A](dests: List[XML.Body => A])(ts: XML.Body): A = + ts match { + case List(t) => + val (tag, ts) = dest_tagged(t) + dests(tag)(ts) case _ => throw new XML_Body(ts) } }