src/Tools/more_conv.ML
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 32402 5731300da417
child 32821 99843bbfaeb2
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
     1 (* Title:  Tools/more_conv.ML
     2    Author: Sascha Boehme
     3 
     4 Further conversions and conversionals.
     5 *)
     6 
     7 signature MORE_CONV =
     8 sig
     9   val rewrs_conv: thm list -> conv
    10 
    11   val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
    12   val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
    13   val top_conv: (Proof.context -> conv) -> Proof.context -> conv
    14   val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
    15 
    16   val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
    17 
    18   val cache_conv: conv -> conv
    19 end
    20 
    21 
    22 
    23 structure More_Conv : MORE_CONV =
    24 struct
    25 
    26 
    27 fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)
    28 
    29 
    30 fun sub_conv conv ctxt =
    31   Conv.comb_conv (conv ctxt) else_conv
    32   Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv
    33   Conv.all_conv
    34 
    35 fun bottom_conv conv ctxt ct =
    36   (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct
    37 
    38 fun top_conv conv ctxt ct =
    39   (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct
    40 
    41 fun top_sweep_conv conv ctxt ct =
    42   (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct
    43 
    44 
    45 fun binder_conv cv ctxt =
    46   Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
    47 
    48 
    49 fun cache_conv conv =   (* FIXME not thread-safe *)
    50   let 
    51     val tab = Unsynchronized.ref Termtab.empty
    52     fun add_result t thm =
    53       let val _ = Unsynchronized.change tab (Termtab.insert Thm.eq_thm (t, thm))
    54       in thm end
    55     fun cconv ct =  
    56       (case Termtab.lookup (!tab) (Thm.term_of ct) of
    57         SOME thm => thm
    58       | NONE => add_result (Thm.term_of ct) (conv ct))
    59   in cconv end
    60 
    61 end