29 case class Free(name: String, typ: Typ = dummyT) extends Term |
29 case class Free(name: String, typ: Typ = dummyT) extends Term |
30 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
30 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
31 case class Bound(index: Int) extends Term |
31 case class Bound(index: Int) extends Term |
32 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
32 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
33 case class App(fun: Term, arg: Term) extends Term |
33 case class App(fun: Term, arg: Term) extends Term |
|
34 } |
|
35 |
|
36 |
|
37 object Term_XML |
|
38 { |
|
39 import Term._ |
34 |
40 |
35 |
41 |
36 /* XML data representation */ |
42 /* XML data representation */ |
37 |
43 |
38 object XML |
44 object Encode |
39 { |
45 { |
40 object Make |
46 import XML_Data.Encode._ |
41 { |
|
42 import XML_Data.Make._ |
|
43 |
47 |
44 val indexname: T[Indexname] = pair(string, int) |
48 val indexname: T[Indexname] = pair(string, int) |
45 |
49 |
46 val sort: T[Sort] = list(string) |
50 val sort: T[Sort] = list(string) |
47 |
51 |
48 def typ: T[Typ] = |
52 def typ: T[Typ] = |
49 variant[Typ](List( |
53 variant[Typ](List( |
50 { case Type(a, b) => pair(string, list(typ))((a, b)) }, |
54 { case Type(a, b) => pair(string, list(typ))((a, b)) }, |
51 { case TFree(a, b) => pair(string, sort)((a, b)) }, |
55 { case TFree(a, b) => pair(string, sort)((a, b)) }, |
52 { case TVar(a, b) => pair(indexname, sort)((a, b)) })) |
56 { case TVar(a, b) => pair(indexname, sort)((a, b)) })) |
53 |
57 |
54 def term: T[Term] = |
58 def term: T[Term] = |
55 variant[Term](List( |
59 variant[Term](List( |
56 { case Const(a, b) => pair(string, typ)((a, b)) }, |
60 { case Const(a, b) => pair(string, typ)((a, b)) }, |
57 { case Free(a, b) => pair(string, typ)((a, b)) }, |
61 { case Free(a, b) => pair(string, typ)((a, b)) }, |
58 { case Var(a, b) => pair(indexname, typ)((a, b)) }, |
62 { case Var(a, b) => pair(indexname, typ)((a, b)) }, |
59 { case Bound(a) => int(a) }, |
63 { case Bound(a) => int(a) }, |
60 { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) }, |
64 { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) }, |
61 { case App(a, b) => pair(term, term)((a, b)) })) |
65 { case App(a, b) => pair(term, term)((a, b)) })) |
62 } |
66 } |
63 |
67 |
64 object Dest |
68 object Decode |
65 { |
69 { |
66 import XML_Data.Dest._ |
70 import XML_Data.Decode._ |
67 |
71 |
68 val indexname: T[Indexname] = pair(string, int) |
72 val indexname: T[Indexname] = pair(string, int) |
69 |
73 |
70 val sort: T[Sort] = list(string) |
74 val sort: T[Sort] = list(string) |
71 |
75 |
72 def typ: T[Typ] = |
76 def typ: T[Typ] = |
73 variant[Typ](List( |
77 variant[Typ](List( |
74 (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }), |
78 (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }), |
75 (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }), |
79 (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }), |
76 (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) }))) |
80 (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) }))) |
77 |
81 |
78 def term: T[Term] = |
82 def term: T[Term] = |
79 variant[Term](List( |
83 variant[Term](List( |
80 (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }), |
84 (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }), |
81 (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }), |
85 (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }), |
82 (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }), |
86 (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }), |
83 (x => Bound(int(x))), |
87 (x => Bound(int(x))), |
84 (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }), |
88 (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }), |
85 (x => { val (a, b) = pair(term, term)(x); App(a, b) }))) |
89 (x => { val (a, b) = pair(term, term)(x); App(a, b) }))) |
86 } |
|
87 } |
90 } |
88 } |
91 } |