1/*  Title:      Pure/term_xml.scala
2    Author:     Makarius
3
4XML data representation of lambda terms.
5*/
6
7package isabelle
8
9
10object Term_XML
11{
12  import Term._
13
14  object Encode
15  {
16    import XML.Encode._
17
18    val indexname: P[Indexname] =
19      { case Indexname(a, 0) => List(a)
20        case Indexname(a, b) => List(a, int_atom(b)) }
21
22    val sort: T[Sort] = list(string)
23
24    def typ: T[Typ] =
25      variant[Typ](List(
26        { case Type(a, b) => (List(a), list(typ)(b)) },
27        { case TFree(a, b) => (List(a), sort(b)) },
28        { case TVar(a, b) => (indexname(a), sort(b)) }))
29
30    val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t)
31
32    def term: T[Term] =
33      variant[Term](List(
34        { case Const(a, b) => (List(a), list(typ)(b)) },
35        { case Free(a, b) => (List(a), typ_body(b)) },
36        { case Var(a, b) => (indexname(a), typ_body(b)) },
37        { case Bound(a) => (Nil, int(a)) },
38        { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
39        { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
40  }
41
42  object Decode
43  {
44    import XML.Decode._
45
46    val indexname: P[Indexname] =
47      { case List(a) => Indexname(a, 0)
48        case List(a, b) => Indexname(a, int_atom(b)) }
49
50    val sort: T[Sort] = list(string)
51
52    def typ: T[Typ] =
53      variant[Typ](List(
54        { case (List(a), b) => Type(a, list(typ)(b)) },
55        { case (List(a), b) => TFree(a, sort(b)) },
56        { case (a, b) => TVar(indexname(a), sort(b)) }))
57
58    val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
59
60    def term: T[Term] =
61      variant[Term](List(
62        { case (List(a), b) => Const(a, list(typ)(b)) },
63        { case (List(a), b) => Free(a, typ_body(b)) },
64        { case (a, b) => Var(indexname(a), typ_body(b)) },
65        { case (Nil, a) => Bound(int(a)) },
66        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
67        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
68
69    def term_env(env: Map[String, Typ]): T[Term] =
70    {
71      def env_type(x: String, t: Typ): Typ =
72        if (t == dummyT && env.isDefinedAt(x)) env(x) else t
73
74      def term: T[Term] =
75        variant[Term](List(
76          { case (List(a), b) => Const(a, list(typ)(b)) },
77          { case (List(a), b) => Free(a, env_type(a, typ_body(b))) },
78          { case (a, b) => Var(indexname(a), typ_body(b)) },
79          { case (Nil, a) => Bound(int(a)) },
80          { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
81          { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
82      term
83    }
84
85    def proof_env(env: Map[String, Typ]): T[Proof] =
86    {
87      val term = term_env(env)
88      def proof: T[Proof] =
89        variant[Proof](List(
90          { case (Nil, Nil) => MinProof },
91          { case (Nil, a) => PBound(int(a)) },
92          { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
93          { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
94          { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
95          { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
96          { case (Nil, a) => Hyp(term(a)) },
97          { case (List(a), b) => PAxm(a, list(typ)(b)) },
98          { case (List(a), b) => OfClass(typ(b), a) },
99          { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
100          { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
101      proof
102    }
103
104    val proof: T[Proof] = proof_env(Map.empty)
105  }
106}
107