equal
deleted
inserted
replaced
91 definition computation_future :: "unit \<Rightarrow> nat list \<times> rat" where |
91 definition computation_future :: "unit \<Rightarrow> nat list \<times> rat" where |
92 "computation_future = Debug.timing (STR ''overall computation'') |
92 "computation_future = Debug.timing (STR ''overall computation'') |
93 (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic |
93 (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic |
94 in (computation_primes (), Parallel.join c))" |
94 in (computation_primes (), Parallel.join c))" |
95 |
95 |
96 value [code] "computation_future ()" |
96 value "computation_future ()" |
97 |
97 |
98 definition computation_factorise :: "nat \<Rightarrow> nat list" where |
98 definition computation_factorise :: "nat \<Rightarrow> nat list" where |
99 "computation_factorise = Debug.timing (STR ''factorise'') factorise" |
99 "computation_factorise = Debug.timing (STR ''factorise'') factorise" |
100 |
100 |
101 definition computation_parallel :: "unit \<Rightarrow> nat list list" where |
101 definition computation_parallel :: "unit \<Rightarrow> nat list list" where |
102 "computation_parallel _ = Debug.timing (STR ''overall computation'') |
102 "computation_parallel _ = Debug.timing (STR ''overall computation'') |
103 (Parallel.map computation_factorise) [20000..<20100]" |
103 (Parallel.map computation_factorise) [20000..<20100]" |
104 |
104 |
105 value [code] "computation_parallel ()" |
105 value "computation_parallel ()" |
106 |
106 |
107 end |
107 end |
108 |
108 |