@@ -0,0 +1,183 @@
1+--------------------------------------------------------------------------------
2+-- Okasaki-style maxiphobic heaps. See the paper:
3+-- ``Fun with binary heap trees'', Chris Okasaki, Fun of programming, 2003.
4+--------------------------------------------------------------------------------
11+import prelude.algebra
17+abstract data MaxiphobicHeap : Set -> Set where
18+ Empty : MaxiphobicHeap a
19+ Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a -> MaxiphobicHeap a
21+----------------------------------------- ---------------------------------------
23+--------------------------------------------------------------------------------
25+total isEmpty : MaxiphobicHeap a -> Bool
29+total size : MaxiphobicHeap a -> Nat
31+size (Node s l e r) = s
33+--------------------------------------------------------------------------------
35+--------------------------------------------------------------------------------
37+total empty : MaxiphobicHeap a
40+total singleton : a -> MaxiphobicHeap a
41+singleton e = Node 1 Empty e Empty
43+--------------------------------------------------------------------------------
44+-- Inserting items and merging heaps
45+--------------------------------------------------------------------------------
47+private orderBySize : MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a ->
48+ (MaxiphobicHeap a, MaxiphobicHeap a, MaxiphobicHeap a)
49+orderBySize left centre right =
50+ if size left == largest then
51+ (left, centre, right)
52+ else if size centre == largest then
53+ (centre, left, right)
55+ (right, left, centre)
58+ largest = maximum (size left) $ maximum (size centre) (size right)
60+merge : Ord a => MaxiphobicHeap a -> MaxiphobicHeap a -> MaxiphobicHeap a
61+merge Empty right = right
62+merge left Empty = left
63+merge (Node ls ll le lr) (Node rs rl re rr) =
65+ let (largest, b, c) = orderBySize ll lr (Node rs rl re rr) in
66+ Node mergedSize largest le (merge b c)
68+ let (largest, b, c) = orderBySize rl rr (Node ls ll le lr) in
69+ Node mergedSize largest re (merge b c)
74+insert : Ord a => a -> MaxiphobicHeap a -> MaxiphobicHeap a
75+insert e = merge $ singleton e
77+--------------------------------------------------------------------------------
79+--------------------------------------------------------------------------------
81+findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a
82+findMinimum Empty p = ?findMinimumEmptyAbsurd
83+findMinimum (Node s l e r) p = e
85+deleteMinimum : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> MaxiphobicHeap a
86+deleteMinimum Empty p = ?deleteMinimumEmptyAbsurd
87+deleteMinimum (Node s l e r) p = merge l r
89+--------------------------------------------------------------------------------
90+-- Conversions to and from lists (and a derived heap sorting algorithm)
91+--------------------------------------------------------------------------------
93+toList : Ord a => MaxiphobicHeap a -> List a
95+toList (Node s l e r) = toList' (Node s l e r) refl
97+ toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
98+ toList' heap p = findMinimum heap p :: toList $ deleteMinimum heap p
100+fromList : Ord a => List a -> MaxiphobicHeap a
101+fromList = foldr insert empty
103+sort : Ord a => List a -> List a
104+sort = prelude.heap.toList . prelude.heap.fromList
106+--------------------------------------------------------------------------------
108+--------------------------------------------------------------------------------
110+instance Show a => Show (MaxiphobicHeap a) where
111+ show Empty = "Empty"
112+ show (Node s l e r) = "Node (" ++ show l ++ " " ++ show e ++ " " ++ show r ++ ")"
114+instance Eq a => Eq (MaxiphobicHeap a) where
115+ Empty == Empty = True
116+ (Node ls ll le lr) == (Node rs rl re rr) =
117+ ls == rs && ll == rl && le == re && lr == rr
120+instance Ord a => Semigroup (MaxiphobicHeap a) where
123+instance Ord a => Monoid (MaxiphobicHeap a) where
126+instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
129+--------------------------------------------------------------------------------
131+--------------------------------------------------------------------------------
133+total absurdBoolDischarge : False = True -> _|_
134+absurdBoolDischarge p = replace {P = disjointTy} p ()
136+ total disjointTy : Bool -> Set
137+ disjointTy False = ()
138+ disjointTy True = _|_
140+total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = O
141+isEmptySizeZero Empty p = refl
142+isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd
144+--------------------------------------------------------------------------------
146+--------------------------------------------------------------------------------
148+isEmptySizeZeroNodeAbsurd = proof {
151+ refine absurdBoolDischarge;
155+findMinimumEmptyAbsurd = proof {
158+ refine absurdBoolDischarge;
163+deleteMinimumEmptyAbsurd = proof {
166+ refine absurdBoolDischarge;
171+--------------------------------------------------------------------------------
173+--------------------------------------------------------------------------------
175+{- XXX: poor performance when compiled, diverges when used in the REPL, but it
176+ does seem to work correctly!
179+ _ <- print $ main.sort [10, 3, 7, 2, 9, 1, 8, 0, 6, 4, 5]
180+ _ <- print $ main.sort ["orange", "apple", "pear", "lime", "durian"]
181+ _ <- print $ main.sort [("jim", 19, "cs"), ("alice", 20, "english"), ("bob", 50, "engineering")]