equal
deleted
inserted
replaced
8 sig |
8 sig |
9 val no_frees_conv: conv -> conv |
9 val no_frees_conv: conv -> conv |
10 val map_ss: (simpset -> simpset) -> theory -> theory |
10 val map_ss: (simpset -> simpset) -> theory -> theory |
11 val current_conv: theory -> conv |
11 val current_conv: theory -> conv |
12 val current_tac: theory -> int -> tactic |
12 val current_tac: theory -> int -> tactic |
|
13 val current_value: theory -> term -> term |
13 val make_conv: theory -> simpset option -> string list -> conv |
14 val make_conv: theory -> simpset option -> string list -> conv |
14 val make_tac: theory -> simpset option -> string list -> int -> tactic |
15 val make_tac: theory -> simpset option -> string list -> int -> tactic |
15 val setup: theory -> theory |
16 val setup: theory -> theory |
16 end; |
17 end; |
17 |
18 |
66 fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy |
67 fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy |
67 (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)); |
68 (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program)); |
68 |
69 |
69 fun current_tac thy = CONVERSION (current_conv thy); |
70 fun current_tac thy = CONVERSION (current_conv thy); |
70 |
71 |
|
72 fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy |
|
73 |
71 val setup = Method.setup (Binding.name "code_simp") |
74 val setup = Method.setup (Binding.name "code_simp") |
72 (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of)) |
75 (Scan.succeed (SIMPLE_METHOD' o current_tac o ProofContext.theory_of)) |
73 "simplification with code equations" |
76 "simplification with code equations" |
|
77 #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of); |
74 |
78 |
75 |
79 |
76 (* evaluation with freezed code context *) |
80 (* evaluation with freezed code context *) |
77 |
81 |
78 fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy |
82 fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy |