Types/Data/Map.hs

   1 {-# LANGUAGE
   2   EmptyDataDecls,
   3   TypeFamilies,
   4   TypeOperators,
   5   UndecidableInstances
   6   #-}
   7 module Types.Data.Map
   8     ( Map
   9
  10     , Null
  11     , Size
  12     , Lookup
  13     , LookupAssoc
  14     , Member
  15     , NotMember
  16     , Find
  17     , FindWithDefault
  18
  19     , Empty
  20     , Singleton
  21
  22     , Insert
  23     )
  24     where
  25
  26 import Types.Data.Bool
  27 import Types.Data.List hiding (Null)
  28 import Types.Data.Maybe
  29 import Types.Data.Num
  30 import Types.Data.Ord
  31
  32 data Tip
  33 data Bin size key value left right
  34
  35 class    Map m
  36 instance Map Tip
  37 instance Map (Bin s k v l r)
  38
  39 -- Null
  40 type family   Null m
  41 type instance Null Tip             = True
  42 type instance Null (Bin s k v l r) = False
  43
  44 -- Size
  45 type family   Size m
  46 type instance Size Tip             = D0
  47 type instance Size (Bin s k v l r) = s
  48
  49 -- Lookup
  50 type family   Lookup k m
  51 type instance Lookup k Tip              = Nothing
  52 type instance Lookup k (Bin s k' v l r)
  53     = If (IsLT (Compare k k'))
  54          (Lookup k l)
  55          (If (IsGT (Compare k k'))
  56              (Lookup k r)
  57              (Just v))
  58
  59 -- LookupAssoc
  60 type family   LookupAssoc k m
  61 type instance LookupAssoc k Tip              = Nothing
  62 type instance LookupAssoc k (Bin s k' v l r)
  63     = If (IsLT (Compare k k'))
  64          (LookupAssoc k l)
  65          (If (IsGT (Compare k k'))
  66              (LookupAssoc k r)
  67              (Just (Cons k v)))
  68
  69 -- Member
  70 type Member k m = IsJust (Lookup k m)
  71
  72 -- NotMember
  73 type NotMember k m = Not (Member k m)
  74
  75 -- Find
  76 type Find k m = FromJust (Lookup k m)
  77
  78 -- FindWithDefault
  79 type FindWithDefault a k m
  80     = FromMaybe a (Lookup k m)
  81
  82 -- Empty
  83 type Empty = Tip
  84
  85 -- Singleton
  86 type Singleton k v = Bin D1 k v Tip Tip
  87
  88 -- Insert
  89 type family   Insert k v m
  90 type instance Insert k v Tip              = Singleton k v
  91 type instance Insert k v (Bin s k' v' l r)
  92     = If (IsLT (Compare k k'))
  93          (Balance k' v' (Insert k v l) r)
  94          (If (IsGT (Compare k k'))
  95              (Balance k' v' l (Insert k v r))
  96              (Bin s k v l r))
  97
  98 -- Balance
  99 type Delta = D5
 100 type Ratio = D2
 101
 102 type Balance k v l r
 103     = If (Size l :+: Size r :<: 1)
 104          (Bin (Size l :+: Size r :+: D1) k v l r)
 105          (If (Size r :>=: Delta :*: Size l)
 106              (RotateL k v l r)
 107              (If (Size l :>=: Delta :*: Size r)
 108                  (RotateR k v l r)
 109                  (Bin (Size l :+: Size r :+: D1) k v l r)))
 110
 111 -- Rotate
 112 type family   RotateL k v l r
 113 type instance RotateL k v l (Bin s k' v' l' r')
 114     = If (Size l' :<: Ratio :*: Size r')
 115          (SingleL k v l (Bin s k' v' l' r'))
 116          (DoubleL k v l (Bin s k' v' l' r'))
 117
 118 type family   RotateR k v l r
 119 type instance RotateR k v (Bin s k' v' l' r') r
 120     = If (Size r' :<: Ratio :*: Size l')
 121          (SingleR k v (Bin s k' v' l' r') r)
 122          (DoubleR k v (Bin s k' v' l' r') r)
 123
 124 -- Rotations
 125 type family   SingleL k v l r
 126 type instance SingleL k v l (Bin s k' v' l' r')
 127     = Bin' k' v' (Bin' k v l l') r'
 128
 129 type family   SingleR k v l r
 130 type instance SingleR k v (Bin s k' v' l r) r'
 131     = Bin' k' v' l (Bin' k v r r')
 132
 133 type family   DoubleL k v l r
 134 type instance DoubleL k v l (Bin s k' v' (Bin s' k'' v'' l' r) r')
 135     = Bin' k'' v'' (Bin' k v l l') (Bin' k' v' r r')
 136
 137 type family   DoubleR k v l r
 138 type instance DoubleR k v (Bin s k' v' l (Bin s' k'' v'' l' r)) r'
 139     = Bin' k'' v'' (Bin' k' v' l l') (Bin' k v r r')
 140
 141 -- Bin'
 142 type Bin' k v l r
 143     = Bin (Size l :+: Size r :+: D1) k v l r
 144