# HG changeset patch
# User haftmann
# Date 1464269464 -7200
# Node ID c12845e8e80a664611f0b437709c2ff21be183f1
# Parent  72aaf69328fc627bf467bb9feacf07cfa0316386
examples and documentation for code generator time measurements

diff -r 72aaf69328fc -r c12845e8e80a NEWS
--- 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 
diff -r 72aaf69328fc -r c12845e8e80a src/HOL/ROOT
--- 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"
diff -r 72aaf69328fc -r c12845e8e80a src/HOL/ex/Code_Timing.thy
--- /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