equal
deleted
inserted
replaced
4 Connecting the simplifier and the code generator. |
4 Connecting the simplifier and the code generator. |
5 *) |
5 *) |
6 |
6 |
7 signature CODE_SIMP = |
7 signature CODE_SIMP = |
8 sig |
8 sig |
9 val no_frees_conv: conv -> conv |
|
10 val map_ss: (simpset -> simpset) -> theory -> theory |
9 val map_ss: (simpset -> simpset) -> theory -> theory |
11 val dynamic_eval_conv: conv |
10 val dynamic_eval_conv: conv |
12 val dynamic_eval_tac: theory -> int -> tactic |
11 val dynamic_eval_tac: theory -> int -> tactic |
13 val dynamic_eval_value: theory -> term -> term |
12 val dynamic_eval_value: theory -> term -> term |
14 val static_eval_conv: theory -> simpset option -> string list -> conv |
13 val static_eval_conv: theory -> simpset option -> string list -> conv |
16 val setup: theory -> theory |
15 val setup: theory -> theory |
17 end; |
16 end; |
18 |
17 |
19 structure Code_Simp : CODE_SIMP = |
18 structure Code_Simp : CODE_SIMP = |
20 struct |
19 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 |
20 |
38 (* dedicated simpset *) |
21 (* dedicated simpset *) |
39 |
22 |
40 structure Simpset = Theory_Data |
23 structure Simpset = Theory_Data |
41 ( |
24 ( |
66 fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss); |
49 fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss); |
67 |
50 |
68 |
51 |
69 (* evaluation with dynamic code context *) |
52 (* evaluation with dynamic code context *) |
70 |
53 |
71 val dynamic_eval_conv = Conv.tap_thy (fn thy => no_frees_conv (Code_Thingol.dynamic_eval_conv thy |
54 val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy |
72 (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program))); |
55 (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)); |
73 |
56 |
74 fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE; |
57 fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE; |
75 |
58 |
76 fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv o Thm.cterm_of thy; |
59 fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv o Thm.cterm_of thy; |
77 |
60 |
81 #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of); |
64 #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of); |
82 |
65 |
83 |
66 |
84 (* evaluation with static code context *) |
67 (* evaluation with static code context *) |
85 |
68 |
86 fun static_eval_conv thy some_ss consts = no_frees_conv |
69 fun static_eval_conv thy some_ss consts = |
87 (Code_Thingol.static_eval_conv_simple thy consts |
70 Code_Thingol.static_eval_conv_simple thy consts |
88 (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program)); |
71 (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program); |
89 |
72 |
90 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) |
73 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts) |
91 THEN' conclude_tac thy some_ss; |
74 THEN' conclude_tac thy some_ss; |
92 |
75 |
93 end; |
76 end; |