1 (* Title: Tools/Code/code_simp.ML
2 Author: Florian Haftmann, TU Muenchen
4 Connecting the simplifier and the code generator.
9 val map_ss: (simpset -> simpset) -> theory -> theory
10 val dynamic_conv: theory -> conv
11 val dynamic_tac: theory -> int -> tactic
12 val dynamic_value: theory -> term -> term
13 val static_conv: theory -> simpset option -> string list -> conv
14 val static_tac: theory -> simpset option -> string list -> int -> tactic
15 val setup: theory -> theory
18 structure Code_Simp : CODE_SIMP =
21 (* dedicated simpset *)
23 structure Simpset = Theory_Data
27 fun extend ss = Simplifier.inherit_context empty_ss ss;
31 val map_ss = Simpset.map;
33 fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy);
36 (* build simpset and conversion from program *)
38 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
39 ss addsimps (map_filter (fst o snd)) eqs
40 |> fold Simplifier.add_cong (the_list some_cong)
41 | add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
42 ss addsimps (map (fst o snd) classparam_instances)
45 val add_program = Graph.fold (add_stmt o fst o snd);
47 fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite
48 (add_program program (simpset_default thy some_ss));
50 fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss);
53 (* evaluation with dynamic code context *)
55 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy
56 (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program);
58 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE;
60 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
63 Method.setup @{binding code_simp}
64 (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
65 "simplification with code equations"
66 #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
69 (* evaluation with static code context *)
71 fun static_conv thy some_ss consts =
72 Code_Thingol.static_conv_simple thy consts
73 (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
75 fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
76 THEN' conclude_tac thy some_ss;