6 |
6 |
7 signature CODE_SIMP = |
7 signature CODE_SIMP = |
8 sig |
8 sig |
9 val map_ss: (simpset -> simpset) -> theory -> theory |
9 val map_ss: (simpset -> simpset) -> theory -> theory |
10 val dynamic_conv: conv |
10 val dynamic_conv: conv |
11 val dynamic_eval_tac: theory -> int -> tactic |
11 val dynamic_tac: theory -> int -> tactic |
12 val dynamic_value: theory -> term -> term |
12 val dynamic_value: theory -> term -> term |
13 val static_conv: theory -> simpset option -> string list -> conv |
13 val static_conv: theory -> simpset option -> string list -> conv |
14 val static_eval_tac: theory -> simpset option -> string list -> int -> tactic |
14 val static_tac: theory -> simpset option -> string list -> int -> tactic |
15 val setup: theory -> theory |
15 val setup: theory -> theory |
16 end; |
16 end; |
17 |
17 |
18 structure Code_Simp : CODE_SIMP = |
18 structure Code_Simp : CODE_SIMP = |
19 struct |
19 struct |
52 (* evaluation with dynamic code context *) |
52 (* evaluation with dynamic code context *) |
53 |
53 |
54 val dynamic_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy |
54 val dynamic_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_conv thy |
55 (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)); |
56 |
56 |
57 fun dynamic_eval_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE; |
57 fun dynamic_tac thy = CONVERSION dynamic_conv THEN' conclude_tac thy NONE; |
58 |
58 |
59 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv o Thm.cterm_of thy; |
59 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv o Thm.cterm_of thy; |
60 |
60 |
61 val setup = Method.setup (Binding.name "code_simp") |
61 val setup = Method.setup (Binding.name "code_simp") |
62 (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of))) |
62 (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o ProofContext.theory_of))) |
63 "simplification with code equations" |
63 "simplification with code equations" |
64 #> Value.add_evaluator ("simp", dynamic_value o ProofContext.theory_of); |
64 #> Value.add_evaluator ("simp", dynamic_value o ProofContext.theory_of); |
65 |
65 |
66 |
66 |
67 (* evaluation with static code context *) |
67 (* evaluation with static code context *) |
68 |
68 |
69 fun static_conv thy some_ss consts = |
69 fun static_conv thy some_ss consts = |
70 Code_Thingol.static_conv_simple thy consts |
70 Code_Thingol.static_conv_simple thy consts |
71 (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); |
72 |
72 |
73 fun static_eval_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts) |
73 fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts) |
74 THEN' conclude_tac thy some_ss; |
74 THEN' conclude_tac thy some_ss; |
75 |
75 |
76 end; |
76 end; |