{- |

Description : labels which are also lenses (or prisms)

A simple problem is being solved here, but unfortunately it
is a bit involved. The idea is to use the same haskell identifier
for a lens and for other purposes. In other words, get the same
behavior as:

 > x = hLens (Label :: Label "x")
 > r ^. x

While still being able to extract the symbol \"x\" from x, so that things
like @x .=. 123@ could be acceptable. In this case we don't overload '.=.',
so instead you have to write @x .==. 123@.


Elaboration of some ideas from edwardk.
-}
module Data.HList.Labelable
    (Labelable(..),
     LabeledOptic,
     (.==.),


     -- * multiple lookups
     Projected(..), projected',

    -- * comparison with 'hLens'
    -- $comparisonWithhLensFunction

    -- * likely unneeded (re)exports
    LabeledCxt1,
    LabeledTo(LabeledTo),
    LabeledR(LabeledR),
    ToSym, EnsureLabel(toLabel), toLabelSym,
    Identity,
    LabelableTIPCxt,
    LabeledOpticType(..),

    LabeledOpticF,
    LabeledOpticP,
    LabeledOpticTo,
    ) where



import Data.HList.HListPrelude
import Data.HList.FakePrelude
import Data.HList.Record
import Data.HList.Variant
import Data.HList.TIP
import Data.HList.TIC
import Data.HList.Label3

import Control.Monad.Identity
import GHC.TypeLits
import LensDefs
import GHC.Exts (Constraint)

{- | This alias is the same as Control.Lens.Optic, except the (->) in Optic
is a type parameter 'to' in LabeledOptic.

Depending on the collection type (see instances of 'LabelableTy'),
the type variables @to, p, f@ are constrained such that the resulting
type is a @Lens (r s) (r t) a b@, @Prism (r s) (r t) a b@ or a
@LabeledTo x _ _@. The latter can be used to recover the label (@x@) when
used as an argument to '.==.' or equivalently 'toLabel'.
-}
type LabeledOptic (x :: k) (r :: [*] -> *) (s :: [*]) (t :: [*]) (a :: *) (b :: *)
    = forall ty to p f.
                     (ty ~ LabelableTy r,
                      LabeledOpticF ty f,
                      LabeledOpticP ty p,
                      LabeledOpticTo ty x to) => (a `p` f b) `to` (r s `p` f (r t))

data LabeledOpticType = LabelableLens | LabelablePrism | LabelableLabel

type family LabeledOpticF (ty :: LabeledOpticType) :: (* -> *) -> Constraint
type instance LabeledOpticF LabelableLens = Functor
type instance LabeledOpticF LabelablePrism = Applicative
type instance LabeledOpticF LabelableLabel = (~) Identity

type family LabeledOpticP (ty :: LabeledOpticType) :: (* -> * -> *) -> Constraint
type instance LabeledOpticP LabelableLens = (~) (->)
type instance LabeledOpticP LabelablePrism = Choice
type instance LabeledOpticP LabelableLabel = (~) (->)

type family LabeledOpticTo (ty :: LabeledOpticType) (x :: k) :: (* -> * -> *) -> Constraint
type instance LabeledOpticTo LabelableLens x = (~) (->)
type instance LabeledOpticTo LabelablePrism x = (~) (->)
type instance LabeledOpticTo LabelableLabel x = (~) (LabeledTo x)


{- |

[@r@] is 'Record', 'Variant'. 'TIP' and 'TIC' also have instances, but generally
'tipyLens'' and 'ticPrism'' are more appropriate.

[@x@] is the label for the field. It tends to have kind 'GHC.TypeLits.Symbol',
but others are supported in principle.

-}
class SameLength s t => Labelable (x :: k) (r :: [*] -> *) s t a b
          | x s -> a, x t -> b,    -- lookup
            x s b -> t, x t a -> s -- update
  where
    type LabelableTy r :: LabeledOpticType
    hLens' :: Label x -> LabeledOptic x r s t a b

data LabeledTo (x :: k) (a :: *) (b :: *) = LabeledTo deriving (Int -> LabeledTo x a b -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (x :: k) a b. Int -> LabeledTo x a b -> ShowS
forall k (x :: k) a b. [LabeledTo x a b] -> ShowS
forall k (x :: k) a b. LabeledTo x a b -> String
showList :: [LabeledTo x a b] -> ShowS
$cshowList :: forall k (x :: k) a b. [LabeledTo x a b] -> ShowS
show :: LabeledTo x a b -> String
$cshow :: forall k (x :: k) a b. LabeledTo x a b -> String
showsPrec :: Int -> LabeledTo x a b -> ShowS
$cshowsPrec :: forall k (x :: k) a b. Int -> LabeledTo x a b -> ShowS
Show)

data LabeledR (x :: [*]) = LabeledR

{- if __GLASGOW_HASKELL__ > 800
-- should this orphan instance really be supplied? ghc 8's
-- -XOverloadedLabels is uglier syntax than HListPP, and it
-- seems likely that other users of IsLabel probably define
-- an instance for (->) which will be chosen over this one
-- when labels are composed with (.),
-- (or alternatively there will be complaints about overlap)
instance (x ~ x', Labelable x r s t a b) => IsLabel x (LabeledOptic x' r s t a b) where
    fromLabel _ = hLens' (Label :: Label x)
-- endif
-}


-- | make a @Lens (Record s) (Record t) a b@
instance HLens x Record s t a b
        => Labelable x Record s t a b where
            type LabelableTy Record = LabelableLens
            hLens' :: Label x -> LabeledOptic x Record s t a b
hLens' Label x
x = 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 x
x

-- | used with 'toLabel' and/or '.==.'
instance LabeledCxt1 s t a b => Labelable x LabeledR s t a b where
        type LabelableTy LabeledR = LabelableLabel
        hLens' :: Label x -> LabeledOptic x LabeledR s t a b
hLens' Label x
_ = forall k (x :: k) a b. LabeledTo x a b
LabeledTo

-- | sets all type variables to dummy values: only the @Labeled x@
-- part is actually needed
type LabeledCxt1 s t a b = (s ~ '[], t ~ '[], a ~ (), b ~ ())

-- | make a @Prism (Variant s) (Variant t) a b@
instance (HPrism x s t a b,
          to ~ (->)) => Labelable x Variant s t a b where
    type LabelableTy Variant = LabelablePrism
    hLens' :: Label x -> LabeledOptic x Variant s t a b
hLens' Label x
x p a (f b)
s = forall {k} (x :: k) (s :: [*]) (t :: [*]) a b (p :: * -> * -> *)
       (f :: * -> *).
(HPrism x s t a b, Choice p, Applicative f) =>
Label x -> p a (f b) -> p (Variant s) (f (Variant t))
hPrism Label x
x p a (f b)
s

-- | @hLens' :: Label a -> Prism' (TIC s) a@
--
-- note that a more general function @'ticPrism' :: Prism (TIC s) (TIC t) a b@,
-- cannot have an instance of Labelable
--
-- Note: `x :: k` according to the instance head, but the instance body
-- forces the kind variable to be * later on. IE. (k ~ *)
instance (TICPrism s t a b, Label x ~ Label a,a ~ b, s ~ t,
          SameLength s t) =>
    Labelable (x :: k) TIC s t a b where
      type LabelableTy TIC = LabelablePrism
      hLens' :: Label x -> LabeledOptic x TIC s t a b
hLens' Label x
_ = forall (s :: [*]) (t :: [*]) a b (p :: * -> * -> *) (f :: * -> *).
(TICPrism s t a b, SameLength s t, Choice p, Applicative f) =>
p a (f b) -> p (TIC s) (f (TIC t))
ticPrism


-- | make a @Lens' (TIP s) a@.
--
-- 'tipyLens' provides a @Lens (TIP s) (TIP t) a b@, which tends to need
-- too many type annotations to be practical
instance LabelableTIPCxt x s t a b =>
    Labelable (x :: k) TIP s t a b where
    type LabelableTy TIP = LabelableLens
    hLens' :: Label x -> LabeledOptic x TIP s t a b
hLens' Label x
x = 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 x
x

type LabelableTIPCxt x s t a b =
     (s ~ t, a ~ b, Label x ~ Label a,
      HLens x TIP s t a b)


-- | modification of '.=.' which works with the labels from this module,
-- and those from "Data.HList.Label6". Note that this is not strictly a
-- generalization of '.=.', since it does not work with labels like
-- "Data.HList.Label3" which have the wrong kind.
x
l .==. :: x -> v -> Tagged l v
.==. v
v = forall x y. EnsureLabel x y => x -> y
toLabel x
l forall {k} (l :: k) v. Label l -> v -> Tagged l v
.=. v
v

infixr 4 .==.

-- | Get the Symbol out of a 'Label' or 'LabeledTo'
class ToSym label (s :: Symbol) | label -> s

instance LabeledTo x (a `p` f b) (LabeledR s `p` f (LabeledR t)) ~ v1 v2 v3
    => ToSym (v1 v2 v3) x

instance ToSym (label x) x

{- | Convert a type to @Label :: Label blah@

> toLabel :: LabeledTo x _ _ -> Label (x :: Symbol)
> toLabel (hLens' lx)         = (lx :: Label x)
> toLabel :: Label x         -> Label x
> toLabel :: Proxy x         -> Label x

-}
class EnsureLabel x y | x -> y where
  toLabel :: x -> y

instance EnsureLabel (Label x) (Label (x :: k)) where
  toLabel :: Label x -> Label x
toLabel Label x
_ = forall {k} (l :: k). Label l
Label

instance EnsureLabel (Proxy x) (Label (x :: k)) where
  toLabel :: Proxy x -> Label x
toLabel Proxy x
_ = forall {k} (l :: k). Label l
Label

-- | get the Label out of a 'LabeledTo' (ie. `foobar when using HListPP).
instance ToSym (a b c) (x :: Symbol) => EnsureLabel (a b c) (Label x) where
  toLabel :: a b c -> Label x
toLabel a b c
_ = forall {k} (l :: k). Label l
Label


-- | fix the `k` kind variable to 'Symbol'
toLabelSym :: x -> Label x
toLabelSym x
label = forall x y. EnsureLabel x y => x -> y
toLabel x
label forall a. a -> a -> a
`asTypeOf` (forall {k} (l :: k). Label l
Label :: Label (x :: Symbol))


{- $comparisonWithhLensFunction

Note that passing around variables defined with 'hLens'' doesn't get
you exactly the same thing as calling 'hLens' at the call-site:

The following code needs to apply the @x@ for different @Functor
f =>@, so you would have to write a type signature (rank-2) to allow this
definition:

 > -- with the x defined using hLens'
 > let f x r = let
 >          a = r ^. x
 >          b = r & x .~ "6"
 >        in (a,b)

This alternative won't need a type signature

 > -- with the x defined as x = Label :: Label "x"
 > let f x r = let
 >          a = r ^. hLens x
 >          b = r & hLens x .~ "7"
 >        in (a,b)

It may work to use 'hLens'' instead of 'hLens' in the second code,
but that is a bit beside the point being made here.

The same points apply to the use of 'hPrism' over 'hLens''.

-}

{- | Sometimes it may be more convenient to operate on a record/variant
that only contains the fields of interest. 'projected' can then be used
to apply that function to a record that contains additional elements.


>>> :set -XViewPatterns
>>> import Data.HList.RecordPuns
>>> let f [pun| (x y) |] = case x+y of z -> [pun| z |]
>>> :t f
f :: Num v =>
     Record '[Tagged "x" v, Tagged "y" v] -> Record '[Tagged "z" v]

>>> let r = (let x = 1; y = 2; z = () in [pun| x y z |])
>>> r
Record{x=1,y=2,z=()}

>>> r & sameLabels . projected %~ f
Record{x=1,y=2,z=3}




-}
class Projected r s t a b where
    projected :: (ty ~ LabelableTy r,
                LabeledOpticP ty p,
                LabeledOpticF ty f) => r a `p` f (r b) -> r s `p` f (r t)

-- | @Lens rs rt ra rb@
--
-- where @rs ~ Record s, rt ~ Record t, ra ~ Record a, rb ~ Record b@
instance (-- for Record s -> Record a
          H2ProjectByLabels (LabelsOf a) s a_ _s_minus_a,
          HRLabelSet a_, HRLabelSet a,
          HRearrange (LabelsOf a) a_ a,

          HLeftUnion b s bs, HRLabelSet bs,
          HRearrange (LabelsOf t) bs t, HRLabelSet t
        ) => Projected Record s t a b where
    projected :: forall (ty :: LabeledOpticType) (p :: * -> * -> *) (f :: * -> *).
(ty ~ LabelableTy Record, LabeledOpticP ty p,
 LabeledOpticF ty f) =>
p (Record a) (f (Record b)) -> p (Record s) (f (Record t))
projected p (Record a) (f (Record b))
f Record s
s = (\Record b
b -> 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' (Record b
b forall (r :: [*]) (r' :: [*]) (r'' :: [*]).
HLeftUnion r r' r'' =>
Record r -> Record r' -> Record r''
.<++. Record s
s)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> p (Record a) (f (Record b))
f (forall {l :: [*]} {r :: [*]} {t :: [*]} {b :: [*]}.
(HRearrange3 (LabelsOf l) r l, SameLength' r l,
 SameLength' r (LabelsOf l), SameLength' l r,
 SameLength' (LabelsOf l) r, HLabelSet (LabelsOf l),
 HLabelSet (LabelsOf r), HAllTaggedLV r,
 H2ProjectByLabels (LabelsOf l) t r b) =>
Record t -> Record l
hProjectByLabels' Record s
s :: Record a)

-- | @Prism (Variant s) (Variant t) (Variant a) (Variant b)@
instance (ExtendsVariant b t,
          ProjectVariant s a,
          ProjectExtendVariant s t,

          HLeftUnion b s bs, HRLabelSet bs,
          HRearrange (LabelsOf t) bs t)
      => Projected Variant s t a b where
    projected :: forall (ty :: LabeledOpticType) (p :: * -> * -> *) (f :: * -> *).
(ty ~ LabelableTy Variant, LabeledOpticP ty p,
 LabeledOpticF ty f) =>
p (Variant a) (f (Variant b)) -> p (Variant s) (f (Variant t))
projected = forall b t s a.
(b -> t)
-> (s -> Either t a)
-> forall (p :: * -> * -> *) (f :: * -> *).
   (Choice p, Applicative f) =>
   p a (f b) -> p s (f t)
prism forall (x :: [*]) (y :: [*]).
ExtendsVariant x y =>
Variant x -> Variant y
extendsVariant
            (\Variant s
s -> case forall (x :: [*]) (y :: [*]).
ProjectVariant x y =>
Variant x -> Maybe (Variant y)
projectVariant Variant s
s of
                    Just Variant a
a -> forall a b. b -> Either a b
Right Variant a
a
                    Maybe (Variant a)
Nothing | Just Variant t
t <- forall (x :: [*]) (y :: [*]).
ProjectExtendVariant x y =>
Variant x -> Maybe (Variant y)
projectExtendVariant Variant s
s -> forall a b. a -> Either a b
Left Variant t
t
                    Maybe (Variant a)
_ -> forall a. HasCallStack => String -> a
error String
"Data.HList.Labelable.projected impossible"
                    -- projectExtendVariant gives Nothing when the element of
                    -- `t` that is actually stored in the variant comes
                    -- from the `b`. But in that case the projectVariant
                    -- above must have been Just
              )


{- | @Lens' (Record s) (Record a)@

@Prism' (Variant s) (Variant a)@
-}
projected' :: p (r b) (f (r b)) -> p (r t) (f (r t))
projected' p (r b) (f (r b))
s = 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 :: [*] -> *) (s :: [*]) (t :: [*]) (a :: [*]) (b :: [*])
       (ty :: LabeledOpticType) (p :: * -> * -> *) (f :: * -> *).
(Projected r s t a b, ty ~ LabelableTy r, LabeledOpticP ty p,
 LabeledOpticF ty f) =>
p (r a) (f (r b)) -> p (r s) (f (r t))
projected p (r b) (f (r b))
s


{- | Together with the instance below, this allows writing

@
'makeLabelable' "x y z"
p = x .*. y .*. z .*. 'emptyProxy'
@

Or with HListPP

@
p = `x .*. `y .*. `z .*. emptyProxy
@

instead of

> p = Proxy :: Proxy ["x","y","z"]

-}
instance (to ~ LabeledTo x, ToSym (to p q) x)
       => HExtend (to p q) (Proxy ('[] :: [*])) where
    type HExtendR (to p q) (Proxy ('[] :: [*])) = Proxy '[GetXFromLabeledTo to]
    .*. :: to p q -> Proxy '[] -> HExtendR (to p q) (Proxy '[])
(.*.) to p q
_ Proxy '[]
_ = forall {k} (t :: k). Proxy t
Proxy

instance (to ~ LabeledTo x, ToSym (to p q) x)
       => HExtend (to p q) (Proxy (x ': xs)) where
    type HExtendR (to p q) (Proxy (x ': xs)) = Proxy (GetXFromLabeledTo to ': x ': xs)
    .*. :: to p q -> Proxy (x : xs) -> HExtendR (to p q) (Proxy (x : xs))
(.*.) to p q
_ Proxy (x : xs)
_ = forall {k} (t :: k). Proxy t
Proxy

-- | if the proxy has Data.HList.Label3."Lbl", then everything has to be
-- wrapped in Label to make the kinds match up.
instance (to ~ LabeledTo x, ToSym (to p q) x)
       => HExtend (to p q) (Proxy (Lbl n ns desc ': xs)) where
    type HExtendR (to p q) (Proxy (Lbl n ns desc ': xs))
        = Proxy (Label (GetXFromLabeledTo to) ': MapLabel (Lbl n ns desc ': xs))
    .*. :: to p q
-> Proxy (Lbl n ns desc : xs)
-> HExtendR (to p q) (Proxy (Lbl n ns desc : xs))
(.*.) to p q
_ Proxy (Lbl n ns desc : xs)
_ = forall {k} (t :: k). Proxy t
Proxy

type family GetXFromLabeledTo (to :: * -> * -> *) :: Symbol
type instance GetXFromLabeledTo (LabeledTo x) = x