Theory Stream_Fusion_Examples
section ‹Examples and test cases for stream fusion›
theory Stream_Fusion_Examples imports Stream_Fusion_LList begin
lemma fixes rhs z
defines "rhs ≡ nth_cons (flatten (λs'. s') (upto_prod 17) (upto_prod z)) (2, None) 8"
shows "nth (List.maps (λx. upto x 17) (upto 2 z)) 8 = rhs"
using [[simproc add: stream_fusion, stream_fusion_trace]]
apply(simp del: id_apply)
by(unfold rhs_def) rule
lemma fixes rhs z
defines "rhs ≡ nth_cons (flatten (λs. (s, 1)) (fix_gen (λx. upto_prod (id x))) (upto_prod z)) (2, None) 8"
shows "nth (List.maps (λx. upto 1 (id x)) (upto 2 z)) 8 = rhs"
using [[simproc add: stream_fusion, stream_fusion_trace]]
apply(simp del: id_apply)
by(unfold rhs_def) rule
lemma fixes rhs n
defines "rhs ≡ List.maps (λx. [Suc 0..<sum_list_cons (replicate_prod x) x]) [2..<n]"
shows "(concat (map (λx. [1..<sum_list (replicate x x)]) [2..<n])) = rhs"
using [[simproc add: stream_fusion, stream_fusion_trace]]
apply(simp add: concat_map_maps)
by(unfold rhs_def) rule
subsection ‹Micro-benchmarks from Farmer et al. \<^cite>‹"FarmerHoenerGill2014PEPM"››
definition test_enum :: "nat ⇒ nat"
where "test_enum n = foldl (+) 0 (List.maps (λx. upt 1 (id x)) (upt 1 n))"
definition test_nested :: "nat ⇒ nat"
where "test_nested n = foldl (+) 0 (List.maps (λx. List.maps (λy. upt y x) (upt 1 x)) (upt 1 n))"
definition test_merge :: "integer ⇒ nat"
where "test_merge n = foldl (+) 0 (List.maps (λx. if 2 dvd x then upt 1 x else upt 2 x) (upt 1 (nat_of_integer n)))"
text ‹
This rule performs the merge operation from \<^cite>‹‹\S 5.2› in "FarmerHoenerGill2014PEPM"› for ‹if›.
In general, we would also need it for all case operators.
›
lemma unstream_if [stream_fusion]:
"unstream (if b then g else g') (if b then s else s') =
(if b then unstream g s else unstream g' s')"
by simp
lemma if_same [code_unfold]: "(if b then x else x) = x"
by simp
code_thms test_enum
code_thms test_nested
code_thms test_merge
subsection ‹Test stream fusion in the code generator›
definition fuse_test :: integer
where "fuse_test =
integer_of_int (lhd (lfilter (λx. x < 1) (lappend (lmap (λx. x + 1) (llist_of (map (λx. if x = 0 then undefined else x) [-3..5]))) (repeat 3))))"
ML_val ‹val ~2 = @{code fuse_test}›
end