src/Pure/term_xml.ML

XML data representation of lambda terms;

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