{- |
   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 :: proxy1 e -> proxy l -> Proxy n
hType2HNat proxy1 e
_ proxy l
_ = Proxy n
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 :: Proxy es -> hlist l -> Proxy ns
hTypes2HNats Proxy es
_ hlist l
_ = Proxy ns
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 '[]
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 l) =
      Proxy b -> Proxy e1 -> e -> HList l -> HList l1
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 (Proxy b
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 = Proxy e -> HList l -> HList l1
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 = e -> HList l1 -> HList (e : l1)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e (Proxy e1 -> HList l -> HList l1
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 = Proxy n -> HList l -> HList (HDeleteAtHNatR n l)
forall (n :: HNat) (l :: [*]).
HDeleteAtHNat n l =>
Proxy n -> HList l -> HList (HDeleteAtHNatR n l)
hDeleteAtHNat (proxy1 e -> HList l -> Proxy n
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 = Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l)
forall (n :: HNat) e (l :: [*]).
HUpdateAtHNat n e l =>
Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l)
hUpdateAtHNat (Maybe e -> HList l -> Proxy n
forall k (e :: k) (l :: [k]) (n :: HNat) (proxy1 :: k -> *)
       (proxy :: [k] -> *).
HType2HNat e l n =>
proxy1 e -> proxy l -> Proxy n
hType2HNat (e -> Maybe e
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 = Proxy ns -> hlist l -> HList z
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 (Proxy es -> hlist l -> Proxy ns
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 = Proxy ns -> hlist l -> (HList z1, HList z2)
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 (Proxy es -> hlist l -> Proxy ns
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
_ = Proxy n -> HList l -> HList (HDeleteAtHNatR n l)
forall (n :: HNat) (l :: [*]).
HDeleteAtHNat n l =>
Proxy n -> HList l -> HList (HDeleteAtHNatR n l)
hDeleteAtHNat (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n)