src/Pure/term_ord.ML
changeset 32841 57dcddf81b01
parent 31976 17414e2736f4
child 35404 de56579ae229
     1.1 --- a/src/Pure/term_ord.ML	Thu Oct 01 22:39:06 2009 +0200
     1.2 +++ b/src/Pure/term_ord.ML	Thu Oct 01 22:39:58 2009 +0200
     1.3 @@ -4,8 +4,17 @@
     1.4  Term orderings.
     1.5  *)
     1.6  
     1.7 +signature BASIC_TERM_ORD =
     1.8 +sig
     1.9 +  structure Vartab: TABLE
    1.10 +  structure Sorttab: TABLE
    1.11 +  structure Typtab: TABLE
    1.12 +  structure Termtab: TABLE
    1.13 +end;
    1.14 +
    1.15  signature TERM_ORD =
    1.16  sig
    1.17 +  include BASIC_TERM_ORD
    1.18    val fast_indexname_ord: indexname * indexname -> order
    1.19    val sort_ord: sort * sort -> order
    1.20    val typ_ord: typ * typ -> order
    1.21 @@ -17,6 +26,7 @@
    1.22    val hd_ord: term * term -> order
    1.23    val termless: term * term -> bool
    1.24    val term_lpo: (term -> int) -> term * term -> order
    1.25 +  val term_cache: (term -> 'a) -> term -> 'a
    1.26  end;
    1.27  
    1.28  structure TermOrd: TERM_ORD =
    1.29 @@ -202,9 +212,17 @@
    1.30  end;
    1.31  
    1.32  
    1.33 +(* tables and caches *)
    1.34 +
    1.35 +structure Vartab = Table(type key = indexname val ord = fast_indexname_ord);
    1.36 +structure Sorttab = Table(type key = sort val ord = sort_ord);
    1.37 +structure Typtab = Table(type key = typ val ord = typ_ord);
    1.38 +structure Termtab = Table(type key = term val ord = fast_term_ord);
    1.39 +
    1.40 +fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
    1.41 +
    1.42  end;
    1.43  
    1.44 -structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord);
    1.45 -structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord);
    1.46 -structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord);
    1.47 -structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord);
    1.48 +structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
    1.49 +open Basic_Term_Ord;
    1.50 +