module Strongweak.Strengthen.Unsafe where

import Strongweak.Weaken
import Data.Word
import Data.Int
import Refined ( Refined )
import Refined.Unsafe ( reallyUnsafeRefine )
import Data.Vector.Sized ( Vector )
import Data.Vector.Generic.Sized.Internal qualified
import Data.Vector 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.

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 (sized vectors
    will probably do this).

Only consider using this if you have a guarantee that your value is safe to
treat as strong.

Instances should /either/ handle an invariant, or decompose. See "Strongweak"
for a discussion on this design.
-}
class Weaken a => UnsafeStrengthen a where
    -- | Unsafely transform a weak value to its associated strong one.
    unsafeStrengthen :: Weak a -> a

-- | Unsafely assume a list is non-empty.
instance UnsafeStrengthen (NonEmpty a) where
    unsafeStrengthen :: Weak (NonEmpty a) -> NonEmpty a
unsafeStrengthen = Weak (NonEmpty a) -> NonEmpty a
forall a. [a] -> NonEmpty a
NonEmpty.fromList

-- | Unsafely assume the size of a plain list.
instance UnsafeStrengthen (Vector n a) where
    unsafeStrengthen :: Weak (Vector n a) -> Vector n a
unsafeStrengthen = Vector a -> Vector n a
forall (v :: * -> *) (n :: Nat) a. v a -> Vector v n a
Data.Vector.Generic.Sized.Internal.Vector (Vector a -> Vector n a) -> ([a] -> Vector a) -> [a] -> Vector n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Vector a
forall a. [a] -> Vector a
Data.Vector.fromList

-- | Wrap a value to a refined one without checking the predicate.
instance UnsafeStrengthen (Refined p a) where
    unsafeStrengthen :: Weak (Refined p a) -> Refined p a
unsafeStrengthen = Weak (Refined p a) -> Refined p a
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine

-- 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 = Weak Word8 -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word16 where unsafeStrengthen :: Weak Word16 -> Word16
unsafeStrengthen = Weak Word16 -> Word16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word32 where unsafeStrengthen :: Weak Word32 -> Word32
unsafeStrengthen = Weak Word32 -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Word64 where unsafeStrengthen :: Weak Word64 -> Word64
unsafeStrengthen = 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 = Weak Int8 -> Int8
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int16  where unsafeStrengthen :: Weak Int16 -> Int16
unsafeStrengthen = Weak Int16 -> Int16
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int32  where unsafeStrengthen :: Weak Int32 -> Int32
unsafeStrengthen = Weak Int32 -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral
instance UnsafeStrengthen Int64  where unsafeStrengthen :: Weak Int64 -> Int64
unsafeStrengthen = 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.
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.
instance UnsafeStrengthen a => UnsafeStrengthen (Maybe a) where
    unsafeStrengthen :: Weak (Maybe a) -> Maybe a
unsafeStrengthen = \case Just Weak a
a  -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Weak a -> a
forall a. UnsafeStrengthen a => Weak a -> a
unsafeStrengthen Weak a
a
                             Maybe (Weak a)
Weak (Maybe a)
Nothing -> Maybe a
forall a. Maybe a
Nothing

-- | Decomposer.
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

-- | Decomposer.
instance UnsafeStrengthen a => UnsafeStrengthen (Identity a) where
    unsafeStrengthen :: Weak (Identity a) -> Identity a
unsafeStrengthen = a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a)
-> (Identity (Weak a) -> a) -> Identity (Weak a) -> Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Weak a -> a
forall a. UnsafeStrengthen a => Weak a -> a
unsafeStrengthen (Weak a -> a)
-> (Identity (Weak a) -> Weak a) -> Identity (Weak a) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity (Weak a) -> Weak a
forall a. Identity a -> a
runIdentity

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