moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
authorwenzelm
Thu Oct 01 23:27:05 2009 +0200 (2009-10-01)
changeset 32843c8f5a7c8353f
parent 32842 98702c579ad0
child 32844 044711ee3f21
moved cache_conv to src/Pure/conv.ML, use Thm.cterm_cache;
src/HOL/Library/positivstellensatz.ML
src/Pure/conv.ML
src/Tools/more_conv.ML
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Oct 01 22:40:29 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Oct 01 23:27:05 2009 +0200
     1.3 @@ -538,7 +538,7 @@
     1.4     val nnf_norm_conv' = 
     1.5       nnf_conv then_conv 
     1.6       literals_conv [@{term "op &"}, @{term "op |"}] [] 
     1.7 -     (More_Conv.cache_conv 
     1.8 +     (Conv.cache_conv 
     1.9         (first_conv [real_lt_conv, real_le_conv, 
    1.10                      real_eq_conv, real_not_lt_conv, 
    1.11                      real_not_le_conv, real_not_eq_conv, all_conv]))
     2.1 --- a/src/Pure/conv.ML	Thu Oct 01 22:40:29 2009 +0200
     2.2 +++ b/src/Pure/conv.ML	Thu Oct 01 23:27:05 2009 +0200
     2.3 @@ -1,5 +1,6 @@
     2.4  (*  Title:      Pure/conv.ML
     2.5 -    Author:     Amine Chaieb and Makarius
     2.6 +    Author:     Amine Chaieb, TU Muenchen
     2.7 +    Author:     Makarius
     2.8  
     2.9  Conversions: primitive equality reasoning.
    2.10  *)
    2.11 @@ -22,6 +23,7 @@
    2.12    val every_conv: conv list -> conv
    2.13    val try_conv: conv -> conv
    2.14    val repeat_conv: conv -> conv
    2.15 +  val cache_conv: conv -> conv
    2.16    val abs_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
    2.17    val combination_conv: conv -> conv -> conv
    2.18    val comb_conv: conv -> conv
    2.19 @@ -44,7 +46,7 @@
    2.20  structure Conv: CONV =
    2.21  struct
    2.22  
    2.23 -(* conversionals *)
    2.24 +(* basic conversionals *)
    2.25  
    2.26  fun no_conv _ = raise CTERM ("no conversion", []);
    2.27  val all_conv = Thm.reflexive;
    2.28 @@ -72,6 +74,8 @@
    2.29  fun try_conv cv = cv else_conv all_conv;
    2.30  fun repeat_conv cv ct = try_conv (cv then_conv repeat_conv cv) ct;
    2.31  
    2.32 +fun cache_conv (cv: conv) = Thm.cterm_cache cv;
    2.33 +
    2.34  
    2.35  
    2.36  (** Pure conversions **)
    2.37 @@ -177,5 +181,5 @@
    2.38  
    2.39  end;
    2.40  
    2.41 -structure BasicConv: BASIC_CONV = Conv;
    2.42 -open BasicConv;
    2.43 +structure Basic_Conv: BASIC_CONV = Conv;
    2.44 +open Basic_Conv;
     3.1 --- a/src/Tools/more_conv.ML	Thu Oct 01 22:40:29 2009 +0200
     3.2 +++ b/src/Tools/more_conv.ML	Thu Oct 01 23:27:05 2009 +0200
     3.3 @@ -1,5 +1,5 @@
     3.4 -(* Title:  Tools/more_conv.ML
     3.5 -   Author: Sascha Boehme
     3.6 +(*  Title:       Tools/more_conv.ML
     3.7 +    Author:      Sascha Boehme, TU Muenchen
     3.8  
     3.9  Further conversions and conversionals.
    3.10  *)
    3.11 @@ -14,16 +14,11 @@
    3.12    val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
    3.13  
    3.14    val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
    3.15 -
    3.16 -  val cache_conv: conv -> conv
    3.17  end
    3.18  
    3.19 -
    3.20 -
    3.21  structure More_Conv : MORE_CONV =
    3.22  struct
    3.23  
    3.24 -
    3.25  fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)
    3.26  
    3.27  
    3.28 @@ -45,19 +40,4 @@
    3.29  fun binder_conv cv ctxt =
    3.30    Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
    3.31  
    3.32 -
    3.33 -fun cache_conv conv =
    3.34 -  let
    3.35 -    val cache = Synchronized.var "cache_conv" Termtab.empty
    3.36 -    fun lookup t =
    3.37 -      Synchronized.change_result cache (fn tab => (Termtab.lookup tab t, tab))
    3.38 -    val keep = Synchronized.change cache o Termtab.insert Thm.eq_thm
    3.39 -    fun keep_result t thm = (keep (t, thm); thm)
    3.40 -
    3.41 -    fun cconv ct =
    3.42 -      (case lookup (Thm.term_of ct) of
    3.43 -        SOME thm => thm
    3.44 -      | NONE => keep_result (Thm.term_of ct) (conv ct))
    3.45 -  in cconv end
    3.46 -
    3.47  end