okasaki

Okasaki's Purely Functional Data Structures
git clone git://git.jtobin.io/okasaki.git
Log | Files | Refs | LICENSE

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]