{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE UndecidableInstances #-} -- for GHC <= 9.4, WROE

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.Refine
import GHC.TypeError
import Data.Kind ( type Constraint )
import TypeLevelShow.Utils
import TypeLevelShow.Natural
import Data.Text.Builder.Linear qualified as TBL

-- | Compare length to a type-level 'Natural' using the given 'RelOp'.
data CompareLength (op :: RelOp) (n :: Natural)

-- | Precedence of 4 (matching base relational operators e.g. '>=').
instance Predicate (CompareLength op n) where
    type PredicateName d (CompareLength op n) = ShowParen (d > 4)
        ("Length " ++ ShowRelOp op ++ ShowChar ' ' ++ ShowNatDec n)

-- | Compare the length of a 'Foldable' to a type-level 'Natural' using the
--   given 'RelOp'.
instance
  ( KnownNat n, Foldable f, ReifyRelOp op
  , KnownPredicateName (CompareLength op n)
  ) => Refine1 (CompareLength op n) f where
    validate1 :: forall a. Proxy# (CompareLength op n) -> f a -> Maybe RefineFailure
validate1 Proxy# (CompareLength op n)
p = Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
forall (op :: RelOp) (n :: Natural).
(KnownNat n, ReifyRelOp op,
 KnownPredicateName (CompareLength op n)) =>
Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
validateCompareLength Proxy# (CompareLength op n)
p (Int -> Maybe RefineFailure)
-> (f a -> Int) -> f a -> Maybe RefineFailure
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
  , KnownPredicateName (CompareLength op n)
  ) => Refine (CompareLength op n) a where
    validate :: Proxy# (CompareLength op n) -> a -> Maybe RefineFailure
validate Proxy# (CompareLength op n)
p = Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
forall (op :: RelOp) (n :: Natural).
(KnownNat n, ReifyRelOp op,
 KnownPredicateName (CompareLength op n)) =>
Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
validateCompareLength Proxy# (CompareLength op n)
p (Int -> Maybe RefineFailure)
-> (a -> Int) -> a -> Maybe RefineFailure
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
       , KnownPredicateName (CompareLength op n)
    ) => Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
validateCompareLength :: forall (op :: RelOp) (n :: Natural).
(KnownNat n, ReifyRelOp op,
 KnownPredicateName (CompareLength op n)) =>
Proxy# (CompareLength op n) -> Int -> Maybe RefineFailure
validateCompareLength Proxy# (CompareLength op n)
p Int
len =
    Proxy# (CompareLength op n)
-> Bool -> Builder -> Maybe RefineFailure
forall {k} (p :: k).
(Predicate p, KnownPredicateName p) =>
Proxy# p -> Bool -> Builder -> Maybe RefineFailure
validateBool Proxy# (CompareLength op n)
p (forall (op :: RelOp) a. (ReifyRelOp op, Ord a) => a -> a -> Bool
reifyRelOp @op Int
len Int
n) (Builder -> Maybe RefineFailure) -> Builder -> Maybe RefineFailure
forall a b. (a -> b) -> a -> b
$ Builder
"length: "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Int -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec Int
n
  where n :: Int
n = Natural -> Int
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))

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

-- | 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 @Refined1 (CompareLength GTE 1) f a@ into a @Refined1
-- (CompareLength GTE 0) f a@.
--
-- TODO improve type error here
widenCompareLength1
    :: forall m op n f a
    .  WROE op n m
    => Refined1 (CompareLength op n) f a
    -> Refined1 (CompareLength op m) f a
widenCompareLength1 :: forall {k1} (m :: Natural) (op :: RelOp) (n :: Natural)
       (f :: k1 -> Type) (a :: k1).
WROE op n m =>
Refined1 (CompareLength op n) f a
-> Refined1 (CompareLength op m) f a
widenCompareLength1 = Refined1 (CompareLength op n) f a
-> Refined1 (CompareLength op m) f a
forall {k1} {k2} {k3} (pNew :: k1) (pOld :: k2) (f :: k3 -> Type)
       (a :: k3).
Refined1 pOld f a -> Refined1 pNew f a
unsafeRerefine1

type WROE op n m = WROE' op n m (WidenRelOp op n m)
type WROE' :: k -> Natural -> Natural -> Bool -> Constraint
type family WROE' op n m b 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
      )