{-# LANGUAGE ScopedTypeVariables, TemplateHaskell #-}
module Main where

--------------------------------------------------------------------------
-- imports

import Test.QuickCheck
import Test.QuickCheck.Text
import Test.QuickCheck.All

import Data.List
  ( sort
  , (\\)
  )

import Control.Monad
  ( liftM
  , liftM2
  )

--------------------------------------------------------------------------
-- skew heaps

data Heap a
  = Node a (Heap a) (Heap a)
  | Empty
 deriving ( Eq, Ord, Show )

empty :: Heap a
empty = Empty

isEmpty :: Heap a -> Bool
isEmpty Empty = True
isEmpty _     = False

unit :: a -> Heap a
unit x = Node x empty empty

size :: Heap a -> Int
size Empty          = 0
size (Node _ h1 h2) = 1 + size h1 + size h2

insert :: Ord a => a -> Heap a -> Heap a
insert x h = unit x `merge` h

removeMin :: Ord a => Heap a -> Maybe (a, Heap a)
removeMin Empty          = Nothing
removeMin (Node x h1 h2) = Just (x, h1 `merge` h2)

merge :: Ord a => Heap a -> Heap a -> Heap a
h1    `merge` Empty = h1
Empty `merge` h2    = h2
h1@(Node x h11 h12) `merge` h2@(Node y h21 h22)
  | x <= y    = Node x (h12 `merge` h2) h11
  | otherwise = Node y (h22 `merge` h1) h21

fromList :: Ord a => [a] -> Heap a
fromList xs = merging [ unit x | x <- xs ]
 where
  merging []  = empty
  merging [h] = h
  merging hs  = merging (sweep hs)

  sweep []         = []
  sweep [h]        = [h]
  sweep (h1:h2:hs) = (h1 `merge` h2) : sweep hs

toList :: Heap a -> [a]
toList h = toList' [h]
 where
  toList' []                  = []
  toList' (Empty        : hs) = toList' hs
  toList' (Node x h1 h2 : hs) = x : toList' (h1:h2:hs)

toSortedList :: Ord a => Heap a -> [a]
toSortedList Empty          = []
toSortedList (Node x h1 h2) = x : toList (h1 `merge` h2)

--------------------------------------------------------------------------
-- specification

invariant :: Ord a => Heap a -> Bool
invariant Empty          = True
invariant (Node x h1 h2) = x <=? h1 && x <=? h2 && invariant h1 && invariant h2

(<=?) :: Ord a => a -> Heap a -> Bool
x <=? Empty      = True
x <=? Node y _ _ = x <= y

(==?) :: Ord a => Heap a -> [a] -> Bool
h ==? xs = invariant h && sort (toList h) == sort xs

--------------------------------------------------------------------------
-- properties

prop_Empty =
  empty ==? ([] :: [Int])

prop_IsEmpty (h :: Heap Int) =
  isEmpty h == null (toList h)

prop_Unit (x :: Int) =
  unit x ==? [x]

prop_Size (h :: Heap Int) =
  size h == length (toList h)

prop_Insert x (h :: Heap Int) =
  insert x h ==? (x : toList h)

prop_RemoveMin (h :: Heap Int) =
  cover (size h > 1) 80 "non-trivial" $
  case removeMin h of
    Nothing     -> h ==? []
    Just (x,h') -> x == minimum (toList h) && h' ==? (toList h \\ [x])

prop_Merge h1 (h2 :: Heap Int) =
  (h1 `merge` h2) ==? (toList h1 ++ toList h2)

prop_FromList (xs :: [Int]) =
  fromList xs ==? xs

prop_ToSortedList (h :: Heap Int) =
  h ==? xs && xs == sort xs
 where
  xs = toSortedList h

--------------------------------------------------------------------------
-- generators

instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where
  arbitrary = sized (arbHeap Nothing)
   where
    arbHeap mx n =
      frequency $
        [ (1, return Empty) ] ++
        [ (7, do my <- arbitrary `suchThatMaybe` ((>= mx) . Just)
                 case my of
                   Nothing -> return Empty
                   Just y  -> liftM2 (Node y) arbHeap2 arbHeap2
                    where arbHeap2 = arbHeap (Just y) (n `div` 2))
        | n > 0
        ]

--------------------------------------------------------------------------
-- main

return []
main = $quickCheckAll

--------------------------------------------------------------------------
-- the end.
{-
  shrink Empty          = []
  shrink (Node x h1 h2) =
       [ h1, h2 ]
    ++ [ Node x  h1' h2  | h1' <- shrink h1, x  <=? h1' ]
    ++ [ Node x  h1  h2' | h2' <- shrink h2, x  <=? h2' ]
    ++ [ Node x' h1  h2  | x'  <- shrink x,  x' <=? h1, x' <=? h2 ]
-}

-- toSortedList (Node x h1 h2) = x : toSortedList (h1 `merge` h2)

{-
prop_HeapIsNotSorted (h :: Heap Int) =
  expectFailure $
    toList h == toSortedList h
-}