# HG changeset patch # User wenzelm # Date 1254432425 -7200 # Node ID c8f5a7c8353fb4dbf6002cbfc557f5bb09fb80df # Parent 98702c579ad0f62b7349a840c0e0043facc78b38 moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache; diff -r 98702c579ad0 -r c8f5a7c8353f src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Thu Oct 01 22:40:29 2009 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Thu Oct 01 23:27:05 2009 +0200 @@ -538,7 +538,7 @@ val nnf_norm_conv' = nnf_conv then_conv literals_conv [@{term "op &"}, @{term "op |"}] [] - (More_Conv.cache_conv + (Conv.cache_conv (first_conv [real_lt_conv, real_le_conv, real_eq_conv, real_not_lt_conv, real_not_le_conv, real_not_eq_conv, all_conv])) diff -r 98702c579ad0 -r c8f5a7c8353f src/Pure/conv.ML --- a/src/Pure/conv.ML Thu Oct 01 22:40:29 2009 +0200 +++ b/src/Pure/conv.ML Thu Oct 01 23:27:05 2009 +0200 @@ -1,5 +1,6 @@ (* Title: Pure/conv.ML - Author: Amine Chaieb and Makarius + Author: Amine Chaieb, TU Muenchen + Author: Makarius Conversions: primitive equality reasoning. *) @@ -22,6 +23,7 @@ val every_conv: conv list -> conv val try_conv: conv -> conv val repeat_conv: conv -> conv + val cache_conv: conv -> conv val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv val combination_conv: conv -> conv -> conv val comb_conv: conv -> conv @@ -44,7 +46,7 @@ structure Conv: CONV = struct -(* conversionals *) +(* basic conversionals *) fun no_conv _ = raise CTERM ("no conversion", []); val all_conv = Thm.reflexive; @@ -72,6 +74,8 @@ fun try_conv cv = cv else_conv all_conv; fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct; +fun cache_conv (cv: conv) = Thm.cterm_cache cv; + (** Pure conversions **) @@ -177,5 +181,5 @@ end; -structure BasicConv: BASIC_CONV = Conv; -open BasicConv; +structure Basic_Conv: BASIC_CONV = Conv; +open Basic_Conv; diff -r 98702c579ad0 -r c8f5a7c8353f src/Tools/more_conv.ML --- a/src/Tools/more_conv.ML Thu Oct 01 22:40:29 2009 +0200 +++ b/src/Tools/more_conv.ML Thu Oct 01 23:27:05 2009 +0200 @@ -1,5 +1,5 @@ -(* Title: Tools/more_conv.ML - Author: Sascha Boehme +(* Title: Tools/more_conv.ML + Author: Sascha Boehme, TU Muenchen Further conversions and conversionals. *) @@ -14,16 +14,11 @@ val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv val binder_conv: (Proof.context -> conv) -> Proof.context -> conv - - val cache_conv: conv -> conv end - - structure More_Conv : MORE_CONV = struct - fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs) @@ -45,19 +40,4 @@ fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt) - -fun cache_conv conv = - let - val cache = Synchronized.var "cache_conv" Termtab.empty - fun lookup t = - Synchronized.change_result cache (fn tab => (Termtab.lookup tab t, tab)) - val keep = Synchronized.change cache o Termtab.insert Thm.eq_thm - fun keep_result t thm = (keep (t, thm); thm) - - fun cconv ct = - (case lookup (Thm.term_of ct) of - SOME thm => thm - | NONE => keep_result (Thm.term_of ct) (conv ct)) - in cconv end - end