module Type.BST.BST (
BST(Leaf, Node), Record(None, Triple), Union(Top, GoL, GoR)
, Fromlistable(Fromlist, fromlist)
, Fromsumable(fromsum)
, Foldable(virtual), tolist, tosum, Tolist
, Accessible(At), at, proj, inj, (!)
, AccessibleF(), smap, supdate, adjust, update, (<$*>)
, Contains, ContainedBy
, Searchable(Smap, atX, projX, injX), (!?), SearchableF(smapX), supdateX, adjustX, updateX, (<$*?>)
, Unioncasable, unioncase, UnioncasableX(unioncaseX)
, Includes, IncludedBy, shrink, expand
, Balanceable(Balance, balance)
, Metamorphosable(metamorphose)
, Mergeable(Merge, merge, MergeE, mergeE)
, Insertable(Insert, insert)
, Deletable(Delete, delete)
, Minnable(Findmin, splitmin), findmin, deletemin
, Maxable(Findmax, splitmax), findmax, deletemax
) where
import Data.Maybe
import GHC.TypeLits
import Type.BST.Proxy
import Type.BST.Item
import Type.BST.Compare
import Type.BST.List
import Type.BST.Sum
data BST a = Leaf | Node (BST a) a (BST a)
data family Record (s :: BST *)
data instance Record Leaf = None
data instance Record (Node l a r) = Triple (Record l) a (Record r)
instance (Foldable s, Show (List (Tolist s))) => Show (Record s) where
showsPrec p rc = showParen (p > 10) $ showString "<Record> " . showsPrec 11 (tolist rc)
data family Union (s :: BST *)
data instance Union Leaf
data instance Union (Node l a r) = Top a | GoL (Union l) | GoR (Union r)
instance Show (Union Leaf) where
show !_ = undefined
instance (Show a, Show (Union l), Show (Union r)) => Show (Union (Node l a r)) where
showsPrec p (Top x) = showParen (p > 10) $ showString "<Union> " . showsPrec 11 x
showsPrec p (GoL l) = showsPrec p l
showsPrec p (GoR r) = showsPrec p r
class Fromlistable (as :: [*]) where
type Fromlist as :: BST *
fromlist :: List as -> Record (Fromlist as)
instance (Sortable as, Fromslistable (Sort as)) => Fromlistable as where
type Fromlist as = Fromslist (Sort as)
fromlist xs = fromslist (sort xs)
type Fromslist as = Fromslist' True (Length as) 0 as '[]
type Fromslistable as = Fromslistable' True (Length as) 0 as '[]
fromslist :: Fromslistable as => List as -> Record (Fromslist as)
fromslist (xs :: List as) = fromslist' (Proxy :: Proxy True) (Proxy :: Proxy (Length as)) (Proxy :: Proxy 0) xs Nil
type FromslistR as = Fromslist' False (Length as) 0 as '[]
type FromslistableR as = Fromslistable' False (Length as) 0 as '[]
fromslistR :: FromslistableR as => List as -> Record (FromslistR as)
fromslistR (xs :: List as) = fromslist' (Proxy :: Proxy False) (Proxy :: Proxy (Length as)) (Proxy :: Proxy 0) xs Nil
class Fromslistable' (fw :: Bool) (m :: Nat) (n :: Nat) (as :: [*]) (bs :: [*]) where
type Fromslist' fw m n as bs :: BST *
fromslist' :: Proxy fw -> Proxy m -> Proxy n -> List as -> List bs -> Record (Fromslist' fw m n as bs)
instance Fromslistable' fw 0 0 '[] '[] where
type Fromslist' fw 0 0 '[] '[] = Leaf
fromslist' _ _ _ _ _ = None
instance Fromslistable' fw 0 1 '[] '[b] where
type Fromslist' fw 0 1 '[] '[b] = Node Leaf b Leaf
fromslist' _ _ _ _ (Cons y _) = Triple None y None
instance Fromslistable'' (m <=? n + 1) fw m n (a ': as) bs => Fromslistable' fw m n (a ': as) bs where
type Fromslist' fw m n (a ': as) bs = Fromslist'' (m <=? n + 1) fw m n (a ': as) bs
fromslist' = fromslist'' (Proxy :: Proxy (m <=? n + 1))
class Fromslistable'' (b :: Bool) (fw :: Bool) (m :: Nat) (n :: Nat) (as :: [*]) (bs :: [*]) where
type Fromslist'' b fw m n as bs :: BST *
fromslist'' :: Proxy b -> Proxy fw -> Proxy m -> Proxy n -> List as -> List bs -> Record (Fromslist'' b fw m n as bs)
instance (Fromslistable as, FromslistableR bs) => Fromslistable'' True True m n (a ': as) bs where
type Fromslist'' True True m n (a ': as) bs = Node (FromslistR bs) a (Fromslist as)
fromslist'' _ _ _ _ (Cons x xs) ys = Triple (fromslistR ys) x (fromslist xs)
instance (FromslistableR as, Fromslistable bs) => Fromslistable'' True False m n (a ': as) bs where
type Fromslist'' True False m n (a ': as) bs = Node (FromslistR as) a (Fromslist bs)
fromslist'' _ _ _ _ (Cons x xs) ys = Triple (fromslistR xs) x (fromslist ys)
instance Fromslistable' fw (m 1) (n + 1) as (a ': bs) => Fromslistable'' False fw m n (a ': as) bs where
type Fromslist'' False fw m n (a ': as) bs = Fromslist' fw (m 1) (n + 1) as (a ': bs)
fromslist'' _ _ _ _ (Cons x xs) ys = fromslist' (Proxy :: Proxy fw) (Proxy :: Proxy (m 1)) (Proxy :: Proxy (n + 1)) xs (x .:. ys)
class Fromsumable (as :: [*]) where
fromsum :: Sum as -> Union (Fromlist as)
instance Fromsumable' as (Fromlist as) => Fromsumable as where
fromsum = fromsum'
class Fromsumable' (as :: [*]) (t :: BST *) where
fromsum' :: Sum as -> Union t
instance Fromsumable' '[] t where
fromsum' !_ = undefined
instance (Contains t key a, Fromsumable' as t) => Fromsumable' (key |> a ': as) t where
fromsum' (Head (Item x)) = inj (Proxy :: Proxy key) x
fromsum' (Tail s) = fromsum' s
class Foldable (t :: BST *) where
type Tolist' t (as :: [*]) :: [*]
tolist' :: Record t -> List as -> List (Tolist' t as)
tosum' :: Either (Sum as) (Union t) -> Sum (Tolist' t as)
virtual :: Record t
type family Tolist (t :: BST *) :: [*]
type instance Tolist t = Tolist' t '[]
tolist :: Foldable t => Record t -> List (Tolist t)
tolist rc = tolist' rc Nil
tosum :: Foldable t => Union t -> Sum (Tolist t)
tosum (u :: Union t) = tosum' (Right u :: Either (Sum '[]) (Union t))
instance Foldable Leaf where
type Tolist' Leaf as = as
tolist' _ xs = xs
tosum' (Right !_) = undefined
tosum' (Left s) = s
virtual = None
instance (Foldable l, Foldable r) => Foldable (Node l a r) where
type Tolist' (Node l a r) as = Tolist' l (a ': Tolist' r as)
tolist' (Triple l x r) xs = tolist' l (x .:. tolist' r xs)
tosum' (Right (Top x) :: Either (Sum as) (Union (Node l a r))) = tosum' (Left $ Head x :: Either (Sum (a ': Tolist' r as)) (Union l))
tosum' (Right (GoL u) :: Either (Sum as) (Union (Node l a r))) = tosum' (Right u :: Either (Sum (a ': Tolist' r as)) (Union l))
tosum' (Right (GoR u) :: Either (Sum as) (Union (Node l a r))) = tosum' (Left $ Tail $ tosum' (Right u :: Either (Sum as) (Union r)) :: Either (Sum (a ': Tolist' r as)) (Union l))
tosum' (Left s :: Either (Sum as) (Union (Node l a r))) = tosum' (Left $ Tail $ tosum' (Left s :: Either (Sum as) (Union r)) :: Either (Sum (a ': Tolist' r as)) (Union l))
virtual = Triple (virtual :: Record l) (error "Type.BST.BST.virtual: an empty item") (virtual :: Record r)
class Searchable t key (At t key) => Accessible (t :: BST *) (key :: k) where
type At t key :: *
instance Accessible' (Compare key key') (Node l (key' |> a) r) key => Accessible (Node l (key' |> a) r) key where
type At (Node l (key' |> a) r) key = At' (Compare key key') (Node l (key' |> a) r) key
class Searchable' o t key (At' o t key) => Accessible' (o :: Ordering) (t :: BST *) (key :: k) where
type At' o t key :: *
instance Accessible' EQ (Node _' (key |> a) _'') key where
type At' EQ (Node _' (key |> a) _'') key = a
instance Accessible l key => Accessible' LT (Node l _' _'') key where
type At' LT (Node l _' _'') key = At l key
instance Accessible r key => Accessible' GT (Node _' _'' r) key where
type At' GT (Node _' _'' r) key = At r key
at :: Accessible t key => Record t -> proxy key -> At t key
at rc p = fromJust $ atX rc p
proj :: Accessible t key => Union t -> proxy key -> Maybe (At t key)
proj = projX
inj :: Accessible t key => proxy key -> At t key -> Union t
inj p x = fromJust $ injX p x
(!) :: Accessible t key => Record t -> proxy key -> At t key
(!) = at
infixl 9 !
class (Accessible t key, SearchableF f t key (At t key)) => AccessibleF (f :: BST * -> *) (t :: BST *) (key :: k)
instance Accessible t key => AccessibleF Record t key
instance Accessible t key => AccessibleF Union t key
smap :: AccessibleF f t key => proxy key -> (At t key -> b) -> f t -> f (Smap t key (At t key) b)
smap = smapX
supdate :: AccessibleF f t key => proxy key -> b -> f t -> f (Smap t key (At t key) b)
supdate = supdateX
adjust :: AccessibleF f t key => proxy key -> (At t key -> At t key) -> f t -> f t
adjust = adjustX
update :: AccessibleF f t key => proxy key -> At t key -> f t -> f t
update p x = adjust p (const x)
(<$*>) :: AccessibleF f t key => key |> (At t key -> b) -> f t -> f (Smap t key (At t key) b)
(<$*>) (Item f :: key |> (At t key -> b)) (c :: f t) = smap (Proxy :: Proxy key) f c
infixl 4 <$*>
class (Accessible t key, a ~ At t key) => Contains (t :: BST *) (key :: k) (a :: *) | t key -> a
instance (Accessible t key, a ~ At t key) => Contains t key a
class Contains t key a => ContainedBy (key :: k) (a :: *) (t :: BST *) | t key -> a
instance Contains t key a => ContainedBy key a t
class Smap t key a a ~ t => Searchable (t :: BST *) (key :: k) (a :: *) where
atX :: Record t -> proxy key -> Maybe a
projX :: Union t -> proxy key -> Maybe a
injX :: proxy key -> a -> Maybe (Union t)
type Smap t key a (b :: *) :: BST *
smapXR :: proxy key -> (a -> b) -> Record t -> Record (Smap t key a b)
smapXU :: proxy key -> (a -> b) -> Union t -> Union (Smap t key a b)
(!?) :: Searchable t key a => Record t -> proxy key -> Maybe a
(!?) = atX
instance Searchable Leaf _' _'' where
atX _ _ = Nothing
projX _ _ = Nothing
injX _ _ = Nothing
type Smap Leaf key a b = Leaf
smapXR _ _ _ = None
smapXU _ _ u = u
instance Searchable' (Compare key key') (Node l (key' |> c) r) key a => Searchable (Node l (key' |> c) r) key a where
atX rc _ = atX' (Proxy :: Proxy '(Compare key key', key)) rc
projX u _ = projX' (Proxy :: Proxy '(Compare key key', key)) u
injX _ x = injX' (Proxy :: Proxy '(Compare key key', key)) x
type Smap (Node l (key' |> c) r) key a b = Smap' (Compare key key') (Node l (key' |> c) r) key a b
smapXR _ = smapXR' (Proxy :: Proxy '(Compare key key', key))
smapXU _ = smapXU' (Proxy :: Proxy '(Compare key key', key))
class Smap' o t key a a ~ t => Searchable' (o :: Ordering) (t :: BST *) (key :: k) (a :: *) where
atX' :: Proxy '(o, key) -> Record t -> Maybe a
projX' :: Proxy '(o, key) -> Union t -> Maybe a
injX' :: Proxy '(o, key) -> a -> Maybe (Union t)
type Smap' o t key a (b :: *) :: BST *
smapXR' :: Proxy '(o, key) -> (a -> b) -> Record t -> Record (Smap' o t key a b)
smapXU' :: Proxy '(o, key) -> (a -> b) -> Union t -> Union (Smap' o t key a b)
instance Searchable' EQ (Node _' (key |> a) _'') key a where
atX' _ (Triple _ (Item x) _) = Just x
projX' _ (Top (Item x)) = Just x
projX' _ _ = Nothing
injX' _ x = Just $ Top $ (Item :: With key) x
type Smap' EQ (Node l (key |> a) r) key a b = Node l (key |> b) r
smapXR' _ f (Triple l (Item x) r) = Triple l (Item $ f x) r
smapXU' _ f (Top (Item x)) = Top $ Item $ f x
smapXU' _ _ (GoL l) = GoL l
smapXU' _ _ (GoR r) = GoR r
instance Searchable l key a => Searchable' LT (Node l _' _'') key a where
atX' _ (Triple l _ _) = atX l (Proxy :: Proxy key)
projX' _ (GoL u) = projX u (Proxy :: Proxy key)
projX' _ _ = Nothing
injX' _ x = fmap GoL $ injX (Proxy :: Proxy key) x
type Smap' LT (Node l c r) key a b = Node (Smap l key a b) c r
smapXR' _ f (Triple l x r) = Triple (smapXR (Proxy :: Proxy key) f l) x r
smapXU' _ f (GoL l) = GoL $ smapXU (Proxy :: Proxy key) f l
smapXU' _ _ (GoR r) = GoR r
smapXU' _ _ (Top x) = Top x
instance Searchable r key a => Searchable' GT (Node _' _'' r) key a where
atX' _ (Triple _ _ r) = atX r (Proxy :: Proxy key)
projX' _ (GoR u) = projX u (Proxy :: Proxy key)
projX' _ _ = Nothing
injX' _ x = fmap GoR $ injX (Proxy :: Proxy key) x
type Smap' GT (Node l c r) key a b = Node l c (Smap r key a b)
smapXR' _ f (Triple l x r) = Triple l x (smapXR (Proxy :: Proxy key) f r)
smapXU' _ f (GoR r) = GoR $ smapXU (Proxy :: Proxy key) f r
smapXU' _ _ (GoL l) = GoL l
smapXU' _ _ (Top x) = Top x
class Searchable t key a => SearchableF (f :: BST * -> *) (t :: BST *) (key :: k) (a :: *) where
smapX :: proxy key -> (a -> b) -> f t -> f (Smap t key a b)
supdateX :: SearchableF f t key (At t key) => proxy key -> b -> f t -> f (Smap t key (At t key) b)
supdateX (p :: proxy key) (x :: b) (c :: f t) = smapX p (const x :: At t key -> b) c
adjustX :: SearchableF f t key a => proxy key -> (a -> a) -> f t -> f t
adjustX = smapX
updateX :: SearchableF f t key a => proxy key -> a -> f t -> f t
updateX p x = adjustX p (const x)
(<$*?>) :: SearchableF f t key a => key |> (a -> b) -> f t -> f (Smap t key a b)
(<$*?>) (Item f :: key |> (a -> b)) = smapX (Proxy :: Proxy key) f
infixl 4 <$*?>
instance Searchable t key a => SearchableF Record t key a where
smapX = smapXR
instance Searchable t key a => SearchableF Union t key a where
smapX = smapXU
class UnioncasableX t t' res => Unioncasable (t :: BST *) (t' :: BST *) (res :: *)
instance Unioncasable Leaf t' res
instance (Contains t' key (a -> res), Unioncasable l t' res, Unioncasable r t' res) => Unioncasable (Node l (Item key a) r) t' res
unioncase :: Unioncasable t t' res => Union t -> Record t' -> res
unioncase = unioncaseX
class UnioncasableX (t :: BST *) (t' :: BST *) (res :: *) where
unioncaseX :: Union t -> Record t' -> res
instance UnioncasableX Leaf t' res where
unioncaseX !_ _ = undefined
instance (Searchable t' key (a -> res), UnioncasableX l t' res, UnioncasableX r t' res) => UnioncasableX (Node l (Item key a) r) t' res where
unioncaseX (Top (Item x)) rc = case rc !? (Proxy :: Proxy key) of
Just f -> f x
Nothing -> error "Type.BST.BST.unioncaseX: corresponding function not found"
unioncaseX (GoL l) rc = unioncaseX l rc
unioncaseX (GoR r) rc = unioncaseX r rc
class Includes (t :: BST *) (t' :: BST *)
instance Includes t Leaf
instance (Contains t key a, Includes t l, Includes t r) => Includes t (Node l (key |> a) r)
class Includes t' t => IncludedBy (t :: BST *) (t' :: BST *)
instance Includes t' t => IncludedBy t t'
shrink :: (Metamorphosable Record t t', Includes t t') => Record t -> Record t'
shrink = metamorphose
expand :: (Metamorphosable Union t t', IncludedBy t t') => Union t -> Union t'
expand = metamorphose
class (Foldable t, Fromlistable (Tolist t)) => Balanceable (t :: BST *) where
type Balance t :: BST *
balance :: Record t -> Record (Balance t)
instance (Foldable t, Fromlistable (Tolist t)) => Balanceable t where
type Balance t = Fromlist (Tolist t)
balance = fromlist . tolist
class Metamorphosable (f :: BST * -> *) (t :: BST *) (t' :: BST *) where
metamorphose :: f t -> f t'
instance MetamorphosableR t t' => Metamorphosable Record t t' where
metamorphose = metamorphoseR
instance MetamorphosableU t t' => Metamorphosable Union t t' where
metamorphose = metamorphoseU
class MetamorphosableR t t' where
metamorphoseR :: Record t -> Record t'
instance (Foldable t', MetamorphosableR' t t') => MetamorphosableR t t' where
metamorphoseR = metamorphoseR' virtual
class MetamorphosableR' (t :: BST *) (t' :: BST *) where
metamorphoseR' :: Record t' -> Record t -> Record t'
instance MetamorphosableR' Leaf t where
metamorphoseR' rc _ = rc
instance (Searchable t key a, MetamorphosableR' l t, MetamorphosableR' r t) => MetamorphosableR' (Node l (key |> a) r) t where
metamorphoseR' rc (Triple l (Item x) r) = metamorphoseR' ((updateX (Proxy :: Proxy key) x) $ metamorphoseR' rc r) l
class MetamorphosableU (t :: BST *) (t' :: BST *) where
metamorphoseU :: Union t -> Union t'
instance MetamorphosableU Leaf t where
metamorphoseU _ = error "Type.BST.BST.metamorphoseU: bad luck!"
instance (Searchable t key a, MetamorphosableU l t, MetamorphosableU r t) => MetamorphosableU (Node l (key |> a) r) t where
metamorphoseU (Top (Item x)) = case injX (Proxy :: Proxy key) x of
Nothing -> error "Type.BST.BST.metamorphoseU: bad luck!"
Just u -> u
metamorphoseU (GoL l) = metamorphoseU l
metamorphoseU (GoR r) = metamorphoseU r
class Mergeable (t :: BST *) (t' :: BST *) where
type Merge t t' :: BST *
merge :: Record t -> Record t' -> Record (Merge t t')
type MergeE t t' :: BST *
mergeE :: Record t -> Record t' -> Record (MergeE t t')
instance (Foldable t, Foldable t', MergeableL (Tolist t) (Tolist t'), Fromlistable (MergeL (Tolist t) (Tolist t')), Fromlistable (MergeEL (Tolist t) (Tolist t'))) => Mergeable t t' where
type Merge t t' = Fromlist (MergeL (Tolist t) (Tolist t'))
merge rc rc' = fromlist $ mergeL (tolist rc) (tolist rc')
type MergeE t t' = Fromlist (MergeEL (Tolist t) (Tolist t'))
mergeE rc rc' = fromlist $ mergeEL (tolist rc) (tolist rc')
class Insertable (t :: BST *) (key :: k) where
type Insert t key (a :: *) :: BST *
insert :: proxy key -> a -> Record t -> Record (Insert t key a)
instance Insertable Leaf key where
type Insert Leaf key a = Node Leaf (key |> a) Leaf
insert _ x _ = Triple None ((Item :: With key) x) None
instance Insertable' (Compare key key') (Node l (key' |> b) r) key => Insertable (Node l (key' |> b) r) key where
type Insert (Node l (key' |> b) r) key a = Insert' (Compare key key') (Node l (key' |> b) r) key a
insert _ = insert' (Proxy :: Proxy '(Compare key key', key))
class Insertable' (o :: Ordering) (t :: BST *) (key :: k) where
type Insert' o t key (a :: *) :: BST *
insert' :: Proxy '(o, key) -> a -> Record t -> Record (Insert' o t key a)
instance Insertable' EQ (Node l (key |> _') r) key where
type Insert' EQ (Node l (key |> _') r) key a = Node l (key |> a) r
insert' _ x (Triple l _ r) = Triple l ((Item :: With key) x) r
instance Insertable l key => Insertable' LT (Node l b r) key where
type Insert' LT (Node l b r) key a = Node (Insert l key a) b r
insert' _ x (Triple l y r) = Triple (insert (Proxy :: Proxy key) x l) y r
instance Insertable r key => Insertable' GT (Node l b r) key where
type Insert' GT (Node l b r) key a = Node l b (Insert r key a)
insert' _ x (Triple l y r) = Triple l y (insert (Proxy :: Proxy key) x r)
class Deletable (t :: BST *) (key :: k) where
type Delete t key :: BST *
delete :: proxy key -> Record t -> Record (Delete t key)
instance Deletable Leaf key where
type Delete Leaf key = Leaf
delete _ rc = rc
instance Deletable' (Compare key key') (Node l (key' |> a) r) key => Deletable (Node l (key' |> a) r) key where
type Delete (Node l (key' |> a) r) key = Delete' (Compare key key') (Node l (key' |> a) r) key
delete _ = delete' (Proxy :: Proxy '(Compare key key', key))
class Deletable' (o :: Ordering) (t :: BST *) (key :: k) where
type Delete' o t key :: BST *
delete' :: Proxy '(o, key) -> Record t -> Record (Delete' o t key)
instance Deletable' EQ (Node Leaf (key |> _') r) key where
type Delete' EQ (Node Leaf (key |> _') r) key = r
delete' _ (Triple _ _ r) = r
instance Deletable' EQ (Node (Node l a r) (key |> _') Leaf) key where
type Delete' EQ (Node (Node l a r) (key |> _') Leaf) key = Node l a r
delete' _ (Triple l _ _) = l
instance Maxable (Node l a r) => Deletable' EQ (Node (Node l a r) (key |> _') (Node l' b r')) key where
type Delete' EQ (Node (Node l a r) (key |> _') (Node l' b r')) key = Node (Deletemax (Node l a r)) (Findmax (Node l a r)) (Node l' b r')
delete' _ (Triple l _ r) = let (y, rc) = splitmax l in Triple rc y r
instance Deletable l key => Deletable' LT (Node l a r) key where
type Delete' LT (Node l a r) key = Node (Delete l key) a r
delete' _ (Triple l x r) = Triple (delete (Proxy :: Proxy key) l) x r
instance Deletable r key => Deletable' GT (Node l a r) key where
type Delete' GT (Node l a r) key = Node l a (Delete r key)
delete' _ (Triple l x r) = Triple l x (delete (Proxy :: Proxy key) r)
class Minnable (t :: BST *) where
type Deletemin t :: BST *
type Findmin t :: *
splitmin :: Record t -> (Findmin t, Record (Deletemin t))
findmin :: Minnable t => Record t -> Findmin t
findmin = fst . splitmin
deletemin :: Minnable t => Record t ->Record (Deletemin t)
deletemin = snd . splitmin
instance Minnable (Node Leaf a r) where
type Deletemin (Node Leaf a r) = r
type Findmin (Node Leaf a r) = a
splitmin (Triple _ x r) = (x, r)
instance Minnable (Node l' b r') => Minnable (Node (Node l' b r') a r) where
type Deletemin (Node (Node l' b r') a r) = Node (Deletemin (Node l' b r')) a r
type Findmin (Node (Node l' b r') a r) = Findmin (Node l' b r')
splitmin (Triple l x r) = let (y, rc) = splitmin l in (y, Triple rc x r)
class Maxable (t :: BST *) where
type Deletemax t :: BST *
type Findmax t :: *
splitmax :: Record t -> (Findmax t, Record (Deletemax t))
findmax :: Maxable t => Record t -> Findmax t
findmax = fst . splitmax
deletemax :: Maxable t => Record t ->Record (Deletemax t)
deletemax = snd . splitmax
instance Maxable (Node l a Leaf) where
type Deletemax (Node l a Leaf) = l
type Findmax (Node l a Leaf) = a
splitmax (Triple l x _) = (x, l)
instance Maxable (Node l' b r') => Maxable (Node l a (Node l' b r')) where
type Deletemax (Node l a (Node l' b r')) = Node l a (Deletemax (Node l' b r'))
type Findmax (Node l a (Node l' b r')) = Findmax (Node l' b r')
splitmax (Triple l x r) = let (y, rc) = splitmax r in (y, Triple l x rc)