{-# LANGUAGE UndecidableInstances #-} -- for SWDepth

module Strongweak.Weaken
  (
  -- * 'Weaken' class
    Weaken(..)
  , liftWeakF

  -- * Strength switch helper
  , Strength(..)
  , type SW
  , type SWDepth
  ) where

import Refined ( Refined, unrefine, Refined1, unrefine1 )
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

{- | 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 Weak a :: Type

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

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

-- | Strength enumeration: is it strong, or weak?
--
-- Primarily interesting at the type level (using DataKinds).
data Strength = Strong | Weak

{- | Get either the strong or weak representation of a type, depending on the
     type-level "switch" provided.

This is intended to be used in data types that take a 'Strength' type. Define
your type using strong fields wrapped in @SW s@. You then get the weak
representation for free, using the same definition.

@
data A (s :: Strength) = A
  { a1 :: SW s Word8
  , a2 :: String }
@
-}
type family SW (s :: Strength) a :: Type where
    SW 'Strong a = a
    SW 'Weak   a = Weak a

-- | Track multiple levels of weakening. Silly thought I had, don't think it's
--   useful.
type family SWDepth (n :: Natural) a :: Type where
    SWDepth 0 a = a
    SWDepth n a = Weak (SWDepth (n-1) a)

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

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

-- | Weaken non-empty lists into plain lists.
instance Weaken (NonEmpty a) where
    type Weak (NonEmpty a) = [a]
    weaken :: NonEmpty a -> Weak (NonEmpty a)
weaken = NonEmpty a -> [a]
NonEmpty a -> Weak (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 Weak (VGS.Vector v n a) = [a]
    weaken :: Vector v n a -> Weak (Vector v n a)
weaken = Vector v n a -> [a]
Vector v n a -> Weak (Vector v n a)
forall (v :: Type -> Type) a (n :: Nat).
Vector v a =>
Vector v n a -> [a]
VGS.toList

-- | Strip wrapper.
instance Weaken (Identity a) where
    type Weak (Identity a) = a
    weaken :: Identity a -> Weak (Identity a)
weaken = Identity a -> a
Identity a -> Weak (Identity a)
forall a. Identity a -> a
runIdentity

-- | Strip wrapper.
instance Weaken (Const a b) where
    type Weak (Const a b) = a
    weaken :: Const a b -> Weak (Const a b)
weaken = Const a b -> a
Const a b -> Weak (Const a b)
forall {k} a (b :: k). Const a b -> a
getConst

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

-- Weaken the bounded Haskell numeric types using 'fromIntegral'.
instance Weaken Word8  where
    type Weak Word8  = Natural
    weaken :: Word8 -> Weak Word8
weaken = Word8 -> Nat
Word8 -> Weak Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word16 where
    type Weak Word16 = Natural
    weaken :: Word16 -> Weak Word16
weaken = Word16 -> Nat
Word16 -> Weak Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word32 where
    type Weak Word32 = Natural
    weaken :: Word32 -> Weak Word32
weaken = Word32 -> Nat
Word32 -> Weak Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Word64 where
    type Weak Word64 = Natural
    weaken :: Word64 -> Weak Word64
weaken = Word64 -> Nat
Word64 -> Weak Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int8   where
    type Weak Int8   = Integer
    weaken :: Int8 -> Weak Int8
weaken = Int8 -> Integer
Int8 -> Weak Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int16  where
    type Weak Int16  = Integer
    weaken :: Int16 -> Weak Int16
weaken = Int16 -> Integer
Int16 -> Weak Int16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int32  where
    type Weak Int32  = Integer
    weaken :: Int32 -> Weak Int32
weaken = Int32 -> Integer
Int32 -> Weak Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance Weaken Int64  where
    type Weak Int64  = Integer
    weaken :: Int64 -> Weak Int64
weaken = Int64 -> Integer
Int64 -> Weak 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 Weak [a] = [Weak a]
    weaken :: [a] -> Weak [a]
weaken = (a -> Weak a) -> [a] -> [Weak a]
forall a b. (a -> b) -> [a] -> [b]
map a -> Weak a
forall a. Weaken a => a -> Weak a
weaken

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

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