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