29 case class Free(name: String, typ: Typ = dummyT) extends Term |
29 case class Free(name: String, typ: Typ = dummyT) extends Term |
30 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
30 case class Var(name: Indexname, typ: Typ = dummyT) extends Term |
31 case class Bound(index: Int) extends Term |
31 case class Bound(index: Int) extends Term |
32 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
32 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term |
33 case class App(fun: Term, arg: Term) extends Term |
33 case class App(fun: Term, arg: Term) extends Term |
|
34 |
|
35 sealed abstract class Proof |
|
36 case object MinProof extends Proof |
|
37 case class PBound(index: Int) extends Proof |
|
38 case class Abst(name: String, typ: Typ, body: Proof) extends Proof |
|
39 case class AbsP(name: String, hyp: Term, body: Proof) extends Proof |
|
40 case class Appt(fun: Proof, arg: Term) extends Proof |
|
41 case class AppP(fun: Proof, arg: Proof) extends Proof |
|
42 case class Hyp(hyp: Term) extends Proof |
|
43 case class PAxm(name: String, types: List[Typ]) extends Proof |
|
44 case class OfClass(typ: Typ, cls: String) extends Proof |
|
45 case class Oracle(name: String, prop: Term, types: List[Typ]) extends Proof |
|
46 case class PThm(serial: Long, pseudo_name: String, types: List[Typ]) extends Proof |
34 |
47 |
35 |
48 |
36 /* Pure logic */ |
49 /* Pure logic */ |
37 |
50 |
38 def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty)) |
51 def itselfT(ty: Typ): Typ = Type(Pure_Thy.ITSELF, List(ty)) |
99 else |
112 else |
100 lookup(x) match { |
113 lookup(x) match { |
101 case Some(y) => y |
114 case Some(y) => y |
102 case None => |
115 case None => |
103 x match { |
116 x match { |
104 case Type(name, args) => store(Type(cache_string(name), args.map(cache_typ(_)))) |
117 case Type(name, args) => store(Type(cache_string(name), cache_typs(args))) |
105 case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort))) |
118 case TFree(name, sort) => store(TFree(cache_string(name), cache_sort(sort))) |
106 case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort))) |
119 case TVar(name, sort) => store(TVar(cache_indexname(name), cache_sort(sort))) |
107 } |
120 } |
108 } |
121 } |
|
122 } |
|
123 |
|
124 protected def cache_typs(x: List[Typ]): List[Typ] = |
|
125 { |
|
126 if (x.isEmpty) Nil |
|
127 else { |
|
128 lookup(x) match { |
|
129 case Some(y) => y |
|
130 case None => store(x.map(cache_typ(_))) |
|
131 } |
|
132 } |
109 } |
133 } |
110 |
134 |
111 protected def cache_term(x: Term): Term = |
135 protected def cache_term(x: Term): Term = |
112 { |
136 { |
113 lookup(x) match { |
137 lookup(x) match { |
123 case App(fun, arg) => store(App(cache_term(fun), cache_term(arg))) |
147 case App(fun, arg) => store(App(cache_term(fun), cache_term(arg))) |
124 } |
148 } |
125 } |
149 } |
126 } |
150 } |
127 |
151 |
|
152 protected def cache_proof(x: Proof): Proof = |
|
153 { |
|
154 if (x == MinProof) MinProof |
|
155 else { |
|
156 lookup(x) match { |
|
157 case Some(y) => y |
|
158 case None => |
|
159 x match { |
|
160 case MinProof => x |
|
161 case PBound(index) => store(PBound(cache_int(index))) |
|
162 case Abst(name, typ, body) => |
|
163 store(Abst(cache_string(name), cache_typ(typ), cache_proof(body))) |
|
164 case AbsP(name, hyp, body) => |
|
165 store(AbsP(cache_string(name), cache_term(hyp), cache_proof(body))) |
|
166 case Appt(fun, arg) => store(Appt(cache_proof(fun), cache_term(arg))) |
|
167 case AppP(fun, arg) => store(AppP(cache_proof(fun), cache_proof(arg))) |
|
168 case OfClass(typ, cls) => store(OfClass(cache_typ(typ), cache_string(cls))) |
|
169 case Oracle(name, prop, types) => |
|
170 store(Oracle(cache_string(name), cache_term(prop), cache_typs(types))) |
|
171 case PThm(serial, name, types) => |
|
172 store(PThm(serial, cache_string(name), cache_typs(types))) |
|
173 } |
|
174 } |
|
175 } |
|
176 } |
|
177 |
128 // main methods |
178 // main methods |
129 def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) } |
179 def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) } |
130 def sort(x: Sort): Sort = synchronized { cache_sort(x) } |
180 def sort(x: Sort): Sort = synchronized { cache_sort(x) } |
131 def typ(x: Typ): Typ = synchronized { cache_typ(x) } |
181 def typ(x: Typ): Typ = synchronized { cache_typ(x) } |
132 def term(x: Term): Term = synchronized { cache_term(x) } |
182 def term(x: Term): Term = synchronized { cache_term(x) } |
|
183 def proof(x: Proof): Proof = synchronized { cache_proof(x) } |
133 |
184 |
134 def position(x: Position.T): Position.T = |
185 def position(x: Position.T): Position.T = |
135 synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } |
186 synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } |
136 } |
187 } |
137 } |
188 } |