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