{-# LANGUAGE UndecidableInstances #-} -- for WeakenedN
{-# LANGUAGE AllowAmbiguousTypes #-} -- for weakenN

module Strongweak.Weaken
  (
    Weaken(Weakened, weaken)
  , type WeakenedN
  , WeakenN(weakenN)
  , liftWeakF
  , SWCoercibly(..)
  ) where

import Rerefined
import Data.Word
import Data.Int
import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
import Data.Vector.Generic qualified as VG
import Data.Kind ( Type )
import Data.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty qualified as NonEmpty
import Data.List.NonEmpty ( NonEmpty )
import GHC.TypeNats

import Unsafe.Coerce ( unsafeCoerce )

{- | Weaken some @a@, relaxing certain invariants.

See "Strongweak" for class design notes and laws.
-}
class Weaken a where
    -- | The weakened type for some type.
    type Weakened a :: Type

    -- | Weaken some @a@ to its associated weak type @'Weakened' a@.
    weaken :: a -> Weakened a

-- | Lift a function on a weak type to the associated strong type by weakening
--   first.
liftWeakF :: Weaken a => (Weakened a -> b) -> a -> b
liftWeakF :: forall a b. Weaken a => (Weakened a -> b) -> a -> b
liftWeakF Weakened a -> b
f = Weakened a -> b
f (Weakened a -> b) -> (a -> Weakened a) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Weakened a
forall a. Weaken a => a -> Weakened a
weaken

-- | The type of @a@ after weakening @n@ times.
type family WeakenedN (n :: Natural) a :: Type where
    WeakenedN 0 a = a
    WeakenedN n a = Weakened (WeakenedN (n-1) a)

{- | A "via type" newtype for defining strongweak instances for zero-invariant,
     coercible newtypes.

Use like so:

@
deriving 'Weaken' via 'SWCoercibly' a
@

Or standalone:

@
via 'SWCoercibly' a instance 'Weaken' ('Identity' a)
@

Note that usage of this incurs UndecidableInstances. That's life. You can
write the trivial instances this generates yourself if you so wish.
-}
newtype SWCoercibly a = SWCoercibly { forall a. SWCoercibly a -> a
unSWCoercibly :: a }
instance Weaken (SWCoercibly a) where
    type Weakened (SWCoercibly a) = a
    weaken :: SWCoercibly a -> Weakened (SWCoercibly a)
weaken = SWCoercibly a -> a
SWCoercibly a -> Weakened (SWCoercibly a)
forall a. SWCoercibly a -> a
unSWCoercibly

deriving via SWCoercibly a instance Weaken (Identity a)
deriving via SWCoercibly a instance Weaken (Const a b)

-- | Strip refined type refinement.
instance Weaken   (Refined p a) where
    type Weakened (Refined p a) = a
    weaken :: Refined p a -> Weakened (Refined p a)
weaken = Refined p a -> a
Refined p a -> Weakened (Refined p a)
forall {k} (p :: k) a. Refined p a -> a
unrefine

-- | Strip refined functor type refinement.
instance Weaken   (Refined1 p f a) where
    type Weakened (Refined1 p f a) = f a
    weaken :: Refined1 p f a -> Weakened (Refined1 p f a)
weaken = Refined1 p f a -> f a
Refined1 p f a -> Weakened (Refined1 p f a)
forall {k1} {k2} (p :: k1) (f :: k2 -> Type) (a :: k2).
Refined1 p f a -> f a
unrefine1

-- | Weaken non-empty lists into plain lists.
instance Weaken   (NonEmpty a) where
    type Weakened (NonEmpty a) = [a]
    weaken :: NonEmpty a -> Weakened (NonEmpty a)
weaken = NonEmpty a -> [a]
NonEmpty a -> Weakened (NonEmpty a)
forall a. NonEmpty a -> [a]
NonEmpty.toList

-- | Weaken sized vectors into plain lists.
instance VG.Vector v a => Weaken (VGS.Vector v n a) where
    type Weakened (VGS.Vector v n a) = [a]
    weaken :: Vector v n a -> Weakened (Vector v n a)
weaken = Vector v n a -> [a]
Vector v n a -> Weakened (Vector v n a)
forall (v :: Type -> Type) a (n :: Nat).
Vector v a =>
Vector v n a -> [a]
VGS.toList

{- TODO controversial. seems logical, but also kinda annoying.
-- | Weaken 'Maybe' (0 or 1) into '[]' (0 to n).
instance Weaken (Maybe a) where
    type Weakened (Maybe a) = [a]
    weaken = \case Just a  -> [a]
                   Nothing -> []
-}

-- Weaken the bounded Haskell numeric types using 'fromIntegral'.
instance Weaken   Word8  where
    type Weakened Word8  = Natural
    weaken :: Word8 -> Weakened Word8
weaken = Word8 -> Nat
Word8 -> Weakened Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken   Word16 where
    type Weakened Word16 = Natural
    weaken :: Word16 -> Weakened Word16
weaken = Word16 -> Nat
Word16 -> Weakened Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken   Word32 where
    type Weakened Word32 = Natural
    weaken :: Word32 -> Weakened Word32
weaken = Word32 -> Nat
Word32 -> Weakened Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken   Word64 where
    type Weakened Word64 = Natural
    weaken :: Word64 -> Weakened Word64
weaken = Word64 -> Nat
Word64 -> Weakened Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken   Int8   where
    type Weakened Int8   = Integer
    weaken :: Int8 -> Weakened Int8
weaken = Int8 -> Integer
Int8 -> Weakened Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken   Int16  where
    type Weakened Int16  = Integer
    weaken :: Int16 -> Weakened Int16
weaken = Int16 -> Integer
Int16 -> Weakened Int16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken   Int32  where
    type Weakened Int32  = Integer
    weaken :: Int32 -> Weakened Int32
weaken = Int32 -> Integer
Int32 -> Weakened Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken   Int64  where
    type Weakened Int64  = Integer
    weaken :: Int64 -> Weakened Int64
weaken = Int64 -> Integer
Int64 -> Weakened Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral

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

-- | Decomposer. Weaken every element in a list.
instance Weaken a => Weaken [a] where
    type Weakened [a] = [Weakened a]
    weaken :: [a] -> Weakened [a]
weaken = (a -> Weakened a) -> [a] -> [Weakened a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Weakened a
forall a. Weaken a => a -> Weakened a
weaken

-- | Decomposer. Weaken both elements of a tuple.
instance (Weaken a, Weaken b) => Weaken (a, b) where
    type Weakened (a, b) = (Weakened a, Weakened b)
    weaken :: (a, b) -> Weakened (a, b)
weaken (a
a, b
b) = (a -> Weakened a
forall a. Weaken a => a -> Weakened a
weaken a
a, b -> Weakened b
forall a. Weaken a => a -> Weakened a
weaken b
b)

-- | Decomposer. Weaken either side of an 'Either'.
instance (Weaken a, Weaken b) => Weaken (Either a b) where
    type Weakened (Either a b) = Either (Weakened a) (Weakened b)
    weaken :: Either a b -> Weakened (Either a b)
weaken = \case Left  a
a -> Weakened a -> Either (Weakened a) (Weakened b)
forall a b. a -> Either a b
Left  (Weakened a -> Either (Weakened a) (Weakened b))
-> Weakened a -> Either (Weakened a) (Weakened b)
forall a b. (a -> b) -> a -> b
$ a -> Weakened a
forall a. Weaken a => a -> Weakened a
weaken a
a
                   Right b
b -> Weakened b -> Either (Weakened a) (Weakened b)
forall a b. b -> Either a b
Right (Weakened b -> Either (Weakened a) (Weakened b))
-> Weakened b -> Either (Weakened a) (Weakened b)
forall a b. (a -> b) -> a -> b
$ b -> Weakened b
forall a. Weaken a => a -> Weakened a
weaken b
b

class WeakenN (n :: Natural) a where
    weakenN :: a -> WeakenedN n a

-- | Zero case: return the value as-is.
instance {-# OVERLAPPING #-} WeakenN 0 a where
    weakenN :: a -> WeakenedN 0 a
weakenN = a -> a
a -> WeakenedN 0 a
forall a. a -> a
id

-- | Inductive case. @n /= 0@, else this explodes.
instance (Weaken a, WeakenN (n-1) (Weakened a))
  => WeakenN n a where
    weakenN :: a -> WeakenedN n a
weakenN a
a =
        case forall (n :: Nat) a. WeakenN n a => a -> WeakenedN n a
weakenN @(n-1) @(Weakened a) (a -> Weakened a
forall a. Weaken a => a -> Weakened a
weaken a
a) of
          WeakenedN (n - 1) (Weakened a)
x -> forall (n :: Nat) a.
WeakenedN (n - 1) (Weakened a) -> WeakenedN n a
weakenedNRL1 @n @a WeakenedN (n - 1) (Weakened a)
x

-- | Inverted inductive 'WeakenedN'case.
--
-- @n@ must not be 0.
weakenedNRL1 :: forall n a. WeakenedN (n-1) (Weakened a) -> WeakenedN n a
weakenedNRL1 :: forall (n :: Nat) a.
WeakenedN (n - 1) (Weakened a) -> WeakenedN n a
weakenedNRL1 = WeakenedN (n - 1) (Weakened a) -> WeakenedN n a
forall a b. a -> b
unsafeCoerce