# HG changeset patch # User wenzelm # Date 1254429598 -7200 # Node ID 57dcddf81b01dcb010f576671b7fb0083b78d790 # Parent 75dff0bd4d5dac20e9ceeb4f9ef612ff6a44bc45 added term_cache; tuned; diff -r 75dff0bd4d5d -r 57dcddf81b01 src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML Thu Oct 01 22:39:06 2009 +0200 +++ b/src/Pure/term_ord.ML Thu Oct 01 22:39:58 2009 +0200 @@ -4,8 +4,17 @@ Term orderings. *) +signature BASIC_TERM_ORD = +sig + structure Vartab: TABLE + structure Sorttab: TABLE + structure Typtab: TABLE + structure Termtab: TABLE +end; + signature TERM_ORD = sig + include BASIC_TERM_ORD val fast_indexname_ord: indexname * indexname -> order val sort_ord: sort * sort -> order val typ_ord: typ * typ -> order @@ -17,6 +26,7 @@ val hd_ord: term * term -> order val termless: term * term -> bool val term_lpo: (term -> int) -> term * term -> order + val term_cache: (term -> 'a) -> term -> 'a end; structure TermOrd: TERM_ORD = @@ -202,9 +212,17 @@ end; +(* tables and caches *) + +structure Vartab = Table(type key = indexname val ord = fast_indexname_ord); +structure Sorttab = Table(type key = sort val ord = sort_ord); +structure Typtab = Table(type key = typ val ord = typ_ord); +structure Termtab = Table(type key = term val ord = fast_term_ord); + +fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f; + end; -structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord); -structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord); -structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord); -structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord); +structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd; +open Basic_Term_Ord; +