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

    , Null
    , Size
    , Lookup
    , LookupAssoc
    , Member
    , NotMember
    , Find
    , FindWithDefault

    , Empty
    , Singleton

    , Insert
    )
    where

import Types.Data.Bool
import Types.Data.List hiding (Null)
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

-- Lookup
type family   Lookup k m
type instance Lookup k Tip              = Nothing
type instance Lookup k (Bin s k' v l r)
    = If (IsLT (Compare k k'))
         (Lookup k l)
         (If (IsGT (Compare k k'))
             (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)
    = If (IsLT (Compare k k'))
         (LookupAssoc k l)
         (If (IsGT (Compare k k'))
             (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)
    = If (IsLT (Compare k k'))
         (Balance k' v' (Insert k v l) r)
         (If (IsGT (Compare k k'))
             (Balance k' v' l (Insert k v r))
             (Bin s k v l r))

-- Balance
type Delta = D5
type Ratio = D2

type Balance k v l r
    = If (Size l :+: Size r :<: 1)
         (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