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