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