9 val map_ss: (Proof.context -> Proof.context) -> theory -> theory |
9 val map_ss: (Proof.context -> Proof.context) -> theory -> theory |
10 val dynamic_conv: theory -> conv |
10 val dynamic_conv: theory -> conv |
11 val dynamic_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_tac: theory -> simpset option -> string list -> int -> tactic |
14 val static_tac: theory -> simpset option -> string list -> Proof.context -> 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 |
28 val merge = merge_ss; |
28 val merge = merge_ss; |
29 ); |
29 ); |
30 |
30 |
31 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy; |
31 fun map_ss f thy = Simpset.map (simpset_map (Proof_Context.init_global thy) f) thy; |
32 |
32 |
33 fun simpset_default thy = Simplifier.global_context thy o the_default (Simpset.get thy); |
33 fun simpset_default thy = the_default (Simpset.get thy); |
34 |
34 |
35 |
35 |
36 (* build simpset and conversion from program *) |
36 (* build simpset and conversion from program *) |
37 |
37 |
38 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss = |
38 fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss = |
39 ss addsimps (map_filter (fst o snd)) eqs |
39 ss |
|
40 |> fold Simplifier.add_simp ((map_filter (fst o snd)) eqs) |
40 |> fold Simplifier.add_cong (the_list some_cong) |
41 |> fold Simplifier.add_cong (the_list some_cong) |
41 | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss = |
42 | add_stmt (Code_Thingol.Classinst { inst_params, ... }) ss = |
42 ss addsimps (map (fst o snd) inst_params) |
43 ss |
|
44 |> fold Simplifier.add_simp (map (fst o snd) inst_params) |
43 | add_stmt _ ss = ss; |
45 | add_stmt _ ss = ss; |
44 |
46 |
45 val add_program = Graph.fold (add_stmt o fst o snd); |
47 val add_program = Graph.fold (add_stmt o fst o snd); |
46 |
48 |
47 fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite |
49 fun simpset_program thy some_ss program = |
48 (add_program program (simpset_default thy some_ss)); |
50 simpset_map (Proof_Context.init_global thy) (add_program program) (simpset_default thy some_ss); |
49 |
51 |
50 fun conclude_tac thy some_ss = Simplifier.full_simp_tac (simpset_default thy some_ss); |
52 fun lift_ss_conv f ss ct = f (Simplifier.put_simpset ss (Proof_Context.init_global (theory_of_cterm ct))) ct; |
|
53 |
|
54 fun rewrite_modulo thy some_ss program = |
|
55 lift_ss_conv Simplifier.full_rewrite (simpset_program thy some_ss program); |
|
56 |
|
57 fun conclude_tac thy some_ss = |
|
58 let |
|
59 val ss = simpset_default thy some_ss; |
|
60 in fn ctxt => Simplifier.full_simp_tac (Simplifier.put_simpset ss ctxt) end; |
51 |
61 |
52 |
62 |
53 (* evaluation with dynamic code context *) |
63 (* evaluation with dynamic code context *) |
54 |
64 |
55 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy |
65 fun dynamic_conv thy = Code_Thingol.dynamic_conv thy |
56 (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program); |
66 (fn _ => fn program => fn _ => fn _ => rewrite_modulo thy NONE program); |
57 |
67 |
58 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE; |
68 fun dynamic_tac thy = CONVERSION (dynamic_conv thy) THEN' conclude_tac thy NONE (Proof_Context.init_global thy); |
59 |
69 |
60 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy; |
70 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy; |
61 |
71 |
62 val setup = |
72 val setup = |
63 Method.setup @{binding code_simp} |
73 Method.setup @{binding code_simp} |
70 |
80 |
71 fun static_conv thy some_ss consts = |
81 fun static_conv thy some_ss consts = |
72 Code_Thingol.static_conv_simple thy consts |
82 Code_Thingol.static_conv_simple thy consts |
73 (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program); |
83 (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program); |
74 |
84 |
75 fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts) |
85 fun static_tac thy some_ss consts = |
76 THEN' conclude_tac thy some_ss; |
86 let |
|
87 val conv = static_conv thy some_ss consts; |
|
88 val tac = conclude_tac thy some_ss; |
|
89 in fn ctxt => CONVERSION conv THEN' tac ctxt end; |
77 |
90 |
78 end; |
91 end; |