author | wenzelm |
Fri, 17 Dec 2010 18:33:35 +0100 | |
changeset 41499 | 1e6d86821718 |
parent 41488 | c5cb19ecbd41 |
parent 41491 | bd4ecd48c21f |
child 41594 | 6673f6fa94ca |
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 map_ss: (simpset -> simpset) -> theory -> theory |
haftmann@41488 | 10 |
val dynamic_conv: theory -> conv |
haftmann@41436 | 11 |
val dynamic_tac: theory -> int -> tactic |
haftmann@41432 | 12 |
val dynamic_value: theory -> term -> term |
haftmann@41432 | 13 |
val static_conv: theory -> simpset option -> string list -> conv |
haftmann@41436 | 14 |
val static_tac: theory -> simpset option -> string list -> int -> tactic |
haftmann@37417 | 15 |
val setup: theory -> theory |
haftmann@37417 | 16 |
end; |
haftmann@37417 | 17 |
|
haftmann@37417 | 18 |
structure Code_Simp : CODE_SIMP = |
haftmann@37417 | 19 |
struct |
haftmann@37417 | 20 |
|
haftmann@37417 | 21 |
(* dedicated simpset *) |
haftmann@37417 | 22 |
|
wenzelm@39034 | 23 |
structure Simpset = Theory_Data |
wenzelm@39034 | 24 |
( |
haftmann@37417 | 25 |
type T = simpset; |
haftmann@37417 | 26 |
val empty = empty_ss; |
wenzelm@41491 | 27 |
fun extend ss = Simplifier.inherit_context empty_ss ss; |
haftmann@37417 | 28 |
val merge = merge_ss; |
haftmann@37417 | 29 |
); |
haftmann@37417 | 30 |
|
haftmann@37417 | 31 |
val map_ss = Simpset.map; |
haftmann@37417 | 32 |
|
haftmann@37436 | 33 |
fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy); |
haftmann@37436 | 34 |
|
haftmann@37417 | 35 |
|
haftmann@37417 | 36 |
(* build simpset and conversion from program *) |
haftmann@37417 | 37 |
|
haftmann@37417 | 38 |
fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss = |
haftmann@37417 | 39 |
ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong) |
haftmann@37424 | 40 |
| add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss = |
haftmann@37424 | 41 |
ss addsimps (map (fst o snd) classparam_instances) |
haftmann@37417 | 42 |
| add_stmt _ ss = ss; |
haftmann@37417 | 43 |
|
haftmann@37839 | 44 |
val add_program = Graph.fold (add_stmt o fst o snd); |
haftmann@37417 | 45 |
|
haftmann@37417 | 46 |
fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite |
haftmann@37436 | 47 |
(add_program program (simpset_default thy some_ss)); |
haftmann@37436 | 48 |
|
haftmann@37436 | 49 |
fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss); |
haftmann@37417 | 50 |
|
haftmann@37417 | 51 |
|
haftmann@39726 | 52 |
(* evaluation with dynamic code context *) |
haftmann@37417 | 53 |
|
haftmann@41488 | 54 |
fun dynamic_conv thy = Code_Thingol.dynamic_conv thy |
haftmann@41488 | 55 |
(fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program); |
haftmann@37417 | 56 |
|
haftmann@41488 | 57 |
fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE; |
haftmann@37417 | 58 |
|
haftmann@41488 | 59 |
fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy; |
haftmann@37419 | 60 |
|
haftmann@37417 | 61 |
val setup = Method.setup (Binding.name "code_simp") |
haftmann@41436 | 62 |
(Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o ProofContext.theory_of))) |
haftmann@37417 | 63 |
"simplification with code equations" |
haftmann@41432 | 64 |
#> Value.add_evaluator ("simp", dynamic_value o ProofContext.theory_of); |
haftmann@37417 | 65 |
|
haftmann@37417 | 66 |
|
haftmann@39726 | 67 |
(* evaluation with static code context *) |
haftmann@37417 | 68 |
|
haftmann@41432 | 69 |
fun static_conv thy some_ss consts = |
haftmann@41432 | 70 |
Code_Thingol.static_conv_simple thy consts |
haftmann@39830 | 71 |
(fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program); |
haftmann@37417 | 72 |
|
haftmann@41436 | 73 |
fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts) |
haftmann@37436 | 74 |
THEN' conclude_tac thy some_ss; |
haftmann@37417 | 75 |
|
haftmann@37417 | 76 |
end; |