46 |
46 |
47 val sort: T[Sort] = list(string) |
47 val sort: T[Sort] = list(string) |
48 |
48 |
49 def typ: T[Typ] = |
49 def typ: T[Typ] = |
50 variant[Typ](List( |
50 variant[Typ](List( |
51 { case (List(a), b) => Type(a, list(typ)(b)) }, |
51 { case (List(a), b) => Type(a, list(typ)(b)) case _ => ??? }, |
52 { case (List(a), b) => TFree(a, sort(b)) }, |
52 { case (List(a), b) => TFree(a, sort(b)) case _ => ??? }, |
53 { case (a, b) => TVar(indexname(a), sort(b)) })) |
53 { case (a, b) => TVar(indexname(a), sort(b)) case _ => ??? })) |
54 |
54 |
55 val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) } |
55 val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) } |
56 |
56 |
57 def term: T[Term] = |
57 def term: T[Term] = |
58 variant[Term](List( |
58 variant[Term](List( |
59 { case (List(a), b) => Const(a, list(typ)(b)) }, |
59 { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? }, |
60 { case (List(a), b) => Free(a, typ_body(b)) }, |
60 { case (List(a), b) => Free(a, typ_body(b)) case _ => ??? }, |
61 { case (a, b) => Var(indexname(a), typ_body(b)) }, |
61 { case (a, b) => Var(indexname(a), typ_body(b)) case _ => ??? }, |
62 { case (Nil, a) => Bound(int(a)) }, |
62 { case (Nil, a) => Bound(int(a)) case _ => ??? }, |
63 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, |
63 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? }, |
64 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) |
64 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? })) |
65 |
65 |
66 def term_env(env: Map[String, Typ]): T[Term] = { |
66 def term_env(env: Map[String, Typ]): T[Term] = { |
67 def env_type(x: String, t: Typ): Typ = |
67 def env_type(x: String, t: Typ): Typ = |
68 if (t == dummyT && env.isDefinedAt(x)) env(x) else t |
68 if (t == dummyT && env.isDefinedAt(x)) env(x) else t |
69 |
69 |
70 def term: T[Term] = |
70 def term: T[Term] = |
71 variant[Term](List( |
71 variant[Term](List( |
72 { case (List(a), b) => Const(a, list(typ)(b)) }, |
72 { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? }, |
73 { case (List(a), b) => Free(a, env_type(a, typ_body(b))) }, |
73 { case (List(a), b) => Free(a, env_type(a, typ_body(b))) case _ => ??? }, |
74 { case (a, b) => Var(indexname(a), typ_body(b)) }, |
74 { case (a, b) => Var(indexname(a), typ_body(b)) case _ => ??? }, |
75 { case (Nil, a) => Bound(int(a)) }, |
75 { case (Nil, a) => Bound(int(a)) case _ => ??? }, |
76 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, |
76 { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? }, |
77 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) |
77 { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? })) |
78 term |
78 term |
79 } |
79 } |
80 |
80 |
81 def proof_env(env: Map[String, Typ]): T[Proof] = { |
81 def proof_env(env: Map[String, Typ]): T[Proof] = { |
82 val term = term_env(env) |
82 val term = term_env(env) |
83 def proof: T[Proof] = |
83 def proof: T[Proof] = |
84 variant[Proof](List( |
84 variant[Proof](List( |
85 { case (Nil, Nil) => MinProof }, |
85 { case (Nil, Nil) => MinProof case _ => ??? }, |
86 { case (Nil, a) => PBound(int(a)) }, |
86 { case (Nil, a) => PBound(int(a)) case _ => ??? }, |
87 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) }, |
87 { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) case _ => ??? }, |
88 { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) }, |
88 { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) case _ => ??? }, |
89 { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) }, |
89 { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) case _ => ??? }, |
90 { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) }, |
90 { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) case _ => ??? }, |
91 { case (Nil, a) => Hyp(term(a)) }, |
91 { case (Nil, a) => Hyp(term(a)) case _ => ??? }, |
92 { case (List(a), b) => PAxm(a, list(typ)(b)) }, |
92 { case (List(a), b) => PAxm(a, list(typ)(b)) case _ => ??? }, |
93 { case (List(a), b) => PClass(typ(b), a) }, |
93 { case (List(a), b) => PClass(typ(b), a) case _ => ??? }, |
94 { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) }, |
94 { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) case _ => ??? }, |
95 { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) })) |
95 { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) case _ => ??? })) |
96 proof |
96 proof |
97 } |
97 } |
98 |
98 |
99 val proof: T[Proof] = proof_env(Map.empty) |
99 val proof: T[Proof] = proof_env(Map.empty) |
100 } |
100 } |