37442
|
1 |
(* Title: Tools/code/code_simp.ML
|
|
2 |
Author: Florian Haftmann, TU Muenchen
|
|
3 |
|
|
4 |
Connecting the simplifier and the code generator.
|
|
5 |
*)
|
|
6 |
|
|
7 |
signature CODE_SIMP =
|
|
8 |
sig
|
|
9 |
val no_frees_conv: conv -> conv
|
|
10 |
val map_ss: (simpset -> simpset) -> theory -> theory
|
|
11 |
val current_conv: theory -> conv
|
|
12 |
val current_tac: theory -> int -> tactic
|
37444
|
13 |
val current_value: theory -> term -> term
|
37442
|
14 |
val make_conv: theory -> simpset option -> string list -> conv
|
|
15 |
val make_tac: theory -> simpset option -> string list -> int -> tactic
|
|
16 |
val setup: theory -> theory
|
|
17 |
end;
|
|
18 |
|
|
19 |
structure Code_Simp : CODE_SIMP =
|
|
20 |
struct
|
|
21 |
|
|
22 |
(* avoid free variables during conversion *)
|
|
23 |
|
|
24 |
fun no_frees_conv conv ct =
|
|
25 |
let
|
|
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));
|
|
30 |
in
|
|
31 |
ct
|
|
32 |
|> fold_rev Thm.cabs frees
|
|
33 |
|> conv
|
|
34 |
|> fold apply_beta frees
|
|
35 |
end;
|
|
36 |
|
|
37 |
|
|
38 |
(* dedicated simpset *)
|
|
39 |
|
|
40 |
structure Simpset = Theory_Data (
|
|
41 |
type T = simpset;
|
|
42 |
val empty = empty_ss;
|
|
43 |
fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
|
|
44 |
val merge = merge_ss;
|
|
45 |
);
|
|
46 |
|
|
47 |
val map_ss = Simpset.map;
|
|
48 |
|
|
49 |
|
|
50 |
(* build simpset and conversion from program *)
|
|
51 |
|
|
52 |
fun add_stmt (Code_Thingol.Fun (_, ((_, eqs), some_cong))) ss =
|
|
53 |
ss addsimps (map_filter (fst o snd)) eqs addcongs (the_list some_cong)
|
37449
|
54 |
| add_stmt (Code_Thingol.Classinst (_, (_, (classparam_instances, _)))) ss =
|
|
55 |
ss addsimps (map (fst o snd) classparam_instances)
|
37442
|
56 |
| add_stmt _ ss = ss;
|
|
57 |
|
|
58 |
val add_program = Graph.fold (add_stmt o fst o snd)
|
|
59 |
|
|
60 |
fun rewrite_modulo thy some_ss program = Simplifier.full_rewrite
|
|
61 |
(add_program program (Simplifier.global_context thy
|
|
62 |
(the_default (Simpset.get thy) some_ss)));
|
|
63 |
|
|
64 |
|
|
65 |
(* evaluation with current code context *)
|
|
66 |
|
|
67 |
fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy
|
|
68 |
(fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
|
|
69 |
|
|
70 |
fun current_tac thy = CONVERSION (current_conv thy);
|
|
71 |
|
37444
|
72 |
fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy
|
|
73 |
|
37442
|
74 |
val setup = Method.setup (Binding.name "code_simp")
|
|
75 |
(Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of))
|
|
76 |
"simplification with code equations"
|
37444
|
77 |
#> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
|
37442
|
78 |
|
|
79 |
|
|
80 |
(* evaluation with freezed code context *)
|
|
81 |
|
|
82 |
fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
|
|
83 |
((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
|
|
84 |
|
|
85 |
fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts);
|
|
86 |
|
|
87 |
end;
|