module Strongweak.Chain ( SWChain(..), strengthenN ) where

import Strongweak.Weaken ( Weaken(..), WeakenN(weakenN), type WeakenedN )
import Strongweak.Strengthen ( Strengthen(..), StrengthenN(strengthenN) )
import GHC.TypeNats ( type Natural )

{- | When weakening (or strengthening), chain the operation @n@ times.

You may achieve this without extra newtypes by nesting uses of
'Strongweak.Strength.SW'. However, strongweak generics can't handle this,
forcing you to write manual instances.

'SWChain' provides this nesting behaviour in a type. In return for adding a
boring newtype layer to the strong representation, you can chain weakening and
strengthenings without having to write them manually.

The type works as follows:

@
'Weakened' ('SWChain' 0 a) = a
'Weakened' ('SWChain' 1 a) = 'Weakened' a
'Weakened' ('SWChain' 2 a) = 'Weakened' ('Weakened' a)
'Weakened' ('SWChain' n a) = 'WeakenedN' n a
@

And so on. (This type is only much use from @n = 2@ onwards.)

You may also use this as a "via" type:

@
newtype A (s :: 'Strength') = A { a1 :: 'SW' s (Identity ('SW' s Word8)) }
deriving via 'SWChain' 2 (Identity Word8) instance     'Weaken' (A 'Strong')
deriving via 'SWChain' 2 (Identity Word8) instance 'Strengthen' (A 'Strong')
@
-}
newtype SWChain (n :: Natural) a = SWChain { forall (n :: Natural) a. SWChain n a -> a
unSWChain :: a }
    deriving stock Int -> SWChain n a -> ShowS
[SWChain n a] -> ShowS
SWChain n a -> String
(Int -> SWChain n a -> ShowS)
-> (SWChain n a -> String)
-> ([SWChain n a] -> ShowS)
-> Show (SWChain n a)
forall (n :: Natural) a. Show a => Int -> SWChain n a -> ShowS
forall (n :: Natural) a. Show a => [SWChain n a] -> ShowS
forall (n :: Natural) a. Show a => SWChain n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: Natural) a. Show a => Int -> SWChain n a -> ShowS
showsPrec :: Int -> SWChain n a -> ShowS
$cshow :: forall (n :: Natural) a. Show a => SWChain n a -> String
show :: SWChain n a -> String
$cshowList :: forall (n :: Natural) a. Show a => [SWChain n a] -> ShowS
showList :: [SWChain n a] -> ShowS
Show
    deriving (Eq (SWChain n a)
Eq (SWChain n a) =>
(SWChain n a -> SWChain n a -> Ordering)
-> (SWChain n a -> SWChain n a -> Bool)
-> (SWChain n a -> SWChain n a -> Bool)
-> (SWChain n a -> SWChain n a -> Bool)
-> (SWChain n a -> SWChain n a -> Bool)
-> (SWChain n a -> SWChain n a -> SWChain n a)
-> (SWChain n a -> SWChain n a -> SWChain n a)
-> Ord (SWChain n a)
SWChain n a -> SWChain n a -> Bool
SWChain n a -> SWChain n a -> Ordering
SWChain n a -> SWChain n a -> SWChain n a
forall (n :: Natural) a. Ord a => Eq (SWChain n a)
forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> Bool
forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> Ordering
forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> SWChain n a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> Ordering
compare :: SWChain n a -> SWChain n a -> Ordering
$c< :: forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> Bool
< :: SWChain n a -> SWChain n a -> Bool
$c<= :: forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> Bool
<= :: SWChain n a -> SWChain n a -> Bool
$c> :: forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> Bool
> :: SWChain n a -> SWChain n a -> Bool
$c>= :: forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> Bool
>= :: SWChain n a -> SWChain n a -> Bool
$cmax :: forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> SWChain n a
max :: SWChain n a -> SWChain n a -> SWChain n a
$cmin :: forall (n :: Natural) a.
Ord a =>
SWChain n a -> SWChain n a -> SWChain n a
min :: SWChain n a -> SWChain n a -> SWChain n a
Ord, SWChain n a -> SWChain n a -> Bool
(SWChain n a -> SWChain n a -> Bool)
-> (SWChain n a -> SWChain n a -> Bool) -> Eq (SWChain n a)
forall (n :: Natural) a. Eq a => SWChain n a -> SWChain n a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Natural) a. Eq a => SWChain n a -> SWChain n a -> Bool
== :: SWChain n a -> SWChain n a -> Bool
$c/= :: forall (n :: Natural) a. Eq a => SWChain n a -> SWChain n a -> Bool
/= :: SWChain n a -> SWChain n a -> Bool
Eq) via a

instance WeakenN n a => Weaken (SWChain n a) where
    type Weakened (SWChain n a) = WeakenedN n a
    weaken :: SWChain n a -> Weakened (SWChain n a)
weaken = forall (n :: Natural) a. WeakenN n a => a -> WeakenedN n a
weakenN @n (a -> WeakenedN n a)
-> (SWChain n a -> a) -> SWChain n a -> WeakenedN n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SWChain n a -> a
forall (n :: Natural) a. SWChain n a -> a
unSWChain

instance StrengthenN n a => Strengthen (SWChain n a) where
    strengthen :: Weakened (SWChain n a) -> Either StrengthenFailure' (SWChain n a)
strengthen = (a -> SWChain n a)
-> Either StrengthenFailure' a
-> Either StrengthenFailure' (SWChain n a)
forall a b.
(a -> b)
-> Either StrengthenFailure' a -> Either StrengthenFailure' b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> SWChain n a
forall (n :: Natural) a. a -> SWChain n a
SWChain (Either StrengthenFailure' a
 -> Either StrengthenFailure' (SWChain n a))
-> (WeakenedN n a -> Either StrengthenFailure' a)
-> WeakenedN n a
-> Either StrengthenFailure' (SWChain n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Natural) a.
StrengthenN n a =>
WeakenedN n a -> Either StrengthenFailure' a
strengthenN @n