liquidhaskell-0.8.0.2: tests/todo/AbsRefNameClash.hs
-----------------------------------------------------------------------
-- Weight-Biased Leftist Heap, verified using LiquidHaskell -----------
-----------------------------------------------------------------------
-- ORIGINAL SOURCE ----------------------------------------------------
-----------------------------------------------------------------------
-- Copyright: 2014, Jan Stolarek, Politechnika Łódzka --
-- --
-- License: See LICENSE file in root of the repo --
-- Repo address: https://github.com/jstolarek/dep-typed-wbl-heaps-hs --
-- --
-- Basic implementation of weight-biased leftist heap. No proofs --
-- and no dependent types. Uses a two-pass merging algorithm. --
-----------------------------------------------------------------------
{-@ LIQUID "--no-termination" @-}
module WBL where
type Priority = Int
type Rank = Int
type Nat = Int
data Heap a = Empty | Node { pri :: a
, rnk :: Rank
, left :: Heap a
, right :: Heap a
}
{-@ data Heap a <p :: a -> a -> Prop> =
Empty | Node { pri :: a
, rnk :: Nat
, left :: {v: Heap<p> (a<p pri>) | ValidRank v}
, right :: {v: Heap<p> (a<p pri>) | ValidRank v}
}
@-}
{-@ predicate ValidRank V = okRank V && realRank V = rank V @-}
{-@ type PHeap a = {v:OHeap a | ValidRank v} @-}
{-@ type OHeap a = Heap <{\root v -> root <= v}> a @-}
{-@ measure okRank :: Heap a -> Prop
okRank (Empty) = true
okRank (Node p k l r) = (realRank l >= realRank r && k = 1 + realRank l + realRank r )
@-}
{-@ measure realRank :: Heap a -> Int
realRank (Empty) = 0
realRank (Node p k l r) = (1 + realRank l + realRank r)
@-}
{-@ measure rank @-}
{-@ rank :: h:PHeap a -> {v:Nat | v = realRank h} @-}
rank Empty = 0
rank (Node _ r _ _) = r
-- Creates heap containing a single element with a given Priority
{-@ singleton :: a -> PHeap a @-}
singleton p = Node p 1 Empty Empty
-- Note [Two-pass merging algorithm]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- We use a two-pass implementation of merging algorithm. One pass,
-- implemented by merge, performs merging in a top-down manner. Second
-- one, implemented by makeT, ensures that rank invariant of weight
-- biased leftist tree is not violated after merging.
--
-- Notation:
--
-- h1, h2 - heaps being merged
-- p1, p2 - priority of root element in h1 and h2
-- l1 - left subtree in the first heap
-- r1 - right subtree in the first heap
-- l2 - left subtree in the second heap
-- r2 - right subtree in the second heap
--
-- Merge function analyzes four cases. Two of them are base cases:
--
-- a) h1 is empty - return h2
--
-- b) h2 is empty - return h1
--
-- The other two cases form the inductive definition of merge:
--
-- c) priority p1 is higher than p2 - p1 becomes new root, l1
-- becomes its one child and result of merging r1 with h2
-- becomes the other child:
--
-- p1
-- / \
-- / \
-- l1 r1+h2 -- here "+" denotes merging
--
-- d) priority p2 is higher than p2 - p2 becomes new root, l2
-- becomes its one child and result of merging r2 with h1
-- becomes the other child.
--
-- p2
-- / \
-- / \
-- l2 r2+h1
--
-- Note that there is no guarantee that rank of r1+h2 (or r2+h1) will
-- be smaller than rank of l1 (or l2). To ensure that merged heap
-- maintains the rank invariant we pass both childred - ie. either l1
-- and r1+h2 or l2 and r2+h1 - to makeT, which creates a new node by
-- inspecting sizes of children and swapping them if necessary.
-- makeT takes an element (Priority) and two heaps (trees). It
-- constructs a new heap with element at the root and two heaps as
-- children. makeT ensures that WBL heap rank invariant is maintained
-- in the newly created tree by reversing left and right subtrees when
-- necessary (note the inversed r and l in the False alternative of
-- case expression).
{-@ makeT :: p:a -> h1:PHeap {v:a | p <= v} -> h2:PHeap {v:a | p <= v}
-> {v:PHeap a | realRank v = 1 + realRank h1 + realRank h2} @-}
makeT p l r = case rank l >= rank r of
True -> Node p (1 + rank l + rank r) l r
False -> Node p (1 + rank l + rank r) r l
-- merge combines two heaps into one. There are two base cases and two
-- recursive cases - see [Two-pass Merging algorithm]. Recursive cases
-- call makeT to ensure that rank invariant is maintained after
-- merging.
{-@ merge :: (Ord a) => h1:PHeap a -> h2:PHeap a -> {v:PHeap a | realRank v = realRank h1 + realRank h2} @-}
merge Empty h2 = h2
merge h1 Empty = h1
merge h1@(Node p1 k1 l1 r1) h2@(Node p2 k2 l2 r2) = case p1 < p2 of
True -> makeT p1 l1 (merge r1 (Node p2 k2 l2 r2))
False -> makeT p2 l2 (merge (Node p1 k1 l1 r1) r2)
-- Inserting into a heap is performed by merging that heap with newly
-- created singleton heap.
{-@ insert :: (Ord a) => a -> PHeap a -> PHeap a @-}
insert p h = merge (singleton p) h
-- findMin returns element with highest priority, ie. root
-- element. Here we encounter first serious problem: we can't return
-- anything sensible for empty node.
{-@ findMin :: PHeap a -> a @-}
findMin Empty = undefined
findMin (Node p _ _ _) = p
-- and write a safer version of findMinM
{-@ findMinM :: PHeap a -> Maybe a @-}
findMinM Empty = Nothing
findMinM (Node p _ _ _) = Just p
-- deleteMin removes the element with the highest priority by merging
-- subtrees of a root element. Again the case of empty heap is
-- problematic. We could give it semantics by returning Empty, but
-- this just doesn't feel right. Why should we be able to remove
-- elements from an empty heap?
{-@ deleteMin :: (Ord a) => PHeap a -> PHeap a @-}
deleteMin Empty = undefined -- should we insert empty?
deleteMin (Node _ _ l r) = merge l r
-- As a quick sanity check let's construct some examples. Here's a
-- heap constructed by inserting following priorities into an empty
-- heap: 3, 0, 1, 2.
{-@ heap :: PHeap Int @-}
heap = insert (2 :: Int)
(insert 1
(insert 0
(insert 3 Empty)))
-- Example usage of findMin
findMinInHeap :: Priority
findMinInHeap = findMin heap
-- Example usage of deleteMin
deleteMinFromHeap :: Heap Int
deleteMinFromHeap = deleteMin heap