32 def term: T[Term] = |
32 def term: T[Term] = |
33 variant[Term](List( |
33 variant[Term](List( |
34 { case Const(a, b) => (List(a), list(typ)(b)) }, |
34 { case Const(a, b) => (List(a), list(typ)(b)) }, |
35 { case Free(a, b) => (List(a), typ_body(b)) }, |
35 { case Free(a, b) => (List(a), typ_body(b)) }, |
36 { case Var(a, b) => (indexname(a), typ_body(b)) }, |
36 { case Var(a, b) => (indexname(a), typ_body(b)) }, |
37 { case Bound(a) => (List(int_atom(a)), Nil) }, |
37 { case Bound(a) => (Nil, int(a)) }, |
38 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) }, |
38 { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) }, |
39 { case App(a, b) => (Nil, pair(term, term)(a, b)) })) |
39 { case App(a, b) => (Nil, pair(term, term)(a, b)) })) |
40 } |
40 } |
41 |
41 |
42 object Decode |
42 object Decode |
60 def term: T[Term] = |
60 def term: T[Term] = |
61 variant[Term](List( |
61 variant[Term](List( |
62 { case (List(a), b) => Const(a, list(typ)(b)) }, |
62 { case (List(a), b) => Const(a, list(typ)(b)) }, |
63 { case (List(a), b) => Free(a, typ_body(b)) }, |
63 { case (List(a), b) => Free(a, typ_body(b)) }, |
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 (Nil, a) => Bound(int(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 term_env(env: Map[String, Typ]): T[Term] = |
69 def term_env(env: Map[String, Typ]): T[Term] = |
70 { |
70 { |
74 def term: T[Term] = |
74 def term: T[Term] = |
75 variant[Term](List( |
75 variant[Term](List( |
76 { case (List(a), b) => Const(a, list(typ)(b)) }, |
76 { case (List(a), b) => Const(a, list(typ)(b)) }, |
77 { case (List(a), b) => Free(a, env_type(a, typ_body(b))) }, |
77 { case (List(a), b) => Free(a, env_type(a, typ_body(b))) }, |
78 { case (a, b) => Var(indexname(a), typ_body(b)) }, |
78 { case (a, b) => Var(indexname(a), typ_body(b)) }, |
79 { case (List(a), Nil) => Bound(int_atom(a)) }, |
79 { case (Nil, a) => Bound(int(a)) }, |
80 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, |
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) })) |
81 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) |
82 term |
82 term |
83 } |
83 } |
84 |
84 |
86 { |
86 { |
87 val term = term_env(env) |
87 val term = term_env(env) |
88 def proof: T[Proof] = |
88 def proof: T[Proof] = |
89 variant[Proof](List( |
89 variant[Proof](List( |
90 { case (Nil, Nil) => MinProof }, |
90 { case (Nil, Nil) => MinProof }, |
91 { case (List(a), Nil) => PBound(int_atom(a)) }, |
91 { case (Nil, a) => PBound(int(a)) }, |
92 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) }, |
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) }, |
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) }, |
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) }, |
95 { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) }, |
96 { case (Nil, a) => Hyp(term(a)) }, |
96 { case (Nil, a) => Hyp(term(a)) }, |