1 (* Title: Tools/Code/code_simp.ML
2 Author: Florian Haftmann, TU Muenchen
4 Connecting the simplifier and the code generator.
9 val no_frees_conv: conv -> conv
10 val map_ss: (simpset -> simpset) -> theory -> theory
11 val dynamic_eval_conv: conv
12 val dynamic_eval_tac: theory -> int -> tactic
13 val dynamic_eval_value: theory -> term -> term
14 val static_eval_conv: theory -> simpset option -> string list -> conv
15 val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
16 val setup: theory -> theory
19 structure Code_Simp : CODE_SIMP =
22 (* avoid free variables during conversion *)
24 fun no_frees_conv conv ct =
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));
32 |> fold_rev Thm.cabs frees
34 |> fold apply_beta frees
38 (* dedicated simpset *)
40 structure Simpset = Theory_Data
44 fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
48 val map_ss = Simpset.map;
50 fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy);
53 (* build simpset and conversion from program *)
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)
57 | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
58 ss addsimps (map (fst o snd) classparam_instances)
61 val add_program = Graph.fold (add_stmt o fst o snd);
63 fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite
64 (add_program program (simpset_default thy some_ss));
66 fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss);
69 (* evaluation with dynamic code context *)
71 val dynamic_eval_conv = Conv.tap_thy (fn thy => no_frees_conv (Code_Thingol.dynamic_eval_conv thy
72 (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)));
74 fun dynamic_eval_tac thy = CONVERSION dynamic_eval_conv THEN' conclude_tac thy NONE;
76 fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv o Thm.cterm_of thy;
78 val setup = Method.setup (Binding.name "code_simp")
79 (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
80 "simplification with code equations"
81 #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of);
84 (* evaluation with static code context *)
86 fun static_eval_conv thy some_ss consts = no_frees_conv
87 (Code_Thingol.static_eval_conv_simple thy consts
88 (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program));
90 fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
91 THEN' conclude_tac thy some_ss;