{- |
   The HList library

   (C) 2004, Oleg Kiselyov, Ralf Laemmel, Keean Schupke

   Type-indexed operations on typeful heterogeneous lists.
-}

module Data.HList.HTypeIndexed where

import Data.HList.FakePrelude
import Data.HList.HListPrelude
import Data.HList.HList
import Data.HList.HArray
import Data.HList.HOccurs ()

-- --------------------------------------------------------------------------
-- | Map a type to a natural (index within the collection)
-- This is a purely type-level computation

instance (HEq e1 e b, HType2HNatCase b e1 l n) => HType2HNat e1 (e ': l) n

-- | Helper class
class HType2HNatCase (b :: Bool) (e :: *) (l :: [*]) (n :: HNat) | b e l -> n
instance HOccursNot e l => HType2HNatCase True e l HZero
instance HType2HNat e l n => HType2HNatCase False e l (HSucc n)

hType2HNat :: HType2HNat e l n => proxy1 e -> proxy l -> Proxy n
hType2HNat :: forall {k} (e :: k) (l :: [k]) (n :: HNat) (proxy1 :: k -> *)
       (proxy :: [k] -> *).
HType2HNat e l n =>
proxy1 e -> proxy l -> Proxy n
hType2HNat proxy1 e
_ proxy l
_ = forall {k} (t :: k). Proxy t
Proxy

-- | And lift to the list of types

instance HTypes2HNats ('[] :: [*]) (l :: [*]) '[]

instance (HType2HNat e l n, HTypes2HNats es l ns)
      => HTypes2HNats (e ': es) (l :: [*]) (n ': ns)

hTypes2HNats :: HTypes2HNats es l ns =>
                Proxy (es :: [*]) -> hlist l -> Proxy (ns :: [HNat])
hTypes2HNats :: forall {k} (es :: [*]) (l :: k) (ns :: [HNat]) (hlist :: k -> *).
HTypes2HNats es l ns =>
Proxy es -> hlist l -> Proxy ns
hTypes2HNats Proxy es
_ hlist l
_ = forall {k} (t :: k). Proxy t
Proxy

-- --------------------------------------------------------------------------
-- Implementing the generic interfaces

instance HDeleteMany e (HList '[]) (HList '[]) where
  hDeleteMany :: Proxy e -> HList '[] -> HList '[]
hDeleteMany Proxy e
_ HList '[]
R:HList[]
HNil = HList '[]
HNil

instance (HEq e1 e b, HDeleteManyCase b e1 e l l1)
      => HDeleteMany e1 (HList (e ': l)) (HList l1) where
  hDeleteMany :: Proxy e1 -> HList (e : l) -> HList l1
hDeleteMany Proxy e1
p (HCons e
e HList l
l) =
      forall {k} (b :: Bool) (e1 :: k) e (l :: [*]) (l1 :: [*]).
HDeleteManyCase b e1 e l l1 =>
Proxy b -> Proxy e1 -> e -> HList l -> HList l1
hDeleteManyCase (forall {k} (t :: k). Proxy t
Proxy :: Proxy b) Proxy e1
p e
e HList l
l

class HDeleteManyCase (b :: Bool) e1 e l l1 | b e1 e l -> l1 where
  hDeleteManyCase :: Proxy b -> Proxy e1 -> e -> HList l -> HList l1

instance HDeleteMany e (HList l) (HList l1) => HDeleteManyCase True e e l l1
 where
  hDeleteManyCase :: Proxy 'True -> Proxy e -> e -> HList l -> HList l1
hDeleteManyCase Proxy 'True
_ Proxy e
p e
_ HList l
l = forall {k} (e :: k) l l'. HDeleteMany e l l' => Proxy e -> l -> l'
hDeleteMany Proxy e
p HList l
l


instance HDeleteMany e1 (HList l) (HList l1)
      => HDeleteManyCase False e1 e l (e ': l1) where
  hDeleteManyCase :: Proxy 'False -> Proxy e1 -> e -> HList l -> HList (e : l1)
hDeleteManyCase Proxy 'False
_ Proxy e1
p e
e HList l
l = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e (forall {k} (e :: k) l l'. HDeleteMany e l l' => Proxy e -> l -> l'
hDeleteMany Proxy e1
p HList l
l)

-- --------------------------------------------------------------------------
-- Type-indexed operations in terms of the natural-based primitives

hDeleteAt :: proxy1 e -> HList l -> HList (HDeleteAtHNatR n l)
hDeleteAt proxy1 e
p HList l
l = forall (n :: HNat) (l :: [*]).
HDeleteAtHNat n l =>
Proxy n -> HList l -> HList (HDeleteAtHNatR n l)
hDeleteAtHNat (forall {k} (e :: k) (l :: [k]) (n :: HNat) (proxy1 :: k -> *)
       (proxy :: [k] -> *).
HType2HNat e l n =>
proxy1 e -> proxy l -> Proxy n
hType2HNat proxy1 e
p HList l
l) HList l
l

hUpdateAt :: e -> HList l -> HList (HUpdateAtHNatR n e l)
hUpdateAt e
e HList l
l = forall (n :: HNat) e (l :: [*]).
HUpdateAtHNat n e l =>
Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l)
hUpdateAtHNat (forall {k} (e :: k) (l :: [k]) (n :: HNat) (proxy1 :: k -> *)
       (proxy :: [k] -> *).
HType2HNat e l n =>
proxy1 e -> proxy l -> Proxy n
hType2HNat (forall a. a -> Maybe a
Just e
e) HList l
l) e
e HList l
l

hProjectBy :: Proxy es -> hlist l -> HList z
hProjectBy Proxy es
ps hlist l
l = forall {ns :: [HNat]} {a} {z :: [*]}.
(HUnfoldFD
   (FHUProj 'True ns) (ApplyR (FHUProj 'True ns) (a, Proxy 'HZero)) z,
 Apply (FHUProj 'True ns) (a, Proxy 'HZero)) =>
Proxy ns -> a -> HList z
hProjectByHNats (forall {k} (es :: [*]) (l :: k) (ns :: [HNat]) (hlist :: k -> *).
HTypes2HNats es l ns =>
Proxy es -> hlist l -> Proxy ns
hTypes2HNats Proxy es
ps hlist l
l) hlist l
l

hSplitBy :: Proxy es -> hlist l -> (HList z1, HList z2)
hSplitBy Proxy es
ps hlist l
l = forall {ns :: [HNat]} {a} {z1 :: [*]} {z2 :: [*]}.
(HUnfoldFD
   (FHUProj 'True ns)
   (ApplyR (FHUProj 'True ns) (a, Proxy 'HZero))
   z1,
 HUnfoldFD
   (FHUProj 'False ns)
   (ApplyR (FHUProj 'False ns) (a, Proxy 'HZero))
   z2,
 Apply (FHUProj 'True ns) (a, Proxy 'HZero),
 Apply (FHUProj 'False ns) (a, Proxy 'HZero)) =>
Proxy ns -> a -> (HList z1, HList z2)
hSplitByHNats (forall {k} (es :: [*]) (l :: k) (ns :: [HNat]) (hlist :: k -> *).
HTypes2HNats es l ns =>
Proxy es -> hlist l -> Proxy ns
hTypes2HNats Proxy es
ps hlist l
l) hlist l
l


-- | should this instead delete the first element of that type?
instance (HDeleteAtHNat n l, HType2HNat e l n, l' ~ HDeleteAtHNatR n l)
      => HDeleteAtLabel HList e l l' where
    hDeleteAtLabel :: Label e -> HList l -> HList l'
hDeleteAtLabel Label e
_ = forall (n :: HNat) (l :: [*]).
HDeleteAtHNat n l =>
Proxy n -> HList l -> HList (HDeleteAtHNatR n l)
hDeleteAtHNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)