19 { case Indexname(a, 0) => List(a) |
19 { case Indexname(a, 0) => List(a) |
20 case Indexname(a, b) => List(a, int_atom(b)) } |
20 case Indexname(a, b) => List(a, int_atom(b)) } |
21 |
21 |
22 val sort: T[Sort] = list(string) |
22 val sort: T[Sort] = list(string) |
23 |
23 |
24 def typ_raw: T[Typ] = |
24 def typ: T[Typ] = |
25 variant[Typ](List( |
25 variant[Typ](List( |
26 { case Type(a, b) => (List(a), list(typ_raw)(b)) }, |
26 { case Type(a, b) => (List(a), list(typ)(b)) }, |
27 { case TFree(a, b) => (List(a), sort(b)) }, |
27 { case TFree(a, b) => (List(a), sort(b)) }, |
28 { case TVar(a, b) => (indexname(a), sort(b)) })) |
28 { case TVar(a, b) => (indexname(a), sort(b)) })) |
29 |
29 |
30 val typ: T[Typ] = |
30 val typ_body: T[Typ] = (t: Typ) => if (t == dummyT) Nil else typ(t) |
31 { case t => option(typ_raw)(if (t == dummyT) None else Some(t)) } |
|
32 |
31 |
33 def term: T[Term] = |
32 def term: T[Term] = |
34 variant[Term](List( |
33 variant[Term](List( |
35 { case Const(a, b) => (List(a), list(typ)(b)) }, |
34 { case Const(a, b) => (List(a), list(typ)(b)) }, |
36 { case Free(a, b) => (List(a), typ(b)) }, |
35 { case Free(a, b) => (List(a), typ_body(b)) }, |
37 { case Var(a, b) => (indexname(a), typ(b)) }, |
36 { case Var(a, b) => (indexname(a), typ_body(b)) }, |
38 { case Bound(a) => (List(int_atom(a)), Nil) }, |
37 { case Bound(a) => (List(int_atom(a)), Nil) }, |
39 { 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)) }, |
40 { case App(a, b) => (Nil, pair(term, term)(a, b)) })) |
39 { case App(a, b) => (Nil, pair(term, term)(a, b)) })) |
41 } |
40 } |
42 |
41 |
48 { case List(a) => Indexname(a, 0) |
47 { case List(a) => Indexname(a, 0) |
49 case List(a, b) => Indexname(a, int_atom(b)) } |
48 case List(a, b) => Indexname(a, int_atom(b)) } |
50 |
49 |
51 val sort: T[Sort] = list(string) |
50 val sort: T[Sort] = list(string) |
52 |
51 |
53 def typ_raw: T[Typ] = |
52 def typ: T[Typ] = |
54 variant[Typ](List( |
53 variant[Typ](List( |
55 { case (List(a), b) => Type(a, list(typ_raw)(b)) }, |
54 { case (List(a), b) => Type(a, list(typ)(b)) }, |
56 { case (List(a), b) => TFree(a, sort(b)) }, |
55 { case (List(a), b) => TFree(a, sort(b)) }, |
57 { case (a, b) => TVar(indexname(a), sort(b)) })) |
56 { case (a, b) => TVar(indexname(a), sort(b)) })) |
58 |
57 |
59 def typ(body: XML.Body): Typ = option(typ_raw)(body).getOrElse(dummyT) |
58 val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) } |
60 |
59 |
61 def term: T[Term] = |
60 def term: T[Term] = |
62 variant[Term](List( |
61 variant[Term](List( |
63 { case (List(a), b) => Const(a, list(typ)(b)) }, |
62 { case (List(a), b) => Const(a, list(typ)(b)) }, |
64 { case (List(a), b) => Free(a, typ(b)) }, |
63 { case (List(a), b) => Free(a, typ_body(b)) }, |
65 { case (a, b) => Var(indexname(a), typ(b)) }, |
64 { case (a, b) => Var(indexname(a), typ_body(b)) }, |
66 { case (List(a), Nil) => Bound(int_atom(a)) }, |
65 { case (List(a), Nil) => Bound(int_atom(a)) }, |
67 { 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) }, |
68 { 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) })) |
69 |
68 |
70 def proof: T[Proof] = |
69 def proof: T[Proof] = |