1(*  Title: HOL/ex/Code_Timing.thy
2    Author: Florian Haftmann, TU Muenchen, 2016
3*)
4
5section \<open>Examples for code generation timing measures\<close>
6
7theory Code_Timing
8imports "HOL-Number_Theory.Eratosthenes"
9begin
10
11declare [[code_timing]]
12
13definition primes_upto :: "nat \<Rightarrow> int list"
14where
15  "primes_upto = map int \<circ> Eratosthenes.primes_upto"
16
17definition "required_symbols _ = (primes_upto, 0 :: nat, Suc, 1 :: nat,
18  numeral :: num \<Rightarrow> nat, Num.One, Num.Bit0, Num.Bit1,
19  Code_Evaluation.TERM_OF_EQUAL :: int list itself)"
20
21ML \<open>
22local
23  val ctxt = \<^context>;
24  val consts = [\<^const_name>\<open>required_symbols\<close>];
25in
26  val simp = Code_Simp.static_conv
27    { ctxt = ctxt, consts = consts, simpset = NONE };
28  val nbe = Nbe.static_conv
29    { ctxt = ctxt, consts = consts };
30end;
31\<close>
32
33ML_val \<open>
34  simp \<^context> \<^cterm>\<open>primes_upto 100\<close>
35\<close>
36
37ML_val \<open>
38  simp \<^context> \<^cterm>\<open>primes_upto 200\<close>
39\<close>
40
41ML_val \<open>
42  nbe \<^context> \<^cterm>\<open>primes_upto 200\<close>
43\<close>
44
45ML_val \<open>
46  nbe \<^context> \<^cterm>\<open>primes_upto 400\<close>
47\<close>
48
49ML_val \<open>
50  nbe \<^context> \<^cterm>\<open>primes_upto 600\<close>
51\<close>
52
53end
54