# HG changeset patch
# User wenzelm
# Date 1310485986 -7200
# Node ID ce91894504473b6c6a492f4518e978127281c395
# Parent  22c87ff1b8a9601ac12209a874de7037003cf16e
more compact representation of XML data (notably sort/typ/term), using properties as vector of atomic values;

diff -r 22c87ff1b8a9 -r ce9189450447 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Tue Jul 12 15:32:16 2011 +0200
+++ b/src/Pure/General/xml.ML	Tue Jul 12 17:53:06 2011 +0200
@@ -1,12 +1,17 @@
 (*  Title:      Pure/General/xml.ML
     Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
 
-Simple XML tree values.
+Untyped XML trees.
 *)
 
 signature XML_DATA_OPS =
 sig
+  type 'a A
   type 'a T
+  type 'a V
+  val int_atom: int A
+  val bool_atom: bool A
+  val unit_atom: unit A
   val properties: Properties.T T
   val string: string T
   val int: int T
@@ -16,7 +21,7 @@
   val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   val list: 'a T -> 'a list T
   val option: 'a T -> 'a option T
-  val variant: 'a T list -> 'a T
+  val variant: 'a V list -> 'a T
 end;
 
 signature XML =
@@ -41,8 +46,8 @@
   val parse: string -> tree
   exception XML_ATOM of string
   exception XML_BODY of body
-  structure Encode: XML_DATA_OPS where type 'a T = 'a -> body
-  structure Decode: XML_DATA_OPS where type 'a T = body -> 'a
+  structure Encode: XML_DATA_OPS
+  structure Decode: XML_DATA_OPS
 end;
 
 structure XML: XML =
@@ -220,10 +225,12 @@
 structure Encode =
 struct
 
+type 'a A = 'a -> string;
 type 'a T = 'a -> body;
+type 'a V = 'a -> string list * body;
 
 
-(* basic values *)
+(* atomic values *)
 
 fun int_atom i = signed_string_of_int i;
 
@@ -237,7 +244,9 @@
 
 fun node ts = Elem ((":", []), ts);
 
-fun tagged (tag, ts) = Elem ((int_atom tag, []), ts);
+fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
+
+fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
 
 
 (* representation of standard types *)
@@ -270,10 +279,12 @@
 structure Decode =
 struct
 
+type 'a A = string -> 'a;
 type 'a T = body -> 'a;
+type 'a V = string list * body -> 'a;
 
 
-(* basic values *)
+(* atomic values *)
 
 fun int_atom s =
   (case Int.fromString s of
@@ -293,7 +304,10 @@
 fun node (Elem ((":", []), ts)) = ts
   | node t = raise XML_BODY [t];
 
-fun tagged (Elem ((s, []), ts)) = (int_atom s, ts)
+val vector =
+  fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a);
+
+fun tagged (Elem ((name, props), ts)) = (int_atom name, (#1 (vector props 0), ts))
   | tagged t = raise XML_BODY [t];
 
 
@@ -326,9 +340,9 @@
 
 fun variant fs [t] =
       let
-        val (tag, ts) = tagged t;
+        val (tag, (xs, ts)) = tagged t;
         val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
-      in f ts end
+      in f (xs, ts) end
   | variant _ ts = raise XML_BODY ts;
 
 end;
diff -r 22c87ff1b8a9 -r ce9189450447 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Tue Jul 12 15:32:16 2011 +0200
+++ b/src/Pure/General/xml.scala	Tue Jul 12 17:53:06 2011 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/General/xml.scala
     Author:     Makarius
 
-Simple XML tree values.
+Untyped XML trees.
 */
 
 package isabelle
@@ -12,6 +12,7 @@
 import javax.xml.parsers.DocumentBuilderFactory
 
 import scala.actors.Actor._
+import scala.collection.mutable
 
 
 object XML
@@ -216,23 +217,26 @@
     type T[A] = A => XML.Body
 
 
-    /* basic values */
+    /* atomic values */
 
-    private def long_atom(i: Long): String = i.toString
+    def long_atom(i: Long): String = i.toString
 
-    private def int_atom(i: Int): String = i.toString
+    def int_atom(i: Int): String = i.toString
 
-    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
+    def bool_atom(b: Boolean): String = if (b) "1" else "0"
 
-    private def unit_atom(u: Unit) = ""
+    def unit_atom(u: Unit) = ""
 
 
     /* structural nodes */
 
     private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
 
-    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
-      XML.Elem(Markup(int_atom(tag), Nil), ts)
+    private def vector(xs: List[String]): List[(String, String)] =
+      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
+
+    private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
+      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
 
 
     /* representation of standard types */
@@ -265,7 +269,7 @@
       case Some(x) => List(node(f(x)))
     }
 
-    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
+    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
     {
       case x =>
         val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
@@ -276,24 +280,25 @@
   object Decode
   {
     type T[A] = XML.Body => A
+    type V[A] = (List[String], XML.Body) => A
 
 
-     /* basic values */
+    /* atomic values */
 
-    private def long_atom(s: String): Long =
+    def long_atom(s: String): Long =
       try { java.lang.Long.parseLong(s) }
       catch { case e: NumberFormatException => throw new XML_Atom(s) }
 
-    private def int_atom(s: String): Int =
+    def int_atom(s: String): Int =
       try { Integer.parseInt(s) }
       catch { case e: NumberFormatException => throw new XML_Atom(s) }
 
-    private def bool_atom(s: String): Boolean =
+    def bool_atom(s: String): Boolean =
       if (s == "1") true
       else if (s == "0") false
       else throw new XML_Atom(s)
 
-    private def unit_atom(s: String): Unit =
+    def unit_atom(s: String): Unit =
       if (s == "") () else throw new XML_Atom(s)
 
 
@@ -305,9 +310,20 @@
         case _ => throw new XML_Body(List(t))
       }
 
-    private def tagged(t: XML.Tree): (Int, XML.Body) =
+    private def vector(props: List[(String, String)]): List[String] =
+    {
+      val xs = new mutable.ListBuffer[String]
+      var i = 0
+      for ((a, x) <- props) {
+        if (int_atom(a) == i) { xs += x; i = i + 1 }
+        else throw new XML_Atom(a)
+      }
+      xs.toList
+    }
+
+    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
       t match {
-        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
+        case XML.Elem(Markup(name, props), ts) => (int_atom(name), (vector(props), ts))
         case _ => throw new XML_Body(List(t))
       }
 
@@ -357,14 +373,14 @@
       case ts => throw new XML_Body(ts)
     }
 
-    def variant[A](fs: List[T[A]]): T[A] =
+    def variant[A](fs: List[V[A]]): T[A] =
     {
       case List(t) =>
-        val (tag, ts) = tagged(t)
+        val (tag, (xs, ts)) = tagged(t)
         val f =
           try { fs(tag) }
           catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
-        f(ts)
+        f(xs, ts)
       case ts => throw new XML_Body(ts)
     }
   }
diff -r 22c87ff1b8a9 -r ce9189450447 src/Pure/term.scala
--- a/src/Pure/term.scala	Tue Jul 12 15:32:16 2011 +0200
+++ b/src/Pure/term.scala	Tue Jul 12 17:53:06 2011 +0200
@@ -45,47 +45,43 @@
   {
     import XML.Encode._
 
-    val indexname: T[Indexname] = pair(string, int)
-
     val sort: T[Sort] = list(string)
 
     def typ: T[Typ] =
       variant[Typ](List(
-        { case Type(a, b) => pair(string, list(typ))((a, b)) },
-        { case TFree(a, b) => pair(string, sort)((a, b)) },
-        { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
+        { case Type(a, b) => (List(a), list(typ)(b)) },
+        { case TFree(a, b) => (List(a), sort(b)) },
+        { case TVar((a, b), c) => (List(a, int_atom(b)), sort(c)) }))
 
     def term: T[Term] =
       variant[Term](List(
-        { case Const(a, b) => pair(string, typ)((a, b)) },
-        { case Free(a, b) => pair(string, typ)((a, b)) },
-        { case Var(a, b) => pair(indexname, typ)((a, b)) },
-        { case Bound(a) => int(a) },
-        { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
-        { case App(a, b) => pair(term, term)((a, b)) }))
+        { case Const(a, b) => (List(a), typ(b)) },
+        { case Free(a, b) => (List(a), typ(b)) },
+        { case Var((a, b), c) => (List(a, int_atom(b)), typ(c)) },
+        { case Bound(a) => (List(int_atom(a)), Nil) },
+        { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
+        { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
   }
 
   object Decode
   {
     import XML.Decode._
 
-    val indexname: T[Indexname] = pair(string, int)
-
     val sort: T[Sort] = list(string)
 
     def typ: T[Typ] =
       variant[Typ](List(
-        (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
-        (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
-        (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
+        { case (List(a), b) => Type(a, list(typ)(b)) },
+        { case (List(a), b) => TFree(a, sort(b)) },
+        { case (List(a, b), c) => TVar((a, int_atom(b)), sort(c)) }))
 
     def term: T[Term] =
       variant[Term](List(
-        (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
-        (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
-        (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
-        (x => Bound(int(x))),
-        (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
-        (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
+        { case (List(a), b) => Const(a, typ(b)) },
+        { case (List(a), b) => Free(a, typ(b)) },
+        { case (List(a, b), c) => Var((a, int_atom(b)), typ(c)) },
+        { case (List(a), Nil) => Bound(int_atom(a)) },
+        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
+        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
   }
 }
diff -r 22c87ff1b8a9 -r ce9189450447 src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Tue Jul 12 15:32:16 2011 +0200
+++ b/src/Pure/term_xml.ML	Tue Jul 12 17:53:06 2011 +0200
@@ -7,7 +7,6 @@
 signature TERM_XML_OPS =
 sig
   type 'a T
-  val indexname: indexname T
   val sort: sort T
   val typ: typ T
   val term: term T
@@ -29,22 +28,20 @@
 
 open XML.Encode;
 
-val indexname = pair string int;
-
 val sort = list string;
 
 fun typ T = T |> variant
- [fn Type x => pair string (list typ) x,
-  fn TFree x => pair string sort x,
-  fn TVar x => pair indexname sort x];
+ [fn Type (a, b) => ([a], (list typ) b),
+  fn TFree (a, b) => ([a], sort b),
+  fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
 
 fun term t = t |> variant
- [fn Const x => pair string typ x,
-  fn Free x => pair string typ x,
-  fn Var x => pair indexname typ x,
-  fn Bound x => int x,
-  fn Abs x => triple string typ term x,
-  fn op $ x => pair term term x];
+ [fn Const (a, b) => ([a], typ b),
+  fn Free (a, b) => ([a], typ b),
+  fn Var ((a, b), c) => ([a, int_atom b], typ c),
+  fn Bound a => ([int_atom a], []),
+  fn Abs (a, b, c) => ([a], pair typ term (b, c)),
+  fn a $ b => ([], pair term term (a, b))];
 
 end;
 
@@ -56,22 +53,20 @@
 
 open XML.Decode;
 
-val indexname = pair string int;
-
 val sort = list string;
 
 fun typ T = T |> variant
- [Type o pair string (list typ),
-  TFree o pair string sort,
-  TVar o pair indexname sort];
+ [fn ([a], b) => Type (a, list typ b),
+  fn ([a], b) => TFree (a, sort b),
+  fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
 
 fun term t = t |> variant
- [Const o pair string typ,
-  Free o pair string typ,
-  Var o pair indexname typ,
-  Bound o int,
-  Abs o triple string typ term,
-  op $ o pair term term];
+ [fn ([a], b) => Const (a, typ b),
+  fn ([a], b) => Free (a, typ b),
+  fn ([a, b], c) => Var ((a, int_atom b), typ c),
+  fn ([a], []) => Bound (int_atom a),
+  fn ([a], b) => let val (c, d) = pair typ term b in Abs (a, c, d) end,
+  fn ([], a) => op $ (pair term term a)];
 
 end;