-- | 'weaken' over generic representations.

module Strongweak.Weaken.Generic where

import Strongweak.Weaken
import GHC.Generics

-- | Weaken a value generically.
--
-- The weak and strong types must be /compatible/. See 'Strongweak.Generic' for
-- the definition of compatibility in this context.
weakenGeneric :: (Generic s, Generic w, GWeaken (Rep s) (Rep w)) => s -> w
weakenGeneric :: forall s w.
(Generic s, Generic w, GWeaken (Rep s) (Rep w)) =>
s -> w
weakenGeneric = Rep w Any -> w
forall a x. Generic a => Rep a x -> a
forall x. Rep w x -> w
to (Rep w Any -> w) -> (s -> Rep w Any) -> s -> w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep s Any -> Rep w Any
forall p. Rep s p -> Rep w p
forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken (Rep s Any -> Rep w Any) -> (s -> Rep s Any) -> s -> Rep w Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> Rep s Any
forall x. s -> Rep s x
forall a x. Generic a => a -> Rep a x
from

class GWeaken s w where
    gweaken :: s p -> w p

-- | Strip all meta.
instance GWeaken s w => GWeaken (M1 is ms s) (M1 iw mw w) where
    gweaken :: forall (p :: k). M1 is ms s p -> M1 iw mw w p
gweaken = w p -> M1 iw mw w p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). f p -> M1 i c f p
M1 (w p -> M1 iw mw w p)
-> (M1 is ms s p -> w p) -> M1 is ms s p -> M1 iw mw w p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s p -> w p
forall (p :: k). s p -> w p
forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken (s p -> w p) -> (M1 is ms s p -> s p) -> M1 is ms s p -> w p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 is ms s p -> s p
forall k i (c :: Meta) (f :: k -> Type) (p :: k). M1 i c f p -> f p
unM1

-- | Nothing to do for empty datatypes.
instance GWeaken V1 V1 where
    gweaken :: forall (p :: k). V1 p -> V1 p
gweaken = V1 p -> V1 p
forall a. a -> a
id

-- | Nothing to do for empty constructors.
instance GWeaken U1 U1 where
    gweaken :: forall (p :: k). U1 p -> U1 p
gweaken = U1 p -> U1 p
forall a. a -> a
id

-- | Special case: if source and target types are equal, copy the value through.
instance {-# OVERLAPPING #-} GWeaken (Rec0 s) (Rec0 s) where
    gweaken :: forall (p :: k). Rec0 s p -> Rec0 s p
gweaken = Rec0 s p -> Rec0 s p
forall a. a -> a
id

-- | Weaken a field using the existing 'Weaken' instance.
instance (Weaken s, Weakened s ~ w) => GWeaken (Rec0 s) (Rec0 w) where
    gweaken :: forall (p :: k). Rec0 s p -> Rec0 w p
gweaken = w -> K1 R w p
forall k i c (p :: k). c -> K1 i c p
K1 (w -> K1 R w p) -> (Rec0 s p -> w) -> Rec0 s p -> K1 R w p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> w
s -> Weakened s
forall a. Weaken a => a -> Weakened a
weaken (s -> w) -> (Rec0 s p -> s) -> Rec0 s p -> w
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rec0 s p -> s
forall k i c (p :: k). K1 i c p -> c
unK1

-- | Weaken product types by weakening left and right.
instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :*: rs) (lw :*: rw) where
    gweaken :: forall (p :: k). (:*:) ls rs p -> (:*:) lw rw p
gweaken (ls p
l :*: rs p
r) = ls p -> lw p
forall (p :: k). ls p -> lw p
forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken ls p
l lw p -> rw p -> (:*:) lw rw p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: rs p -> rw p
forall (p :: k). rs p -> rw p
forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken rs p
r

-- | Weaken sum types by casing and weakening left or right.
instance (GWeaken ls lw, GWeaken rs rw) => GWeaken (ls :+: rs) (lw :+: rw) where
    gweaken :: forall (p :: k). (:+:) ls rs p -> (:+:) lw rw p
gweaken = \case L1 ls p
l -> lw p -> (:+:) lw rw p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> (:+:) f g p
L1 (lw p -> (:+:) lw rw p) -> lw p -> (:+:) lw rw p
forall a b. (a -> b) -> a -> b
$ ls p -> lw p
forall (p :: k). ls p -> lw p
forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken ls p
l
                    R1 rs p
r -> rw p -> (:+:) lw rw p
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
g p -> (:+:) f g p
R1 (rw p -> (:+:) lw rw p) -> rw p -> (:+:) lw rw p
forall a b. (a -> b) -> a -> b
$ rs p -> rw p
forall (p :: k). rs p -> rw p
forall {k} (s :: k -> Type) (w :: k -> Type) (p :: k).
GWeaken s w =>
s p -> w p
gweaken rs p
r