author | wenzelm |
Tue, 05 Nov 2019 14:28:00 +0100 | |
changeset 71047 | 87c132cf5860 |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/Code_Timing.thy |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
2 |
Author: Florian Haftmann, TU Muenchen, 2016 |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
3 |
*) |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
4 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
5 |
section \<open>Examples for code generation timing measures\<close> |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
6 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
7 |
theory Code_Timing |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
65062
diff
changeset
|
8 |
imports "HOL-Number_Theory.Eratosthenes" |
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
9 |
begin |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
10 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
11 |
declare [[code_timing]] |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
12 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
13 |
definition primes_upto :: "nat \<Rightarrow> int list" |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
14 |
where |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
15 |
"primes_upto = map int \<circ> Eratosthenes.primes_upto" |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
16 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
17 |
definition "required_symbols _ = (primes_upto, 0 :: nat, Suc, 1 :: nat, |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
18 |
numeral :: num \<Rightarrow> nat, Num.One, Num.Bit0, Num.Bit1, |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
19 |
Code_Evaluation.TERM_OF_EQUAL :: int list itself)" |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
20 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
21 |
ML \<open> |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
22 |
local |
69597 | 23 |
val ctxt = \<^context>; |
24 |
val consts = [\<^const_name>\<open>required_symbols\<close>]; |
|
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
25 |
in |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
26 |
val simp = Code_Simp.static_conv |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
27 |
{ ctxt = ctxt, consts = consts, simpset = NONE }; |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
28 |
val nbe = Nbe.static_conv |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
29 |
{ ctxt = ctxt, consts = consts }; |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
30 |
end; |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
31 |
\<close> |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
32 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
33 |
ML_val \<open> |
69597 | 34 |
simp \<^context> \<^cterm>\<open>primes_upto 100\<close> |
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
35 |
\<close> |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
36 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
37 |
ML_val \<open> |
69597 | 38 |
simp \<^context> \<^cterm>\<open>primes_upto 200\<close> |
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
39 |
\<close> |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
40 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
41 |
ML_val \<open> |
69597 | 42 |
nbe \<^context> \<^cterm>\<open>primes_upto 200\<close> |
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
43 |
\<close> |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
44 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
45 |
ML_val \<open> |
69597 | 46 |
nbe \<^context> \<^cterm>\<open>primes_upto 400\<close> |
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
47 |
\<close> |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
48 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
49 |
ML_val \<open> |
69597 | 50 |
nbe \<^context> \<^cterm>\<open>primes_upto 600\<close> |
63165
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
51 |
\<close> |
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
52 |
|
c12845e8e80a
examples and documentation for code generator time measurements
haftmann
parents:
diff
changeset
|
53 |
end |