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
```