--- a/NEWS Thu May 26 15:27:50 2016 +0200
+++ b/NEWS Thu May 26 15:31:04 2016 +0200
@@ -91,6 +91,13 @@
Isabelle2016). INCOMPATIBILITY, use "standard" instead.
+*** Pure ***
+
+* Code generator: config option "code_timinger" triggers
+measurements of different phases of code generation. See
+src/HOL/ex/Code_Timing.thy for examples.
+
+
*** HOL ***
* Probability/Random_Permutations.thy contains some theory about
--- a/src/HOL/ROOT Thu May 26 15:27:50 2016 +0200
+++ b/src/HOL/ROOT Thu May 26 15:31:04 2016 +0200
@@ -619,6 +619,7 @@
Erdoes_Szekeres
Sum_of_Powers
Sudoku
+ Code_Timing
theories [skip_proofs = false]
Meson_Test
document_files "root.bib" "root.tex"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Code_Timing.thy Thu May 26 15:31:04 2016 +0200
@@ -0,0 +1,63 @@
+(* Title: HOL/ex/Code_Timing.thy
+ Author: Florian Haftmann, TU Muenchen, 2016
+*)
+
+section \<open>Examples for code generation timing measures\<close>
+
+theory Code_Timing
+imports "~~/src/HOL/Number_Theory/Eratosthenes"
+begin
+
+declare [[code_timing]]
+
+definition primes_upto :: "nat \<Rightarrow> int list"
+where
+ "primes_upto = map int \<circ> Eratosthenes.primes_upto"
+
+definition "required_symbols _ = (primes_upto, 0 :: nat, Suc, 1 :: nat,
+ numeral :: num \<Rightarrow> nat, Num.One, Num.Bit0, Num.Bit1,
+ Code_Evaluation.TERM_OF_EQUAL :: int list itself)"
+
+ML \<open>
+local
+ val ctxt = @{context};
+ val consts = [@{const_name required_symbols}];
+in
+ val simp = Code_Simp.static_conv
+ { ctxt = ctxt, consts = consts, simpset = NONE };
+ val nbe = Nbe.static_conv
+ { ctxt = ctxt, consts = consts };
+ val eval = Code_Evaluation.static_conv
+ { ctxt = ctxt, consts = consts };
+end;
+\<close>
+
+ML_val \<open>
+ simp @{context} @{cterm "primes_upto 100"}
+\<close>
+
+ML_val \<open>
+ simp @{context} @{cterm "primes_upto 200"}
+\<close>
+
+ML_val \<open>
+ nbe @{context} @{cterm "primes_upto 200"}
+\<close>
+
+ML_val \<open>
+ nbe @{context} @{cterm "primes_upto 400"}
+\<close>
+
+ML_val \<open>
+ nbe @{context} @{cterm "primes_upto 600"}
+\<close>
+
+ML_val \<open>
+ eval @{context} @{cterm "primes_upto 800"}
+\<close>
+
+ML_val \<open>
+ eval @{context} @{cterm "primes_upto 1000"}
+\<close>
+
+end