slightly more complete check of code generation for immutable arrays
authorhaftmann
Thu Mar 14 09:46:04 2019 +0100 (11 days ago)
changeset 699081bd74a0944b3
parent 69907 4343c1bfa52d
child 69909 5382f5691a11
slightly more complete check of code generation for immutable arrays
src/HOL/ex/IArray_Examples.thy
     1.1 --- a/src/HOL/ex/IArray_Examples.thy	Wed Mar 13 20:44:39 2019 +0100
     1.2 +++ b/src/HOL/ex/IArray_Examples.thy	Thu Mar 14 09:46:04 2019 +0100
     1.3 @@ -29,5 +29,13 @@
     1.4  lemma "sum (IArray [1,2,3,4,5,6,7,8,9::int]) = 45"
     1.5  by eval
     1.6  
     1.7 +definition partial_geometric_sum :: "'a::comm_ring_1 list \<Rightarrow> 'a"
     1.8 +  where "partial_geometric_sum xs = (let
     1.9 +    values = IArray xs;
    1.10 +    coefficients = IArray.of_fun of_nat (length xs)
    1.11 +  in sum_list (map (\<lambda>i. values !! i * coefficients !! i) [0..<IArray.length values]))"
    1.12 +
    1.13 +export_code partial_geometric_sum checking SML OCaml? Haskell? Scala
    1.14 +
    1.15  end
    1.16