{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}

-- This Source Code Form is subject to the terms of the Mozilla Public
-- License, v. 2.0. If a copy of the MPL was not distributed with this
-- file, You can obtain one at https://mozilla.org/MPL/2.0/.

{- |
Copyright   :  (c) 2024 Yamada Ryo
License     :  MPL-2.0 (see the file LICENSE)
Maintainer  :  ymdfield@outlook.jp
Stability   :  experimental
Portability :  portable
-}
module Data.Hefty.Union.Weaken where

import Control.Effect (type (~>))
import Data.Hefty.Union (Union (inject0, weaken, (|+:)))
import Data.Type.Equality (type (==))
import GHC.TypeNats (Natural, type (-))

class
    (isMZero ~ (m == 0), isNZero ~ (n == 0)) =>
    WeakenUnder_ (isMZero :: Bool) (m :: Natural) (isNZero :: Bool) (n :: Natural) es es'
        | m n es' -> es
    where
    weakenNUnderM_ :: Union u => u es f ~> u es' f

type WeakenUnder n m = WeakenUnder_ (m == 0) m (n == 0) n
type Weaken n = WeakenUnder_ 'True 0 (n == 0) n

weakenNUnderM :: forall n m u es' f es. (Union u, WeakenUnder n m es es') => u es f ~> u es' f
weakenNUnderM :: forall (n :: Natural) (m :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
(Union u, WeakenUnder n m es es') =>
u es f ~> u es' f
weakenNUnderM = forall (isMZero :: Bool) (m :: Natural) (isNZero :: Bool)
       (n :: Natural) (es :: [SigClass]) (es' :: [SigClass])
       (u :: [SigClass] -> SigClass) (f :: * -> *).
(WeakenUnder_ isMZero m isNZero n es es', Union u) =>
u es f ~> u es' f
weakenNUnderM_ @(m == 0) @m @(n == 0) @n
{-# INLINE weakenNUnderM #-}

weakenN :: forall n u es' f es. (Union u, Weaken n es es') => u es f ~> u es' f
weakenN :: forall (n :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
(Union u, Weaken n es es') =>
u es f ~> u es' f
weakenN = forall (isMZero :: Bool) (m :: Natural) (isNZero :: Bool)
       (n :: Natural) (es :: [SigClass]) (es' :: [SigClass])
       (u :: [SigClass] -> SigClass) (f :: * -> *).
(WeakenUnder_ isMZero m isNZero n es es', Union u) =>
u es f ~> u es' f
weakenNUnderM_ @( 'True) @0 @(n == 0) @n
{-# INLINE weakenN #-}

instance
    (WeakenUnder n (m - 1) es es', (m == 0) ~ 'False, isNZero ~ (n == 0)) =>
    WeakenUnder_ 'False m isNZero n (e ': es) (e ': es')
    where
    weakenNUnderM_ :: forall (u :: [SigClass] -> SigClass) (f :: * -> *).
Union u =>
u (e : es) f ~> u (e : es') f
weakenNUnderM_ = forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       (es :: [SigClass]).
Union u =>
e f ~> u (e : es) f
inject0 forall (u :: [SigClass] -> SigClass) (e :: SigClass) (f :: * -> *)
       a r (es :: [SigClass]).
Union u =>
(e f a -> r) -> (u es f a -> r) -> u (e : es) f a -> r
|+: forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Natural) (m :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
(Union u, WeakenUnder n m es es') =>
u es f ~> u es' f
weakenNUnderM @n @(m - 1)
    {-# INLINE weakenNUnderM_ #-}

instance
    (Weaken (n - 1) es es', (n == 0) ~ 'False) =>
    WeakenUnder_ 'True 0 'False n es (e ': es')
    where
    weakenNUnderM_ :: forall (u :: [SigClass] -> SigClass) (f :: * -> *).
Union u =>
u es f ~> u (e : es') f
weakenNUnderM_ = forall (u :: [SigClass] -> SigClass) (es :: [SigClass])
       (f :: * -> *) (e :: SigClass).
Union u =>
u es f ~> u (e : es) f
weaken forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Natural) (u :: [SigClass] -> SigClass)
       (es' :: [SigClass]) (f :: * -> *) (es :: [SigClass]).
(Union u, Weaken n es es') =>
u es f ~> u es' f
weakenN @(n - 1)
    {-# INLINE weakenNUnderM_ #-}

instance WeakenUnder_ 'True 0 'True 0 es es where
    weakenNUnderM_ :: forall (u :: [SigClass] -> SigClass) (f :: * -> *).
Union u =>
u es f ~> u es f
weakenNUnderM_ = forall a. a -> a
id
    {-# INLINE weakenNUnderM_ #-}