module Rerefined.Predicate.Relational.Length where

import Rerefined.Predicate.Common
import Rerefined.Predicate.Relational.Internal
import GHC.TypeNats ( Natural, KnownNat, natVal' )
import Data.MonoTraversable ( MonoFoldable(olength) )
import GHC.Exts ( Proxy# )

import Rerefined.Refined
import Rerefined.Refine.Unsafe ( unsafeRerefine )
import GHC.TypeError
import Data.Kind ( type Constraint )

-- | Compare length to a type-level 'Natural' using the given 'RelOp'.
data CompareLength (op :: RelOp) (n :: Natural)
    deriving Proxy# (CompareLength op n) -> Int -> ShowS
(Proxy# (CompareLength op n) -> Int -> ShowS)
-> Predicate (CompareLength op n)
forall {k} (p :: k). (Proxy# p -> Int -> ShowS) -> Predicate p
forall (op :: RelOp) (n :: Natural).
(Typeable op, KnownNat n) =>
Proxy# (CompareLength op n) -> Int -> ShowS
$cpredicateName :: forall (op :: RelOp) (n :: Natural).
(Typeable op, KnownNat n) =>
Proxy# (CompareLength op n) -> Int -> ShowS
predicateName :: Proxy# (CompareLength op n) -> Int -> ShowS
Predicate via Typeably (CompareLength op n)

-- | Compare the length of a 'Foldable' to a type-level 'Natural' using the
--   given 'RelOp'.
instance (KnownNat n, Foldable f, ReifyRelOp op)
  => Refine1 (CompareLength op n) f where
    validate1 :: forall a.
Proxy# (CompareLength op n) -> f a -> Maybe (RefineFailure String)
validate1 Proxy# (CompareLength op n)
p = Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)
forall (op :: RelOp) (n :: Natural).
(KnownNat n, ReifyRelOp op) =>
Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)
validateCompareLength Proxy# (CompareLength op n)
p (Int -> Maybe (RefineFailure String))
-> (f a -> Int) -> f a -> Maybe (RefineFailure String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Int
forall a. f a -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length

-- | Compare the length of a 'MonoFoldable' to a type-level 'Natural' using the
--   given 'RelOp'.
instance (KnownNat n, MonoFoldable a, ReifyRelOp op)
  => Refine (CompareLength op n) a where
    validate :: Proxy# (CompareLength op n) -> a -> Maybe (RefineFailure String)
validate Proxy# (CompareLength op n)
p = Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)
forall (op :: RelOp) (n :: Natural).
(KnownNat n, ReifyRelOp op) =>
Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)
validateCompareLength Proxy# (CompareLength op n)
p (Int -> Maybe (RefineFailure String))
-> (a -> Int) -> a -> Maybe (RefineFailure String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Int
forall mono. MonoFoldable mono => mono -> Int
olength

validateCompareLength
    :: forall op n. (KnownNat n, ReifyRelOp op)
    => Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)
validateCompareLength :: forall (op :: RelOp) (n :: Natural).
(KnownNat n, ReifyRelOp op) =>
Proxy# (CompareLength op n) -> Int -> Maybe (RefineFailure String)
validateCompareLength Proxy# (CompareLength op n)
p Int
len =
    Proxy# (CompareLength op n)
-> String -> Bool -> Maybe (RefineFailure String)
forall {k} (p :: k).
Predicate p =>
Proxy# p -> String -> Bool -> Maybe (RefineFailure String)
validateBool Proxy# (CompareLength op n)
p (String
"length 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
<>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 Int
len (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
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)

-- | Widen a length comparison predicate.
--
-- Only valid widenings are permitted, checked at compile time.
--
-- Example: Given a >= 1, we know also that a >= 0. Thus, this function allows
-- you to turn a @Refined (CompareLength GTE 1) a@ into a @Refined
-- (CompareLength GTE 0) a@.
--
-- TODO improve type error here
widenCompareLength
    :: forall m op n a
    .  WROE op n m
    => Refined (CompareLength op n) a
    -> Refined (CompareLength op m) a
widenCompareLength :: forall (m :: Natural) (op :: RelOp) (n :: Natural) a.
WROE op n m =>
Refined (CompareLength op n) a -> Refined (CompareLength op m) a
widenCompareLength = Refined (CompareLength op n) a -> Refined (CompareLength op m) a
forall {k1} {k2} (pNew :: k1) (pOld :: k2) a.
Refined pOld a -> Refined pNew a
unsafeRerefine

type WROE op n m = WROE' op n m (WidenRelOp op n m)
type WROE' :: RelOp -> Natural -> Natural -> Bool -> Constraint
type family WROE' (op :: RelOp) (n :: Natural) (m :: Natural) (b :: Bool) where
    WROE' op n m True  = ()
    WROE' op n m False = TypeError
      (      Text "can't widen relational equation "
        :$$: ShowType op :<>: Text " " :<>: ShowType n
        :$$: Text "to"
        :$$: ShowType op :<>: Text " " :<>: ShowType m
      )