module Strongweak.Strengthen.Unsafe where

import Strongweak.Weaken
import Data.Word
import Data.Int
import Refined ( Refined )
import Refined.Unsafe ( reallyUnsafeRefine )
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.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty qualified as NonEmpty
import Data.List.NonEmpty ( NonEmpty )

{- | Unsafely transform a @'Weak' 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 @'Weak' a@ to its associated strong type @a@.
    unsafeStrengthen :: Weak a -> a

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

-- | Assume a plain list is non-empty.
instance UnsafeStrengthen (NonEmpty a) where
    unsafeStrengthen :: Weak (NonEmpty a) -> NonEmpty a
unsafeStrengthen = [a] -> NonEmpty a
Weak (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 :: Weak (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

-- | Add wrapper.
instance UnsafeStrengthen (Identity a) where
    unsafeStrengthen :: Weak (Identity a) -> Identity a
unsafeStrengthen = a -> Identity a
Weak (Identity a) -> Identity a
forall a. a -> Identity a
Identity

-- | Add wrapper.
instance UnsafeStrengthen (Const a b) where
    unsafeStrengthen :: Weak (Const a b) -> Const a b
unsafeStrengthen = a -> Const a b
Weak (Const a b) -> Const a b
forall {k} a (b :: k). a -> Const a b
Const

{- 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 :: Weak Word8 -> Word8
unsafeStrengthen = Nat -> Word8
Weak Word8 -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word16 where unsafeStrengthen :: Weak Word16 -> Word16
unsafeStrengthen = Nat -> Word16
Weak Word16 -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word32 where unsafeStrengthen :: Weak Word32 -> Word32
unsafeStrengthen = Nat -> Word32
Weak Word32 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word64 where unsafeStrengthen :: Weak Word64 -> Word64
unsafeStrengthen = Nat -> Word64
Weak 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 :: Weak Int8 -> Int8
unsafeStrengthen = Integer -> Int8
Weak Int8 -> Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int16  where unsafeStrengthen :: Weak Int16 -> Int16
unsafeStrengthen = Integer -> Int16
Weak Int16 -> Int16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int32  where unsafeStrengthen :: Weak Int32 -> Int32
unsafeStrengthen = Integer -> Int32
Weak Int32 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int64  where unsafeStrengthen :: Weak Int64 -> Int64
unsafeStrengthen = Integer -> Int64
Weak 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 :: Weak [a] -> [a]
unsafeStrengthen = (Weak a -> a) -> [Weak a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Weak a -> a
forall a. UnsafeStrengthen a => Weak a -> a
unsafeStrengthen

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

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