{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE AllowAmbiguousTypes #-}

module Strongweak.Strengthen
  (
  -- * 'Strengthen' class
    Strengthen(..)
  , restrengthen
  , Result

  -- ** Helpers
  , strengthenBounded

  -- * Strengthen failures
  , StrengthenFailure(..)
  , failStrengthen1
  , failStrengthen

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

import Strongweak.Util.Typeable ( typeRep' )
import Strongweak.Util.TypeNats ( natVal'' )
import Strongweak.Weaken ( Weaken(..) )
import Data.Either.Validation
import Data.Typeable ( Typeable )

import GHC.TypeNats ( KnownNat )
import Data.Word
import Data.Int
import Rerefined
import Data.Vector.Generic.Sized qualified as VGS -- Shazbot!
import Data.Vector.Generic qualified as VG
import Data.Functor.Identity
import Data.Functor.Const
import Data.List.NonEmpty qualified as NonEmpty
import Data.List.NonEmpty ( NonEmpty )

import Data.Text.Builder.Linear qualified as TBL
import GHC.Exts ( fromString )

import Data.Bits ( FiniteBits )

type Result = Validation StrengthenFailure

{- | Attempt to strengthen some @'Weak' a@, asserting certain invariants.

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. That does mean the instances for this class
are a little confusingly worded. Alas.

See "Strongweak" for class design notes and laws.
-}
class Weaken a => Strengthen a where
    -- | Attempt to strengthen some @'Weak' a@ to its associated strong type
    --   @a@.
    strengthen :: Weak a -> Result 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 -> Result a
restrengthen :: forall a. (Strengthen a, Weaken a) => a -> Result a
restrengthen = Weak a -> Result a
forall a. Strengthen a => Weak a -> Result a
strengthen (Weak a -> Result a) -> (a -> Weak a) -> a -> Result a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Weak a
forall a. Weaken a => a -> Weak a
weaken

-- | A failure encountered during strengthening.
data StrengthenFailure = StrengthenFailure
  { StrengthenFailure -> [Builder]
strengthenFailDetail :: [TBL.Builder]
  -- ^ Detail on strengthen failure.
  --
  -- We use a list here for the cases where you want multiple lines of detail.
  -- Separating with a newline would make prettifying later harder, so we delay.

  , StrengthenFailure -> [(Builder, StrengthenFailure)]
strengthenFailInner  :: [(TBL.Builder, StrengthenFailure)]
  -- ^ Indexed.
  } deriving stock Int -> StrengthenFailure -> ShowS
[StrengthenFailure] -> ShowS
StrengthenFailure -> String
(Int -> StrengthenFailure -> ShowS)
-> (StrengthenFailure -> String)
-> ([StrengthenFailure] -> ShowS)
-> Show StrengthenFailure
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StrengthenFailure -> ShowS
showsPrec :: Int -> StrengthenFailure -> ShowS
$cshow :: StrengthenFailure -> String
show :: StrengthenFailure -> String
$cshowList :: [StrengthenFailure] -> ShowS
showList :: [StrengthenFailure] -> ShowS
Show

failStrengthen
    :: [TBL.Builder] -> [(TBL.Builder, StrengthenFailure)] -> Result a
failStrengthen :: forall a. [Builder] -> [(Builder, StrengthenFailure)] -> Result a
failStrengthen [Builder]
t [(Builder, StrengthenFailure)]
fs = StrengthenFailure -> Validation StrengthenFailure a
forall e a. e -> Validation e a
Failure (StrengthenFailure -> Validation StrengthenFailure a)
-> StrengthenFailure -> Validation StrengthenFailure a
forall a b. (a -> b) -> a -> b
$ [Builder] -> [(Builder, StrengthenFailure)] -> StrengthenFailure
StrengthenFailure [Builder]
t [(Builder, StrengthenFailure)]
fs

failStrengthen1 :: [TBL.Builder] -> Result a
failStrengthen1 :: forall a. [Builder] -> Result a
failStrengthen1 [Builder]
t = [Builder] -> [(Builder, StrengthenFailure)] -> Result a
forall a. [Builder] -> [(Builder, StrengthenFailure)] -> Result a
failStrengthen [Builder]
t []

-- | Strengthen a type by refining it with a predicate.
instance Refine p a => Strengthen (Refined p a) where
    strengthen :: Weak (Refined p a) -> Result (Refined p a)
strengthen = a -> Either RefineFailure (Refined p a)
forall {k} (p :: k) a.
Refine p a =>
a -> Either RefineFailure (Refined p a)
refine (a -> Either RefineFailure (Refined p a))
-> (Either RefineFailure (Refined p a) -> Result (Refined p a))
-> a
-> Result (Refined p a)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> \case
      Right Refined p a
ra -> Refined p a -> Result (Refined p a)
forall e a. a -> Validation e a
Success Refined p a
ra
      Left  RefineFailure
rf -> [Builder] -> Result (Refined p a)
forall a. [Builder] -> Result a
failStrengthen1
        [ Builder
"refinement failure:"
        , Text -> Builder
TBL.fromText (RefineFailure -> Text
prettyRefineFailure RefineFailure
rf) ]
        -- ^ TODO rerefined: provide a TBL pretty function

-- | Strengthen a type by refining it with a functor predicate.
instance Refine1 p f => Strengthen (Refined1 p f a) where
    strengthen :: Weak (Refined1 p f a) -> Result (Refined1 p f a)
strengthen = f a -> Either RefineFailure (Refined1 p f a)
forall {k1} {k2} (p :: k1) (f :: k2 -> Type) (a :: k2).
Refine1 p f =>
f a -> Either RefineFailure (Refined1 p f a)
refine1 (f a -> Either RefineFailure (Refined1 p f a))
-> (Either RefineFailure (Refined1 p f a)
    -> Result (Refined1 p f a))
-> f a
-> Result (Refined1 p f a)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> \case
      Right Refined1 p f a
ra -> Refined1 p f a -> Result (Refined1 p f a)
forall e a. a -> Validation e a
Success Refined1 p f a
ra
      Left  RefineFailure
rf -> [Builder] -> Result (Refined1 p f a)
forall a. [Builder] -> Result a
failStrengthen1
        [ Builder
"refinement failure:"
        , Text -> Builder
TBL.fromText (RefineFailure -> Text
prettyRefineFailure RefineFailure
rf) ]

-- | Strengthen a plain list into a non-empty list by asserting non-emptiness.
instance Strengthen (NonEmpty a) where
    strengthen :: Weak (NonEmpty a) -> Result (NonEmpty a)
strengthen = [a] -> Maybe (NonEmpty a)
forall a. [a] -> Maybe (NonEmpty a)
NonEmpty.nonEmpty ([a] -> Maybe (NonEmpty a))
-> (Maybe (NonEmpty a) -> Result (NonEmpty a))
-> [a]
-> Result (NonEmpty a)
forall a b c. (a -> b) -> (b -> c) -> a -> c
.> \case
      Just NonEmpty a
neas -> NonEmpty a -> Result (NonEmpty a)
forall e a. a -> Validation e a
Success NonEmpty a
neas
      Maybe (NonEmpty a)
Nothing   -> [Builder] -> Result (NonEmpty a)
forall a. [Builder] -> Result a
failStrengthen1 ([Builder] -> Result (NonEmpty a))
-> [Builder] -> Result (NonEmpty a)
forall a b. (a -> b) -> a -> b
$
        [ Builder
"type: [a] -> NonEmpty a"
        , Builder
"fail: empty list" ]

-- | Strengthen a plain list into a sized vector by asserting length.
instance (VG.Vector v a, KnownNat n) => Strengthen (VGS.Vector v n a) where
    -- TODO another case of TBL not supporting unbounded integrals
    strengthen :: Weak (Vector v n a) -> Result (Vector v n a)
strengthen Weak (Vector v n a)
as =
        case [a] -> Maybe (Vector v n a)
forall (v :: Type -> Type) a (n :: Nat).
(Vector v a, KnownNat n) =>
[a] -> Maybe (Vector v n a)
VGS.fromList [a]
Weak (Vector v n a)
as of
          Just Vector v n a
va -> Vector v n a -> Result (Vector v n a)
forall e a. a -> Validation e a
Success Vector v n a
va
          Maybe (Vector v n a)
Nothing -> [Builder] -> Result (Vector v n a)
forall a. [Builder] -> Result a
failStrengthen1 ([Builder] -> Result (Vector v n a))
-> [Builder] -> Result (Vector v n a)
forall a b. (a -> b) -> a -> b
$
            [ Builder
"type: [a] -> Vector v "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>String -> Builder
forall a. IsString a => String -> a
fromString (Nat -> String
forall a. Show a => a -> String
show Nat
n)Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" a"
            , Builder
"fail: wrong length (got "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Int -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec ([a] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [a]
Weak (Vector v n a)
as)Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
")" ]
      where n :: Nat
n = forall (n :: Nat). KnownNat n => Nat
natVal'' @n

-- | Add wrapper.
instance Strengthen (Identity a) where
    strengthen :: Weak (Identity a) -> Result (Identity a)
strengthen = Identity a -> Result (Identity a)
forall e a. a -> Validation e a
Success (Identity a -> Result (Identity a))
-> (a -> Identity a) -> a -> Result (Identity a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Identity a
forall a. a -> Identity a
Identity

-- | Add wrapper.
instance Strengthen (Const a b) where
    strengthen :: Weak (Const a b) -> Result (Const a b)
strengthen = Const a b -> Result (Const a b)
forall e a. a -> Validation e a
Success (Const a b -> Result (Const a b))
-> (a -> Const a b) -> a -> Result (Const a b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Const a 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 -> Result Word8
strengthen = Nat -> Result Word8
Weak Word8 -> Result Word8
forall m n.
(Typeable n, Integral n, Show n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Result m
strengthenBounded
instance Strengthen Word16 where strengthen :: Weak Word16 -> Result Word16
strengthen = Nat -> Result Word16
Weak Word16 -> Result Word16
forall m n.
(Typeable n, Integral n, Show n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Result m
strengthenBounded
instance Strengthen Word32 where strengthen :: Weak Word32 -> Result Word32
strengthen = Nat -> Result Word32
Weak Word32 -> Result Word32
forall m n.
(Typeable n, Integral n, Show n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Result m
strengthenBounded
instance Strengthen Word64 where strengthen :: Weak Word64 -> Result Word64
strengthen = Nat -> Result Word64
Weak Word64 -> Result Word64
forall m n.
(Typeable n, Integral n, Show n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Result m
strengthenBounded

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

-- | Strengthen one numeric type into another.
--
-- @n@ must be "wider" than @m@.
--
-- @'FiniteBits' m@ and @'Show' n@ are for error printing. We're forced to
-- @'Show' n@ because linear-text-builder can't print unbounded integrals. PR:
-- https://github.com/Bodigrim/linear-builder/pull/20
strengthenBounded
    :: forall m n
    .  ( Typeable n, Integral n, Show n
       , Typeable m, Integral m, Bounded m, FiniteBits m
       ) => n -> Result m
strengthenBounded :: forall m n.
(Typeable n, Integral n, Show n, Typeable m, Integral m, Bounded m,
 FiniteBits m) =>
n -> Result m
strengthenBounded n
n
  | n
n n -> n -> Bool
forall a. Ord a => a -> a -> Bool
<= n
maxBn Bool -> Bool -> Bool
&& n
n n -> n -> Bool
forall a. Ord a => a -> a -> Bool
>= n
minBn = m -> Validation StrengthenFailure m
forall e a. a -> Validation e a
Success (n -> m
forall a b. (Integral a, Num b) => a -> b
fromIntegral n
n)
  | Bool
otherwise = [Builder] -> Validation StrengthenFailure m
forall a. [Builder] -> Result a
failStrengthen1
        [ Builder
"numeric strengthen: "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>String -> Builder
forall a. IsString a => String -> a
fromString (TypeRep -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep
forall {k} (a :: k). Typeable a => TypeRep
typeRep' @n))
          Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" -> "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>String -> Builder
forall a. IsString a => String -> a
fromString (TypeRep -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep
forall {k} (a :: k). Typeable a => TypeRep
typeRep' @m))
        , Builder
"bounds check does not hold: "
          Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>m -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec m
minBmBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" <= "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>String -> Builder
forall a. IsString a => String -> a
fromString (n -> String
forall a. Show a => a -> String
show n
n)
          Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" <= "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>m -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec m
maxBm
        ]
  where
    maxBn :: n
maxBn = forall a b. (Integral a, Num b) => a -> b
fromIntegral @m @n m
maxBm
    minBn :: n
minBn = forall a b. (Integral a, Num b) => a -> b
fromIntegral @m @n m
minBm
    maxBm :: m
maxBm = forall a. Bounded a => a
maxBound @m
    minBm :: m
minBm = forall a. Bounded a => a
minBound @m

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

-- | Decomposer. Strengthen every element in a list.
instance Strengthen a => Strengthen [a] where
    strengthen :: Weak [a] -> Result [a]
strengthen = [Weak a] -> Result [a]
Weak [a] -> Result [a]
forall a. Strengthen a => [Weak a] -> Result [a]
strengthenList

strengthenList :: Strengthen a => [Weak a] -> Result [a]
strengthenList :: forall a. Strengthen a => [Weak a] -> Result [a]
strengthenList = Int -> [a] -> [Validation StrengthenFailure a] -> Result [a]
forall {a} {a}.
(Integral a, FiniteBits a) =>
a -> [a] -> [Validation StrengthenFailure a] -> Result [a]
goR (Int
0 :: Int) [] ([Validation StrengthenFailure a] -> Result [a])
-> ([Weak a] -> [Validation StrengthenFailure a])
-> [Weak a]
-> Result [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Weak a -> Validation StrengthenFailure a)
-> [Weak a] -> [Validation StrengthenFailure a]
forall a b. (a -> b) -> [a] -> [b]
map Weak a -> Validation StrengthenFailure a
forall a. Strengthen a => Weak a -> Result a
strengthen
  where
    goR :: a -> [a] -> [Validation StrengthenFailure a] -> Result [a]
goR a
i [a]
as = \case
      Validation StrengthenFailure a
r:[Validation StrengthenFailure a]
rs ->
        case Validation StrengthenFailure a
r of
          Success a
a -> a -> [a] -> [Validation StrengthenFailure a] -> Result [a]
goR (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as) [Validation StrengthenFailure a]
rs
          Failure StrengthenFailure
e -> a
-> [(Builder, StrengthenFailure)]
-> [Validation StrengthenFailure a]
-> Result [a]
forall {a} {a} {a}.
(Integral a, FiniteBits a) =>
a
-> [(Builder, StrengthenFailure)]
-> [Validation StrengthenFailure a]
-> Result a
goL (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) [(a -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec a
i, StrengthenFailure
e)]    [Validation StrengthenFailure a]
rs
      []   -> [a] -> Result [a]
forall e a. a -> Validation e a
Success [a]
as
    goL :: a
-> [(Builder, StrengthenFailure)]
-> [Validation StrengthenFailure a]
-> Result a
goL a
i [(Builder, StrengthenFailure)]
es = \case
      Validation StrengthenFailure a
r:[Validation StrengthenFailure a]
rs ->
        case Validation StrengthenFailure a
r of
          Success a
_ -> a
-> [(Builder, StrengthenFailure)]
-> [Validation StrengthenFailure a]
-> Result a
goL (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) [(Builder, StrengthenFailure)]
es                      [Validation StrengthenFailure a]
rs
          Failure StrengthenFailure
e -> a
-> [(Builder, StrengthenFailure)]
-> [Validation StrengthenFailure a]
-> Result a
goL (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) ((a -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec a
i, StrengthenFailure
e)(Builder, StrengthenFailure)
-> [(Builder, StrengthenFailure)] -> [(Builder, StrengthenFailure)]
forall a. a -> [a] -> [a]
:[(Builder, StrengthenFailure)]
es) [Validation StrengthenFailure a]
rs
      []   -> [Builder] -> [(Builder, StrengthenFailure)] -> Result a
forall a. [Builder] -> [(Builder, StrengthenFailure)] -> Result a
failStrengthen [Builder
"list had failures"] [(Builder, StrengthenFailure)]
es

-- | Decomposer. Strengthen both elements of a tuple.
instance (Strengthen l, Strengthen r) => Strengthen (l, r) where
    strengthen :: Weak (l, r) -> Result (l, r)
strengthen (Weak l
l, Weak r
r) =
        case Weak l -> Result l
forall a. Strengthen a => Weak a -> Result a
strengthen Weak l
l of
          Success l
sl ->
            case Weak r -> Result r
forall a. Strengthen a => Weak a -> Result a
strengthen Weak r
r of
              Success r
sr -> (l, r) -> Result (l, r)
forall e a. a -> Validation e a
Success (l
sl, r
sr)
              Failure StrengthenFailure
er -> [Builder] -> [(Builder, StrengthenFailure)] -> Result (l, r)
forall a. [Builder] -> [(Builder, StrengthenFailure)] -> Result a
failStrengthen [Builder
"2-tuple: right failed"]
                [(Builder
"R", StrengthenFailure
er)]
          Failure StrengthenFailure
el ->
            case forall a. Strengthen a => Weak a -> Result a
strengthen @r Weak r
r of
              Success r
_  -> [Builder] -> [(Builder, StrengthenFailure)] -> Result (l, r)
forall a. [Builder] -> [(Builder, StrengthenFailure)] -> Result a
failStrengthen [Builder
"2-tuple:  left failed"]
                [(Builder
"L", StrengthenFailure
el)]
              Failure StrengthenFailure
er -> [Builder] -> [(Builder, StrengthenFailure)] -> Result (l, r)
forall a. [Builder] -> [(Builder, StrengthenFailure)] -> Result a
failStrengthen [Builder
"2-tuple:   l&r failed"]
                [(Builder
"R", StrengthenFailure
er), (Builder
"L", StrengthenFailure
el)]

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

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

-- from flow
(.>) :: (a -> b) -> (b -> c) -> a -> c
a -> b
f .> :: forall a b c. (a -> b) -> (b -> c) -> a -> c
.> b -> c
g = b -> c
g (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f