# Theory Code_Timing

theory Code_Timing
imports Eratosthenes
```(*  Title: HOL/ex/Code_Timing.thy
Author: Florian Haftmann, TU Muenchen, 2016
*)

section ‹Examples for code generation timing measures›

theory Code_Timing
imports "HOL-Number_Theory.Eratosthenes"
begin

declare [[code_timing]]

definition primes_upto :: "nat ⇒ int list"
where
"primes_upto = map int ∘ Eratosthenes.primes_upto"

definition "required_symbols _ = (primes_upto, 0 :: nat, Suc, 1 :: nat,
numeral :: num ⇒ nat, Num.One, Num.Bit0, Num.Bit1,
Code_Evaluation.TERM_OF_EQUAL :: int list itself)"

ML ‹
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 };
end;
›

ML_val ‹
simp @{context} @{cterm "primes_upto 100"}
›

ML_val ‹
simp @{context} @{cterm "primes_upto 200"}
›

ML_val ‹
nbe @{context} @{cterm "primes_upto 200"}
›

ML_val ‹
nbe @{context} @{cterm "primes_upto 400"}
›

ML_val ‹
nbe @{context} @{cterm "primes_upto 600"}
›

end
```