64 { case (a, b) => Var(indexname(a), typ_body(b)) }, |
64 { case (a, b) => Var(indexname(a), typ_body(b)) }, |
65 { case (List(a), Nil) => Bound(int_atom(a)) }, |
65 { case (List(a), Nil) => Bound(int_atom(a)) }, |
66 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, |
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) })) |
67 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) |
68 |
68 |
69 def proof: T[Proof] = |
69 def term_env(env: Map[String, Typ]): T[Term] = |
70 variant[Proof](List( |
70 { |
71 { case (Nil, Nil) => MinProof }, |
71 def env_type(x: String, t: Typ): Typ = |
72 { case (List(a), Nil) => PBound(int_atom(a)) }, |
72 if (t == dummyT && env.isDefinedAt(x)) env(x) else t |
73 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) }, |
73 |
74 { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) }, |
74 def term: T[Term] = |
75 { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) }, |
75 variant[Term](List( |
76 { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) }, |
76 { case (List(a), b) => Const(a, list(typ)(b)) }, |
77 { case (Nil, a) => Hyp(term(a)) }, |
77 { case (List(a), b) => Free(a, env_type(a, typ_body(b))) }, |
78 { case (List(a), b) => PAxm(a, list(typ)(b)) }, |
78 { case (a, b) => Var(indexname(a), typ_body(b)) }, |
79 { case (List(a), b) => OfClass(typ(b), a) }, |
79 { case (List(a), Nil) => Bound(int_atom(a)) }, |
80 { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) }, |
80 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, |
81 { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(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 (List(a), Nil) => PBound(int_atom(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) |
82 } |
105 } |
83 } |
106 } |