XML data representation of lambda terms;

--- a/src/Pure/IsaMakefile	Sun Jul 10 16:31:04 2011 +0200
+++ b/src/Pure/IsaMakefile	Sun Jul 10 16:34:17 2011 +0200
@@ -250,6 +250,7 @@
   term.ML						\
   term_ord.ML						\
   term_subst.ML						\
+  term_xml.ML						\
   theory.ML						\
   thm.ML						\
   type.ML						\

--- a/src/Pure/ROOT.ML	Sun Jul 10 16:31:04 2011 +0200
+++ b/src/Pure/ROOT.ML	Sun Jul 10 16:34:17 2011 +0200
@@ -127,6 +127,7 @@
 
 use "term_ord.ML";
 use "term_subst.ML";
+use "term_xml.ML";
 use "old_term.ML";
 use "General/name_space.ML";
 use "sorts.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_xml.ML	Sun Jul 10 16:34:17 2011 +0200
@@ -0,0 +1,79 @@
+(*  Title:      Pure/term_xml.ML
+    Author:     Makarius
+
+XML data representation of lambda terms.
+*)
+
+signature TERM_XML_OPS =
+sig
+  type 'a T
+  val indexname: indexname T
+  val class: class T
+  val sort: sort T
+  val typ: typ T
+  val term: term T
+end
+
+signature TERM_XML =
+sig
+  structure Make: TERM_XML_OPS where type 'a T = 'a XML_Data.Make.T
+  structure Dest: TERM_XML_OPS where type 'a T = 'a XML_Data.Dest.T
+end;
+
+structure Term_XML: TERM_XML =
+struct
+
+(* make *)
+
+structure Make =
+struct
+
+open XML_Data.Make;
+
+val indexname = pair string int;
+val class = string;
+val sort = list class;
+
+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];
+
+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];
+
+end;
+
+
+(* dest *)
+
+structure Dest =
+struct
+
+open XML_Data.Dest;
+
+val indexname = pair string int;
+val class = string;
+val sort = list class;
+
+fun typ T = T |> variant
+ [Type o pair string (list typ),
+  TFree o pair string sort,
+  TVar o pair indexname sort];
+
+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];
+
+end;
+
+end;