{- |
   The HList library

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

   Array-like access to HLists.
 -}

module Data.HList.HArray where

import Data.HList.FakePrelude
import Data.HList.HList


-- --------------------------------------------------------------------------
-- * Lookup

class HLookupByHNat (n :: HNat) (l :: [*]) where
  type HLookupByHNatR (n :: HNat) (l :: [*]) :: *
  hLookupByHNat :: Proxy n -> HList l -> HLookupByHNatR n l

instance HLookupByHNat HZero (e ': l) where
  type HLookupByHNatR HZero (e ': l) = e
  hLookupByHNat :: Proxy 'HZero -> HList (e : l) -> HLookupByHNatR 'HZero (e : l)
hLookupByHNat Proxy 'HZero
_ (HCons e
e HList l
_)        = e
e

instance HLookupByHNat n l => HLookupByHNat (HSucc n) (e ': l) where
  type HLookupByHNatR (HSucc n) (e ': l) = HLookupByHNatR n l
  hLookupByHNat :: Proxy ('HSucc n)
-> HList (e : l) -> HLookupByHNatR ('HSucc n) (e : l)
hLookupByHNat Proxy ('HSucc n)
n (HCons e
_ HList l
l) = forall (n :: HNat) (l :: [*]).
HLookupByHNat n l =>
Proxy n -> HList l -> HLookupByHNatR n l
hLookupByHNat (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
n) HList l
l


-- --------------------------------------------------------------------------
-- * Delete

class HDeleteAtHNat (n :: HNat) (l :: [*]) where
  type HDeleteAtHNatR (n :: HNat) (l :: [*]) :: [*]
  hDeleteAtHNat :: Proxy n -> HList l -> HList (HDeleteAtHNatR n l)

instance HDeleteAtHNat HZero (e ': l) where
  type HDeleteAtHNatR  HZero (e ': l) = l
  hDeleteAtHNat :: Proxy 'HZero
-> HList (e : l) -> HList (HDeleteAtHNatR 'HZero (e : l))
hDeleteAtHNat Proxy 'HZero
_ (HCons e
_ HList l
l)         = HList l
l

instance HDeleteAtHNat n l => HDeleteAtHNat (HSucc n) (e ': l) where
  type HDeleteAtHNatR  (HSucc n) (e ': l) = e ': (HDeleteAtHNatR n l)
  hDeleteAtHNat :: Proxy ('HSucc n)
-> HList (e : l) -> HList (HDeleteAtHNatR ('HSucc n) (e : l))
hDeleteAtHNat Proxy ('HSucc n)
n (HCons e
e HList l
l) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e (forall (n :: HNat) (l :: [*]).
HDeleteAtHNat n l =>
Proxy n -> HList l -> HList (HDeleteAtHNatR n l)
hDeleteAtHNat (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
n) HList l
l)


-- --------------------------------------------------------------------------
-- * Update
class HUpdateAtHNat' n e l l => HUpdateAtHNat n e l where
    hUpdateAtHNat :: Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l)

instance HUpdateAtHNat' n e l l => HUpdateAtHNat n e l where
    hUpdateAtHNat :: Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l)
hUpdateAtHNat = forall (n :: HNat) e (l :: [*]) (l0 :: [*]).
HUpdateAtHNat' n e l l0 =>
Proxy l0 -> Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l)
hUpdateAtHNat' (forall {k} (t :: k). Proxy t
Proxy :: Proxy l)

class HUpdateAtHNat' (n :: HNat) e (l :: [*]) (l0 :: [*]) where
  type HUpdateAtHNatR (n :: HNat) e (l :: [*]) :: [*]
  hUpdateAtHNat' :: Proxy l0 -> Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l)

instance HUpdateAtHNat' HZero e1 (e ': l) l0 where
  type HUpdateAtHNatR  HZero e1 (e ': l) = e1 ': l
  hUpdateAtHNat' :: Proxy l0
-> Proxy 'HZero
-> e1
-> HList (e : l)
-> HList (HUpdateAtHNatR 'HZero e1 (e : l))
hUpdateAtHNat' Proxy l0
_ Proxy 'HZero
_ e1
e1 (HCons e
_ HList l
l)      = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e1
e1 HList l
l

instance HUpdateAtHNat' n e1 l l0 => HUpdateAtHNat' (HSucc n) e1 (e ': l) l0 where
  type HUpdateAtHNatR  (HSucc n) e1 (e ': l) = e ': (HUpdateAtHNatR n e1 l)
  hUpdateAtHNat' :: Proxy l0
-> Proxy ('HSucc n)
-> e1
-> HList (e : l)
-> HList (HUpdateAtHNatR ('HSucc n) e1 (e : l))
hUpdateAtHNat' Proxy l0
l0 Proxy ('HSucc n)
n e1
e1 (HCons e
e HList l
l) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons e
e (forall (n :: HNat) e (l :: [*]) (l0 :: [*]).
HUpdateAtHNat' n e l l0 =>
Proxy l0 -> Proxy n -> e -> HList l -> HList (HUpdateAtHNatR n e l)
hUpdateAtHNat' Proxy l0
l0 (forall (n :: HNat). Proxy ('HSucc n) -> Proxy n
hPred Proxy ('HSucc n)
n) e1
e1 HList l
l)

instance Fail (HNatIndexTooLarge n HList l0) => HUpdateAtHNat' n e1 '[] l0 where
  type HUpdateAtHNatR n e1 '[] = '[]
  hUpdateAtHNat' :: Proxy l0
-> Proxy n -> e1 -> HList '[] -> HList (HUpdateAtHNatR n e1 '[])
hUpdateAtHNat' Proxy l0
_ Proxy n
_ e1
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Data.HList.HArray.HUpdateAtHNat: Fail must have no instances"

-- --------------------------------------------------------------------------
-- * Projection

-- One way of implementing it:

hProjectByHNats' :: r a -> HList l -> r b
hProjectByHNats' r a
ns HList l
l = forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap (forall (l :: [*]). HList l -> FHLookupByHNat l
FHLookupByHNat HList l
l) r a
ns

newtype FHLookupByHNat (l :: [*]) = FHLookupByHNat (HList l)

instance HLookupByHNat n l =>
    Apply (FHLookupByHNat l) (Proxy (n :: HNat)) where
  type ApplyR (FHLookupByHNat l) (Proxy n) = HLookupByHNatR n l
  apply :: FHLookupByHNat l -> Proxy n -> ApplyR (FHLookupByHNat l) (Proxy n)
apply (FHLookupByHNat HList l
l) Proxy n
n               = forall (n :: HNat) (l :: [*]).
HLookupByHNat n l =>
Proxy n -> HList l -> HLookupByHNatR n l
hLookupByHNat  Proxy n
n HList l
l

-- The drawback is that the list ns must be a constructed value.
-- We cannot lazily pattern-match on GADTs. Moreover, there are
-- repeated traversals of the HList l at run-time.

-- Here is a more optimal version with a better separation of
-- compile-time and run-time computation.
-- The list of labels to project is type-level only.
-- We treat this list of labels as a set -- that is, we will
-- ignore duplicates.
-- We traverse the HList l only once. The lookup in the list of
-- indices is compile-time only.
-- (In contrast, hProjectByHNats' does not ignore duplicates).
-- We unify hProjectByHNats and hProjectAwayByHNats in one
-- function, distinguished by the sel :: Bool in
-- FHUProj below. The operation hProjectByHNats corresponds
-- to sel = True (that is, elements of l whose indices are found in
-- ns are to be included in the result), whereas hProjectByHNats
-- corresponds to set = False.

hProjectByHNats :: Proxy ns -> a -> HList z
hProjectByHNats (Proxy ns
_ :: Proxy (ns :: [HNat])) a
l =
    forall {f} {a} {z :: [*]}.
(HUnfoldFD f (ApplyR f a) z, Apply f a) =>
f -> a -> HList z
hUnfold (forall (sel :: Bool) (ns :: [HNat]). FHUProj sel ns
FHUProj :: FHUProj True ns) (a
l,Proxy 'HZero
hZero)

data FHUProj (sel :: Bool) (ns :: [HNat]) = FHUProj

instance Apply (FHUProj sel ns) (HList '[],n) where
    type ApplyR (FHUProj sel ns) (HList '[],n) = HNothing
    apply :: FHUProj sel ns
-> (HList '[], n) -> ApplyR (FHUProj sel ns) (HList '[], n)
apply FHUProj sel ns
_ (HList '[], n)
_ = HNothing
HNothing

instance (ch ~ Proxy (HBoolEQ sel (KMember n ns)),
          Apply (ch, FHUProj sel ns) (HList (e ': l),Proxy (n :: HNat))) =>
    Apply (FHUProj sel ns) (HList (e ': l),Proxy (n :: HNat)) where
    type ApplyR (FHUProj sel ns) (HList (e ': l),Proxy n) =
       ApplyR (Proxy (HBoolEQ sel (KMember n ns)), FHUProj sel ns)
              (HList (e ': l),Proxy n)
    apply :: FHUProj sel ns
-> (HList (e : l), Proxy n)
-> ApplyR (FHUProj sel ns) (HList (e : l), Proxy n)
apply FHUProj sel ns
fn (HList (e : l), Proxy n)
s = forall f a. Apply f a => f -> a -> ApplyR f a
apply (forall {k} (t :: k). Proxy t
Proxy::ch,FHUProj sel ns
fn) (HList (e : l), Proxy n)
s

instance Apply (Proxy True, FHUProj sel ns)
               (HList (e ': l),Proxy (n::HNat)) where
    type ApplyR (Proxy True, FHUProj sel ns) (HList (e ': l),Proxy n) =
        (HJust (e, (HList l,Proxy (HSucc n))))
    apply :: (Proxy 'True, FHUProj sel ns)
-> (HList (e : l), Proxy n)
-> ApplyR (Proxy 'True, FHUProj sel ns) (HList (e : l), Proxy n)
apply (Proxy 'True, FHUProj sel ns)
_ (HCons e
e HList l
l,Proxy n
n) = (forall x. x -> HJust x
HJust (e
e,(HList l
l,forall (n :: HNat). Proxy n -> Proxy ('HSucc n)
hSucc Proxy n
n)))

instance (Apply (FHUProj sel ns) (HList l, Proxy (HSucc n))) =>
    Apply (Proxy False, FHUProj sel ns)
          (HList (e ': l),Proxy (n::HNat)) where
    type ApplyR (Proxy False, FHUProj sel ns) (HList (e ': l),Proxy n) =
        ApplyR (FHUProj sel ns) (HList l, Proxy (HSucc n))
    apply :: (Proxy 'False, FHUProj sel ns)
-> (HList (e : l), Proxy n)
-> ApplyR (Proxy 'False, FHUProj sel ns) (HList (e : l), Proxy n)
apply (Proxy 'False
_,FHUProj sel ns
fn) (HCons e
_ HList l
l,Proxy n
n) = forall f a. Apply f a => f -> a -> ApplyR f a
apply FHUProj sel ns
fn (HList l
l,forall (n :: HNat). Proxy n -> Proxy ('HSucc n)
hSucc Proxy n
n)


-- lifted member on naturals
type family KMember (n :: HNat) (ns :: [HNat]) :: Bool
type instance KMember n '[]       = False
type instance KMember n (n1 ': l) = HOr (HNatEq n n1) (KMember n l)

-- Useful abbreviations for complex types (which are inferred)
type HProjectByHNatsR (ns :: [HNat]) (l :: [*]) =
    HUnfold (FHUProj True ns) (HList l, Proxy 'HZero)

type HProjectByHNatsCtx ns l =
  (Apply (FHUProj True ns) (HList l, Proxy 'HZero),
      HUnfold' (FHUProj True ns)
       (HList l, Proxy 'HZero)
    )

-- * Complement of Projection

-- The naive approach is repeated deletion (which is a bit subtle
-- sine we need to adjust indices)
-- Instead, we compute the complement of indices to project away
-- to obtain the indices to project to, and then use hProjectByHNats.
-- Only the latter requires run-time computation. The rest
-- are done at compile-time only.

hProjectAwayByHNats :: Proxy ns -> a -> HList z
hProjectAwayByHNats (Proxy ns
_ :: Proxy (ns :: [HNat])) a
l =
    forall {f} {a} {z :: [*]}.
(HUnfoldFD f (ApplyR f a) z, Apply f a) =>
f -> a -> HList z
hUnfold (forall (sel :: Bool) (ns :: [HNat]). FHUProj sel ns
FHUProj :: FHUProj False ns) (a
l,Proxy 'HZero
hZero)


-- Useful abbreviations for complex types (which are inferred)
type HProjectAwayByHNatsR (ns :: [HNat]) (l :: [*]) =
    HUnfold (FHUProj False ns) (HList l, Proxy 'HZero)

type HProjectAwayByHNatsCtx ns l =
  (Apply (FHUProj False ns) (HList l, Proxy 'HZero),
      HUnfold' (FHUProj False ns) (HList l, Proxy 'HZero)
  )

-- * Splitting
-- | Splitting an array according to indices

-- The following is not optimal; we'll optimize later if needed

hSplitByHNats :: Proxy ns -> a -> (HList z, HList z)
hSplitByHNats Proxy ns
ns a
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 Proxy ns
ns a
l,
                      forall {ns :: [HNat]} {a} {z :: [*]}.
(HUnfoldFD
   (FHUProj 'False ns)
   (ApplyR (FHUProj 'False ns) (a, Proxy 'HZero))
   z,
 Apply (FHUProj 'False ns) (a, Proxy 'HZero)) =>
Proxy ns -> a -> HList z
hProjectAwayByHNats Proxy ns
ns a
l)
{-
hSplitByHNats ns l = hSplitByHNats' ns (hFlag l)

class HNats ns => HSplitByHNats' ns l l' l'' | ns l -> l' l''
 where
  hSplitByHNats' :: ns -> l -> (l',l'')

instance HSplit l l' l''
      => HSplitByHNats' HNil l HNil l'
 where
  hSplitByHNats' HNil l = (HNil,l')
   where
    (l',_) = hSplit l

instance ( HLookupByHNat n l (e,b)
         , HUpdateAtHNat n (e,HFalse) l l'''
         , HSplitByHNats' ns l''' l' l''
         )
      =>   HSplitByHNats' (HCons n ns) l (HCons e l') l''
 where
  hSplitByHNats' (HCons n ns) l = (HCons e l',l'')
   where
    (e,_)    = hLookupByHNat  n l
    l'''     = hUpdateAtHNat  n (e,hFalse) l
    (l',l'') = hSplitByHNats' ns l'''
-}


{-

-- --------------------------------------------------------------------------
-- * Bounded lists

class HMaxLength l s
instance (HLength l s', HLt s' (HSucc s) HTrue) => HMaxLength l s

class HMinLength l s
instance (HLength l s', HLt s (HSucc s') HTrue) => HMinLength l s

class HSingleton l
instance HLength l (HSucc HZero) => HSingleton l

hSingle :: (HSingleton l, HHead l e) => l -> e
hSingle = hHead

-}