{-# LANGUAGE
  EmptyDataDecls,
  TypeFamilies,
  TypeOperators,
  UndecidableInstances
  #-}
module Types.Data.Map
    ( -- * Map class
      Map

      -- * Query
    , Null
    , Size
    , Lookup
    , LookupAssoc
    , Member
    , NotMember
    , Find
    , FindWithDefault

      -- * Construction
    , Empty
    , Singleton

      -- ** Insertion
    , Insert

      -- ** Delete\/Update
    , Delete
    , Adjust
    , AdjustWithKey
    , UpdateWithKey

      -- * Traversal
      -- ** Map
    , MapValue
    , MapWithKey

      -- ** Fold
    , FoldrWithKey
    , FoldlWithKey

      -- * Conversion
    , Keys
    , Assocs

      -- ** Lists
    , ToList
    , FromList

      -- ** Ordered lists
    , ToAscList
    , ToDescList

      -- * Min\/Max
    , DeleteFindMin
    , DeleteFindMax
    , MinView
    , MaxView
    , MinViewWithKey
    , MaxViewWithKey
    )
    where

import qualified Types.Data.List as L
import qualified Types.Data.List.Ops as L

import Types.Data.Bool
import Types.Data.List hiding (Null)
import Types.Data.List.Ops hiding (Map)
import Types.Data.Maybe
import Types.Data.Num
import Types.Data.Ord

data Tip
data Bin size key value left right

class    Map m
instance Map Tip
instance Map (Bin s k v l r)

-- Null
type family   Null m
type instance Null Tip             = True
type instance Null (Bin s k v l r) = False

-- Size
type family   Size m
type instance Size Tip             = D0
type instance Size (Bin s k v l r) = s

-- CompCase
type CompCase a b ifLT ifGT ifEQ
    = If (IsLT (Compare a b))
         ifLT
         (If (IsGT (Compare a b))
             ifGT
             ifEQ)

-- Lookup
type family   Lookup k m
type instance Lookup k Tip              = Nothing
type instance Lookup k (Bin s k' v l r)
    = CompCase k k'
               (Lookup k l)
               (Lookup k r)
               (Just v)

-- LookupAssoc
type family   LookupAssoc k m
type instance LookupAssoc k Tip              = Nothing
type instance LookupAssoc k (Bin s k' v l r)
    = CompCase k k'
               (LookupAssoc k l)
               (LookupAssoc k r)
               (Just (Cons k v))

-- Member
type Member k m = IsJust (Lookup k m)

-- NotMember
type NotMember k m = Not (Member k m)

-- Find
type Find k m = FromJust (Lookup k m)

-- FindWithDefault
type FindWithDefault a k m
    = FromMaybe a (Lookup k m)

-- Empty
type Empty = Tip

-- Singleton
type Singleton k v = Bin D1 k v Tip Tip

-- Insert
type family   Insert k v m
type instance Insert k v Tip              = Singleton k v
type instance Insert k v (Bin s k' v' l r)
    = CompCase k k'
               (Balance k' v' (Insert k v l) r)
               (Balance k' v' l (Insert k v r))
               (Bin s k v l r)

-- Delete
type family   Delete k m
type instance Delete k Tip              = Tip
type instance Delete k (Bin s k' v l r)
    = CompCase k k'
               (Balance k' v (Delete k l) r)
               (Balance k' v l (Delete k r))
               (Glue l r)

-- Balance
type Delta = D5
type Ratio = D2

type Balance k v l r
    = If ((Size l :+: Size r) :<=: D1)
         (Bin (Size l :+: Size r :+: D1) k v l r)
         (If (Size r :>=: (Delta :*: Size l))
             (RotateL k v l r)
             (If (Size l :>=: (Delta :*: Size r))
                 (RotateR k v l r)
                 (Bin (Size l :+: Size r :+: D1) k v l r)))

-- Rotate
type family   RotateL k v l r
type instance RotateL k v l (Bin s k' v' l' r')
    = If (Size l' :<: (Ratio :*: Size r'))
         (SingleL k v l (Bin s k' v' l' r'))
         (DoubleL k v l (Bin s k' v' l' r'))

type family   RotateR k v l r
type instance RotateR k v (Bin s k' v' l' r') r
    = If (Size r' :<: (Ratio :*: Size l'))
         (SingleR k v (Bin s k' v' l' r') r)
         (DoubleR k v (Bin s k' v' l' r') r)

-- Rotations
type family   SingleL k v l r
type instance SingleL k v l (Bin s k' v' l' r')
    = Bin' k' v' (Bin' k v l l') r'

type family   SingleR k v l r
type instance SingleR k v (Bin s k' v' l r) r'
    = Bin' k' v' l (Bin' k v r r')

type family   DoubleL k v l r
type instance DoubleL k v l (Bin s k' v' (Bin s' k'' v'' l' r) r')
    = Bin' k'' v'' (Bin' k v l l') (Bin' k' v' r r')

type family   DoubleR k v l r
type instance DoubleR k v (Bin s k' v' l (Bin s' k'' v'' l' r)) r'
    = Bin' k'' v'' (Bin' k' v' l l') (Bin' k v r r')

-- Bin'
type Bin' k v l r
    = Bin (Size l :+: Size r :+: D1) k v l r

-- Glue
type Glue l r
    = If (Null l)
         r
         (If (Null r)
             l
             (If (Size l :>: Size r)
                 (GlueL (DeleteFindMax l) r)
                 (GlueR l (DeleteFindMin r))))

type family   GlueL dfm r
type instance GlueL (Cons (Cons km m) l') r = Balance km m l' r

type family   GlueR l dfm
type instance GlueR l (Cons (Cons km m) r') = Balance km m l r'

-- DeleteFindMin
type family   DeleteFindMin m
type instance DeleteFindMin (Bin s k v l r)
    = If (Null l)
         (Cons (Cons k v) r)
         (DeleteFindMin' k v (DeleteFindMin l) r)

type family   DeleteFindMin' k v dfm r
type instance DeleteFindMin' k v (Cons km l') r
    = Cons km (Balance k v l' r)

-- DeleteFindMax
type family   DeleteFindMax m
type instance DeleteFindMax (Bin s k v l r)
    = If (Null r)
         (Cons (Cons k v) l)
         (DeleteFindMax' k v l (DeleteFindMax r))

type family   DeleteFindMax' k v l dfm
type instance DeleteFindMax' k v l (Cons km r')
    = Cons km (Balance k v l r')

-- MinViewWithKey
type MinViewWithKey m
    = If (Null m)
         Nothing
         (Just (DeleteFindMin m))

-- MaxViewWithKey
type MaxViewWithKey m
    = If (Null m)
         Nothing
         (Just (DeleteFindMax m))

-- MinView
type MinView m
    = If (Null m)
         Nothing
         (Just (View' (DeleteFindMin m)))

type family   View' m
type instance View' (Cons (Cons k v) m') = Cons v m'

-- MaxView
type MaxView m
    = If (Null m)
         Nothing
         (Just (View' (DeleteFindMax m)))

-- Adjust
type Adjust f k m
    = AdjustWithKey (Adjust' f) k m

data Adjust' f
type instance App2 (Adjust' f) k v = App f v

-- AdjustWithKey
type AdjustWithKey f k m
    = UpdateWithKey (AdjustWithKey' f) k m

data AdjustWithKey' f
type instance App2 (AdjustWithKey' f) k v = Just (App2 f k v)

-- UpdateWithKey
type family   UpdateWithKey f k m
type instance UpdateWithKey f k Tip              = Tip
type instance UpdateWithKey f k (Bin s k' v l r)
    = CompCase k k'
               (Balance k' v (UpdateWithKey f k l) r)
               (Balance k' v l (UpdateWithKey f k r))
               (If (IsJust (App2 f k' v))
                   (Bin s k' (FromJust (App2 f k' v)) l r)
                   (Glue l r))

-- Map
type MapValue f m = MapWithKey (MapValue' f) m

data MapValue' f
type instance App2 (MapValue' f) k v = App f v

-- MapWithKey
type family   MapWithKey f m
type instance MapWithKey f Tip             = Tip
type instance MapWithKey f (Bin s k v l r)
    = Bin s k (App2 f k v) (MapWithKey f l) (MapWithKey f r)

-- FoldrWithKey
type family   FoldrWithKey f z m
type instance FoldrWithKey f z Tip             = z
type instance FoldrWithKey f z (Bin s k v l r)
    = FoldrWithKey f (App3 f k v (FoldrWithKey f z r)) l

-- FoldlWithKey
type family   FoldlWithKey f z m
type instance FoldlWithKey f z Tip             = z
type instance FoldlWithKey f z (Bin s k v l r)
    = FoldlWithKey f (App3 f (FoldlWithKey f z l) k v) r

-- Keys
type Keys m = L.Map Key' (Assocs m)

data Key'
type instance App Key' (Cons k v) = k

-- Assocs
type Assocs m = ToList m

-- ToList
type ToList m = ToAscList m

-- FromList
type FromList xs = Foldl Ins' Empty xs

data Ins'
type instance App2 Ins' m (Cons k v) = Insert k v m

-- ToAscList
type ToAscList m = FoldrWithKey ToAscList' L.Null m

data ToAscList'
type instance App3 ToAscList' k v vs = Cons (Cons k v) vs

-- ToDescList
type ToDescList m = FoldlWithKey ToDescList' L.Null m

data ToDescList'
type instance App3 ToDescList' vs k v = Cons (Cons k v) vs