--- a/src/Pure/term.scala Sun Jul 10 17:58:11 2011 +0200
+++ b/src/Pure/term.scala Sun Jul 10 20:59:04 2011 +0200
@@ -31,58 +31,61 @@
case class Bound(index: Int) extends Term
case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
case class App(fun: Term, arg: Term) extends Term
+}
+
+
+object Term_XML
+{
+ import Term._
/* XML data representation */
- object XML
+ object Encode
{
- object Make
- {
- import XML_Data.Make._
+ import XML_Data.Encode._
- val indexname: T[Indexname] = pair(string, int)
+ val indexname: T[Indexname] = pair(string, int)
- val sort: T[Sort] = list(string)
+ 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)) }))
+ 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)) }))
- 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)) }))
- }
+ 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)) }))
+ }
- object Dest
- {
- import XML_Data.Dest._
+ object Decode
+ {
+ import XML_Data.Decode._
- val indexname: T[Indexname] = pair(string, int)
+ val indexname: T[Indexname] = pair(string, int)
- val sort: T[Sort] = list(string)
+ 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) })))
+ 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) })))
- 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) })))
- }
+ 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) })))
}
}