equal
deleted
inserted
replaced
29 val merge = merge_ss; |
29 val merge = merge_ss; |
30 ); |
30 ); |
31 |
31 |
32 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy; |
32 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy; |
33 |
33 |
34 fun simpset_default thy = the_default (Simpset.get thy); |
34 fun simpset_default thy some_ss = the_default (Simpset.get thy) some_ss; |
|
35 |
|
36 fun simp_ctxt_default thy some_ss = |
|
37 Proof_Context.init_global thy |
|
38 |> put_simpset (simpset_default thy some_ss); |
35 |
39 |
36 |
40 |
37 (* diagnostic *) |
41 (* diagnostic *) |
38 |
42 |
39 val trace = Attrib.setup_config_bool @{binding "code_simp_trace"} (K false); |
43 val trace = Attrib.setup_config_bool @{binding "code_simp_trace"} (K false); |
57 |> fold Simplifier.add_simp (map (fst o snd) inst_params) |
61 |> fold Simplifier.add_simp (map (fst o snd) inst_params) |
58 | add_stmt _ ss = ss; |
62 | add_stmt _ ss = ss; |
59 |
63 |
60 val add_program = Graph.fold (add_stmt o fst o snd); |
64 val add_program = Graph.fold (add_stmt o fst o snd); |
61 |
65 |
62 fun simpset_program thy some_ss program = |
66 fun simp_ctxt_program thy some_ss program = |
63 simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss); |
67 simp_ctxt_default thy some_ss |
64 |
68 |> add_program program; |
65 fun lift_ss_conv f ss ct = (* FIXME proper context!? *) |
|
66 f (Proof_Context.init_global (theory_of_cterm ct) |> put_simpset ss |> set_trace) ct; |
|
67 |
69 |
68 fun rewrite_modulo thy some_ss program = |
70 fun rewrite_modulo thy some_ss program = |
69 lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program); |
71 Simplifier.full_rewrite (simp_ctxt_program thy some_ss program |> set_trace); |
70 |
72 |
71 fun conclude_tac thy some_ss = |
73 fun conclude_tac thy some_ss = |
72 let |
74 Simplifier.full_simp_tac o Simplifier.put_simpset (simpset_default thy some_ss); |
73 val ss = simpset_default thy some_ss; |
|
74 in fn ctxt => Simplifier.full_simp_tac (Simplifier.put_simpset ss ctxt) end; |
|
75 |
75 |
76 |
76 |
77 (* evaluation with dynamic code context *) |
77 (* evaluation with dynamic code context *) |
78 |
78 |
79 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy |
79 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy |