@@ -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+--------------------------------------------------------------------------------
5+
6+module prelude.heap
7+
8+import builtins
9+
10+import prelude
11+import prelude.algebra
12+import prelude.list
13+import prelude.nat
14+
15+%access public
16+
17+abstract data MaxiphobicHeap : Set -> Set where
18+ Empty : MaxiphobicHeap a
19+ Node : Nat -> MaxiphobicHeap a -> a -> MaxiphobicHeap a -> MaxiphobicHeap a
20+
21+----------------------------------------- ---------------------------------------
22+-- Syntactic tests
23+--------------------------------------------------------------------------------
24+
25+total isEmpty : MaxiphobicHeap a -> Bool
26+isEmpty Empty = True
27+isEmpty _ = False
28+
29+total size : MaxiphobicHeap a -> Nat
30+size Empty = O
31+size (Node s l e r) = s
32+
33+--------------------------------------------------------------------------------
34+-- Basic heaps
35+--------------------------------------------------------------------------------
36+
37+total empty : MaxiphobicHeap a
38+empty = Empty
39+
40+total singleton : a -> MaxiphobicHeap a
41+singleton e = Node 1 Empty e Empty
42+
43+--------------------------------------------------------------------------------
44+-- Inserting items and merging heaps
45+--------------------------------------------------------------------------------
46+
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)
54+ else
55+ (right, left, centre)
56+ where
57+ largest : Nat
58+ largest = maximum (size left) $ maximum (size centre) (size right)
59+
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) =
64+ if le < re then
65+ let (largest, b, c) = orderBySize ll lr (Node rs rl re rr) in
66+ Node mergedSize largest le (merge b c)
67+ else
68+ let (largest, b, c) = orderBySize rl rr (Node ls ll le lr) in
69+ Node mergedSize largest re (merge b c)
70+ where
71+ mergedSize : Nat
72+ mergedSize = ls + rs
73+
74+insert : Ord a => a -> MaxiphobicHeap a -> MaxiphobicHeap a
75+insert e = merge $ singleton e
76+
77+--------------------------------------------------------------------------------
78+-- Heap operations
79+--------------------------------------------------------------------------------
80+
81+findMinimum : (h : MaxiphobicHeap a) -> (isEmpty h = False) -> a
82+findMinimum Empty p = ?findMinimumEmptyAbsurd
83+findMinimum (Node s l e r) p = e
84+
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
88+
89+--------------------------------------------------------------------------------
90+-- Conversions to and from lists (and a derived heap sorting algorithm)
91+--------------------------------------------------------------------------------
92+
93+toList : Ord a => MaxiphobicHeap a -> List a
94+toList Empty = []
95+toList (Node s l e r) = toList' (Node s l e r) refl
96+ where
97+ toList' : Ord a => (h : MaxiphobicHeap a) -> (isEmpty h = False) -> List a
98+ toList' heap p = findMinimum heap p :: toList $ deleteMinimum heap p
99+
100+fromList : Ord a => List a -> MaxiphobicHeap a
101+fromList = foldr insert empty
102+
103+sort : Ord a => List a -> List a
104+sort = prelude.heap.toList . prelude.heap.fromList
105+
106+--------------------------------------------------------------------------------
107+-- Class instances
108+--------------------------------------------------------------------------------
109+
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 ++ ")"
113+
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
118+ _ == _ = False
119+
120+instance Ord a => Semigroup (MaxiphobicHeap a) where
121+ (<+>) = merge
122+
123+instance Ord a => Monoid (MaxiphobicHeap a) where
124+ neutral = empty
125+
126+instance Ord a => JoinSemilattice (MaxiphobicHeap a) where
127+ join = merge
128+
129+--------------------------------------------------------------------------------
130+-- Properties
131+--------------------------------------------------------------------------------
132+
133+total absurdBoolDischarge : False = True -> _|_
134+absurdBoolDischarge p = replace {P = disjointTy} p ()
135+ where
136+ total disjointTy : Bool -> Set
137+ disjointTy False = ()
138+ disjointTy True = _|_
139+
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
143+
144+--------------------------------------------------------------------------------
145+-- Proofs
146+--------------------------------------------------------------------------------
147+
148+isEmptySizeZeroNodeAbsurd = proof {
149+ intros;
150+ refine FalseElim;
151+ refine absurdBoolDischarge;
152+ exact p;
153+}
154+
155+findMinimumEmptyAbsurd = proof {
156+ intros;
157+ refine FalseElim;
158+ refine absurdBoolDischarge;
159+ rewrite p;
160+ trivial;
161+}
162+
163+deleteMinimumEmptyAbsurd = proof {
164+ intros;
165+ refine FalseElim;
166+ refine absurdBoolDischarge;
167+ rewrite p;
168+ trivial;
169+}
170+
171+--------------------------------------------------------------------------------
172+-- Debug
173+--------------------------------------------------------------------------------
174+
175+{- XXX: poor performance when compiled, diverges when used in the REPL, but it
176+ does seem to work correctly!
177+main : IO ()
178+main = do
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")]
182+ return ()
183+-}