{-# LANGUAGE CPP #-}
{- |
   The HList library

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

   Extensible records

   The three-ish models of labels that go with this module;

   * "Data.HList.Label3"

   * "Data.HList.Label5"

   * "Data.HList.Label6"

   * "Data.HList.Labelable"


   These used to work:

   * "Data.HList.Label1"

   * "Data.HList.Label2"

   * "Data.HList.Label4"

-}

module Data.HList.Record
(
    -- ** labels used for doctests
    -- $setup

    -- * Records

    -- ** Labels
    -- $labels
    module Data.Tagged,
    (.=.),

    -- ** Record
    Record(..),
    mkRecord,
    emptyRecord,
    hEndR,
    hEndP,

    hListRecord, hListRecord',

    -- *** Getting Labels
    LabelsOf,
    labelsOf,
    asLabelsOf,

    -- *** Getting Values
    RecordValues(..),
    recordValues,
    hMapTaggedFn,

    unlabeled0,

    Unlabeled,
    unlabeled,
    Unlabeled',
    unlabeled',

    -- * Operations
    -- ** Show
    -- | A corresponding 'Show' instance exists as
    --
    -- > show x = "Record {" ++ showComponents "" x ++ "}"
    ShowComponents(..),
    ShowLabel(..),

    -- ** Extension
    -- | 'hExtend', 'hAppend'
    (.*.),

    -- ** Delete
    -- | 'hDeleteAtLabel' @label record@
    (.-.),
    HDeleteLabels(..),

    -- ** Lookup/update
    -- $lens
    HLens(hLens),

    -- ** Lookup
    HasField(..),
    HasFieldM(..),
    (.!.),

    -- ** Update
    (.@.),
    HUpdateAtLabel(hUpdateAtLabel),
    -- *** type-preserving versions
    -- | Note: these restrict the resulting record type to be the same as in
    -- input record type, which can help reduce the number of type annotations
    -- needed
    (.<.),
    HTPupdateAtLabel,
    hTPupdateAtLabel,

    -- ** Rename Label
    hRenameLabel,

    -- ** Projection

    Labels,

    -- $projection
    hProjectByLabels,
    hProjectByLabels',
    hProjectByLabels2,

    -- *** a lens for projection
    -- | see "Data.HList.Labelable".'Projected'

    -- ** Unions
    -- *** Left
    HLeftUnion(hLeftUnion),
    (.<++.),

    -- *** Symmetric
    -- $symmetricUnion
    UnionSymRec(unionSR),


    -- ** Reorder Labels
    hRearrange,
    hRearrange',

    -- *** isos using hRearrange
    Rearranged(rearranged), rearranged',


    -- ** Apply a function to all values
    hMapR, HMapR(..),

    -- ** cast labels
    Relabeled(relabeled),
    relabeled',

    -- * Hints for type errors
    DuplicatedLabel,
    ExtraField,
    FieldNotFound,

    -- * Unclassified

    -- | Probably internals, that may not be useful
#if __GLASGOW_HASKELL__ != 706
    zipTagged,
#endif
    HasField'(..),
    DemoteMaybe,
    HasFieldM1(..),
    H2ProjectByLabels(h2projectByLabels),
    H2ProjectByLabels'(h2projectByLabels'),
    HLabelSet,
    HLabelSet',
    HRLabelSet,
    HAllTaggedLV,
    HRearrange(hRearrange2),
    HRearrange3(hRearrange3),
    HRearrange4(hRearrange4),
    UnionSymRec'(..),
    HFindLabel,
    labelLVPair,
    newLVPair,
    UnLabel,
    HMemberLabel,
    TaggedFn(..),
    ReadComponent,
    HMapTaggedFn,
    HLensCxt,

    -- ** zip
    -- | use the more general 'HZip' class instead
    HZipRecord(..),
    -- *** alternative implementation
    hZipRecord2, hUnzipRecord2
) where


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

import Data.HList.Label3 (MapLabel)

import Data.Tagged
import Control.Monad

import Text.ParserCombinators.ReadP

import LensDefs

import Data.Array (Ix)
import Data.Semigroup (Semigroup)

-- imports for doctest/examples
import Data.HList.Label6 ()
import Data.HList.TypeEqO ()

{- $setup

>>> let x = Label :: Label "x"
>>> let y = Label :: Label "y"
>>> let z = Label :: Label "z"

-}

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

-- $labels Record types as label-value pairs, where label is purely phantom.
-- Thus the run-time representation of a field is the same as that of
-- its value, and the record, at run-time, is indistinguishable from
-- the HList of field values. At run-time, all information about the
-- labels is erased.
--
-- The type from "Data.Tagged" is used.

-- | Label accessor
labelLVPair :: Tagged l v -> Label l
labelLVPair :: forall {k} (l :: k) v. Tagged l v -> Label l
labelLVPair Tagged l v
_ = forall {k} (l :: k). Label l
Label

newLVPair :: Label l -> v -> Tagged l v
newLVPair :: forall {k} (l :: k) v. Label l -> v -> Tagged l v
newLVPair Label l
_ = forall {k} (s :: k) b. b -> Tagged s b
Tagged



infixr 4 .=.
{-|

  Create a value with the given label. Analagous to a data
  constructor such as 'Just', 'Left', or 'Right'. Higher fixity
  than record-modification operations like ('.*.'), ('.-.'), etc. to
  support expression like the below w/o parentheses:

  >>> x .=. "v1" .*. y .=. '2' .*. emptyRecord
  Record{x="v1",y='2'}

-}
(.=.) :: Label l -> v -> Tagged l v
Label l
l .=. :: forall {k} (l :: k) v. Label l -> v -> Tagged l v
.=. v
v = forall {k} (l :: k) v. Label l -> v -> Tagged l v
newLVPair Label l
l v
v


newtype Record (r :: [*]) = Record (HList r)

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


-- | Build a record
mkRecord :: HRLabelSet r => HList r -> Record r
mkRecord :: forall (r :: [*]). HRLabelSet r => HList r -> Record r
mkRecord = forall (r :: [*]). HList r -> Record r
Record

-- | @HRLabelSet t => Iso (HList s) (HList t) (Record s) (Record t)@
hListRecord :: p (Record r) (f (Record r)) -> p (HList r) (f (HList r))
hListRecord p (Record r) (f (Record r))
x = 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 forall (r :: [*]). HRLabelSet r => HList r -> Record r
mkRecord (\(Record HList r
r) -> HList r
r) p (Record r) (f (Record r))
x

-- | @Iso' (HList s) (Record s)@
hListRecord' :: p (Record r) (f (Record r)) -> p (HList r) (f (HList r))
hListRecord' p (Record r) (f (Record r))
x = 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 forall {p :: * -> * -> *} {f :: * -> *} {r :: [*]} {r :: [*]}.
(Profunctor p, Functor f, HLabelSet (LabelsOf r),
 HAllTaggedLV r) =>
p (Record r) (f (Record r)) -> p (HList r) (f (HList r))
hListRecord p (Record r) (f (Record r))
x

-- | Build an empty record
emptyRecord :: Record '[]
emptyRecord :: Record '[]
emptyRecord = forall (r :: [*]). HRLabelSet r => HList r -> Record r
mkRecord HList '[]
HNil

-- | @Iso (Record s) (Record t) (HList a) (HList b)@
--
-- @view unlabeled == 'recordValues'@
unlabeled0 :: p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
-> p (Record x) (f (Record y))
unlabeled0 p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
x = forall {k1} {k2} {k3} {k4} {k5} (x :: k1) (y :: k2)
       (p :: k3 -> k4 -> *) (r :: k1 -> k3) (f :: k5 -> k4)
       (q :: k2 -> k5).
SameLabels x y =>
p (r x) (f (q y)) -> p (r x) (f (q y))
sameLabels (forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso forall (r :: [*]).
RecordValues r =>
Record r -> HList (RecordValuesR r)
recordValues forall (a :: [*]) (b :: [*]).
HMapTaggedFn a b =>
HList a -> Record b
hMapTaggedFn p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
x)


unlabeled :: (Unlabeled x y, Profunctor p, Functor f) =>
    (HList (RecordValuesR x) `p` f (HList (RecordValuesR y))) ->
    (Record x `p` f (Record y))
unlabeled :: forall (x :: [*]) (y :: [*]) (p :: * -> * -> *) (f :: * -> *).
(Unlabeled x y, Profunctor p, Functor f) =>
p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
-> p (Record x) (f (Record y))
unlabeled p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
x = forall k m (x :: [k]) (y :: [m]) {k1} {k2} {k3}
       (p :: k1 -> k2 -> *) (r :: [k] -> k1) (f :: k3 -> k2)
       (q :: [m] -> k3).
SameLength x y =>
p (r x) (f (q y)) -> p (r x) (f (q y))
sameLength (forall {f :: * -> *} {p :: * -> * -> *} {x :: [*]} {y :: [*]}.
(Functor f, Profunctor p, SameLabels x y,
 HMapAux HList TaggedFn (RecordValuesR y) y, RecordValues x,
 RecordValues y) =>
p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
-> p (Record x) (f (Record y))
unlabeled0 (forall k m (x :: [k]) (y :: [m]) {k1} {k2} {k3}
       (p :: k1 -> k2 -> *) (r :: [k] -> k1) (f :: k3 -> k2)
       (q :: [m] -> k3).
SameLength x y =>
p (r x) (f (q y)) -> p (r x) (f (q y))
sameLength p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
x))

type Unlabeled x y =
      (HMapCxt HList TaggedFn (RecordValuesR y) y,
       RecordValues x, RecordValues y,
       SameLength (RecordValuesR x) (RecordValuesR y),
       SameLength x y, SameLabels x y,
       HAllTaggedLV x, HAllTaggedLV y)
type Unlabeled' x = Unlabeled x x



-- | @Unlabeled' x => Iso' (Record x) (HList (RecordValuesR x))@
unlabeled' :: (Unlabeled' x, Profunctor p, Functor f) =>
    (HList (RecordValuesR x) `p` f (HList (RecordValuesR x))) ->
    (Record x `p` f (Record x))
unlabeled' :: forall (x :: [*]) (p :: * -> * -> *) (f :: * -> *).
(Unlabeled' x, Profunctor p, Functor f) =>
p (HList (RecordValuesR x)) (f (HList (RecordValuesR x)))
-> p (Record x) (f (Record x))
unlabeled' = forall (x :: [*]) (y :: [*]) (p :: * -> * -> *) (f :: * -> *).
(Unlabeled x y, Profunctor p, Functor f) =>
p (HList (RecordValuesR x)) (f (HList (RecordValuesR y)))
-> p (Record x) (f (Record y))
unlabeled

{- | @Iso (Record s) (Record t) (Record a) (Record b)@, such that
@relabeled = unlabeled . from unlabeled@

in other words, pretend a record has different labels, but the same values.

-}
class Relabeled r where
  relabeled :: forall p f s t a b.
      (HMapTaggedFn (RecordValuesR s) a,
       HMapTaggedFn (RecordValuesR b) t,
       SameLengths '[s,a,t,b],
       RecordValuesR t ~ RecordValuesR b,
       RecordValuesR s ~ RecordValuesR a,
       RecordValues b, RecordValues s,
       Profunctor p,
       Functor f
       ) => r a `p` f (r b) -> r s `p` f (r t)

instance Relabeled Record where
  relabeled :: forall (p :: * -> * -> *) (f :: * -> *) (s :: [*]) (t :: [*])
       (a :: [*]) (b :: [*]).
(HMapTaggedFn (RecordValuesR s) a,
 HMapTaggedFn (RecordValuesR b) t, SameLengths '[s, a, t, b],
 RecordValuesR t ~ RecordValuesR b,
 RecordValuesR s ~ RecordValuesR a, RecordValues b, RecordValues s,
 Profunctor p, Functor f) =>
p (Record a) (f (Record b)) -> p (Record s) (f (Record t))
relabeled = forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso
    (\ Record s
s -> forall (a :: [*]) (b :: [*]).
HMapTaggedFn a b =>
HList a -> Record b
hMapTaggedFn (forall (r :: [*]).
RecordValues r =>
Record r -> HList (RecordValuesR r)
recordValues Record s
s))
    (\ Record b
b -> forall (a :: [*]) (b :: [*]).
HMapTaggedFn a b =>
HList a -> Record b
hMapTaggedFn (forall (r :: [*]).
RecordValues r =>
Record r -> HList (RecordValuesR r)
recordValues Record b
b))
    -- isoNewtype should be safe here, but there are no guarantees
    -- http://stackoverflow.com/questions/24222552

-- | @Iso' (Record s) (Record a)@
--
-- such that @RecordValuesR s ~ RecordValuesR a@
relabeled' :: p (r b) (f (r b)) -> p (r t) (f (r t))
relabeled' p (r b) (f (r b))
x = 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 forall (r :: [*] -> *) (p :: * -> * -> *) (f :: * -> *) (s :: [*])
       (t :: [*]) (a :: [*]) (b :: [*]).
(Relabeled r, HMapTaggedFn (RecordValuesR s) a,
 HMapTaggedFn (RecordValuesR b) t, SameLengths '[s, a, t, b],
 RecordValuesR t ~ RecordValuesR b,
 RecordValuesR s ~ RecordValuesR a, RecordValues b, RecordValues s,
 Profunctor p, Functor f) =>
p (r a) (f (r b)) -> p (r s) (f (r t))
relabeled p (r b) (f (r b))
x

data TaggedFn = TaggedFn
instance (tx ~ Tagged t x) => ApplyAB TaggedFn x tx where
    applyAB :: TaggedFn -> x -> tx
applyAB TaggedFn
_ = forall {k} (s :: k) b. b -> Tagged s b
Tagged

type HMapTaggedFn l r =
    (HMapCxt HList TaggedFn l r,
     RecordValuesR r ~ l,
     RecordValues r)

-- | \"inverse\" to 'recordValues'
hMapTaggedFn :: HMapTaggedFn a b => HList a -> Record b
hMapTaggedFn :: forall (a :: [*]) (b :: [*]).
HMapTaggedFn a b =>
HList a -> Record b
hMapTaggedFn = forall (r :: [*]). HList r -> Record r
Record forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap TaggedFn
TaggedFn

-- | Property of a proper label set for a record: no duplication of labels,
-- and every element of the list is @Tagged label value@

data DuplicatedLabel l

class (HLabelSet (LabelsOf ps), HAllTaggedLV ps) => HRLabelSet (ps :: [*])
instance (HLabelSet (LabelsOf ps), HAllTaggedLV ps) => HRLabelSet (ps :: [*])




{- | Relation between HLabelSet and HRLabelSet

> instance HLabelSet (LabelsOf ps) => HRLabelSet ps

see also 'HSet'
-}

class HLabelSet ls
instance HLabelSet '[]
instance HLabelSet '[x]
instance ( HEqK l1 l2 leq
         , HLabelSet' l1 l2 leq r
         ) => HLabelSet (l1 ': l2 ': r)

class HLabelSet' l1 l2 (leq::Bool) r
instance ( HLabelSet (l2 ': r)
         , HLabelSet (l1 ': r)
         ) => HLabelSet' l1 l2 False r
instance ( Fail (DuplicatedLabel l1) ) => HLabelSet' l1 l2 True r

-- | Construct the (phantom) list of labels of a record,
-- or list of Label.
type family LabelsOf (ls :: [*]) :: [*]
type instance LabelsOf '[] = '[]
type instance LabelsOf (Label l ': r)  = Label l ': LabelsOf r
type instance LabelsOf (Tagged l v ': r) = Label l ': LabelsOf r

labelsOf :: hlistOrRecord l -> Proxy (LabelsOf l)
labelsOf :: forall (hlistOrRecord :: [*] -> *) (l :: [*]).
hlistOrRecord l -> Proxy (LabelsOf l)
labelsOf hlistOrRecord l
_ = forall {k} (t :: k). Proxy t
Proxy



-- | remove the Label type constructor. The @proxy@ argument is
-- supplied to make it easier to fix the kind variable @k@.
type family UnLabel (proxy :: k) (ls :: [*]) :: [k]
type instance UnLabel proxy (Label x ': xs) = x ': UnLabel proxy xs
type instance UnLabel proxy '[] = '[]

-- | A version of 'HFind' where the @ls@ type variable is a list of
-- 'Tagged' or 'Label'. This is a bit indirect, and ideally LabelsOf
-- could have kind [*] -> [k].
type HFindLabel (l :: k) (ls :: [*]) (n :: HNat) = HFind l (UnLabel l (LabelsOf ls)) n

-- | Construct the HList of values of the record.
class SameLength r (RecordValuesR r)
      => RecordValues (r :: [*]) where
  type RecordValuesR r :: [*]
  recordValues' :: HList r -> HList (RecordValuesR r)

instance RecordValues '[] where
  type RecordValuesR '[] = '[]
  recordValues' :: HList '[] -> HList (RecordValuesR '[])
recordValues' HList '[]
_ = HList '[]
HNil
instance (SameLength' r (RecordValuesR r),
          SameLength' (RecordValuesR r) r, RecordValues r) => RecordValues (Tagged l v ': r) where
   type RecordValuesR (Tagged l v ': r) = v ': RecordValuesR r
   recordValues' :: HList (Tagged l v : r) -> HList (RecordValuesR (Tagged l v : r))
recordValues' (HCons (Tagged v
v) HList r
r) = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons v
v (forall (r :: [*]).
RecordValues r =>
HList r -> HList (RecordValuesR r)
recordValues' HList r
r)

recordValues :: RecordValues r => Record r -> HList (RecordValuesR r)
recordValues :: forall (r :: [*]).
RecordValues r =>
Record r -> HList (RecordValuesR r)
recordValues (Record HList r
r) = forall (r :: [*]).
RecordValues r =>
HList r -> HList (RecordValuesR r)
recordValues' HList r
r

{- shorter, but worse in terms needing annotations to allow ambiguous types
- but better in terms of inference
recordValues :: RecordValues r rv => Record r -> HList rv
recordValues (Record r) = hMap HUntag r

type RecordValues r rv = HMapCxt HUntag r rv
-}

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

-- 'Show' instance to appeal to normal records

instance ShowComponents r => Show (Record r) where
  show :: Record r -> String
show (Record HList r
r) =  String
"Record{"
                  forall a. [a] -> [a] -> [a]
++ forall (l :: [*]). ShowComponents l => String -> HList l -> String
showComponents String
"" HList r
r
                  forall a. [a] -> [a] -> [a]
++ String
"}"

class ShowComponents l where
  showComponents :: String -> HList l -> String

instance ShowComponents '[] where
  showComponents :: String -> HList '[] -> String
showComponents String
_ HList '[]
_ = String
""

instance ( ShowLabel l
         , Show v
         , ShowComponents r
         )
      =>   ShowComponents (Tagged l v ': r) where
  showComponents :: String -> HList (Tagged l v : r) -> String
showComponents String
comma (HCons f :: Tagged l v
f@(Tagged v
v) HList r
r)
     =  String
comma
     forall a. [a] -> [a] -> [a]
++ forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel ((forall {k} (l :: k) v. Tagged l v -> Label l
labelLVPair Tagged l v
f) :: Label l)
     forall a. [a] -> [a] -> [a]
++ String
"="
     forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show v
v
     forall a. [a] -> [a] -> [a]
++ forall (l :: [*]). ShowComponents l => String -> HList l -> String
showComponents String
"," HList r
r


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

-- 'Read' instance to appeal to normal records


data ReadComponent = ReadComponent Bool -- ^ include comma?

instance (Read v, ShowLabel l,
          x ~ Tagged l v,
          ReadP x ~ y) =>
  ApplyAB ReadComponent (Proxy x) y where
    applyAB :: ReadComponent -> Proxy x -> y
applyAB (ReadComponent Bool
comma) Proxy x
_ = do
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
comma (() forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> ReadP String
string String
",")
      String
_ <- String -> ReadP String
string (forall {k} (l :: k). ShowLabel l => Label l -> String
showLabel (forall {k} (l :: k). Label l
Label :: Label l))
      String
_ <- String -> ReadP String
string String
"="
      v
v <- forall a. ReadS a -> ReadP a
readS_to_P forall a. Read a => ReadS a
reads
      forall (m :: * -> *) a. Monad m => a -> m a
return (forall {k} (s :: k) b. b -> Tagged s b
Tagged v
v)


instance (HMapCxt HList ReadComponent (AddProxy rs) bs,
          ApplyAB ReadComponent (Proxy r) readP_r,
          HProxies rs,
          HSequence ReadP (readP_r ': bs) (r ': rs),
          readP_r ~ ReadP (Tagged l v),

          -- ghc-8.0.2 needs these. The above constraints
          -- should imply them
          r ~ Tagged l v,
          ShowLabel l,
          Read v,
          HSequence ReadP bs rs
          ) => Read (Record (r ': rs)) where
    readsPrec :: Int -> ReadS (Record (r : rs))
readsPrec Int
_ = forall a. ReadP a -> ReadS a
readP_to_S forall a b. (a -> b) -> a -> b
$ do
        String
_ <- String -> ReadP String
string String
"Record{"
        HList (r : rs)
content <- forall (m :: * -> *) (a :: [*]) (b :: [*]).
HSequence m a b =>
HList a -> m (HList b)
hSequence HList (readP_r : bs)
parsers
        String
_ <- String -> ReadP String
string String
"}"
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall (r :: [*]). HList r -> Record r
Record HList (r : rs)
content)

      where
        rs :: HList (AddProxy rs)
        rs :: HList (AddProxy rs)
rs = forall (xs :: [*]) (pxs :: [*]). HProxiesFD xs pxs => HList pxs
hProxies

        readP_r :: readP_r
        readP_r :: readP_r
readP_r = forall f a b. ApplyAB f a b => f -> a -> b
applyAB
                      (Bool -> ReadComponent
ReadComponent Bool
False)
                      (forall {k} (t :: k). Proxy t
Proxy :: Proxy r)

        parsers :: HList (readP_r : bs)
parsers = readP_r
readP_r forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` (forall {a :: [*]} {b :: [*]} {r :: [*] -> *} {f}.
(SameLength' a b, SameLength' b a, HMapAux r f a b) =>
f -> r a -> r b
hMap (Bool -> ReadComponent
ReadComponent Bool
True) HList (AddProxy rs)
rs :: HList bs)





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

-- Extension

instance HRLabelSet (t ': r)
    => HExtend t (Record r) where
  type HExtendR t (Record r) = Record (t ': r)
  t
f .*. :: t -> Record r -> HExtendR t (Record r)
.*. (Record HList r
r) = forall (r :: [*]). HRLabelSet r => HList r -> Record r
mkRecord (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons t
f HList r
r)


-- * For records

{-|

  [@(.*.)@]
           Add a field to a record. Analagous to (++) for
           lists.

  > record .*. field1
  >        .*. field2

-}

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

-- Concatenation

instance (HRLabelSet (HAppendListR r1 r2), HAppend (HList r1) (HList r2))
    => HAppend (Record r1) (Record r2) where
  hAppend :: Record r1 -> Record r2 -> HAppendR (Record r1) (Record r2)
hAppend (Record HList r1
r) (Record HList r2
r') = forall (r :: [*]). HRLabelSet r => HList r -> Record r
mkRecord (forall l1 l2. HAppend l1 l2 => l1 -> l2 -> HAppendR l1 l2
hAppend HList r1
r HList r2
r')

type instance HAppendR (Record r1) (Record r2) = Record (HAppendListR r1 r2)
-- --------------------------------------------------------------------------

-- Lookup
--
-- |
-- This is a baseline implementation.
-- We use a helper class, HasField, to abstract from the implementation.

-- | Because 'hLookupByLabel' is so frequent and important, we implement
-- it separately, more efficiently. The algorithm is familiar assq, only
-- the comparison operation is done at compile-time
class HasField (l::k) r v | l r -> v where
    hLookupByLabel:: Label l -> r -> v

{- alternative "straightforward" implementation
instance ( LabelsOf r ~ ls
         , HFind l ls n
         , HLookupByHNat n r
         , HLookupByHNatR n r ~ LVPair l v
         ) => HasField l (Record r) v
  where
    hLookupByLabel l (Record r) = v
      where
        (LVPair v) = hLookupByHNat (proxy :: Proxy n) r
-}

{- | a version of 'HasField' / 'hLookupByLabel' / '.!.' that
returns a default value when the label is not in the record:

>>> let r = x .=. "the x value" .*. emptyRecord

>>> hLookupByLabelM y r ()
()

>>> hLookupByLabelM x r ()
"the x value"



-}
class HasFieldM (l :: k) r (v :: Maybe *) | l r -> v where
    hLookupByLabelM :: Label l
          -> r -- ^ Record (or Variant,TIP,TIC)
          -> t -- ^ default value
          -> DemoteMaybe t v

type family DemoteMaybe (d :: *) (v :: Maybe *) :: *
type instance DemoteMaybe d (Just a) = a
type instance DemoteMaybe d Nothing = d

class HasFieldM1 (b :: Maybe [*]) (l :: k) r v | b l r -> v where
    hLookupByLabelM1 :: Proxy b -> Label l -> r -> t -> DemoteMaybe t v

instance (HMemberM (Label l) (LabelsOf xs) b,
          HasFieldM1 b l (r xs) v)  => HasFieldM l (r xs) v where
    hLookupByLabelM :: forall t. Label l -> r xs -> t -> DemoteMaybe t v
hLookupByLabelM = forall k (b :: Maybe [*]) (l :: k) r (v :: Maybe (*)) t.
HasFieldM1 b l r v =>
Proxy b -> Label l -> r -> t -> DemoteMaybe t v
hLookupByLabelM1 (forall {k} (t :: k). Proxy t
Proxy :: Proxy b)

instance HasFieldM1 Nothing l r Nothing where
    hLookupByLabelM1 :: forall t.
Proxy 'Nothing -> Label l -> r -> t -> DemoteMaybe t 'Nothing
hLookupByLabelM1 Proxy 'Nothing
_ Label l
_ r
_ t
t = t
t

instance HasField l r v => HasFieldM1 (Just b) l r (Just v) where
    hLookupByLabelM1 :: forall t.
Proxy ('Just b) -> Label l -> r -> t -> DemoteMaybe t ('Just v)
hLookupByLabelM1 Proxy ('Just b)
_ Label l
l r
r t
_t = forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel Label l
l r
r



instance (HEqK l l1 b, HasField' b l (Tagged l1 v1 ': r) v)
    => HasField l (Record (Tagged l1 v1 ': r)) v where
    hLookupByLabel :: Label l -> Record (Tagged l1 v1 : r) -> v
hLookupByLabel Label l
l (Record HList (Tagged l1 v1 : r)
r) =
             forall k (b :: Bool) (l :: k) (r :: [*]) v.
HasField' b l r v =>
Proxy b -> Label l -> HList r -> v
hLookupByLabel' (forall {k} (t :: k). Proxy t
Proxy::Proxy b) Label l
l HList (Tagged l1 v1 : r)
r

-- | XXX
instance (t ~ Any, Fail (FieldNotFound l ())) => HasField l (Record '[]) t where
    hLookupByLabel :: Label l -> Record '[] -> t
hLookupByLabel Label l
_ Record '[]
_ = forall a. HasCallStack => String -> a
error String
"Data.HList.Record.HasField: Fail instances should not exist"


class HasField' (b::Bool) (l :: k) (r::[*]) v | b l r -> v where
    hLookupByLabel':: Proxy b -> Label l -> HList r -> v

instance HasField' True l (Tagged l v ': r) v where
    hLookupByLabel' :: Proxy 'True -> Label l -> HList (Tagged l v : r) -> v
hLookupByLabel' Proxy 'True
_ Label l
_ (HCons (Tagged v
v) HList r
_) = v
v
instance HasField l (Record r) v => HasField' False l (fld ': r) v where
    hLookupByLabel' :: Proxy 'False -> Label l -> HList (fld : r) -> v
hLookupByLabel' Proxy 'False
_ Label l
l (HCons fld
_ HList r
r) = forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel Label l
l (forall (r :: [*]). HList r -> Record r
Record HList r
r)



infixr 9 .!.
{- |
  Lookup a value in a record by its label. Analagous to (!!), the
  list indexing operation. Highest fixity, like ('!!').

  >>> :{
  let record1 = x .=. 3 .*.
                y .=. 'y' .*.
                emptyRecord
  :}


  >>> record1 .!. x
  3

  >>> record1 .!. y
  'y'


  >>> :{
  let r2 = y .=. record1 .!. x .*.
           z .=. record1 .!. y .*.
           emptyRecord
  :}

  >>> r2
  Record{y=3,z='y'}

  Note that labels made following "Data.HList.Labelable" allow
  using "Control.Lens.^." instead.
-}


(.!.) :: (HasField l r v) => r -> Label l -> v
r
r .!. :: forall {k} (l :: k) r v. HasField l r v => r -> Label l -> v
.!. Label l
l =  forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel Label l
l r
r

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

-- Delete

instance (H2ProjectByLabels '[Label l] v t1 v')
      => HDeleteAtLabel Record l v v' where
  hDeleteAtLabel :: Label l -> Record v -> Record v'
hDeleteAtLabel Label l
_ (Record HList v
r) =
    forall (r :: [*]). HList r -> Record r
Record forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall (ls :: [*]) (r :: [*]) (rin :: [*]) (rout :: [*])
       (proxy :: [*] -> *).
H2ProjectByLabels ls r rin rout =>
proxy ls -> HList r -> (HList rin, HList rout)
h2projectByLabels (forall {k} (t :: k). Proxy t
Proxy::Proxy '[Label l]) HList v
r

infixl 2 .-.
{-|
  Remove a field from a record. At the same
  level as other record modification options ('.*.'). Analagous
  to (@\\\\@) in lists.

  > record1 .-. label1

  > label1 .=. value1 .*.
  > label2 .=. value2 .-.
  > label2 .*.
  > emptyRecord

  > label1 .=. value1 .-.
  > label1 .*.
  > label2 .=. value2 .*.
  > emptyRecord

  > record1 .*. label1 .=. record2 .!. label1
  >         .*. label2 .=. record2 .!. label2
  >         .-. label1

-}
(.-.) :: (HDeleteAtLabel r l xs xs') =>
    r xs -> Label l -> r xs'
r xs
r .-. :: forall {k} (r :: [*] -> *) (l :: k) (xs :: [*]) (xs' :: [*]).
HDeleteAtLabel r l xs xs' =>
r xs -> Label l -> r xs'
.-. Label l
l =  forall k (r :: [*] -> *) (l :: k) (v :: [*]) (v' :: [*]).
HDeleteAtLabel r l v v' =>
Label l -> r v -> r v'
hDeleteAtLabel Label l
l r xs
r


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

-- Update

-- | 'hUpdateAtLabel' @label value record@

class
    HUpdateAtLabel record (l :: k) (v :: *) (r :: [*]) (r' :: [*])
          | l v r -> r', l r' -> v where
    hUpdateAtLabel :: SameLength r r' => Label l -> v -> record r -> record r'

instance (HUpdateAtLabel2 l v r r',
        HasField l (Record r') v) =>
        HUpdateAtLabel Record l v r r' where
    hUpdateAtLabel :: SameLength r r' => Label l -> v -> Record r -> Record r'
hUpdateAtLabel = forall k (l :: k) v (r :: [*]) (r' :: [*]).
HUpdateAtLabel2 l v r r' =>
Label l -> v -> Record r -> Record r'
hUpdateAtLabel2

{- alternative impl which reports a Fail constraint that is too long (the
one from HUpdateAtHNat) on ghc 7.10 RC1

instance (HasField l (Record r') v,
          HFindLabel l r n,
          HUpdateAtHNat n (Tagged l v) r,
          HUpdateAtHNatR n (Tagged l v) r ~ r',
          SameLength r r') =>
  HUpdateAtLabel Record l v r r' where
  hUpdateAtLabel l v (Record r) =
    Record (hUpdateAtHNat (Proxy::Proxy n) (newLVPair l v) r)
-}

class HUpdateAtLabel2 (l :: k) (v :: *) (r :: [*]) (r' :: [*])
        | l r v -> r' where
    hUpdateAtLabel2 :: Label l -> v -> Record r -> Record r'

class HUpdateAtLabel1 (b :: Bool) (l :: k) (v :: *) (r :: [*]) (r' :: [*])
        | b l v r -> r' where
    hUpdateAtLabel1 :: Proxy b -> Label l -> v -> Record r -> Record r'

instance HUpdateAtLabel1 True l v (Tagged l e ': xs) (Tagged l v ': xs) where
    hUpdateAtLabel1 :: Proxy 'True
-> Label l
-> v
-> Record (Tagged l e : xs)
-> Record (Tagged l v : xs)
hUpdateAtLabel1 Proxy 'True
_b Label l
_l v
v (Record (Tagged l e
e `HCons` HList xs
xs)) = forall (r :: [*]). HList r -> Record r
Record (Tagged l e
e{ unTagged :: v
unTagged = v
v } forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList xs
xs)

instance HUpdateAtLabel2 l v xs xs' => HUpdateAtLabel1 False l v (x ': xs) (x ': xs') where
    hUpdateAtLabel1 :: Proxy 'False -> Label l -> v -> Record (x : xs) -> Record (x : xs')
hUpdateAtLabel1 Proxy 'False
_b Label l
l v
v (Record (x
x `HCons` HList xs
xs)) = case forall k (l :: k) v (r :: [*]) (r' :: [*]).
HUpdateAtLabel2 l v r r' =>
Label l -> v -> Record r -> Record r'
hUpdateAtLabel2 Label l
l v
v (forall (r :: [*]). HList r -> Record r
Record HList xs
xs) of
        Record HList xs'
xs' -> forall (r :: [*]). HList r -> Record r
Record (x
x forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList xs'
xs')

instance (HEqK l l' b, HUpdateAtLabel1 b l v (Tagged l' e ': xs) xs')
    => HUpdateAtLabel2 l v (Tagged l' e ': xs) xs' where
    hUpdateAtLabel2 :: Label l -> v -> Record (Tagged l' e : xs) -> Record xs'
hUpdateAtLabel2 = forall k (b :: Bool) (l :: k) v (r :: [*]) (r' :: [*]).
HUpdateAtLabel1 b l v r r' =>
Proxy b -> Label l -> v -> Record r -> Record r'
hUpdateAtLabel1 (forall {k} (t :: k). Proxy t
Proxy :: Proxy b)

-- | XXX
instance Fail (FieldNotFound l ()) => HUpdateAtLabel2 l v '[] '[] where
    hUpdateAtLabel2 :: Label l -> v -> Record '[] -> Record '[]
hUpdateAtLabel2 Label l
_ v
_ Record '[]
r = Record '[]
r


infixr 2 .@.
{-|

  Update a field with a particular value.
  Same fixity as (.*.) so that extensions and updates can be chained.
  There is no real list analogue, since there is no Prelude defined
  update.

  > label1 .=. value1 .@. record1

-}
f :: Tagged l v
f@(Tagged v
v) .@. :: Tagged l v -> record r -> record r'
.@. record r
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 (forall {k} (l :: k) v. Tagged l v -> Label l
labelLVPair Tagged l v
f) v
v record r
r


-- --------------------------------------------------------------------------
-- Projection

-- $projection
-- It is also an important operation: the basis of many
-- deconstructors -- so we try to implement it efficiently.


-- | @hProjectByLabels ls r@ returns @r@ with only the labels in @ls@ remaining
hProjectByLabels :: (HRLabelSet a, H2ProjectByLabels ls t a b) =>
        proxy ls -> Record t -> Record a
hProjectByLabels :: forall (a :: [*]) (ls :: [*]) (t :: [*]) (b :: [*])
       (proxy :: [*] -> *).
(HRLabelSet a, H2ProjectByLabels ls t a b) =>
proxy ls -> Record t -> Record a
hProjectByLabels proxy ls
ls (Record HList t
r) = forall (r :: [*]). HRLabelSet r => HList r -> Record r
mkRecord (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall (ls :: [*]) (r :: [*]) (rin :: [*]) (rout :: [*])
       (proxy :: [*] -> *).
H2ProjectByLabels ls r rin rout =>
proxy ls -> HList r -> (HList rin, HList rout)
h2projectByLabels proxy ls
ls HList t
r)

-- | See 'H2ProjectByLabels'
hProjectByLabels2 ::
    (H2ProjectByLabels ls t t1 t2, HRLabelSet t1, HRLabelSet t2) =>
    Proxy ls -> Record t -> (Record t1, Record t2)
hProjectByLabels2 :: forall (ls :: [*]) (t :: [*]) (t1 :: [*]) (t2 :: [*]).
(H2ProjectByLabels ls t t1 t2, HRLabelSet t1, HRLabelSet t2) =>
Proxy ls -> Record t -> (Record t1, Record t2)
hProjectByLabels2 Proxy ls
ls (Record HList t
r) = (forall (r :: [*]). HRLabelSet r => HList r -> Record r
mkRecord HList t1
rin, forall (r :: [*]). HRLabelSet r => HList r -> Record r
mkRecord HList t2
rout)
   where (HList t1
rin,HList t2
rout) = forall (ls :: [*]) (r :: [*]) (rin :: [*]) (rout :: [*])
       (proxy :: [*] -> *).
H2ProjectByLabels ls r rin rout =>
proxy ls -> HList r -> (HList rin, HList rout)
h2projectByLabels Proxy ls
ls HList t
r

-- need to rearrange because the ordering in the result is determined by
-- the ordering in the original record, not the ordering in the proxy. In
-- other words,
--
-- > hProjectByLabels (Proxy :: Proxy ["x","y"]) r == hProjectByLabels (Proxy :: Proxy ["y","x"]) r
hProjectByLabels' :: Record t -> Record l
hProjectByLabels' Record t
r =
    let r' :: Record l
r' = forall {l :: [*]} {r :: [*]}.
(HLabelSet (LabelsOf l), HRearrange3 (LabelsOf l) r l,
 SameLength' r l, SameLength' r (LabelsOf l), SameLength' l r,
 SameLength' (LabelsOf l) r) =>
Record r -> Record l
hRearrange' (forall (a :: [*]) (ls :: [*]) (t :: [*]) (b :: [*])
       (proxy :: [*] -> *).
(HRLabelSet a, H2ProjectByLabels ls t a b) =>
proxy ls -> Record t -> Record a
hProjectByLabels (forall (hlistOrRecord :: [*] -> *) (l :: [*]).
hlistOrRecord l -> Proxy (LabelsOf l)
labelsOf Record l
r') Record t
r)
    in Record l
r'



{- | A helper to make the Proxy needed by hProjectByLabels,
and similar functions which accept a list of kind [*].

For example:

@(rin,rout) = 'hProjectByLabels2' (Proxy :: Labels ["x","y"]) r@

behaves like

> rin = r .!. (Label :: Label "x") .*.
>       r .!. (Label :: Label "y") .*.
>       emptyRecord
>
> rout = r .-. (Label :: Label "x") .-. (Label :: Label "y")

-}
type family Labels (xs :: [k]) :: *
type instance Labels xs = Proxy (Labels1 xs)

type family Labels1 (xs :: [k]) :: [*]
type instance Labels1 '[] = '[]
type instance Labels1 (x ': xs) = Label x ': Labels1 xs

-- | /Invariant/:
--
--  > r === rin `disjoint-union` rout
--  > labels rin === ls
--  >     where (rin,rout) = hProjectByLabels ls r
class H2ProjectByLabels (ls::[*]) r rin rout | ls r -> rin rout where
    h2projectByLabels :: proxy ls -> HList r -> (HList rin,HList rout)

instance H2ProjectByLabels '[] r '[] r where
    h2projectByLabels :: forall (proxy :: [*] -> *).
proxy '[] -> HList r -> (HList '[], HList r)
h2projectByLabels proxy '[]
_ HList r
r = (HList '[]
HNil,HList r
r)

instance H2ProjectByLabels (l ': ls) '[] '[] '[] where
    h2projectByLabels :: forall (proxy :: [*] -> *).
proxy (l : ls) -> HList '[] -> (HList '[], HList '[])
h2projectByLabels proxy (l : ls)
_ HList '[]
_ = (HList '[]
HNil,HList '[]
HNil)

instance (HMemberM (Label l1) ((l :: *) ': ls) (b :: Maybe [*]),
          H2ProjectByLabels' b (l ': ls) (Tagged l1 v1 ': r1) rin rout)
    => H2ProjectByLabels (l ': ls) (Tagged l1 v1 ': r1) rin rout where
    h2projectByLabels :: forall (proxy :: [*] -> *).
proxy (l : ls)
-> HList (Tagged l1 v1 : r1) -> (HList rin, HList rout)
h2projectByLabels = forall (b :: Maybe [*]) (ls :: [*]) (r :: [*]) (rin :: [*])
       (rout :: [*]) (proxy :: [*] -> *).
H2ProjectByLabels' b ls r rin rout =>
Proxy b -> proxy ls -> HList r -> (HList rin, HList rout)
h2projectByLabels' (forall {k} (t :: k). Proxy t
Proxy::Proxy b)

class H2ProjectByLabels' (b::Maybe [*]) (ls::[*]) r rin rout
                         | b ls r -> rin rout where
    h2projectByLabels' :: Proxy b -> proxy ls ->
                                     HList r -> (HList rin,HList rout)

instance H2ProjectByLabels ls1 r rin rout =>
    H2ProjectByLabels' ('Just ls1) ls (f ': r) (f ': rin) rout where
    h2projectByLabels' :: forall (proxy :: [*] -> *).
Proxy ('Just ls1)
-> proxy ls -> HList (f : r) -> (HList (f : rin), HList rout)
h2projectByLabels' Proxy ('Just ls1)
_ proxy ls
_ (HCons f
x HList r
r) = (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons f
x HList rin
rin, HList rout
rout)
        where (HList rin
rin,HList rout
rout) = forall (ls :: [*]) (r :: [*]) (rin :: [*]) (rout :: [*])
       (proxy :: [*] -> *).
H2ProjectByLabels ls r rin rout =>
proxy ls -> HList r -> (HList rin, HList rout)
h2projectByLabels (forall {k} (t :: k). Proxy t
Proxy::Proxy ls1) HList r
r

-- | if ls above has labels not in the record,
-- we get labels (rin `isSubsetOf` ls).
instance H2ProjectByLabels ls r rin rout =>
    H2ProjectByLabels' 'Nothing ls (f ': r) rin (f ': rout) where
    h2projectByLabels' :: forall (proxy :: [*] -> *).
Proxy 'Nothing
-> proxy ls -> HList (f : r) -> (HList rin, HList (f : rout))
h2projectByLabels' Proxy 'Nothing
_ proxy ls
ls (HCons f
x HList r
r) = (HList rin
rin, forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons f
x HList rout
rout)
        where (HList rin
rin,HList rout
rout) = forall (ls :: [*]) (r :: [*]) (rin :: [*]) (rout :: [*])
       (proxy :: [*] -> *).
H2ProjectByLabels ls r rin rout =>
proxy ls -> HList r -> (HList rin, HList rout)
h2projectByLabels proxy ls
ls HList r
r

-- --------------------------------------------------------------------------
{- | Rename the label of record

>>> hRenameLabel x y (x .=. () .*. emptyRecord)
Record{y=()}

-}
hRenameLabel :: Label l -> Label l -> r v -> HExtendR (Tagged l v) (r v')
hRenameLabel Label l
l Label l
l' r v
r = HExtendR (Tagged l v) (r v')
r''
 where
  v :: v
v   = forall k (l :: k) r v. HasField l r v => Label l -> r -> v
hLookupByLabel Label l
l r v
r
  r' :: r v'
r'  = forall k (r :: [*] -> *) (l :: k) (v :: [*]) (v' :: [*]).
HDeleteAtLabel r l v v' =>
Label l -> r v -> r v'
hDeleteAtLabel Label l
l r v
r
  r'' :: HExtendR (Tagged l v) (r v')
r'' = forall {k} (l :: k) v. Label l -> v -> Tagged l v
newLVPair Label l
l' v
v forall e l. HExtend e l => e -> l -> HExtendR e l
.*. r v'
r'


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

type HTPupdateAtLabel record l v r = (HUpdateAtLabel record l v r r, SameLength' r r)

-- | A variation on 'hUpdateAtLabel': type-preserving update.
hTPupdateAtLabel :: HTPupdateAtLabel record l v r => Label l -> v -> record r -> record r
hTPupdateAtLabel :: forall {k} (record :: [*] -> *) (l :: k) v (r :: [*]).
HTPupdateAtLabel record l v r =>
Label l -> v -> record r -> record r
hTPupdateAtLabel Label l
l v
v record r
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 l
l v
v record r
r

{- ^

We could also say:

> hTPupdateAtLabel l v r = hUpdateAtLabel l v r `asTypeOf` r

Then we were taking a dependency on Haskell's type equivalence.
This would also constrain the actual implementation of hUpdateAtLabel.

-}

infixr 2 .<.
{-|
  The same as '.@.', except type preserving. It has the same fixity as (.\@.).

-}
f :: Tagged l v
f@(Tagged v
v) .<. :: Tagged l v -> record r -> record r
.<. record r
r = forall {k} (record :: [*] -> *) (l :: k) v (r :: [*]).
HTPupdateAtLabel record l v r =>
Label l -> v -> record r -> record r
hTPupdateAtLabel (forall {k} (l :: k) v. Tagged l v -> Label l
labelLVPair Tagged l v
f) v
v record r
r

-- --------------------------------------------------------------------------
-- | Subtyping for records

instance H2ProjectByLabels (LabelsOf r2) r1 r2 rout
    => SubType (Record r1) (Record r2)


type HMemberLabel l r b = HMember l (UnLabel l (LabelsOf r)) b

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

-- Left Union

class HDeleteLabels ks r r' | ks r -> r'
 where hDeleteLabels :: proxy (ks :: [*]) -- ^ as provided by labelsOf
          -> Record r -> Record r'

instance (HMember (Label l) ks b,
          HCond b (Record r2) (Record (Tagged l v ': r2)) (Record r3),
          HDeleteLabels ks r1 r2) =>
    HDeleteLabels ks (Tagged l v ': r1) r3 where
      hDeleteLabels :: forall (proxy :: [*] -> *).
proxy ks -> Record (Tagged l v : r1) -> Record r3
hDeleteLabels proxy ks
ks (Record (HCons Tagged l v
lv HList r1
r1)) =
          case forall (ks :: [*]) (r :: [*]) (r' :: [*]) (proxy :: [*] -> *).
HDeleteLabels ks r r' =>
proxy ks -> Record r -> Record r'
hDeleteLabels proxy ks
ks (forall (r :: [*]). HList r -> Record r
Record HList r1
r1) of
             Record HList r2
r2 -> forall (t :: Bool) x y z. HCond t x y z => Proxy t -> x -> y -> z
hCond (forall {k} (t :: k). Proxy t
Proxy :: Proxy b)
                  (forall (r :: [*]). HList r -> Record r
Record HList r2
r2)
                  (forall (r :: [*]). HList r -> Record r
Record (forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons Tagged l v
lv HList r2
r2))
instance HDeleteLabels ks '[] '[] where
    hDeleteLabels :: forall (proxy :: [*] -> *). proxy ks -> Record '[] -> Record '[]
hDeleteLabels proxy ks
_ Record '[]
_ = Record '[]
emptyRecord


class  HLeftUnion r r' r'' | r r' -> r''
 where hLeftUnion :: Record r -> Record r' -> Record r''

instance (HDeleteLabels (LabelsOf l) r r',
         HAppend (Record l) (Record r'),
         HAppendR (Record l) (Record r') ~ (Record lr)) => HLeftUnion l r lr
 where  hLeftUnion :: Record l -> Record r -> Record lr
hLeftUnion Record l
l Record r
r = Record l
l forall l1 l2. HAppend l1 l2 => l1 -> l2 -> HAppendR l1 l2
`hAppend` forall (ks :: [*]) (r :: [*]) (r' :: [*]) (proxy :: [*] -> *).
HDeleteLabels ks r r' =>
proxy ks -> Record r -> Record r'
hDeleteLabels (forall (hlistOrRecord :: [*] -> *) (l :: [*]).
hlistOrRecord l -> Proxy (LabelsOf l)
labelsOf Record l
l) Record r
r


infixl 1 .<++.
{-|
  Similar to list append, so give this slightly lower fixity than
  (.*.), so we can write:

   > field1 .=. value .*. record1 .<++. record2

-}
(.<++.) ::  (HLeftUnion r r' r'') => Record r -> Record r' -> Record r''
Record r
r .<++. :: forall (r :: [*]) (r' :: [*]) (r'' :: [*]).
HLeftUnion r r' r'' =>
Record r -> Record r' -> Record r''
.<++. Record r'
r' = forall (r :: [*]) (r' :: [*]) (r'' :: [*]).
HLeftUnion r r' r'' =>
Record r -> Record r' -> Record r''
hLeftUnion Record r
r Record r'
r'


-- --------------------------------------------------------------------------
-- $symmetricUnion
-- Compute the symmetric union of two records r1 and r2 and
-- return the pair of records injected into the union (ru1, ru2).
--
-- To be more precise, we compute the symmetric union /type/ @ru@
-- of two record /types/ @r1@ and @r2@. The emphasis on types is important.
--
-- The two records (ru1,ru2) in the result of 'unionSR' have the same
-- type ru, but they are generally different values.
-- Here the simple example: suppose
--
-- >  r1 = (Label .=. True)  .*. emptyRecord
-- >  r2 = (Label .=. False) .*. emptyRecord
--
-- Then 'unionSR' r1 r2 will return (r1,r2). Both components of the result
-- are different records of the same type.
--
--
-- To project from the union ru, use 'hProjectByLabels'.
-- It is possible to project from the union obtaining a record
-- that was not used at all when creating the union.
--
-- We do assure however that if @unionSR r1 r2@ gave @(r1u,r2u)@,
-- then projecting r1u onto the type of r1 gives the /value/ identical
-- to r1. Ditto for r2.

class UnionSymRec r1 r2 ru | r1 r2 -> ru where
    unionSR :: Record r1 -> Record r2 -> (Record ru, Record ru)

instance (r1 ~ r1') => UnionSymRec r1 '[] r1' where
    unionSR :: Record r1 -> Record '[] -> (Record r1', Record r1')
unionSR Record r1
r1 Record '[]
_ = (Record r1
r1, Record r1
r1)

instance ( HMemberLabel l r1 b
         , UnionSymRec' b r1 (Tagged l v) r2' ru
         )
    => UnionSymRec r1 (Tagged l v ': r2') ru
    where
    unionSR :: Record r1 -> Record (Tagged l v : r2') -> (Record ru, Record ru)
unionSR Record r1
r1 (Record (HCons Tagged l v
f HList r2'
r2')) =
        forall (b :: Bool) (r1 :: [*]) f2 (r2' :: [*]) (ru :: [*]).
UnionSymRec' b r1 f2 r2' ru =>
Proxy b -> Record r1 -> f2 -> Record r2' -> (Record ru, Record ru)
unionSR' (forall {k} (t :: k). Proxy t
Proxy::Proxy b) Record r1
r1 Tagged l v
f (forall (r :: [*]). HList r -> Record r
Record HList r2'
r2')

class UnionSymRec' (b :: Bool) r1 f2 r2' ru | b r1 f2 r2' -> ru where
    unionSR' :: Proxy b -> Record r1 -> f2 -> Record r2'  -> (Record ru, Record ru)



-- | Field f2 is already in r1, so it will be in the union of r1
-- with the rest of r2.
--
-- To inject (HCons f2 r2) in that union, we should replace the
-- field f2
instance (UnionSymRec r1 r2' ru,
          HTPupdateAtLabel Record l2 v2 ru,
          f2 ~ Tagged l2 v2)
    => UnionSymRec' True r1 f2 r2' ru where
    unionSR' :: Proxy 'True
-> Record r1 -> f2 -> Record r2' -> (Record ru, Record ru)
unionSR' Proxy 'True
_ Record r1
r1 (Tagged v2
v2) Record r2'
r2' =
       case forall (r1 :: [*]) (r2 :: [*]) (ru :: [*]).
UnionSymRec r1 r2 ru =>
Record r1 -> Record r2 -> (Record ru, Record ru)
unionSR Record r1
r1 Record r2'
r2'
        of (Record ru
ul,Record ru
ur) -> (Record ru
ul, forall {k} (record :: [*] -> *) (l :: k) v (r :: [*]).
HTPupdateAtLabel record l v r =>
Label l -> v -> record r -> record r
hTPupdateAtLabel (forall {k} (l :: k). Label l
Label :: Label l2) v2
v2 Record ru
ur)



instance (UnionSymRec r1 r2' ru,
          HExtend f2 (Record ru),
          Record f2ru ~ HExtendR f2 (Record ru)
        )
    => UnionSymRec' False r1 f2 r2' f2ru where
    unionSR' :: Proxy 'False
-> Record r1 -> f2 -> Record r2' -> (Record f2ru, Record f2ru)
unionSR' Proxy 'False
_ Record r1
r1 f2
f2 Record r2'
r2' = (HExtendR f2 (Record ru)
ul', HExtendR f2 (Record ru)
ur')
       where (Record ru
ul,Record ru
ur) = forall (r1 :: [*]) (r2 :: [*]) (ru :: [*]).
UnionSymRec r1 r2 ru =>
Record r1 -> Record r2 -> (Record ru, Record ru)
unionSR Record r1
r1 Record r2'
r2'
             ul' :: HExtendR f2 (Record ru)
ul' = f2
f2 forall e l. HExtend e l => e -> l -> HExtendR e l
.*. Record ru
ul
             ur' :: HExtendR f2 (Record ru)
ur' = f2
f2 forall e l. HExtend e l => e -> l -> HExtendR e l
.*. Record ru
ur

-- --------------------------------------------------------------------------
-- | Rearranges a record by labels. Returns the record r, rearranged such that
-- the labels are in the order given by ls. (LabelsOf r) must be a
-- permutation of ls.
hRearrange :: (HLabelSet ls, HRearrange ls r r') => Proxy ls -> Record r -> Record r'
hRearrange :: forall (ls :: [*]) (r :: [*]) (r' :: [*]).
(HLabelSet ls, HRearrange ls r r') =>
Proxy ls -> Record r -> Record r'
hRearrange Proxy ls
ls (Record HList r
r) = forall (r :: [*]). HList r -> Record r
Record (forall (ls :: [*]) (r :: [*]) (r' :: [*]) (proxy :: [*] -> *).
HRearrange ls r r' =>
proxy ls -> HList r -> HList r'
hRearrange2 Proxy ls
ls HList r
r)

{- | 'hRearrange'' is 'hRearrange' where ordering specified by the Proxy
argument is determined by the result type.

With built-in haskell records, these @e1@ and @e2@ have the same type:

> data R = R { x, y :: Int }
> e1 = R{ x = 1, y = 2}
> e2 = R{ y = 2, x = 1}

'hRearrange'' can be used to allow either ordering to be accepted:

> h1, h2 :: Record [ Tagged "x" Int, Tagged "y" Int ]
> h1 = hRearrange' $
>     x .=. 1 .*.
>     y .=. 2 .*.
>     emptyRecord
>
> h2 = hRearrange' $
>     y .=. 2 .*.
>     x .=. 1 .*.
>     emptyRecord

-}
hRearrange' :: Record r -> Record l
hRearrange' Record r
r =
    let r' :: Record l
r' = forall (ls :: [*]) (r :: [*]) (r' :: [*]).
(HLabelSet ls, HRearrange ls r r') =>
Proxy ls -> Record r -> Record r'
hRearrange (forall (hlistOrRecord :: [*] -> *) (l :: [*]).
hlistOrRecord l -> Proxy (LabelsOf l)
labelsOf Record l
r') Record r
r
    in Record l
r'


class Rearranged r s t a b where
    -- @Iso (r s) (r t) (r a) (r b)@
    rearranged :: (Profunctor p, Functor f) => r a `p` f (r b) -> r s `p` f (r t)


{- | @Iso (Record s) (Record t) (Record a) (Record b)@

where @s@ is a permutation of @a@, @b@ is a permutation of @t@.
In practice 'sameLabels' and 'sameLength' are likely needed on both
sides of @rearranged@, to avoid ambiguous types.

An alternative implementation:

> rearranged x = iso hRearrange' hRearrange' x

-}
instance (la ~ LabelsOf a, lt ~ LabelsOf t,
          HRearrange la s a,
          HRearrange lt b t,
          HLabelSet la,
          HLabelSet lt)
  => Rearranged Record s t a b where
    rearranged :: forall (p :: * -> * -> *) (f :: * -> *).
(Profunctor p, Functor f) =>
p (Record a) (f (Record b)) -> p (Record s) (f (Record t))
rearranged = forall (p :: * -> * -> *) (f :: * -> *) s a b t.
(Profunctor p, Functor f) =>
(s -> a) -> (b -> t) -> p a (f b) -> p s (f t)
iso (forall (ls :: [*]) (r :: [*]) (r' :: [*]).
(HLabelSet ls, HRearrange ls r r') =>
Proxy ls -> Record r -> Record r'
hRearrange (forall {k} (t :: k). Proxy t
Proxy :: Proxy la))
                     (forall (ls :: [*]) (r :: [*]) (r' :: [*]).
(HLabelSet ls, HRearrange ls r r') =>
Proxy ls -> Record r -> Record r'
hRearrange (forall {k} (t :: k). Proxy t
Proxy :: Proxy lt))

{- | @Iso' (r s) (r a)@

where @s@ is a permutation of @a@ -}
rearranged' :: p (r b) (f (r b)) -> p (r t) (f (r t))
rearranged' p (r b) (f (r b))
x = 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 forall {k} (r :: k -> *) (s :: k) (t :: k) (a :: k) (b :: k)
       (p :: * -> * -> *) (f :: * -> *).
(Rearranged r s t a b, Profunctor p, Functor f) =>
p (r a) (f (r b)) -> p (r s) (f (r t))
rearranged p (r b) (f (r b))
x

-- | Helper class for 'hRearrange'
class (HRearrange3 ls r r', LabelsOf r' ~ ls,
       SameLength ls r, SameLength r r')
      => HRearrange (ls :: [*]) r r' | ls r -> r', r' -> ls where
    hRearrange2 :: proxy ls -> HList r -> HList r'


instance (HRearrange3 ls r r', LabelsOf r' ~ ls,
        SameLength ls r, SameLength r r') => HRearrange ls r r' where
    hRearrange2 :: forall (proxy :: [*] -> *). proxy ls -> HList r -> HList r'
hRearrange2 = forall (ls :: [*]) (r :: [*]) (r' :: [*]) (proxy :: [*] -> *).
HRearrange3 ls r r' =>
proxy ls -> HList r -> HList r'
hRearrange3

-- | same as HRearrange, except no backwards FD
class HRearrange3 (ls :: [*]) r r' | ls r -> r' where
    hRearrange3 :: proxy ls -> HList r -> HList r'

instance HRearrange3 '[] '[] '[] where
   hRearrange3 :: forall (proxy :: [*] -> *). proxy '[] -> HList '[] -> HList '[]
hRearrange3 proxy '[]
_ HList '[]
_ = HList '[]
HNil

instance (H2ProjectByLabels '[l] r rin rout,
          HRearrange4 l ls rin rout r',
          l ~ Label ll) =>
        HRearrange3 (l ': ls) r r' where
   hRearrange3 :: forall (proxy :: [*] -> *). proxy (l : ls) -> HList r -> HList r'
hRearrange3 proxy (l : ls)
_ HList r
r = forall l (ls :: [*]) (rin :: [*]) (rout :: [*]) (r' :: [*])
       (proxy :: * -> *).
HRearrange4 l ls rin rout r' =>
proxy l -> Proxy ls -> HList rin -> HList rout -> HList r'
hRearrange4 (forall {k} (t :: k). Proxy t
Proxy :: Proxy l) (forall {k} (t :: k). Proxy t
Proxy :: Proxy ls) HList rin
rin HList rout
rout
      where (HList rin
rin, HList rout
rout) = forall (ls :: [*]) (r :: [*]) (rin :: [*]) (rout :: [*])
       (proxy :: [*] -> *).
H2ProjectByLabels ls r rin rout =>
proxy ls -> HList r -> (HList rin, HList rout)
h2projectByLabels (forall {k} (t :: k). Proxy t
Proxy :: Proxy '[l]) HList r
r


-- | Helper class 2 for 'hRearrange'
class HRearrange4 (l :: *) (ls :: [*]) rin rout r' | l ls rin rout -> r' where
    hRearrange4 :: proxy l -> Proxy ls -> HList rin -> HList rout -> HList r'

instance (HRearrange3 ls rout r',
         r'' ~ (Tagged l v ': r'),
         ll ~ Label l) =>
        HRearrange4 ll ls '[Tagged l v] rout r'' where
   hRearrange4 :: forall (proxy :: * -> *).
proxy ll
-> Proxy ls -> HList '[Tagged l v] -> HList rout -> HList r''
hRearrange4 proxy ll
_ Proxy ls
ls (HCons lv :: Tagged l v
lv@(Tagged v
v) HList '[]
_HNil) HList rout
rout
        = forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
HCons (forall {k} (s :: k) b. b -> Tagged s b
Tagged v
v forall a. a -> a -> a
`asTypeOf` Tagged l v
lv) (forall (ls :: [*]) (r :: [*]) (r' :: [*]) (proxy :: [*] -> *).
HRearrange3 ls r r' =>
proxy ls -> HList r -> HList r'
hRearrange3 Proxy ls
ls HList rout
rout)

-- | For improved error messages. XXX FieldNotFound
instance Fail (FieldNotFound l ()) =>
        HRearrange4 l ls '[] rout '[] where
   hRearrange4 :: forall (proxy :: * -> *).
proxy l -> Proxy ls -> HList '[] -> HList rout -> HList '[]
hRearrange4 proxy l
_ Proxy ls
_ HList '[]
_ HList rout
_ = forall a. HasCallStack => String -> a
error String
"Fail has no instances"

-- | For improved error messages
instance Fail (ExtraField l) =>
          HRearrange3 '[] (Tagged l v ': a) '[] where
   hRearrange3 :: forall (proxy :: [*] -> *).
proxy '[] -> HList (Tagged l v : a) -> HList '[]
hRearrange3 proxy '[]
_ HList (Tagged l v : a)
_ = forall a. HasCallStack => String -> a
error String
"Fail has no instances"


-- --------------------------------------------------------------------------
-- $lens
-- Lens-based setters/getters are popular. hLens packages up
-- 'hUpdateAtLabel' and 'hLookupByLabel'.
--
-- Refer to @examples/lens.hs@ and @examples/labelable.hs@ for examples.

-- | constraints needed to implement 'HLens'
type HLensCxt x r s t a b =
    (HasField x (r s) a,
     HUpdateAtLabel r x b s t,
     HasField x (r t) b,
     HUpdateAtLabel r x a t s,
     SameLength s t,
     SameLabels s t)

class HLensCxt x r s t a b => HLens x r s t a b
        | x s b -> t, x t a -> s, -- need to repeat fundeps implied by HLensCxt
          x s -> a, x t -> b where
    -- | @hLens :: Label x -> Lens (r s) (r t) a b@
    hLens :: Label x -> (forall f. Functor f => (a -> f b) -> (r s -> f (r t)))

instance HLensCxt r x s t a b => HLens r x s t a b where
  hLens :: Label r
-> forall (f :: * -> *). Functor f => (a -> f b) -> x s -> f (x t)
hLens Label r
lab a -> f b
f x s
rec = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\b
v -> 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 r
lab b
v x s
rec) (a -> f b
f (x s
rec forall {k} (l :: k) r v. HasField l r v => r -> Label l -> v
.!. Label r
lab))


{- | map over the values of a record. This is a shortcut for

  > \ f (Record a) -> Record (hMap (HFmap f) a)

[@Example@]

suppose we have a function that should be applied to every element
of a record:

>>> let circSucc_ x | x == maxBound = minBound | otherwise = succ x

>>> :t circSucc_
circSucc_ :: (Bounded a, Enum a, Eq a) => a -> a

Use a shortcut ('Fun') to create a value that has an appropriate 'ApplyAB' instance:

>>> let circSucc = Fun circSucc_ :: Fun '[Eq,Enum,Bounded] '()

Confirm that we got Fun right:

>>> :t applyAB circSucc
applyAB circSucc :: (Bounded b, Enum b, Eq b) => b -> b

>>> applyAB circSucc True
False

define the actual record:

>>> let r = x .=. 'a' .*. y .=. False .*. emptyRecord
>>> r
Record{x='a',y=False}

>>> hMapR circSucc r
Record{x='b',y=True}

-}
hMapR :: f -> Record x -> Record y
hMapR f
f Record x
r = forall f a b. ApplyAB f a b => f -> a -> b
applyAB (forall f. f -> HMapR f
HMapR f
f) Record x
r

newtype HMapR f = HMapR f

instance (HMapCxt Record f x y, rx ~ Record x, ry ~ Record y)
      => ApplyAB (HMapR f) rx ry where
        applyAB :: HMapR f -> rx -> ry
applyAB (HMapR f
f) = forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux f
f

instance HMapAux HList (HFmap f) x y =>
    HMapAux Record f x y where
      hMapAux :: SameLength x y => f -> Record x -> Record y
hMapAux f
f (Record HList x
x) = forall (r :: [*]). HList r -> Record r
Record (forall (r :: [*] -> *) f (x :: [*]) (y :: [*]).
(HMapAux r f x y, SameLength x y) =>
f -> r x -> r y
hMapAux (forall f. f -> HFmap f
HFmap f
f) HList x
x)



-- --------------------------------------------------------------------------
-- | This instance allows creating a Record with
--
-- @hBuild 3 'a' :: Record '[Tagged "x" Int, Tagged "y" Char]@
instance (HReverse l lRev,
         HMapTaggedFn lRev l') => HBuild' l (Record l') where
  hBuild' :: HList l -> Record l'
hBuild' HList l
l = forall (a :: [*]) (b :: [*]).
HMapTaggedFn a b =>
HList a -> Record b
hMapTaggedFn (forall (xs :: [*]) (sx :: [*]).
HReverse xs sx =>
HList xs -> HList sx
hReverse HList l
l)

-- | serves the same purpose as 'hEnd'
hEndR :: Record a -> Record a
hEndR :: forall (a :: [*]). Record a -> Record a
hEndR = forall a. a -> a
id


-- | see 'hEndP'
instance (HRevAppR l '[] ~ lRev,
          HExtendRs lRev (Proxy ('[] :: [*])) ~ Proxy l1,
          l' ~ l1) => HBuild' l (Proxy l') where
  hBuild' :: HList l -> Proxy l'
hBuild' HList l
_ = forall {k} (t :: k). Proxy t
Proxy

{- | @'hEndP' $ 'hBuild' label1 label2@

is one way to make a Proxy of labels (for use with 'asLabelsOf'
for example). Another way is

@label1 .*. label2 .*. 'emptyProxy'@

-}
hEndP :: Proxy (xs :: [k]) -> Proxy xs
hEndP :: forall k (xs :: [k]). Proxy xs -> Proxy xs
hEndP = forall a. a -> a
id

type family HExtendRs (ls :: [*]) (z :: k) :: k
type instance HExtendRs (l ': ls) z = HExtendR l (HExtendRs ls z)
type instance HExtendRs '[] z = z

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

{- |

>>> let x :: Record '[Tagged "x" Int]; x = undefined
>>> let y :: Record '[Tagged "x" Char]; y = undefined
>>> :t hZip x y
hZip x y :: Record '[Tagged "x" (Int, Char)]

-}
instance (HZipRecord x y xy, SameLengths [x,y,xy])
      => HZip Record x y xy where
    hZip :: Record x -> Record y -> Record xy
hZip = forall (x :: [*]) (y :: [*]) (xy :: [*]).
HZipRecord x y xy =>
Record x -> Record y -> Record xy
hZipRecord

instance (HZipRecord x y xy, SameLengths [x,y,xy])
      => HUnzip Record x y xy where
    hUnzip :: Record xy -> (Record x, Record y)
hUnzip = forall (x :: [*]) (y :: [*]) (xy :: [*]).
HZipRecord x y xy =>
Record xy -> (Record x, Record y)
hUnzipRecord


#if __GLASGOW_HASKELL__ != 706
{- | Missing from ghc-7.6, because HZip Proxy instances interfere with HZip
HList instances.

a variation on 'hZip' for 'Proxy', where
the list of labels does not have to include Label
(as in @ts'@)

>>> let ts = Proxy :: Proxy ["x","y"]
>>> let ts' = Proxy :: Proxy [Label "x",Label "y"]
>>> let vs = Proxy :: Proxy [Int,Char]

>>> :t zipTagged ts Proxy
zipTagged ts Proxy :: Proxy '[Tagged "x" y, Tagged "y" y1]

>>> :t zipTagged ts vs
zipTagged ts vs :: Proxy '[Tagged "x" Int, Tagged "y" Char]


And and the case when hZip does the same thing:

>>> :t zipTagged ts' vs
zipTagged ts' vs :: Proxy '[Tagged "x" Int, Tagged "y" Char]

>>> :t hZip ts' vs
hZip ts' vs :: Proxy '[Tagged "x" Int, Tagged "y" Char]

-}
zipTagged :: (MapLabel ts ~ lts,
              HZip Proxy lts vs tvs)
      => Proxy ts -> proxy vs -> Proxy tvs
zipTagged :: forall {k} (ts :: [k]) (lts :: [*]) (vs :: [*]) (tvs :: [*])
       (proxy :: [*] -> *).
(MapLabel ts ~ lts, HZip Proxy lts vs tvs) =>
Proxy ts -> proxy vs -> Proxy tvs
zipTagged Proxy ts
_ proxy vs
_ = forall {k} (t :: k). Proxy t
Proxy
#endif



class HZipRecord x y xy | x y -> xy, xy -> x y where
    hZipRecord :: Record x -> Record y -> Record xy
    hUnzipRecord :: Record xy -> (Record x,Record y)


instance HZipRecord '[] '[] '[] where
    hZipRecord :: Record '[] -> Record '[] -> Record '[]
hZipRecord Record '[]
_ Record '[]
_ = Record '[]
emptyRecord
    hUnzipRecord :: Record '[] -> (Record '[], Record '[])
hUnzipRecord Record '[]
_ = (Record '[]
emptyRecord, Record '[]
emptyRecord)

instance HZipRecord as bs abss
       => HZipRecord (Tagged x a ': as) (Tagged x b ': bs) (Tagged x (a,b) ': abss) where
    hZipRecord :: Record (Tagged x a : as)
-> Record (Tagged x b : bs) -> Record (Tagged x (a, b) : abss)
hZipRecord (Record (Tagged a
a `HCons` HList as
as)) (Record (Tagged b
b `HCons` HList bs
bs)) =
        let Record HList abss
abss = forall (x :: [*]) (y :: [*]) (xy :: [*]).
HZipRecord x y xy =>
Record x -> Record y -> Record xy
hZipRecord (forall (r :: [*]). HList r -> Record r
Record HList as
as) (forall (r :: [*]). HList r -> Record r
Record HList bs
bs)
        in forall (r :: [*]). HList r -> Record r
Record (forall {k} (s :: k) b. b -> Tagged s b
Tagged (a
a,b
b) forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList abss
abss)
    hUnzipRecord :: Record (Tagged x (a, b) : abss)
-> (Record (Tagged x a : as), Record (Tagged x b : bs))
hUnzipRecord (Record (Tagged (a
a,b
b) `HCons` HList abss
abss)) =
        let (Record HList as
as, Record HList bs
bs) = forall (x :: [*]) (y :: [*]) (xy :: [*]).
HZipRecord x y xy =>
Record xy -> (Record x, Record y)
hUnzipRecord (forall (r :: [*]). HList r -> Record r
Record HList abss
abss)
        in (forall (r :: [*]). HList r -> Record r
Record (forall {k} (s :: k) b. b -> Tagged s b
Tagged a
a forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList as
as), forall (r :: [*]). HList r -> Record r
Record (forall {k} (s :: k) b. b -> Tagged s b
Tagged b
b forall x (xs :: [*]). x -> HList xs -> HList (x : xs)
`HCons` HList bs
bs))


-- | instead of explicit recursion above, we could define HZipRecord in
-- terms of 'HZipList'. While all types are inferred, this implementation
-- is probably slower, so explicit recursion is used in the 'HZip' 'Record'
-- instance.
hZipRecord2 :: Record y -> Record y -> Record x
hZipRecord2 Record y
x Record y
y = forall (a :: [*]) (b :: [*]).
HMapTaggedFn a b =>
HList a -> Record b
hMapTaggedFn (forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList x -> HList y -> HList l
hZipList (forall (r :: [*]).
RecordValues r =>
Record r -> HList (RecordValuesR r)
recordValues Record y
x) (forall (r :: [*]).
RecordValues r =>
Record r -> HList (RecordValuesR r)
recordValues Record y
y))
        forall {m} (x :: [*]) (y :: [m]) (r :: [*] -> *) (s :: [m] -> *).
(HAllTaggedLV x, SameLabels x y, SameLength x y) =>
r x -> s y -> r x
`asLabelsOf` Record y
x forall {m} (x :: [*]) (y :: [m]) (r :: [*] -> *) (s :: [m] -> *).
(HAllTaggedLV x, SameLabels x y, SameLength x y) =>
r x -> s y -> r x
`asLabelsOf` Record y
y

hUnzipRecord2 :: Record y -> (Record x, Record x)
hUnzipRecord2 Record y
xy = let (HList (RecordValuesR x)
x,HList (RecordValuesR x)
y) = forall (x :: [*]) (y :: [*]) (l :: [*]).
HZipList x y l =>
HList l -> (HList x, HList y)
hUnzipList (forall (r :: [*]).
RecordValues r =>
Record r -> HList (RecordValuesR r)
recordValues Record y
xy)
                 in (forall (a :: [*]) (b :: [*]).
HMapTaggedFn a b =>
HList a -> Record b
hMapTaggedFn HList (RecordValuesR x)
x forall {m} (x :: [*]) (y :: [m]) (r :: [*] -> *) (s :: [m] -> *).
(HAllTaggedLV x, SameLabels x y, SameLength x y) =>
r x -> s y -> r x
`asLabelsOf` Record y
xy, forall (a :: [*]) (b :: [*]).
HMapTaggedFn a b =>
HList a -> Record b
hMapTaggedFn HList (RecordValuesR x)
y forall {m} (x :: [*]) (y :: [m]) (r :: [*] -> *) (s :: [m] -> *).
(HAllTaggedLV x, SameLabels x y, SameLength x y) =>
r x -> s y -> r x
`asLabelsOf` Record y
xy)


{- | similar to 'asTypeOf':

>>> let s0 = Proxy :: Proxy '["x", "y"]
>>> let s1 = Proxy :: Proxy '[Label "x", Label "y"]
>>> let s2 = Proxy :: Proxy '[Tagged "x" Int, Tagged "y" Char]

>>> let f0 r = () where _ = r `asLabelsOf` s0
>>> let f1 r = () where _ = r `asLabelsOf` s1
>>> let f2 r = () where _ = r `asLabelsOf` s2

>>> :t f0
f0 :: r '[Tagged "x" v, Tagged "y" v1] -> ()

>>> :t f1
f1 :: r '[Tagged "x" v, Tagged "y" v1] -> ()

>>> :t f2
f2 :: r '[Tagged "x" v, Tagged "y" v1] -> ()

-}
asLabelsOf :: (HAllTaggedLV x, SameLabels x y, SameLength x y) => r x -> s y -> r x
asLabelsOf :: forall {m} (x :: [*]) (y :: [m]) (r :: [*] -> *) (s :: [m] -> *).
(HAllTaggedLV x, SameLabels x y, SameLength x y) =>
r x -> s y -> r x
asLabelsOf = forall a b. a -> b -> a
const