src/HOL/ex/Code_Timing.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 63165 c12845e8e80a
child 65062 dc746d43f40e
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title: HOL/ex/Code_Timing.thy
     2     Author: Florian Haftmann, TU Muenchen, 2016
     3 *)
     4 
     5 section \<open>Examples for code generation timing measures\<close>
     6 
     7 theory Code_Timing
     8 imports "~~/src/HOL/Number_Theory/Eratosthenes"
     9 begin
    10 
    11 declare [[code_timing]]
    12 
    13 definition primes_upto :: "nat \<Rightarrow> int list"
    14 where
    15   "primes_upto = map int \<circ> Eratosthenes.primes_upto"
    16 
    17 definition "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 
    21 ML \<open>
    22 local
    23   val ctxt = @{context};
    24   val consts = [@{const_name required_symbols}];
    25 in
    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 };
    30   val eval = Code_Evaluation.static_conv
    31     { ctxt = ctxt, consts = consts };
    32 end;
    33 \<close>
    34 
    35 ML_val \<open>
    36   simp @{context} @{cterm "primes_upto 100"}
    37 \<close>
    38 
    39 ML_val \<open>
    40   simp @{context} @{cterm "primes_upto 200"}
    41 \<close>
    42 
    43 ML_val \<open>
    44   nbe @{context} @{cterm "primes_upto 200"}
    45 \<close>
    46 
    47 ML_val \<open>
    48   nbe @{context} @{cterm "primes_upto 400"}
    49 \<close>
    50 
    51 ML_val \<open>
    52   nbe @{context} @{cterm "primes_upto 600"}
    53 \<close>
    54 
    55 ML_val \<open>
    56   eval @{context} @{cterm "primes_upto 800"}
    57 \<close>
    58 
    59 ML_val \<open>
    60   eval @{context} @{cterm "primes_upto 1000"}
    61 \<close>
    62 
    63 end