|
1 (* Title: HOL/ex/Code_Timing.thy |
|
2 Author: Florian Haftmann, TU Muenchen, 2016 |
|
3 *) |
|
4 |
|
5 section \<open>Examples for code generation timing measures\<close> |
|
6 |
|
7 theory Code_Timing |
|
8 imports "~~/src/HOL/Number_Theory/Eratosthenes" |
|
9 begin |
|
10 |
|
11 declare [[code_timing]] |
|
12 |
|
13 definition primes_upto :: "nat \<Rightarrow> int list" |
|
14 where |
|
15 "primes_upto = map int \<circ> Eratosthenes.primes_upto" |
|
16 |
|
17 definition "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 |
|
21 ML \<open> |
|
22 local |
|
23 val ctxt = @{context}; |
|
24 val consts = [@{const_name required_symbols}]; |
|
25 in |
|
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 }; |
|
30 val eval = Code_Evaluation.static_conv |
|
31 { ctxt = ctxt, consts = consts }; |
|
32 end; |
|
33 \<close> |
|
34 |
|
35 ML_val \<open> |
|
36 simp @{context} @{cterm "primes_upto 100"} |
|
37 \<close> |
|
38 |
|
39 ML_val \<open> |
|
40 simp @{context} @{cterm "primes_upto 200"} |
|
41 \<close> |
|
42 |
|
43 ML_val \<open> |
|
44 nbe @{context} @{cterm "primes_upto 200"} |
|
45 \<close> |
|
46 |
|
47 ML_val \<open> |
|
48 nbe @{context} @{cterm "primes_upto 400"} |
|
49 \<close> |
|
50 |
|
51 ML_val \<open> |
|
52 nbe @{context} @{cterm "primes_upto 600"} |
|
53 \<close> |
|
54 |
|
55 ML_val \<open> |
|
56 eval @{context} @{cterm "primes_upto 800"} |
|
57 \<close> |
|
58 |
|
59 ML_val \<open> |
|
60 eval @{context} @{cterm "primes_upto 1000"} |
|
61 \<close> |
|
62 |
|
63 end |