{-# LANGUAGE AllowAmbiguousTypes #-}

module Rerefined.Predicate.Relational.Value where

import Rerefined.Predicate.Common
import Rerefined.Predicate.Relational.Internal
import GHC.TypeNats ( Natural, KnownNat, natVal' )

-- | Compare value to a type-level 'Natural' using the given 'RelOp'.
data CompareValue (op :: RelOp) (sign :: Sign) (n :: Natural)
    deriving Proxy# (CompareValue op sign n) -> Int -> ShowS
(Proxy# (CompareValue op sign n) -> Int -> ShowS)
-> Predicate (CompareValue op sign n)
forall {k} (p :: k). (Proxy# p -> Int -> ShowS) -> Predicate p
forall (op :: RelOp) (sign :: Sign) (n :: Natural).
(Typeable op, Typeable sign, KnownNat n) =>
Proxy# (CompareValue op sign n) -> Int -> ShowS
$cpredicateName :: forall (op :: RelOp) (sign :: Sign) (n :: Natural).
(Typeable op, Typeable sign, KnownNat n) =>
Proxy# (CompareValue op sign n) -> Int -> ShowS
predicateName :: Proxy# (CompareValue op sign n) -> Int -> ShowS
Predicate via Typeably (CompareValue op sign n)
-- TODO I could write custom predicateNames here if I wanted to override how
-- they display. But I don't mind the expanded type synonyms. @CompareValue
-- 'CBOpLT 10@ still makes sense to me, especially with the extra message.
--
-- I should simplify op names, but not sure what to, since I can't use LT/EQ/GT.
{-
instance KnownNat n => Predicate (LessThan n) where
    predicateName d = showParen (d > 10) $
        showString "LessThan " . showsPrec 11 (natVal' (proxy# :: Proxy# n))
-}

--type LessThan n = CompareValue LT' n

instance
  ( KnownNat n, Num a, Ord a
  , ReifyRelOp op, ReifySignedNat sign n, ReifySign sign
  ) => Refine (CompareValue op sign n) a where
    -- note that we show the reified 'Natural' rather than the coerced numeric
    -- type, as otherwise we'd need a @'Show' a@
    validate :: Proxy# (CompareValue op sign n)
-> a -> Maybe (RefineFailure String)
validate Proxy# (CompareValue op sign n)
p a
a =
        Proxy# (CompareValue op sign n)
-> String -> Bool -> Maybe (RefineFailure String)
forall {k} (p :: k).
Predicate p =>
Proxy# p -> String -> Bool -> Maybe (RefineFailure String)
validateBool Proxy# (CompareValue op sign n)
p
            (String
"value not "String -> ShowS
forall a. Semigroup a => a -> a -> a
<>forall (op :: RelOp). ReifyRelOp op => String
reifyRelOpPretty @opString -> ShowS
forall a. Semigroup a => a -> a -> a
<>String
" "String -> ShowS
forall a. Semigroup a => a -> a -> a
<>forall (sign :: Sign). ReifySign sign => String
signPretty @signString -> ShowS
forall a. Semigroup a => a -> a -> a
<>Natural -> String
forall a. Show a => a -> String
show Natural
n)
            (forall (op :: RelOp) a.
(ReifyRelOp op, Num a, Ord a) =>
a -> a -> Bool
reifyRelOp @op a
a (forall (sign :: Sign) (n :: Natural) a.
(ReifySignedNat sign n, Num a, KnownNat n) =>
a
reifySignedNat @sign @n))
      where n :: Natural
n = Proxy# n -> Natural
forall (n :: Natural). KnownNat n => Proxy# n -> Natural
natVal' (forall (a :: Natural). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @n)

data Sign = Pos | Neg

class Typeable sign => ReifySign (sign :: Sign) where signPretty :: String
instance ReifySign Pos where signPretty :: String
signPretty = String
""
instance ReifySign Neg where signPretty :: String
signPretty = String
"-"

-- TODO do I add any KnownNat constraints anywhere here
class ReifySignedNat (sign :: Sign) (n :: Natural) where
    reifySignedNat :: (Num a, KnownNat n) => a

instance ReifySignedNat Pos n where
    reifySignedNat :: forall a. (Num a, KnownNat n) => a
reifySignedNat = Natural -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy# n -> Natural
forall (n :: Natural). KnownNat n => Proxy# n -> Natural
natVal' (forall (a :: Natural). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @n))

instance ReifySignedNat Neg n where
    reifySignedNat :: forall a. (Num a, KnownNat n) => a
reifySignedNat = a -> a
forall a. Num a => a -> a
negate (Natural -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy# n -> Natural
forall (n :: Natural). KnownNat n => Proxy# n -> Natural
natVal' (forall (a :: Natural). Proxy# a
forall {k} (a :: k). Proxy# a
proxy# @n)))