src/Pure/term_xml.ML

+(*  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;