author | wenzelm |
Thu, 26 Aug 2010 16:34:10 +0200 | |
changeset 38759 | 37a9092de102 |
parent 38671 | febcd1733229 |
child 39475 | 9cc1ba3c5706 |
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 |
||
38759
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38671
diff
changeset
|
40 |
structure Simpset = Theory_Data |
37a9092de102
simplification/standardization of some theory data;
wenzelm
parents:
38671
diff
changeset
|
41 |
( |
37442 | 42 |
type T = simpset; |
43 |
val empty = empty_ss; |
|
44 |
fun extend ss = MetaSimplifier.inherit_context empty_ss ss; |
|
45 |
val merge = merge_ss; |
|
46 |
); |
|
47 |
||
48 |
val map_ss = Simpset.map; |
|
49 |
||
37461 | 50 |
fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy); |
51 |
||
37442 | 52 |
|
53 |
(* build simpset and conversion from program *) |
|
54 |
||
55 |
fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss = |
|
56 |
ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong) |
|
37449 | 57 |
| add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss = |
58 |
ss addsimps (map (fst o snd) classparam_instances) |
|
37442 | 59 |
| add_stmt _ ss = ss; |
60 |
||
37839 | 61 |
val add_program = Graph.fold (add_stmt o fst o snd); |
37442 | 62 |
|
63 |
fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite |
|
37461 | 64 |
(add_program program (simpset_default thy some_ss)); |
65 |
||
66 |
fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss); |
|
37442 | 67 |
|
68 |
||
69 |
(* evaluation with current code context *) |
|
70 |
||
38669
9ff76d0f0610
refined and unified naming convention for dynamic code evaluation techniques
haftmann
parents:
37839
diff
changeset
|
71 |
fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy |
37442 | 72 |
(fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)); |
73 |
||
38669
9ff76d0f0610
refined and unified naming convention for dynamic code evaluation techniques
haftmann
parents:
37839
diff
changeset
|
74 |
fun dynamic_eval_tac thy = CONVERSION (dynamic_eval_conv thy) THEN' conclude_tac thy NONE; |
37442 | 75 |
|
38669
9ff76d0f0610
refined and unified naming convention for dynamic code evaluation techniques
haftmann
parents:
37839
diff
changeset
|
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; |
37444 | 77 |
|
37442 | 78 |
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
|
79 |
(Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of))) |
37442 | 80 |
"simplification with code equations" |
38669
9ff76d0f0610
refined and unified naming convention for dynamic code evaluation techniques
haftmann
parents:
37839
diff
changeset
|
81 |
#> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of); |
37442 | 82 |
|
83 |
||
84 |
(* evaluation with freezed code context *) |
|
85 |
||
38671 | 86 |
fun static_eval_conv thy some_ss consts = no_frees_conv |
87 |
(Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss)); |
|
37442 | 88 |
|
38669
9ff76d0f0610
refined and unified naming convention for dynamic code evaluation techniques
haftmann
parents:
37839
diff
changeset
|
89 |
fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) |
37461 | 90 |
THEN' conclude_tac thy some_ss; |
37442 | 91 |
|
92 |
end; |