CPS.hs (4360B)
1 {-# OPTIONS_GHC -Wall -fno-warn-unused-top-binds #-} 2 {-# LANGUAGE TemplateHaskell #-} 3 4 module Okasaki.Heap.Leftist.CPS where 5 6 import Data.Fix hiding (cata, ana, hylo) 7 import Data.Functor.Foldable 8 import Data.Monoid 9 import Okasaki.Orphans () 10 11 -- NB arguably better to use induction 12 -- 13 -- exercise 3.1: prove right spine contains at most floor(log(n + 1)) 14 -- elements 15 -- 16 -- * observe that rightmost-weighted binary tree satisfying leftist 17 -- property is balanced 18 -- * observe that right spine length is maximized in balanced case 19 -- * observe that tree has depth floor(log(n + 1)) in balanced case. 20 -- * therefore, right spine has at most floor(log(n + 1)) elements. 21 -- (QED) 22 23 newtype HeapF a r = HeapF (forall e. e -> (Sum Int -> a -> r -> r -> e) -> e) 24 deriving Functor 25 26 type Heap a = Fix (HeapF a) 27 28 lefF :: HeapF a r 29 lefF = HeapF const 30 31 lef :: Heap a 32 lef = Fix lefF 33 34 oneF :: a -> HeapF a (Heap b) 35 oneF x = HeapF (\_ c -> c 1 x lef lef) 36 37 one :: a -> Heap a 38 one = Fix . oneF 39 40 ran :: Heap a -> Sum Int 41 ran (project -> HeapF c) = c mempty b where 42 b r _ _ _ = r 43 44 -- mer :: Ord a => Heap a -> Heap a -> Heap a 45 -- mer l = sor . mix l 46 47 -- mix :: Ord a => Heap a -> Heap a -> Heap a 48 -- mix l r = apo lag (l, r) where 49 -- lag (a, b) = case (project a, project b) of 50 -- (c, LeafF) -> fmap Left c 51 -- (LeafF, d) -> fmap Left d 52 -- (NodeF _ m c d, NodeF _ n e f) 53 -- | m <= n -> NodeF (ran d <> ran b) m (Left c) (Right (d, b)) 54 -- | otherwise -> NodeF (ran a <> ran f) n (Left e) (Right (a, f)) 55 56 -- sor :: Heap a -> Heap a 57 -- sor = cata $ \case 58 -- LeafF -> lef 59 -- NodeF _ m l r -> set m l r 60 -- 61 -- set :: a -> Heap a -> Heap a -> Heap a 62 -- set m l r 63 -- | ran l >= ran r = Fix (NodeF (1 <> ran r) m l r) 64 -- | otherwise = Fix (NodeF (1 <> ran l) m r l) 65 -- 66 -- put :: Ord a => a -> Heap a -> Heap a 67 -- put x = mer (one x) 68 -- 69 -- -- exercise 3.2: direct insert 70 -- pat :: Ord a => a -> Heap a -> Heap a 71 -- pat x h = case project h of 72 -- LeafF -> one x 73 -- NodeF _ m a b -> 74 -- let (u, l) 75 -- | x <= m = (x, m) 76 -- | otherwise = (m, x) 77 -- 78 -- in uncurry (set u) (pot l a b) 79 -- where 80 -- pot :: Ord a => a -> Heap a -> Heap a -> (Heap a, Heap a) 81 -- pot l a b = case (project a, project b) of 82 -- (_, LeafF) -> (a, one l) 83 -- (LeafF, _) -> (b, one l) 84 -- (NodeF _ c _ _, NodeF _ d _ _) 85 -- | c > d -> (pat l a, b) 86 -- | otherwise -> (a, pat l b) 87 -- 88 -- bot :: Heap a -> Maybe a 89 -- bot h = case project h of 90 -- LeafF -> Nothing 91 -- NodeF _ b _ _ -> Just b 92 -- 93 -- cut :: Ord a => Heap a -> Heap a 94 -- cut h = case project h of 95 -- LeafF -> h 96 -- NodeF _ _ l r -> mer l r 97 -- 98 -- -- exercise 3.3: hylo gas 99 -- data BinF a r = 100 -- EmpF 101 -- | SinF !a 102 -- | BinF r r 103 -- deriving Functor 104 -- 105 -- gas :: Ord a => [a] -> Heap a 106 -- gas = hylo alg lag where 107 -- lag s = case project s of 108 -- Nil -> EmpF 109 -- Cons h [] -> SinF h 110 -- Cons {} -> 111 -- let (l, r) = splitAt (length s `div` 2) s 112 -- in BinF l r 113 -- 114 -- alg = \case 115 -- EmpF -> lef 116 -- SinF a -> one a 117 -- BinF l r -> mer l r 118 -- 119 -- wyt :: Heap a -> Int 120 -- wyt = getSum . cata alg where 121 -- alg = \case 122 -- LeafF -> mempty 123 -- NodeF _ _ l r -> 1 <> l <> r 124 -- 125 -- -- reference 126 -- 127 -- nodF :: a -> Heap a -> Heap a -> HeapF a (Heap a) 128 -- nodF x l r 129 -- | ran l >= ran r = NodeF (1 <> ran r) x l r 130 -- | otherwise = NodeF (1 <> ran l) x r l 131 -- 132 -- nod :: a -> Heap a -> Heap a -> Heap a 133 -- nod x l r = Fix (nodF x l r) 134 -- 135 -- mux :: Ord a => Heap a -> Heap a -> Heap a 136 -- mux l r = case (project l, project r) of 137 -- (_, LeafF) -> l 138 -- (LeafF, _) -> r 139 -- (NodeF _ m a b, NodeF _ n c d) 140 -- | m <= n -> nod m a (mux b r) 141 -- | otherwise -> nod n c (mux l d) 142 -- 143 -- oil :: Ord a => [a] -> Heap a 144 -- oil = cata $ \case 145 -- Nil -> lef 146 -- Cons h t -> put h t 147 -- 148 -- -- test 149 -- 150 -- -- (2) 1 151 -- -- | \ 152 -- -- (1) 2 (1) 3 153 -- -- | \ | \ 154 -- -- L L (1) 4 L 155 -- -- | \ 156 -- -- (1) 5 L 157 -- -- | \ 158 -- -- L L 159 -- 160 -- test0 :: Heap Int 161 -- test0 = gas [1..5] 162 -- 163 -- -- (1) 1 164 -- -- | \ 165 -- -- (1) 2 L 166 -- -- | \ 167 -- -- (1) 3 L 168 -- -- | \ 169 -- -- (1) 4 L 170 -- -- | \ 171 -- -- (1) 5 L 172 -- -- | \ 173 -- -- L L 174 -- 175 -- test1 :: Heap Int 176 -- test1 = oil [1..5]