{-# LANGUAGE CPP #-}

{- |
   The HList library

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

   Type-indexed products.
   The public interface is described in
   <Data-HList-CommonMain.html#t:TIP CommonMain#TIP>
-}

module Data.HList.TIP
  (module Data.HList.TIPtuple,
   module Data.HList.TIP) where


import Data.HList.HListPrelude
import Data.HList.FakePrelude
import Data.HList.HList
import Data.HList.Record
import Data.HList.HTypeIndexed ()
import Data.HList.TIPtuple
import Data.List (intercalate)
import Data.Array (Ix)
import Data.Semigroup (Semigroup)


#if __GLASGOW_HASKELL__ > 710
import Data.Coerce
#endif

import LensDefs

-- --------------------------------------------------------------------------
-- * The newtype for type-indexed products

-- | TIPs are like 'Record', except element \"i\" of the list \"l\"
-- has type @Tagged e_i e_i@
newtype TIP (l :: [*]) = TIP{TIP l -> HList l
unTIP:: HList l}

deriving instance Semigroup (HList a) => Semigroup (TIP a)
deriving instance Monoid (HList a) => Monoid (TIP a)
deriving instance Eq (HList a) => Eq (TIP a)
deriving instance (Ord (HList r)) => Ord (TIP r)
deriving instance (Ix (HList r)) => Ix (TIP r)
deriving instance (Bounded (HList r)) => Bounded (TIP r)


instance HMapOut (HShow `HComp` HUntag) l String => Show (TIP l) where
  showsPrec :: Int -> TIP l -> ShowS
showsPrec Int
_ (TIP HList l
l) = (String
"TIPH[" String -> ShowS
forall a. [a] -> [a] -> [a]
++)
                              ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," (HComp HShow HUntag -> HList l -> [String]
forall f e (l :: [*]). HMapOut f l e => f -> HList l -> [e]
hMapOut (HShow
HShow HShow -> HUntag -> HComp HShow HUntag
forall g f. g -> f -> HComp g f
`HComp` HUntag
HUntag) HList l
l) String -> ShowS
forall a. [a] -> [a] -> [a]
++)
                              ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char
']' Char -> ShowS
forall a. a -> [a] -> [a]
:)


mkTIP :: HTypeIndexed l => HList l -> TIP l
mkTIP :: HList l -> TIP l
mkTIP = HList l -> TIP l
forall (l :: [*]). HList l -> TIP l
TIP

emptyTIP :: TIP '[]
emptyTIP :: TIP '[]
emptyTIP = HList '[] -> TIP '[]
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP HList '[]
HNil

-- --------------------------------------------------------------------------
-- * Type-indexed type sequences

-- | this constraint ensures that a TIP created by 'mkTIP' has no
-- duplicates
class (HAllTaggedEq l, HRLabelSet l) => HTypeIndexed (l :: [*])

instance (HAllTaggedEq l, HRLabelSet l) => HTypeIndexed l

class HAllTaggedEq (l :: [*])
instance HAllTaggedEq '[]
instance (HAllTaggedEq l, tee ~ Tagged e e') => HAllTaggedEq (tee ': l)

-- --------------------------------------------------------------------------
-- Implementing the HListPrelude interface

instance (HRLabelSet (Tagged e e ': l), HTypeIndexed l) => HExtend e (TIP l)
 where
  type HExtendR e (TIP l) = TIP (Tagged e e ': l)
  e
e .*. :: e -> TIP l -> HExtendR e (TIP l)
.*. TIP HList l
l = HList (Tagged e e : l) -> TIP (Tagged e e : l)
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP (Tagged e e -> HList l -> HList (Tagged e e : l)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons (e -> Tagged e e
forall k (s :: k) b. b -> Tagged s b
Tagged e
e) HList l
l)



instance (e ~ e', HasField e (Record l) e') => HasField e (TIP l) e' where
    hLookupByLabel :: Label e -> TIP l -> e'
hLookupByLabel Label e
lab (TIP HList l
l) = Label e -> Record l -> e'
forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel Label e
lab (HList l -> Record l
forall (r :: [*]). HList r -> Record r
Record HList l
l)

-- | One occurrence and nothing is left
--
-- This variation provides an extra feature for singleton lists.
-- That is, the result type is unified with the element in the list.
-- Hence the explicit provision of a result type can be omitted.
--

instance (tee ~ Tagged e e) => HOccurs e (TIP '[tee]) where
  hOccurs :: TIP '[tee] -> e
hOccurs (TIP (HCons (Tagged e) _)) = e
e

instance HasField e (Record (x ': y ': l)) e
      => HOccurs e (TIP (x ': y ': l)) where
  hOccurs :: TIP (x : y : l) -> e
hOccurs (TIP HList (x : y : l)
l) = HList (x : y : l) -> Record (x : y : l)
forall (r :: [*]). HList r -> Record r
Record HList (x : y : l)
l Record (x : y : l) -> Label e -> e
forall k (l :: k) r v. HasField l r v => r -> Label l -> v
.!. (Label e
forall k (l :: k). Label l
Label :: Label e)


instance (HAppend (HList l) (HList l'), HTypeIndexed (HAppendListR l l'))
           => HAppend (TIP l) (TIP l')
 where
  hAppend :: TIP l -> TIP l' -> HAppendR (TIP l) (TIP l')
hAppend (TIP HList l
l) (TIP HList l'
l') = HList (HAppendListR l l') -> TIP (HAppendListR l l')
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP (HList l -> HList l' -> HAppendR (HList l) (HList l')
forall l1 l2. HAppend l1 l2 => l1 -> l2 -> HAppendR l1 l2
hAppend HList l
l HList l'
l')

type instance HAppendR (TIP l) (TIP l') = TIP (HAppendListR l l')


-- instance HOccurrence HList e l l' => HOccurrence TIP e l l'
--  where
--   hOccurrence e = TIP . hOccurrence e . unTIP

-- --------------------------------------------------------------------------
-- * Shielding type-indexed operations
-- $note The absence of signatures is deliberate! They all must be inferred.

onRecord :: (Record r -> Record l) -> TIP r -> TIP l
onRecord Record r -> Record l
f (TIP HList r
l) = let Record HList l
l' = Record r -> Record l
f (HList r -> Record r
forall (r :: [*]). HList r -> Record r
Record HList r
l) in HList l -> TIP l
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP HList l
l'

instance (HDeleteAtLabel Record e v v',
          HTypeIndexed v')
      => HDeleteAtLabel TIP e v v' where
  hDeleteAtLabel :: Label e -> TIP v -> TIP v'
hDeleteAtLabel Label e
e TIP v
v = (Record v -> Record v') -> TIP v -> TIP v'
forall (l :: [*]) (r :: [*]).
(HAllTaggedEq l, HLabelSet (LabelsOf l), HAllTaggedLV l) =>
(Record r -> Record l) -> TIP r -> TIP l
onRecord (Label e -> Record v -> Record v'
forall k (r :: [*] -> *) (l :: k) (v :: [*]) (v' :: [*]).
HDeleteAtLabel r l v v' =>
Label l -> r v -> r v'
hDeleteAtLabel Label e
e) TIP v
v


tipyUpdate :: v -> record r -> record r
tipyUpdate  v
e record r
t  = Label v -> v -> record r -> record r
forall k (record :: [*] -> *) (l :: k) v (r :: [*]).
HTPupdateAtLabel record l v r =>
Label l -> v -> record r -> record r
hTPupdateAtLabel (v -> Label v
forall e. e -> Label e
fromValue v
e) v
e record r
t
  where fromValue :: e -> Label e
        fromValue :: e -> Label e
fromValue e
_ = Label e
forall k (l :: k). Label l
Label

instance (HUpdateAtLabel Record e' e r r',
          HTypeIndexed r',
         e ~ e') => HUpdateAtLabel TIP e' e r r' where
  hUpdateAtLabel :: Label e' -> e -> TIP r -> TIP r'
hUpdateAtLabel Label e'
l e
e TIP r
r = (Record r -> Record r') -> TIP r -> TIP r'
forall (l :: [*]) (r :: [*]).
(HAllTaggedEq l, HLabelSet (LabelsOf l), HAllTaggedLV l) =>
(Record r -> Record l) -> TIP r -> TIP l
onRecord (Label e' -> e -> Record r -> Record r'
forall k (record :: [*] -> *) (l :: k) v (r :: [*]) (r' :: [*]).
(HUpdateAtLabel record l v r r', SameLength r r') =>
Label l -> v -> record r -> record r'
hUpdateAtLabel Label e'
l e
e) TIP r
r


-- | Use 'Labels' to specify the first argument
tipyProject :: proxy ls -> TIP t -> TIP l
tipyProject proxy ls
ps TIP t
t = (Record t -> Record l) -> TIP t -> TIP l
forall (l :: [*]) (r :: [*]).
(HAllTaggedEq l, HLabelSet (LabelsOf l), HAllTaggedLV l) =>
(Record r -> Record l) -> TIP r -> TIP l
onRecord (proxy ls -> Record t -> Record l
forall (a :: [*]) (ls :: [*]) (t :: [*]) (b :: [*])
       (proxy :: [*] -> *).
(HRLabelSet a, H2ProjectByLabels ls t a b) =>
proxy ls -> Record t -> Record a
hProjectByLabels proxy ls
ps) TIP t
t

-- | provides a @Lens' (TIP s) a@. 'hLens'' @:: Label a -> Lens' (TIP s) a@
-- is another option.
#if __GLASGOW_HASKELL__ < 707
tipyLens' x = isSimple tipyLens x -- rejected by GHC-7.10RC1
#else
tipyLens' :: (a -> f a) -> TIP t -> f (TIP t)
tipyLens' a -> f a
f TIP t
s = ((a -> f a) -> TIP t -> f (TIP t))
-> (a -> f a) -> TIP t -> f (TIP t)
forall k1 k2 optic (p :: k1 -> k2 -> *) (a :: k1) (f :: k1 -> k2)
       (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple (Label a
-> forall (f :: * -> *).
   Functor f =>
   (a -> f a) -> TIP t -> f (TIP t)
forall k (x :: k) (r :: [*] -> *) (s :: [*]) (t :: [*]) a b.
HLens x r s t a b =>
Label x
-> forall (f :: * -> *). Functor f => (a -> f b) -> r s -> f (r t)
hLens Label a
x) a -> f a
f (TIP t -> TIP t
forall (a :: [*]). TIP a -> TIP a
asTIP TIP t
s) -- rejected by GHC-7.6.3
  where
    x :: Label a
x = (a -> f a) -> Label a
forall a (f :: * -> *). (a -> f a) -> Label a
getA a -> f a
f
    getA :: (a -> f a) -> Label a
    getA :: (a -> f a) -> Label a
getA a -> f a
_ = Label a
forall k (l :: k). Label l
Label

    asTIP :: TIP a -> TIP a
    asTIP :: TIP a -> TIP a
asTIP = TIP a -> TIP a
forall a. a -> a
id
#endif

{- | provides a @Lens (TIP s) (TIP t) a b@

When using @set@ (also known as @.~@), 'tipyLens'' can address the
ambiguity as to which field \"a\" should actually be updated.

-}
tipyLens :: (a -> f a)
-> TIP (Tagged x x : xs)
-> f (TIP (HAppendListR l1 (Tagged a a : xs)))
tipyLens a -> f a
f (TIP HList (Tagged x x : xs)
s) =
      case Proxy n
-> HList (Tagged x x : xs) -> (HList l1, HList (Tagged a a : xs))
forall (n :: HNat) (xsys :: [*]) (xs :: [*]) (ys :: [*]).
HSplitAt n xsys xs ys =>
Proxy n -> HList xsys -> (HList xs, HList ys)
hSplitAt (HList (Tagged x x : xs) -> (a -> f a) -> Proxy n
forall k a (s :: [*]) (n :: HNat) (f :: k -> *) (b :: k).
HFind (Label a) (LabelsOf s) n =>
HList s -> (a -> f b) -> Proxy n
getN HList (Tagged x x : xs)
s a -> f a
f) (HList (Tagged x x : xs) -> HList (Tagged x x : xs)
forall x (xs :: [*]).
HList (Tagged x x : xs) -> HList (Tagged x x : xs)
ghc8fix1 HList (Tagged x x : xs)
s) of
          (HList l1
x, ta@(Tagged a) `HCons` ys)
             | () <- Tagged a a -> ()
forall a. Tagged a a -> ()
ghc8fix2 Tagged a a
ta ->
              let mkt :: a -> TIP (HAppendListR l1 (Tagged a a : xs))
mkt a
b = HList (HAppendListR l1 (Tagged a a : xs))
-> TIP (HAppendListR l1 (Tagged a a : xs))
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP (HList l1
x HList l1
-> HList (Tagged a a : xs)
-> HList (HAppendListR l1 (Tagged a a : xs))
forall (l1 :: [*]) (l2 :: [*]).
HAppendList l1 l2 =>
HList l1 -> HList l2 -> HList (HAppendListR l1 l2)
`hAppendList` (a -> Tagged a a
forall a. a -> Tagged a a
tagSelf a
b Tagged a a -> HList xs -> HList (Tagged a a : xs)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList xs
ys))
              in a -> TIP (HAppendListR l1 (Tagged a a : xs))
mkt (a -> TIP (HAppendListR l1 (Tagged a a : xs)))
-> f a -> f (TIP (HAppendListR l1 (Tagged a a : xs)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f a
a
  where
    getN :: HFind (Label a) (LabelsOf s) n => HList s -> (a -> f b) -> Proxy n
    getN :: HList s -> (a -> f b) -> Proxy n
getN HList s
_ a -> f b
_ = Proxy n
forall k (t :: k). Proxy t
Proxy

    -- without these, tipyLens has a type that has kind variables,
    -- (that end up being * when an actual TIP is provided), leading to
    -- a Properties.LengthIndependent compile error:
    -- .../.stack-work/dist/x86_64-linux/Cabal-1.24.2.0/build/Data/HList/TIP.hi
    -- Declaration for tipyLens:
    --   Iface type variable out of scope:  k
    -- Cannot continue after interface file error
    ghc8fix1 :: HList (Tagged x x ': xs) -> HList (Tagged x x ': xs)
    ghc8fix1 :: HList (Tagged x x : xs) -> HList (Tagged x x : xs)
ghc8fix1 = HList (Tagged x x : xs) -> HList (Tagged x x : xs)
forall a. a -> a
id

    ghc8fix2 :: Tagged a a -> ()
    ghc8fix2 :: Tagged a a -> ()
ghc8fix2 Tagged a a
_ = ()



-- | The same as 'tipyProject', except also return the
-- types not requested in the @proxy@ argument
tipyProject2 :: proxy ls -> TIP r -> (TIP l, TIP l)
tipyProject2 proxy ls
ps (TIP HList r
l) = (HList l -> TIP l
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP HList l
l',HList l -> TIP l
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP HList l
l'')
 where
  (HList l
l',HList l
l'') = proxy ls -> HList r -> (HList l, HList l)
forall (ls :: [*]) (r :: [*]) (rin :: [*]) (rout :: [*])
       (proxy :: [*] -> *).
H2ProjectByLabels ls r rin rout =>
proxy ls -> HList r -> (HList rin, HList rout)
h2projectByLabels proxy ls
ps HList r
l


-- --------------------------------------------------------------------------

-- | Subtyping for TIPs

instance SubType (TIP l) (TIP '[])
instance (HOccurs e (TIP l1), SubType (TIP l1) (TIP l2))
      =>  SubType (TIP l1) (TIP (e ': l2))


-- --------------------------------------------------------------------------
-- * conversion to and from 'HList'

{- | 'TagR' can also be used to avoid redundancy when defining types for TIC and TIP.

>  type XShort = TagR [A,B,C,D]

>  type XLong = [Tagged A A, Tagged B B, Tagged C C, Tagged D D]


an equivalent FD version, which is slightly better with respect to
simplifying types containing type variables (in ghc-7.8 and 7.6):
<http://stackoverflow.com/questions/24110410/>

With ghc-7.10 (<http://ghc.haskell.org/trac/ghc/ticket/10009>) the FD version is superior
to the TF version:

@
class (UntagR (TagR a) ~ a) => TagUntag a where
    type TagR a :: [*]
    hTagSelf :: HList a -> HList (TagR a)
    hUntagSelf :: HList (TagR a) -> HList a

instance TagUntag '[] where
    type TagR '[] = '[]
    hTagSelf _ = HNil
    hUntagSelf _ = HNil

instance TagUntag xs => TagUntag (x ': xs) where
    type TagR (x ': xs) = Tagged x x ': TagR xs
    hTagSelf (HCons x xs) = Tagged x `HCons` hTagSelf xs
    hUntagSelf (HCons (Tagged x) xs) = x `HCons` hUntagSelf xs

type family UntagR (xs :: [*]) :: [*]
type instance UntagR '[] = '[]
type instance UntagR (x ': xs) = Untag1 x ': UntagR xs
@

Length information should flow backwards

>>> let len2 x = x `asTypeOf` (undefined :: HList '[a,b])
>>> let f = len2 $ hTagSelf (hReplicate Proxy ())
>>> :t f
f :: HList '[Tagged () (), Tagged () ()]

-}
class SameLength a ta => TagUntagFD a ta | a -> ta, ta -> a where
    hTagSelf :: HList a -> HList ta
    hUntagSelf :: HList ta -> HList a

instance TagUntagFD '[] '[] where
    hTagSelf :: HList '[] -> HList '[]
hTagSelf HList '[]
_ = HList '[]
HNil
    hUntagSelf :: HList '[] -> HList '[]
hUntagSelf HList '[]
_ = HList '[]
HNil

instance (TagUntagFD xs ys, txx ~ Tagged x x)
      => TagUntagFD (x ': xs) (txx ': ys) where
    hTagSelf :: HList (x : xs) -> HList (txx : ys)
hTagSelf (HCons x xs) = x -> Tagged x x
forall k (s :: k) b. b -> Tagged s b
Tagged x
x Tagged x x -> HList ys -> HList (Tagged x x : ys)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList xs -> HList ys
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList a -> HList ta
hTagSelf HList xs
xs
    hUntagSelf :: HList (txx : ys) -> HList (x : xs)
hUntagSelf (HCons (Tagged x) xs) = x
x x -> HList xs -> HList (x : xs)
forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList ys -> HList xs
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList ta -> HList a
hUntagSelf HList ys
xs

type TagUntag xs = TagUntagFD xs (TagR xs)

-- | Sometimes the type variables available have @TagR@ already applied
-- (ie the lists have elements like @Tagged X X@). Then this abbreviation
-- is useful:
type UntagTag xs = (TagR (UntagR xs) ~ xs, TagUntagFD (UntagR xs) xs)

type family TagR (a :: [*]) :: [*]
type family UntagR (ta :: [*]) :: [*]

type instance TagR '[] = '[]
type instance UntagR '[] = '[]

type instance TagR (x ': xs) = Tagged x x ': TagR xs
type instance UntagR (Tagged y y ': ys) = y ': UntagR ys

type family Untag1 (x :: *) :: *
type instance Untag1 (Tagged k x) = x


-- | @Iso (TIP (TagR a)) (TIP (TagR b)) (HList a) (HList b)@
tipHList :: p (HList a) (f (HList a)) -> p (TIP ta) (f (TIP l))
tipHList p (HList a) (f (HList a))
x = (TIP ta -> HList a)
-> (HList a -> TIP l)
-> p (HList a) (f (HList a))
-> p (TIP ta) (f (TIP l))
forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso (\(TIP HList ta
a) -> HList ta -> HList a
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList ta -> HList a
hUntagSelf HList ta
a) (HList l -> TIP l
forall (l :: [*]). HList l -> TIP l
TIP (HList l -> TIP l) -> (HList a -> HList l) -> HList a -> TIP l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HList a -> HList l
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList a -> HList ta
hTagSelf) p (HList a) (f (HList a))
x

-- | @Iso' (TIP (TagR s)) (HList a)@
tipHList' :: p (HList a) (f (HList a)) -> p (TIP l) (f (TIP l))
tipHList' p (HList a) (f (HList a))
x = (p (HList a) (f (HList a)) -> p (TIP l) (f (TIP l)))
-> p (HList a) (f (HList a)) -> p (TIP l) (f (TIP l))
forall k1 k2 optic (p :: k1 -> k2 -> *) (a :: k1) (f :: k1 -> k2)
       (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple p (HList a) (f (HList a)) -> p (TIP l) (f (TIP l))
forall (p :: * -> * -> *) (f :: * -> *) (a :: [*]) (ta :: [*])
       (a :: [*]) (l :: [*]).
(Profunctor p, Functor f, TagUntagFD a ta, TagUntagFD a l) =>
p (HList a) (f (HList a)) -> p (TIP ta) (f (TIP l))
tipHList p (HList a) (f (HList a))
x


-- * conversion to and from 'Record'

-- | @Iso (TIP s) (TIP t) (Record s) (Record t)@
--
-- 'typeIndexed' may be more appropriate
tipRecord :: p (Record r) (f (Record l)) -> p (TIP r) (f (TIP l))
tipRecord p (Record r) (f (Record l))
x = (TIP r -> Record r)
-> (Record l -> TIP l)
-> p (Record r) (f (Record l))
-> p (TIP r) (f (TIP l))
forall (p :: * -> * -> *) (f :: * -> *) b t a s.
(Profunctor p, Functor f, Coercible b t, Coercible a s) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
isoNewtype (\(TIP HList r
a) -> HList r -> Record r
forall (r :: [*]). HList r -> Record r
Record HList r
a) (\(Record HList l
b) -> HList l -> TIP l
forall (l :: [*]). HList l -> TIP l
TIP HList l
b) p (Record r) (f (Record l))
x

-- | @Iso' (TIP (TagR s)) (Record a)@
tipRecord' :: p (Record l) (f (Record l)) -> p (TIP l) (f (TIP l))
tipRecord' p (Record l) (f (Record l))
x = (p (Record l) (f (Record l)) -> p (TIP l) (f (TIP l)))
-> p (Record l) (f (Record l)) -> p (TIP l) (f (TIP l))
forall k1 k2 optic (p :: k1 -> k2 -> *) (a :: k1) (f :: k1 -> k2)
       (s :: k1).
(optic ~ (p a (f a) -> p s (f s))) =>
optic -> optic
isSimple p (Record l) (f (Record l)) -> p (TIP l) (f (TIP l))
forall (p :: * -> * -> *) (f :: * -> *) (r :: [*]) (l :: [*]).
(Profunctor p, Functor f) =>
p (Record r) (f (Record l)) -> p (TIP r) (f (TIP l))
tipRecord p (Record l) (f (Record l))
x

-- --------------------------------------------------------------------------
-- * Zip

#if __GLASGOW_HASKELL__ < 800
-- pre-coerce
instance (HZipList (UntagR x) (UntagR y) (UntagR xy),
          UntagTag x, UntagTag y, UntagTag xy,
          SameLengths [x,y,xy],
          HTypeIndexed x, HTypeIndexed y,
          HUnzip TIP x y xy
          -- HTypeIndexed xy is always satisfied given the above
          -- constraints (with a handwaving proof), so don't require
          -- callers of hZip/hUnzip to supply such proof
    ) => HZip TIP x y xy where
  hZip = hZipTIP


instance (HZipList (UntagR x) (UntagR y) (UntagR xy),
          UntagTag x, UntagTag y, UntagTag xy,
          HTypeIndexed x, HTypeIndexed y,
          SameLengths [x,y,xy]) => HUnzip TIP x y xy where
  hUnzip = hUnzipTIP

#else
-- ghc-7.10.3 has coerce, but rejects these instances
instance (HZipList xL yL xyL,
          lty ~ (HList xyL -> (HList xL,HList yL)),
          Coercible lty (TIP xy -> (TIP x, TIP y)),
          UntagR x ~ xL, TagR xL ~ x, -- `TagR (UntagR x) ~ x` included by UntagTag
          UntagR y ~ yL, TagR yL ~ y,
          UntagR xy ~ xyL, TagR xyL ~ xy,
          SameLengths '[x,y,xy],
          UntagTag x, UntagTag y, UntagTag xy
        ) => HUnzip TIP x y xy where
  hUnzip :: TIP xy -> (TIP x, TIP y)
hUnzip = lty -> TIP xy -> (TIP x, TIP y)
coerce (lty
forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList l -> (HList x, HList y)
hUnzipList :: lty)

instance (HUnzip TIP x y xy,
          HZipList xL yL xyL,
          lty ~ (HList xL -> HList yL -> HList xyL),
          Coercible lty (TIP x -> TIP y -> TIP xy) ,
          UntagR x ~ xL,
          UntagR y ~ yL,
          UntagR xy ~ xyL,
          UntagTag x, UntagTag y, UntagTag xy
        ) => HZip TIP x y xy where
  hZip :: TIP x -> TIP y -> TIP xy
hZip = lty -> TIP x -> TIP y -> TIP xy
coerce (lty
forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList x -> HList y -> HList l
hZipList :: lty)
#endif

-- | specialization of 'hZip'
hZipTIP :: TIP ta -> TIP ta -> TIP l
hZipTIP (TIP HList ta
x) (TIP HList ta
y) = HList l -> TIP l
forall (l :: [*]). HList l -> TIP l
TIP (HList a -> HList l
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList a -> HList ta
hTagSelf (HList x -> HList y -> HList a
forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList x -> HList y -> HList l
hZipList (HList ta -> HList x
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList ta -> HList a
hUntagSelf HList ta
x) (HList ta -> HList y
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList ta -> HList a
hUntagSelf HList ta
y)))

-- | specialization of 'hUnzip'
hUnzipTIP :: TIP ta -> (TIP l, TIP l)
hUnzipTIP (TIP HList ta
xy) = case HList l -> (HList a, HList a)
forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList l -> (HList x, HList y)
hUnzipList (HList ta -> HList l
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList ta -> HList a
hUntagSelf HList ta
xy) of
  (HList a
x,HList a
y) -> (HList l -> TIP l
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP (HList a -> HList l
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList a -> HList ta
hTagSelf HList a
x), HList l -> TIP l
forall (l :: [*]). HTypeIndexed l => HList l -> TIP l
mkTIP (HList a -> HList l
forall (a :: [*]) (ta :: [*]).
TagUntagFD a ta =>
HList a -> HList ta
hTagSelf HList a
y))



-- --------------------------------------------------------------------------
-- * TIP Transform

{- |

Transforming a TIP: applying to a TIP a (polyvariadic) function
that takes arguments from a TIP and updates the TIP with the result.

In more detail: we have a typed-indexed collection TIP and we
would like to apply a transformation function to it, whose argument
types and the result type are all in the TIP. The function should locate
its arguments based on their types, and update the TIP
with the result. The function may have any number of arguments,
including zero; the order of arguments should not matter.

The problem was posed by Andrew U. Frank on Haskell-Cafe, Sep 10, 2009.
<http://www.haskell.org/pipermail/haskell-cafe/2009-September/066217.html>
The problem is an interesting variation of the keyword argument problem.

Examples can be found in @examples/TIPTransform.hs@ and @examples/TIPTransformM.hs@
-}

class TransTIP op db where
    ttip :: op -> TIP db -> TIP db

instance (HMember (Tagged op op) db b,
          Arity op n,
          TransTIP1 b n op db)
    => TransTIP op db where
    ttip :: op -> TIP db -> TIP db
ttip = Proxy b -> Proxy n -> op -> TIP db -> TIP db
forall (b :: Bool) (n :: HNat) op (db :: [*]).
TransTIP1 b n op db =>
Proxy b -> Proxy n -> op -> TIP db -> TIP db
ttip1 (Proxy b
forall k (t :: k). Proxy t
Proxy ::Proxy b) (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n)

class TransTIP1 (b :: Bool) (n :: HNat) op db where
    ttip1 :: Proxy b -> Proxy n -> op -> TIP db -> TIP db

-- If op is found in a TIP, update the TIP with op
instance HTPupdateAtLabel TIP op op db
    => TransTIP1 True n op db where
    ttip1 :: Proxy 'True -> Proxy n -> op -> TIP db -> TIP db
ttip1 Proxy 'True
_ Proxy n
_ = op -> TIP db -> TIP db
forall (record :: [*] -> *) v (r :: [*]).
(HUpdateAtLabel record v v r r, SameLength' r r) =>
v -> record r -> record r
tipyUpdate

-- If op is not found in a TIP, it must be a function. Try to look up
-- its argument in a TIP and recur.
instance (HMember (Tagged arg arg) db b,
          TransTIP2 b arg op db)
    => TransTIP1 False (HSucc n) (arg -> op) db where
    ttip1 :: Proxy 'False -> Proxy ('HSucc n) -> (arg -> op) -> TIP db -> TIP db
ttip1 Proxy 'False
_ Proxy ('HSucc n)
_ = Proxy b -> (arg -> op) -> TIP db -> TIP db
forall (b :: Bool) arg op (db :: [*]).
TransTIP2 b arg op db =>
Proxy b -> (arg -> op) -> TIP db -> TIP db
ttip2 (Proxy b
forall k (t :: k). Proxy t
Proxy :: Proxy b)

instance Fail (FieldNotFound notfun (TIP db))
      => TransTIP1 False HZero notfun db where
    ttip1 :: Proxy 'False -> Proxy 'HZero -> notfun -> TIP db -> TIP db
ttip1 = String
-> Proxy 'False -> Proxy 'HZero -> notfun -> TIP db -> TIP db
forall a. HasCallStack => String -> a
error String
"TransTIP1 Fail failed"

class TransTIP2 (b :: Bool) arg op db where
    ttip2 :: Proxy b -> (arg -> op) -> TIP db -> TIP db

instance (HOccurs arg (TIP db),
         TransTIP op db)
   => TransTIP2 True arg op db where
    ttip2 :: Proxy 'True -> (arg -> op) -> TIP db -> TIP db
ttip2 Proxy 'True
_ arg -> op
f TIP db
db = op -> TIP db -> TIP db
forall op (db :: [*]). TransTIP op db => op -> TIP db -> TIP db
ttip (arg -> op
f (TIP db -> arg
forall e l. HOccurs e l => l -> e
hOccurs TIP db
db)) TIP db
db

instance Fail (FieldNotFound arg (TIP db))
    => TransTIP2 False arg op db where
    ttip2 :: Proxy 'False -> (arg -> op) -> TIP db -> TIP db
ttip2 = String -> Proxy 'False -> (arg -> op) -> TIP db -> TIP db
forall a. HasCallStack => String -> a
error String
"TransTIP2 Fail failed"

-- ** Monadic version

{- |

In March 2010, Andrew Frank extended the problem for monadic operations.
This is the monadic version of @TIPTransform.hs@ in the present directory.

This is the TF implementation. When specifying the operation to perform over
a TIP, we can leave it polymorphic over the monad. The type checker
will instantiate the monad based on the context.

-}
class Monad m => TransTIPM m op db where
    ttipM :: op -> TIP db -> m (TIP db)

-- Check to see if the operation is a computation whose result
-- is in the TIP. The type variable m' of the kind *->* below
-- can be instantiated either to a monad type constructor, or (arg->).
instance (Monad m, HMember (Tagged op op) db b,
           Arity (m' op) n,
           TransTIPM1 b n m (m' op) db)
    => TransTIPM m (m' op) db where
    ttipM :: m' op -> TIP db -> m (TIP db)
ttipM = Proxy b -> Proxy n -> m' op -> TIP db -> m (TIP db)
forall (b :: Bool) (n :: HNat) (m :: * -> *) op (db :: [*]).
TransTIPM1 b n m op db =>
Proxy b -> Proxy n -> op -> TIP db -> m (TIP db)
ttipM1 (Proxy b
forall k (t :: k). Proxy t
Proxy :: Proxy b) (Proxy n
forall k (t :: k). Proxy t
Proxy :: Proxy n)

class Monad m => TransTIPM1 (b :: Bool) (n :: HNat) m op db where
    ttipM1 :: Proxy b -> Proxy n -> op -> TIP db -> m (TIP db)

-- If op is found in a TIP, update the TIP with op.
-- The type variable m' must be equal to the type of the monad
-- in which the final result is reported.
instance (Monad m, m ~ m', HTPupdateAtLabel TIP op op db)
    => TransTIPM1 True n m (m' op) db where
    ttipM1 :: Proxy 'True -> Proxy n -> m' op -> TIP db -> m (TIP db)
ttipM1 Proxy 'True
_ Proxy n
_ m' op
op TIP db
db = do
         op
op' <- m op
m' op
op
         TIP db -> m (TIP db)
forall (m :: * -> *) a. Monad m => a -> m a
return (TIP db -> m (TIP db)) -> TIP db -> m (TIP db)
forall a b. (a -> b) -> a -> b
$ op -> TIP db -> TIP db
forall (record :: [*] -> *) v (r :: [*]).
(HUpdateAtLabel record v v r r, SameLength' r r) =>
v -> record r -> record r
tipyUpdate op
op' TIP db
db

instance (Fail (FieldNotFound op (TIP db)), Monad m)
    => TransTIPM1 False HZero m op db where
    ttipM1 :: Proxy 'False -> Proxy 'HZero -> op -> TIP db -> m (TIP db)
ttipM1 Proxy 'False
_ Proxy 'HZero
_ = String -> op -> TIP db -> m (TIP db)
forall a. HasCallStack => String -> a
error String
"TransTIPM1 Fail failed"

-- If op is not found in a TIP, it must be a function. Look up
-- its argument in a TIP and recur.
instance (Monad m,
          HMember (Tagged arg arg) db b,
          TransTIPM2 b m arg op db)
    => TransTIPM1 False (HSucc n) m (arg-> op) db where
    ttipM1 :: Proxy 'False
-> Proxy ('HSucc n) -> (arg -> op) -> TIP db -> m (TIP db)
ttipM1 Proxy 'False
_ Proxy ('HSucc n)
_ = Proxy b -> (arg -> op) -> TIP db -> m (TIP db)
forall (b :: Bool) (m :: * -> *) arg op (db :: [*]).
TransTIPM2 b m arg op db =>
Proxy b -> (arg -> op) -> TIP db -> m (TIP db)
ttipM2 (Proxy b
forall k (t :: k). Proxy t
Proxy :: Proxy b)


class TransTIPM2 (b :: Bool) m arg op db where
    ttipM2 :: Proxy b -> (arg -> op) -> TIP db -> m (TIP db)

instance (HOccurs arg (TIP db), TransTIPM m op db)
      => TransTIPM2 True m arg op db where
    ttipM2 :: Proxy 'True -> (arg -> op) -> TIP db -> m (TIP db)
ttipM2 Proxy 'True
_ arg -> op
f TIP db
db = op -> TIP db -> m (TIP db)
forall (m :: * -> *) op (db :: [*]).
TransTIPM m op db =>
op -> TIP db -> m (TIP db)
ttipM (arg -> op
f (TIP db -> arg
forall e l. HOccurs e l => l -> e
hOccurs TIP db
db)) TIP db
db


instance Fail (FieldNotFound op (TIP db))
    => TransTIPM2 False m arg op db where
    ttipM2 :: Proxy 'False -> (arg -> op) -> TIP db -> m (TIP db)
ttipM2 Proxy 'False
_ arg -> op
_ = String -> TIP db -> m (TIP db)
forall a. HasCallStack => String -> a
error String
"TransTIPM1 Fail failed"

-- --------------------------------------------------------------------------

-- tests for tipyTuple. These only work if tipyTuple is compiled
-- in a module that has NoMonoLocalBinds enabled
(Char, Bool)
_ = TIP '[Tagged Char Char, Tagged Bool Bool] -> (Char, Bool)
forall b (r :: [*] -> *) (v1 :: [*]) (v2 :: [*]) a (v3 :: [*])
       (v'1 :: [*]) (v'2 :: [*]).
(HOccurs b (r v1), HOccurs b (r v2), HOccurs a (r v2),
 HOccurs a (r v3), HDeleteAtLabel r b v1 v'1,
 HDeleteAtLabel r b v2 v3, HDeleteAtLabel r a v2 v1,
 HDeleteAtLabel r a v3 v'2) =>
r v2 -> (a, b)
tipyTuple ( Char
'1' Char
-> TIP '[Tagged Bool Bool]
-> HExtendR Char (TIP '[Tagged Bool Bool])
forall e l. HExtend e l => e -> l -> HExtendR e l
.*. Bool
True Bool -> TIP '[] -> HExtendR Bool (TIP '[])
forall e l. HExtend e l => e -> l -> HExtendR e l
.*. TIP '[]
emptyTIP ) :: (Char, Bool)
(Bool, Char)
_ = TIP '[Tagged Char Char, Tagged Bool Bool] -> (Bool, Char)
forall b (r :: [*] -> *) (v1 :: [*]) (v2 :: [*]) a (v3 :: [*])
       (v'1 :: [*]) (v'2 :: [*]).
(HOccurs b (r v1), HOccurs b (r v2), HOccurs a (r v2),
 HOccurs a (r v3), HDeleteAtLabel r b v1 v'1,
 HDeleteAtLabel r b v2 v3, HDeleteAtLabel r a v2 v1,
 HDeleteAtLabel r a v3 v'2) =>
r v2 -> (a, b)
tipyTuple ( Char
'1' Char
-> TIP '[Tagged Bool Bool]
-> HExtendR Char (TIP '[Tagged Bool Bool])
forall e l. HExtend e l => e -> l -> HExtendR e l
.*. Bool
True Bool -> TIP '[] -> HExtendR Bool (TIP '[])
forall e l. HExtend e l => e -> l -> HExtendR e l
.*. TIP '[]
emptyTIP ) :: (Bool, Char)


-- --------------------------------------------------------------------------

-- * Sample code

{- $setup

[@Assume@]

>>> import Data.HList.TypeEqO
>>> import Data.HList.FakePrelude
>>> import Data.HList.HOccurs

>>> :{
newtype Key    = Key Integer deriving (Show,Eq,Ord)
newtype Name   = Name String deriving (Show,Eq)
data Breed     = Cow | Sheep deriving (Show,Eq)
newtype Price  = Price Float deriving (Show,Eq,Ord)
data Disease   = BSE | FM deriving (Show,Eq)
type Animal =  TagR '[Key,Name,Breed,Price]
:}

>>> :{
let myTipyCow :: TIP Animal -- optional
    myTipyCow = Key 42 .*.  Name "Angus" .*.  Cow .*.  Price 75.5 .*. emptyTIP
    animalKey :: (HOccurs Key l, SubType l (TIP Animal)) => l -> Key
    animalKey = hOccurs
:}

-}

{- $sessionlog
[@Session log@]

>>> :t myTipyCow
myTipyCow
  :: TIP
       '[Tagged Key Key, Tagged Name Name, Tagged Breed Breed,
         Tagged Price Price]

>>> hOccurs myTipyCow :: Breed
Cow

>>> BSE .*. myTipyCow
TIPH[BSE,Key 42,Name "Angus",Cow,Price 75.5]



>>> Sheep .*. hDeleteAtLabel (Label::Label Breed) myTipyCow
TIPH[Sheep,Key 42,Name "Angus",Price 75.5]

>>> tipyUpdate Sheep myTipyCow
TIPH[Key 42,Name "Angus",Sheep,Price 75.5]


>>> tipyProject2 (Proxy :: Labels '[Name,Price]) myTipyCow
(TIPH[Name "Angus",Price 75.5],TIPH[Key 42,Cow])

>>> tipyProject (Proxy :: Labels '[Name,Price]) myTipyCow
TIPH[Name "Angus",Price 75.5]

-}


{- $sessionlog2

Don't bother repeating the type error:


>>> Sheep .*. myTipyCow
...
...No instance for (Fail (DuplicatedLabel (Label Breed)))
...

-}