type-level maps and maybes

[hs-rrdtool.git] / Types / Data / Map.hs

diff --git a/Types/Data/Map.hs b/Types/Data/Map.hs
new file mode 100644 (file)
index 0000000..95fe59b
--- /dev/null
+++ b/Types/Data/Map.hs
@@ -0,0 +1,144 @@
+{-# 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
+