author | wenzelm |
Thu, 26 Aug 2010 16:34:10 +0200 | |
changeset 39034 | 37a9092de102 |
parent 38910 | febcd1733229 |
child 39715 | 9cc1ba3c5706 |
permissions | -rw-r--r-- |
haftmann@37743 | 1 |
(* Title: Tools/Code/code_simp.ML |
haftmann@37417 | 2 |
Author: Florian Haftmann, TU Muenchen |
haftmann@37417 | 3 |
|
haftmann@37417 | 4 |
Connecting the simplifier and the code generator. |
haftmann@37417 | 5 |
*) |
haftmann@37417 | 6 |
|
haftmann@37417 | 7 |
signature CODE_SIMP = |
haftmann@37417 | 8 |
sig |
haftmann@37417 | 9 |
val no_frees_conv: conv -> conv |
haftmann@37417 | 10 |
val map_ss: (simpset -> simpset) -> theory -> theory |
haftmann@38908 | 11 |
val dynamic_eval_conv: theory -> conv |
haftmann@38908 | 12 |
val dynamic_eval_tac: theory -> int -> tactic |
haftmann@38908 | 13 |
val dynamic_eval_value: theory -> term -> term |
haftmann@38908 | 14 |
val static_eval_conv: theory -> simpset option -> string list -> conv |
haftmann@38908 | 15 |
val static_eval_tac: theory -> simpset option -> string list -> int -> tactic |
haftmann@37417 | 16 |
val setup: theory -> theory |
haftmann@37417 | 17 |
end; |
haftmann@37417 | 18 |
|
haftmann@37417 | 19 |
structure Code_Simp : CODE_SIMP = |
haftmann@37417 | 20 |
struct |
haftmann@37417 | 21 |
|
haftmann@37417 | 22 |
(* avoid free variables during conversion *) |
haftmann@37417 | 23 |
|
haftmann@37417 | 24 |
fun no_frees_conv conv ct = |
haftmann@37417 | 25 |
let |
haftmann@37417 | 26 |
val frees = Thm.add_cterm_frees ct []; |
haftmann@37417 | 27 |
fun apply_beta free thm = Thm.combination thm (Thm.reflexive free) |
haftmann@37417 | 28 |
|> Conv.fconv_rule (Conv.arg_conv (Conv.try_conv (Thm.beta_conversion false))) |
haftmann@37417 | 29 |
|> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false)); |
haftmann@37417 | 30 |
in |
haftmann@37417 | 31 |
ct |
haftmann@37417 | 32 |
|> fold_rev Thm.cabs frees |
haftmann@37417 | 33 |
|> conv |
haftmann@37417 | 34 |
|> fold apply_beta frees |
haftmann@37417 | 35 |
end; |
haftmann@37417 | 36 |
|
haftmann@37417 | 37 |
|
haftmann@37417 | 38 |
(* dedicated simpset *) |
haftmann@37417 | 39 |
|
wenzelm@39034 | 40 |
structure Simpset = Theory_Data |
wenzelm@39034 | 41 |
( |
haftmann@37417 | 42 |
type T = simpset; |
haftmann@37417 | 43 |
val empty = empty_ss; |
haftmann@37417 | 44 |
fun extend ss = MetaSimplifier.inherit_context empty_ss ss; |
haftmann@37417 | 45 |
val merge = merge_ss; |
haftmann@37417 | 46 |
); |
haftmann@37417 | 47 |
|
haftmann@37417 | 48 |
val map_ss = Simpset.map; |
haftmann@37417 | 49 |
|
haftmann@37436 | 50 |
fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy); |
haftmann@37436 | 51 |
|
haftmann@37417 | 52 |
|
haftmann@37417 | 53 |
(* build simpset and conversion from program *) |
haftmann@37417 | 54 |
|
haftmann@37417 | 55 |
fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss = |
haftmann@37417 | 56 |
ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong) |
haftmann@37424 | 57 |
| add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss = |
haftmann@37424 | 58 |
ss addsimps (map (fst o snd) classparam_instances) |
haftmann@37417 | 59 |
| add_stmt _ ss = ss; |
haftmann@37417 | 60 |
|
haftmann@37839 | 61 |
val add_program = Graph.fold (add_stmt o fst o snd); |
haftmann@37417 | 62 |
|
haftmann@37417 | 63 |
fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite |
haftmann@37436 | 64 |
(add_program program (simpset_default thy some_ss)); |
haftmann@37436 | 65 |
|
haftmann@37436 | 66 |
fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss); |
haftmann@37417 | 67 |
|
haftmann@37417 | 68 |
|
haftmann@37417 | 69 |
(* evaluation with current code context *) |
haftmann@37417 | 70 |
|
haftmann@38908 | 71 |
fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy |
haftmann@37417 | 72 |
(fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)); |
haftmann@37417 | 73 |
|
haftmann@38908 | 74 |
fun dynamic_eval_tac thy = CONVERSION (dynamic_eval_conv thy) THEN' conclude_tac thy NONE; |
haftmann@37417 | 75 |
|
haftmann@38908 | 76 |
fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv thy o Thm.cterm_of thy; |
haftmann@37419 | 77 |
|
haftmann@37417 | 78 |
val setup = Method.setup (Binding.name "code_simp") |
haftmann@38908 | 79 |
(Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of))) |
haftmann@37417 | 80 |
"simplification with code equations" |
haftmann@38908 | 81 |
#> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of); |
haftmann@37417 | 82 |
|
haftmann@37417 | 83 |
|
haftmann@37417 | 84 |
(* evaluation with freezed code context *) |
haftmann@37417 | 85 |
|
haftmann@38910 | 86 |
fun static_eval_conv thy some_ss consts = no_frees_conv |
haftmann@38910 | 87 |
(Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss)); |
haftmann@37417 | 88 |
|
haftmann@38908 | 89 |
fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) |
haftmann@37436 | 90 |
THEN' conclude_tac thy some_ss; |
haftmann@37417 | 91 |
|
haftmann@37417 | 92 |
end; |