module Strongweak.Strengthen.Unsafe where

import Strongweak.Weaken ( Weaken(Weakened) )
import Data.Word
import Data.Int
import Rerefined.Refine
import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
import Data.Vector.Generic qualified as VG
import Data.Vector.Generic.Sized.Internal qualified
import Data.List.NonEmpty qualified as NonEmpty
import Data.List.NonEmpty ( NonEmpty )

import Strongweak.Weaken ( SWCoercibly(..) )
import Data.Functor.Identity
import Data.Functor.Const

{- | Unsafely transform a @'Weakened' a@ to an @a@, without asserting invariants.

Naturally, you must only even /consider/ using this if you have a guarantee that
your value is safe to treat as strong.

For example, you may unsafely strengthen some @'Numeric.Natural.Natural' n@ into
a 'Word8' by unsafely coercing the value, ignoring the possibility that @n >=
255@.

What happens if it turns out you're lying to the computer and your weak value
doesn't fit in its strong counterpart? That depends on the strengthen.

  * Numeric coercions should safely overflow.
  * Some will raise an error (e.g. 'NonEmpty').
  * Others will appear to work, but later explode your computer.

See "Strongweak" for class design notes and laws.
-}
class Weaken a => UnsafeStrengthen a where
    -- | Unsafely transform a @'Weakened' a@ to its associated strong type @a@.
    unsafeStrengthen :: Weakened a -> a

instance UnsafeStrengthen (SWCoercibly a) where
    unsafeStrengthen :: Weakened (SWCoercibly a) -> SWCoercibly a
unsafeStrengthen = a -> SWCoercibly a
Weakened (SWCoercibly a) -> SWCoercibly a
forall a. a -> SWCoercibly a
SWCoercibly

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

-- | Add a refinement to a type without checking the associated predicate.
instance UnsafeStrengthen (Refined p a) where
    unsafeStrengthen :: Weakened (Refined p a) -> Refined p a
unsafeStrengthen = a -> Refined p a
Weakened (Refined p a) -> Refined p a
forall {k} a (p :: k). a -> Refined p a
unsafeRefine

-- | Assume a plain list is non-empty.
instance UnsafeStrengthen (NonEmpty a) where
    unsafeStrengthen :: Weakened (NonEmpty a) -> NonEmpty a
unsafeStrengthen = [a] -> NonEmpty a
Weakened (NonEmpty a) -> NonEmpty a
forall a. HasCallStack => [a] -> NonEmpty a
NonEmpty.fromList

-- | Assume the size of a plain list.
instance VG.Vector v a => UnsafeStrengthen (VGS.Vector v n a) where
    unsafeStrengthen :: Weakened (Vector v n a) -> Vector v n a
unsafeStrengthen =
        v a -> Vector v n a
forall (v :: Type -> Type) (n :: Nat) a. v a -> Vector v n a
Data.Vector.Generic.Sized.Internal.Vector (v a -> Vector v n a) -> ([a] -> v a) -> [a] -> Vector v n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> v a
forall (v :: Type -> Type) a. Vector v a => [a] -> v a
VG.fromList

{- TODO controversial. seems logical, but also kinda annoying.
-- | Unsafely grab either 0 or 1 elements from a list.
instance UnsafeStrengthen (Maybe a) where
    unsafeStrengthen = \case [a] -> Just a
                             []  -> Nothing
                             _   -> error "your list wasn't [] or [a]"
-}

-- Coerce 'Natural's into Haskell's bounded unsigned numeric types. Poorly-sized
-- values will safely overflow according to the type's behaviour.
instance UnsafeStrengthen Word8  where unsafeStrengthen :: Weakened Word8 -> Word8
unsafeStrengthen = Nat -> Word8
Weakened Word8 -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word16 where unsafeStrengthen :: Weakened Word16 -> Word16
unsafeStrengthen = Nat -> Word16
Weakened Word16 -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word32 where unsafeStrengthen :: Weakened Word32 -> Word32
unsafeStrengthen = Nat -> Word32
Weakened Word32 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word64 where unsafeStrengthen :: Weakened Word64 -> Word64
unsafeStrengthen = Nat -> Word64
Weakened Word64 -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral

-- Coerce 'Integer's into Haskell's bounded signed numeric types. Poorly-sized
-- values will safely overflow according to the type's behaviour.
instance UnsafeStrengthen Int8   where unsafeStrengthen :: Weakened Int8 -> Int8
unsafeStrengthen = Integer -> Int8
Weakened Int8 -> Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int16  where unsafeStrengthen :: Weakened Int16 -> Int16
unsafeStrengthen = Integer -> Int16
Weakened Int16 -> Int16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int32  where unsafeStrengthen :: Weakened Int32 -> Int32
unsafeStrengthen = Integer -> Int32
Weakened Int32 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int64  where unsafeStrengthen :: Weakened Int64 -> Int64
unsafeStrengthen = Integer -> Int64
Weakened Int64 -> Int64
forall a b. (Integral a, Num b) => a -> b
fromIntegral

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

-- | Decomposer. Unsafely strengthen every element in a list.
instance UnsafeStrengthen a => UnsafeStrengthen [a] where
    unsafeStrengthen :: Weakened [a] -> [a]
unsafeStrengthen = (Weakened a -> a) -> [Weakened a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Weakened a -> a
forall a. UnsafeStrengthen a => Weakened a -> a
unsafeStrengthen

-- | Decomposer. Unsafely strengthen both elements of a tuple.
instance (UnsafeStrengthen a, UnsafeStrengthen b)
  => UnsafeStrengthen (a, b) where
    unsafeStrengthen :: Weakened (a, b) -> (a, b)
unsafeStrengthen (Weakened a
a, Weakened b
b) = (Weakened a -> a
forall a. UnsafeStrengthen a => Weakened a -> a
unsafeStrengthen Weakened a
a, Weakened b -> b
forall a. UnsafeStrengthen a => Weakened a -> a
unsafeStrengthen Weakened b
b)

-- | Decomposer. Unsafely strengthen either side of an 'Either'.
instance (UnsafeStrengthen a, UnsafeStrengthen b)
  => UnsafeStrengthen (Either a b) where
    unsafeStrengthen :: Weakened (Either a b) -> Either a b
unsafeStrengthen = \case Left  Weakened a
a -> a -> Either a b
forall a b. a -> Either a b
Left  (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ Weakened a -> a
forall a. UnsafeStrengthen a => Weakened a -> a
unsafeStrengthen Weakened a
a
                             Right Weakened b
b -> b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ Weakened b -> b
forall a. UnsafeStrengthen a => Weakened a -> a
unsafeStrengthen Weakened b
b