30 lines
761 B
Text
30 lines
761 B
Text
data Skewheap where
|
|
Empty : Skewheap
|
|
Node : Skewheap -> Int -> Skewheap -> Skewheap
|
|
|
|
data Maybe a where
|
|
Nothing : Maybe a
|
|
Just : a -> Maybe a
|
|
|
|
empty = Empty
|
|
|
|
singleton x = Node Empty x Empty
|
|
|
|
peek : Skewheap -> Maybe Int
|
|
peek tree = case tree of
|
|
Node _ x _ => Just x
|
|
_ => Nothing
|
|
|
|
pop tree = case tree of
|
|
Node l x r => Just (Pair x (merge l r))
|
|
Empty => Nothing
|
|
|
|
merge tree1 tree2 = case tree1 of
|
|
Node left1 val1 right1 => case tree2 of
|
|
Node left2 val2 right2 => case val1 < val2 of
|
|
True => Node (merge right1 (Node left2 val2 right2)) val1 left1
|
|
False => Node (merge right2 (Node left1 val1 right1)) val2 left2
|
|
_ => tree1
|
|
Empty => tree2
|
|
|
|
insert x tree = merge (singleton x) tree
|