equal
deleted
inserted
replaced
1 (* Title: Pure/term_ord.ML |
1 (* Title: Pure/term_ord.ML |
2 Author: Tobias Nipkow and Makarius, TU Muenchen |
2 Author: Tobias Nipkow, TU Muenchen |
3 |
3 Author: Makarius |
4 Term orderings. |
4 |
|
5 Term orderings and scalable collections. |
5 *) |
6 *) |
6 |
7 |
7 signature BASIC_TERM_ORD = |
8 signature BASIC_TERM_ORD = |
8 sig |
9 sig |
9 structure Vartab: TABLE |
10 structure Vartab: TABLE |
10 structure Sorttab: TABLE |
11 structure Sorttab: TABLE |
11 structure Typtab: TABLE |
12 structure Typtab: TABLE |
12 structure Termtab: TABLE |
13 structure Termtab: TABLE |
|
14 structure Var_Graph: GRAPH |
|
15 structure Sort_Graph: GRAPH |
|
16 structure Typ_Graph: GRAPH |
|
17 structure Term_Graph: GRAPH |
13 end; |
18 end; |
14 |
19 |
15 signature TERM_ORD = |
20 signature TERM_ORD = |
16 sig |
21 sig |
17 include BASIC_TERM_ORD |
22 include BASIC_TERM_ORD |
207 in |
212 in |
208 val term_lpo = term_lpo |
213 val term_lpo = term_lpo |
209 end; |
214 end; |
210 |
215 |
211 |
216 |
212 (* tables and caches *) |
217 (* scalable collections *) |
213 |
218 |
214 structure Vartab = Table(type key = indexname val ord = fast_indexname_ord); |
219 structure Vartab = Table(type key = indexname val ord = fast_indexname_ord); |
215 structure Sorttab = Table(type key = sort val ord = sort_ord); |
220 structure Sorttab = Table(type key = sort val ord = sort_ord); |
216 structure Typtab = Table(type key = typ val ord = typ_ord); |
221 structure Typtab = Table(type key = typ val ord = typ_ord); |
217 structure Termtab = Table(type key = term val ord = fast_term_ord); |
222 structure Termtab = Table(type key = term val ord = fast_term_ord); |
218 |
223 |
|
224 structure Var_Graph = Graph(type key = indexname val ord = fast_indexname_ord); |
|
225 structure Sort_Graph = Graph(type key = sort val ord = sort_ord); |
|
226 structure Typ_Graph = Graph(type key = typ val ord = typ_ord); |
|
227 structure Term_Graph = Graph(type key = term val ord = fast_term_ord); |
|
228 |
219 fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f; |
229 fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f; |
220 |
230 |
221 end; |
231 end; |
222 |
232 |
223 structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord; |
233 structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord; |
224 open Basic_Term_Ord; |
234 open Basic_Term_Ord; |
225 |
|
226 structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord); |
|
227 structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord); |
|
228 structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord); |
|
229 structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord); |
|
230 |
|