131 |
131 |
132 |
132 |
133 |
133 |
134 /** cache **/ |
134 /** cache **/ |
135 |
135 |
136 def make_cache(initial_size: Int = 131071, max_string: Int = Integer.MAX_VALUE): Cache = |
136 object Cache |
137 new Cache(initial_size, max_string) |
137 { |
138 |
138 def make( |
139 class Cache private[Term](initial_size: Int, max_string: Int) |
139 max_string: Int = Integer.MAX_VALUE, |
140 extends isabelle.Cache(initial_size, max_string) |
140 initial_size: Int = isabelle.Cache.default_initial_size): Cache = |
|
141 new Cache(initial_size, max_string) |
|
142 |
|
143 val none: Cache = make(max_string = 0) |
|
144 } |
|
145 |
|
146 class Cache private[Term](max_string: Int, initial_size: Int) |
|
147 extends isabelle.Cache(max_string = max_string, initial_size = initial_size) |
141 { |
148 { |
142 protected def cache_indexname(x: Indexname): Indexname = |
149 protected def cache_indexname(x: Indexname): Indexname = |
143 lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index)) |
150 lookup(x) getOrElse store(Indexname(cache_string(x.name), x.index)) |
144 |
151 |
145 protected def cache_sort(x: Sort): Sort = |
152 protected def cache_sort(x: Sort): Sort = |
146 if (x.isEmpty) Nil else lookup(x) getOrElse store(x.map(cache_string)) |
153 if (x.isEmpty) Nil |
|
154 else lookup(x) getOrElse store(x.map(cache_string)) |
147 |
155 |
148 protected def cache_typ(x: Typ): Typ = |
156 protected def cache_typ(x: Typ): Typ = |
149 { |
157 { |
150 if (x == dummyT) dummyT |
158 if (x == dummyT) dummyT |
151 else |
159 else |
214 } |
222 } |
215 } |
223 } |
216 } |
224 } |
217 |
225 |
218 // main methods |
226 // main methods |
219 def indexname(x: Indexname): Indexname = synchronized { cache_indexname(x) } |
227 def indexname(x: Indexname): Indexname = |
220 def sort(x: Sort): Sort = synchronized { cache_sort(x) } |
228 if (no_cache) x else synchronized { cache_indexname(x) } |
221 def typ(x: Typ): Typ = synchronized { cache_typ(x) } |
229 def sort(x: Sort): Sort = |
222 def term(x: Term): Term = synchronized { cache_term(x) } |
230 if (no_cache) x else synchronized { cache_sort(x) } |
223 def proof(x: Proof): Proof = synchronized { cache_proof(x) } |
231 def typ(x: Typ): Typ = |
|
232 if (no_cache) x else synchronized { cache_typ(x) } |
|
233 def term(x: Term): Term = |
|
234 if (no_cache) x else synchronized { cache_term(x) } |
|
235 def proof(x: Proof): Proof = |
|
236 if (no_cache) x else synchronized { cache_proof(x) } |
224 |
237 |
225 def position(x: Position.T): Position.T = |
238 def position(x: Position.T): Position.T = |
226 synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } |
239 if (no_cache) x |
|
240 else synchronized { x.map({ case (a, b) => (cache_string(a), cache_string(b)) }) } |
227 } |
241 } |
228 } |
242 } |