{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE CPP #-}

module Strongweak.Strengthen
  (
  -- * 'Strengthen' class
    Strengthen(..)

  -- * Strengthen failures
  , StrengthenFail(..)
  , strengthenFailPretty
  , strengthenFailBase

  -- * Restrengthening
  , restrengthen

  -- * Helpers
  , strengthenBounded

  -- * Re-exports
  , Strongweak.Weaken.Weak
  ) where

import Strongweak.Weaken ( Weaken(..) )
import Data.Either.Validation
import Type.Reflection ( Typeable, typeRep )
import Prettyprinter
import Prettyprinter.Render.String

import GHC.TypeNats ( Natural, KnownNat )
import Data.Word
import Data.Int
import Refined ( Refined, refine, Predicate )
import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
import Data.Vector.Generic qualified as VG
import Data.Foldable qualified as Foldable
import Control.Applicative ( liftA2 )
import Data.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty ( NonEmpty( (:|) ) )
import Data.List.NonEmpty qualified as NonEmpty

{- | You may attempt to transform a @'Weak' a@ to an @a@.

Laws:

  * @a === b -> 'strengthen' a === 'strengthen' b@
  * @'strengthen' ('weaken' a) === 'Success' a@

We take 'Weaken' as a superclass in order to maintain strong/weak type pair
consistency. We choose this dependency direction because we treat the strong
type as the "canonical" one, so 'Weaken' is the more natural (and
straightforward) class to define.

Instances should /either/ handle an invariant, or decompose. See "Strongweak"
for a discussion on this design.
-}
class Weaken a => Strengthen a where
    -- | Attempt to transform a weak value to its associated strong one.
    strengthen :: Weak a -> Validation (NonEmpty StrengthenFail) a

-- | Weaken a strong value, then strengthen it again.
--
-- Potentially useful if you have previously used
-- 'Strongweak.Strengthen.Unsafe.unsafeStrengthen' and now wish to check the
-- invariants. For example:
--
-- >>> restrengthen $ unsafeStrengthen @(Vector 2 Natural) [0]
-- Failure ...
restrengthen
    :: (Strengthen a, Weaken a)
    => a -> Validation (NonEmpty StrengthenFail) a
restrengthen :: forall a.
(Strengthen a, Weaken a) =>
a -> Validation (NonEmpty StrengthenFail) a
restrengthen = forall a.
Strengthen a =>
Weak a -> Validation (NonEmpty StrengthenFail) a
strengthen forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Weaken a => a -> Weak a
weaken

-- | Strengthen failure data type. Don't use these constructors directly, use
--   the existing helper functions.
--
-- Field indices are from 0 in the respective constructor. Field names are
-- provided if present.
data StrengthenFail
  = StrengthenFailBase
        String -- ^ weak   type
        String -- ^ strong type
        String -- ^ weak value
        String -- ^ msg

  | StrengthenFailField
        String                      -- ^ weak   datatype name
        String                      -- ^ strong datatype name
        String                      -- ^ weak   constructor name
        String                      -- ^ strong constructor name
        Natural                     -- ^ weak   field index
        (Maybe String)              -- ^ weak   field name (if present)
        Natural                     -- ^ strong field index
        (Maybe String)              -- ^ strong field name (if present)
        (NonEmpty StrengthenFail)   -- ^ failures
    deriving stock StrengthenFail -> StrengthenFail -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StrengthenFail -> StrengthenFail -> Bool
$c/= :: StrengthenFail -> StrengthenFail -> Bool
== :: StrengthenFail -> StrengthenFail -> Bool
$c== :: StrengthenFail -> StrengthenFail -> Bool
Eq

instance Show StrengthenFail where
    showsPrec :: Int -> StrengthenFail -> ShowS
showsPrec Int
_ = forall ann. SimpleDocStream ann -> ShowS
renderShowS forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty LayoutOptions
defaultLayoutOptions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a ann. Pretty a => a -> Doc ann
pretty

-- TODO shorten value if over e.g. 50 chars. e.g. @[0,1,2,...,255] -> FAIL@
instance Pretty StrengthenFail where
    pretty :: forall ann. StrengthenFail -> Doc ann
pretty = \case
      StrengthenFailBase String
wt String
st String
wv String
msg ->
        forall ann. [Doc ann] -> Doc ann
vsep [ forall a ann. Pretty a => a -> Doc ann
pretty String
wtforall ann. Doc ann -> Doc ann -> Doc ann
<+>Doc ann
"->"forall ann. Doc ann -> Doc ann -> Doc ann
<+>forall a ann. Pretty a => a -> Doc ann
pretty String
st
             , forall a ann. Pretty a => a -> Doc ann
pretty String
wvforall ann. Doc ann -> Doc ann -> Doc ann
<+>Doc ann
"->"forall ann. Doc ann -> Doc ann -> Doc ann
<+>Doc ann
"FAIL"
             , forall a ann. Pretty a => a -> Doc ann
pretty String
msg ]
      StrengthenFailField String
dw String
_ds String
cw String
_cs Natural
iw Maybe String
fw Natural
_is Maybe String
_fs NonEmpty StrengthenFail
es ->
        let sw :: String
sw = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. Show a => a -> String
show Natural
iw) forall a. a -> a
id Maybe String
fw
        in  forall ann. Int -> Doc ann -> Doc ann
nest Int
0 forall a b. (a -> b) -> a -> b
$ forall a ann. Pretty a => a -> Doc ann
pretty String
dwforall a. Semigroup a => a -> a -> a
<>Doc ann
"."forall a. Semigroup a => a -> a -> a
<>forall a ann. Pretty a => a -> Doc ann
pretty String
cwforall a. Semigroup a => a -> a -> a
<>Doc ann
"."forall a. Semigroup a => a -> a -> a
<>forall a ann. Pretty a => a -> Doc ann
pretty String
swforall a. Semigroup a => a -> a -> a
<>forall ann. Doc ann
lineforall a. Semigroup a => a -> a -> a
<>forall a. NonEmpty StrengthenFail -> Doc a
strengthenFailPretty NonEmpty StrengthenFail
es

-- mutually recursive with its 'Pretty' instance. safe, but a bit confusing -
-- clean up
strengthenFailPretty :: NonEmpty StrengthenFail -> Doc a
strengthenFailPretty :: forall a. NonEmpty StrengthenFail -> Doc a
strengthenFailPretty = forall ann. [Doc ann] -> Doc ann
vsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {a} {ann}. Pretty a => a -> Doc ann
go forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList
  where go :: a -> Doc ann
go a
e = Doc ann
"-"forall ann. Doc ann -> Doc ann -> Doc ann
<+>forall ann. Int -> Doc ann -> Doc ann
indent Int
0 (forall a ann. Pretty a => a -> Doc ann
pretty a
e)

strengthenFailBase
    :: forall s w. (Typeable w, Show w, Typeable s)
    => w -> String -> Validation (NonEmpty StrengthenFail) s
strengthenFailBase :: forall s w.
(Typeable w, Show w, Typeable s) =>
w -> String -> Validation (NonEmpty StrengthenFail) s
strengthenFailBase w
w String
msg = forall e a. e -> Validation e a
Failure (StrengthenFail
e forall a. a -> [a] -> NonEmpty a
:| [])
  where e :: StrengthenFail
e = String -> String -> String -> String -> StrengthenFail
StrengthenFailBase (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). Typeable a => TypeRep a
typeRep @w) (forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). Typeable a => TypeRep a
typeRep @s) (forall a. Show a => a -> String
show w
w) String
msg

-- | Assert a predicate to refine a type.
instance (Predicate (p :: k) a, Typeable k, Typeable a, Show a) => Strengthen (Refined p a) where
    strengthen :: Weak (Refined p a)
-> Validation (NonEmpty StrengthenFail) (Refined p a)
strengthen Weak (Refined p a)
a =
        case forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine Weak (Refined p a)
a of
          Left  RefineException
err -> forall s w.
(Typeable w, Show w, Typeable s) =>
w -> String -> Validation (NonEmpty StrengthenFail) s
strengthenFailBase Weak (Refined p a)
a (forall a. Show a => a -> String
show RefineException
err)
          Right Refined p a
ra  -> forall e a. a -> Validation e a
Success Refined p a
ra

-- | Strengthen a plain list into a non-empty list by asserting non-emptiness.
instance (Typeable a, Show a) => Strengthen (NonEmpty a) where
    strengthen :: Weak (NonEmpty a)
-> Validation (NonEmpty StrengthenFail) (NonEmpty a)
strengthen Weak (NonEmpty a)
a =
        case forall a. [a] -> Maybe (NonEmpty a)
NonEmpty.nonEmpty Weak (NonEmpty a)
a of
          Just NonEmpty a
a' -> forall e a. a -> Validation e a
Success NonEmpty a
a'
          Maybe (NonEmpty a)
Nothing -> forall s w.
(Typeable w, Show w, Typeable s) =>
w -> String -> Validation (NonEmpty StrengthenFail) s
strengthenFailBase Weak (NonEmpty a)
a String
"empty list"

-- | Strengthen a plain list into a sized vector by asserting length.
instance (VG.Vector v a, KnownNat n, Typeable v, Typeable a, Show a)
  => Strengthen (VGS.Vector v n a) where
    strengthen :: Weak (Vector v n a)
-> Validation (NonEmpty StrengthenFail) (Vector v n a)
strengthen Weak (Vector v n a)
w =
        case forall (v :: Type -> Type) a (n :: Natural).
(Vector v a, KnownNat n) =>
[a] -> Maybe (Vector v n a)
VGS.fromList Weak (Vector v n a)
w of
          Maybe (Vector v n a)
Nothing -> forall s w.
(Typeable w, Show w, Typeable s) =>
w -> String -> Validation (NonEmpty StrengthenFail) s
strengthenFailBase Weak (Vector v n a)
w String
"TODO bad size vector"
          Just Vector v n a
s  -> forall e a. a -> Validation e a
Success Vector v n a
s

-- | Add wrapper.
instance Strengthen (Identity a) where
    strengthen :: Weak (Identity a)
-> Validation (NonEmpty StrengthenFail) (Identity a)
strengthen = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. a -> Identity a
Identity

-- | Add wrapper.
instance Strengthen (Const a b) where
    strengthen :: Weak (Const a b)
-> Validation (NonEmpty StrengthenFail) (Const a b)
strengthen = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {k} a (b :: k). a -> Const a b
Const

{- TODO controversial. seems logical, but also kinda annoying.
instance (Show a, Typeable a) => Strengthen (Maybe a) where
    strengthen = \case [a] -> pure $ Just a
                       []  -> pure Nothing
                       x   -> strengthenFailBase x "list wasn't [a] or []"
-}

-- Strengthen 'Natural's into Haskell's bounded unsigned numeric types.
instance Strengthen Word8  where strengthen :: Weak Word8 -> Validation (NonEmpty StrengthenFail) Word8
strengthen = forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded
instance Strengthen Word16 where strengthen :: Weak Word16 -> Validation (NonEmpty StrengthenFail) Word16
strengthen = forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded
instance Strengthen Word32 where strengthen :: Weak Word32 -> Validation (NonEmpty StrengthenFail) Word32
strengthen = forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded
instance Strengthen Word64 where strengthen :: Weak Word64 -> Validation (NonEmpty StrengthenFail) Word64
strengthen = forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded

-- Strengthen 'Integer's into Haskell's bounded signed numeric types.
instance Strengthen Int8   where strengthen :: Weak Int8 -> Validation (NonEmpty StrengthenFail) Int8
strengthen = forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded
instance Strengthen Int16  where strengthen :: Weak Int16 -> Validation (NonEmpty StrengthenFail) Int16
strengthen = forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded
instance Strengthen Int32  where strengthen :: Weak Int32 -> Validation (NonEmpty StrengthenFail) Int32
strengthen = forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded
instance Strengthen Int64  where strengthen :: Weak Int64 -> Validation (NonEmpty StrengthenFail) Int64
strengthen = forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded

strengthenBounded
    :: forall b n
    .  (Integral b, Bounded b, Show b, Typeable b, Integral n, Show n, Typeable n)
    => n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded :: forall b n.
(Integral b, Bounded b, Show b, Typeable b, Integral n, Show n,
 Typeable n) =>
n -> Validation (NonEmpty StrengthenFail) b
strengthenBounded n
n =
    if   n
n forall a. Ord a => a -> a -> Bool
<= n
maxB Bool -> Bool -> Bool
&& n
n forall a. Ord a => a -> a -> Bool
>= n
minB then forall e a. a -> Validation e a
Success (forall a b. (Integral a, Num b) => a -> b
fromIntegral n
n)
    else forall s w.
(Typeable w, Show w, Typeable s) =>
w -> String -> Validation (NonEmpty StrengthenFail) s
strengthenFailBase n
n forall a b. (a -> b) -> a -> b
$ String
"not well bounded, require: "
                                 forall a. Semigroup a => a -> a -> a
<>forall a. Show a => a -> String
show n
minBforall a. Semigroup a => a -> a -> a
<>String
" <= n <= "forall a. Semigroup a => a -> a -> a
<>forall a. Show a => a -> String
show n
maxB
  where
    maxB :: n
maxB = forall a b. (Integral a, Num b) => a -> b
fromIntegral @b @n forall a. Bounded a => a
maxBound
    minB :: n
minB = forall a b. (Integral a, Num b) => a -> b
fromIntegral @b @n forall a. Bounded a => a
minBound

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

-- | Decomposer. Strengthen every element in a list.
instance Strengthen a => Strengthen [a] where
    strengthen :: Weak [a] -> Validation (NonEmpty StrengthenFail) [a]
strengthen = forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall a.
Strengthen a =>
Weak a -> Validation (NonEmpty StrengthenFail) a
strengthen

-- | Decomposer. Strengthen both elements of a tuple.
instance (Strengthen a, Strengthen b) => Strengthen (a, b) where
    strengthen :: Weak (a, b) -> Validation (NonEmpty StrengthenFail) (a, b)
strengthen (Weak a
a, Weak b
b) = forall (f :: Type -> Type) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (forall a.
Strengthen a =>
Weak a -> Validation (NonEmpty StrengthenFail) a
strengthen Weak a
a) (forall a.
Strengthen a =>
Weak a -> Validation (NonEmpty StrengthenFail) a
strengthen Weak b
b)

-- | Decomposer. Strengthen either side of an 'Either'.
instance (Strengthen a, Strengthen b) => Strengthen (Either a b) where
    strengthen :: Weak (Either a b)
-> Validation (NonEmpty StrengthenFail) (Either a b)
strengthen = \case Left  Weak a
a -> forall a b. a -> Either a b
Left  forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
Strengthen a =>
Weak a -> Validation (NonEmpty StrengthenFail) a
strengthen Weak a
a
                       Right Weak b
b -> forall a b. b -> Either a b
Right forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a.
Strengthen a =>
Weak a -> Validation (NonEmpty StrengthenFail) a
strengthen Weak b
b