1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
{-# RULES
"fold/build" forall k z (g::forall b. (a->b->b) -> b -> b) .
foldr k z (build g) = g k z
"foldr/augment" forall k z xs (g::forall b. (a->b->b) -> b -> b) .
foldr k z (augment g xs) = g k (foldr k z xs)
"foldr/id" foldr (:) [] = \x -> x
"foldr/app" [1] forall ys. foldr (:) ys = \xs -> xs ++ ys
-- Only activate this from phase 1, because that's
-- when we disable the rule that expands (++) into foldr
-- The foldr/cons rule looks nice, but it can give disastrously
-- bloated code when commpiling
-- array (a,b) [(1,2), (2,2), (3,2), ...very long list... ]
-- i.e. when there are very very long literal lists
-- So I've disabled it for now. We could have special cases
-- for short lists, I suppose.
-- "foldr/cons" forall k z x xs. foldr k z (x:xs) = k x (foldr k z xs)
"foldr/single" forall k z x. foldr k z [x] = k x z
"foldr/nil" forall k z. foldr k z [] = z
"augment/build" forall (g::forall b. (a->b->b) -> b -> b)
(h::forall b. (a->b->b) -> b -> b) .
augment g (build h) = build (\c n -> g c (h c n))
"augment/nil" forall (g::forall b. (a->b->b) -> b -> b) .
augment g [] = build g
#-}
|
