2822 val _ = check_expected_modes preds options modes |
2822 val _ = check_expected_modes preds options modes |
2823 (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*) |
2823 (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*) |
2824 val _ = print_modes options thy' modes |
2824 val _ = print_modes options thy' modes |
2825 val _ = print_step options "Defining executable functions..." |
2825 val _ = print_step options "Defining executable functions..." |
2826 val thy'' = |
2826 val thy'' = |
2827 Output.cond_timeit true "Defining executable functions..." |
2827 Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..." |
2828 (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy' |
2828 (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy' |
2829 |> Theory.checkpoint) |
2829 |> Theory.checkpoint) |
2830 val _ = print_step options "Compiling equations..." |
2830 val _ = print_step options "Compiling equations..." |
2831 val compiled_terms = |
2831 val compiled_terms = |
2832 (*Output.cond_timeit true "Compiling equations...." (fn _ =>*) |
2832 Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ => |
2833 compile_preds options |
2833 compile_preds options |
2834 (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses |
2834 (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses) |
2835 val _ = print_compiled_terms options thy'' compiled_terms |
2835 val _ = print_compiled_terms options thy'' compiled_terms |
2836 val _ = print_step options "Proving equations..." |
2836 val _ = print_step options "Proving equations..." |
2837 val result_thms = |
2837 val result_thms = |
2838 Output.cond_timeit true "Proving equations...." (fn _ => |
2838 Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ => |
2839 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) |
2839 #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms) |
2840 val result_thms' = #add_code_equations (dest_steps steps) thy'' preds |
2840 val result_thms' = #add_code_equations (dest_steps steps) thy'' preds |
2841 (maps_modes result_thms) |
2841 (maps_modes result_thms) |
2842 val qname = #qname (dest_steps steps) |
2842 val qname = #qname (dest_steps steps) |
2843 val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute |
2843 val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute |
2844 (fn thm => Context.mapping (Code.add_eqn thm) I)))) |
2844 (fn thm => Context.mapping (Code.add_eqn thm) I)))) |
2845 val thy''' = |
2845 val thy''' = |
2846 Output.cond_timeit true "Setting code equations...." (fn _ => |
2846 Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ => |
2847 fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss |
2847 fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss |
2848 [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), |
2848 [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), |
2849 [attrib thy ])] thy)) |
2849 [attrib thy ])] thy)) |
2850 result_thms' thy'' |> Theory.checkpoint) |
2850 result_thms' thy'' |> Theory.checkpoint) |
2851 in |
2851 in |