okasaki

Okasaki's Purely Functional Data Structures
Log | Files | Refs | LICENSE

commit 40b2a0aeb92878a2acc851e167438c241114f03e
parent 5424bbee97d7a507eda8bdf47d91401bfe09b200
Author: Jared Tobin <jared@jtobin.io>
Date:   Tue, 14 Mar 2023 17:05:43 +0400

Add weight-biased leftist heap.

Diffstat:
Mlib/Okasaki/Heap/Leftist.hs | 47++++++++++++++++-------------------------------
Alib/Okasaki/Heap/Leftist/Weighted.hs | 123+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Mokasaki.cabal | 1+
3 files changed, 140 insertions(+), 31 deletions(-)

diff --git a/lib/Okasaki/Heap/Leftist.hs b/lib/Okasaki/Heap/Leftist.hs @@ -22,23 +22,21 @@ import Data.Monoid import Okasaki.Orphans () import Text.Show.Deriving --- NB todo +-- NB arguably better to use induction -- --- * verify heap property throughout --- * verify leftist property --- * implement weight-biased variant - --- exercise 3.1: prove right spine contains at most floor(log(n + 1)) elements +-- exercise 3.1: prove right spine contains at most floor(log(n + 1)) +-- elements -- --- * observe that rightmost-weighted binary tree satisfying leftist property --- is balanced +-- * observe that rightmost-weighted binary tree satisfying leftist +-- property is balanced -- * observe that right spine length is maximized in balanced case -- * observe that tree has depth floor(log(n + 1)) in balanced case. --- * therefore, right spine has at most floor(log(n + 1)) elements. (QED) +-- * therefore, right spine has at most floor(log(n + 1)) elements. +-- (QED) data HeapF a r = LeafF - | NodeF !Int !a r r + | NodeF !(Sum Int) !a r r deriving (Eq, Functor, Foldable, Traversable, Show) $(deriveShow1 ''HeapF) @@ -52,7 +50,7 @@ lef = Fix LeafF one :: a -> Heap a one x = Fix (NodeF 1 x lef lef) -ran :: Heap a -> Int +ran :: Heap a -> Sum Int ran h = case project h of LeafF -> 0 NodeF r _ _ _ -> r @@ -66,8 +64,8 @@ mix l r = apo lag (l, r) where (c, LeafF) -> fmap Left c (LeafF, d) -> fmap Left d (NodeF _ m c d, NodeF _ n e f) - | m <= n -> NodeF 0 m (Left c) (Right (d, b)) - | otherwise -> NodeF 0 n (Left e) (Right (a, f)) + | m <= n -> NodeF (ran d <> ran b) m (Left c) (Right (d, b)) + | otherwise -> NodeF (ran a <> ran f) n (Left e) (Right (a, f)) sor :: Heap a -> Heap a sor = cata $ \case @@ -76,8 +74,8 @@ sor = cata $ \case set :: a -> Heap a -> Heap a -> Heap a set m l r - | ran l >= ran r = Fix (NodeF (succ (ran r)) m l r) - | otherwise = Fix (NodeF (succ (ran l)) m r l) + | ran l >= ran r = Fix (NodeF (1 <> ran r) m l r) + | otherwise = Fix (NodeF (1 <> ran l) m r l) put :: Ord a => a -> Heap a -> Heap a put x = mer (one x) @@ -116,7 +114,7 @@ data BinF a r = EmpF | SinF !a | BinF r r - deriving (Eq, Functor, Foldable, Traversable, Show) + deriving Functor gas :: Ord a => [a] -> Heap a gas = hylo alg lag where @@ -132,25 +130,12 @@ gas = hylo alg lag where SinF a -> one a BinF l r -> mer l r -spy :: Ord a => a -> Heap a -> Maybe a -spy x = getLast . cata alg where - alg = \case - LeafF -> mempty - NodeF _ e l r - | x < e -> l - | otherwise -> Last (Just e) <> r - -haz :: Ord a => a -> Heap a -> Bool -haz x t = case spy x t of - Nothing -> False - Just s -> s == x - -- reference nodF :: a -> Heap a -> Heap a -> HeapF a (Heap a) nodF x l r - | ran l >= ran r = NodeF (succ (ran r)) x l r - | otherwise = NodeF (succ (ran l)) x r l + | ran l >= ran r = NodeF (1 <> ran r) x l r + | otherwise = NodeF (1 <> ran l) x r l nod :: a -> Heap a -> Heap a -> Heap a nod x l r = Fix (nodF x l r) diff --git a/lib/Okasaki/Heap/Leftist/Weighted.hs b/lib/Okasaki/Heap/Leftist/Weighted.hs @@ -0,0 +1,123 @@ +{-# OPTIONS_GHC -Wall -fno-warn-unused-top-binds #-} +{-# LANGUAGE TemplateHaskell #-} + +module Okasaki.Heap.Leftist.Weighted ( + HeapF(..) + , Heap + + , lef + , one + , put + , bot + , cut + + , oil + , gas + ) where + +import Data.Eq.Deriving (deriveEq1) +import Data.Fix hiding (cata, ana, hylo) +import Data.Functor.Foldable +import Data.Monoid +import Okasaki.Orphans () +import Text.Show.Deriving + +-- todo +-- +-- * prove right-spine of weight-biased leftist heap contains at most +-- floor(log(n + 1)) elements + +data HeapF a r = + LeafF + | NodeF !(Sum Int) !a r r + deriving (Eq, Functor, Foldable, Traversable, Show) + +$(deriveShow1 ''HeapF) +$(deriveEq1 ''HeapF) + +type Heap a = Fix (HeapF a) + +lef :: Heap a +lef = Fix LeafF + +one :: a -> Heap a +one x = Fix (NodeF 1 x lef lef) + +mer :: Ord a => Heap a -> Heap a -> Heap a +mer l r = apo lag (l, r) where + lag (a, b) = case (project a, project b) of + (c, LeafF) -> fmap Left c + (LeafF, d) -> fmap Left d + (NodeF p m c d, NodeF q n e f) + | m <= n && p >= q -> NodeF (p <> q) m (Left c) (Right (d, b)) + | m <= n && p < q -> NodeF (p <> q) m (Right (d, b)) (Left c) + | m > n && p >= q -> NodeF (p <> q) n (Left e) (Right (a, f)) + | otherwise -> NodeF (p <> q) n (Right (a, f)) (Left e) + +put :: Ord a => a -> Heap a -> Heap a +put x = mer (one x) + +bot :: Heap a -> Maybe a +bot h = case project h of + LeafF -> Nothing + NodeF _ b _ _ -> Just b + +cut :: Ord a => Heap a -> Heap a +cut h = case project h of + LeafF -> h + NodeF _ _ l r -> mer l r + +data BinF a r = + EmpF + | SinF !a + | BinF r r + deriving Functor + +gas :: Ord a => [a] -> Heap a +gas = hylo alg lag where + lag s = case project s of + Nil -> EmpF + Cons h [] -> SinF h + Cons {} -> + let (l, r) = splitAt (length s `div` 2) s + in BinF l r + + alg = \case + EmpF -> lef + SinF a -> one a + BinF l r -> mer l r + +oil :: Ord a => [a] -> Heap a +oil = cata $ \case + Nil -> lef + Cons h t -> put h t + +-- test + +-- (5) 1 +-- | \ +-- (3) 3 (1) 2 +-- | \ | \ +-- (2) 4 L L L +-- | \ +-- (1) 5 L +-- | \ +-- L L + +test0 :: Heap Int +test0 = gas [1..5] + +-- (5) 1 +-- | \ +-- (4) 2 L +-- | \ +-- (3) 3 L +-- | \ +-- (2) 4 L +-- | \ +-- (1) 5 L +-- | \ +-- L L + +test1 :: Heap Int +test1 = oil [1..5] diff --git a/okasaki.cabal b/okasaki.cabal @@ -25,6 +25,7 @@ library Okasaki.Orphans exposed-modules: Okasaki.Heap.Leftist + , Okasaki.Heap.Leftist.Weighted , Okasaki.Map , Okasaki.Stack.CPS , Okasaki.Tree