{-# OPTIONS_GHC -fno-warn-orphans #-}
module System.Process.Quick.Predicate.LowerCase where

import Refined
import System.Process.Quick.Prelude


data LowerCase

instance Predicate LowerCase String where
  validate :: Proxy LowerCase -> String -> Maybe RefineException
validate Proxy LowerCase
p String
value =
    if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isLower String
value
      then Maybe RefineException
forall a. Maybe a
Nothing
      else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy LowerCase -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy LowerCase
p) Text
"Not all chars are lower-case"

type LowerCaseString = Refined LowerCase String


leftError :: Show a => Text -> Either a b -> b
leftError :: forall a b. Show a => Text -> Either a b -> b
leftError Text
m = \case
  Right b
v -> b
v
  Left a
e -> Text -> b
forall a t. (HasCallStack, IsText t) => t -> a
error (Text -> b) -> Text -> b
forall a b. (a -> b) -> a -> b
$ Text
m Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"; due: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall b a. (Show a, IsString b) => a -> b
show a
e

instance {-# OVERLAPPING #-}
  (Arbitrary a, Typeable a, Predicate (SizeEqualTo n) [a], KnownNat n) =>
  Arbitrary (Refined (SizeEqualTo n) [a]) where
  arbitrary :: Gen (Refined (SizeEqualTo n) [a])
arbitrary =
    Text
-> Either RefineException (Refined (SizeEqualTo n) [a])
-> Refined (SizeEqualTo n) [a]
forall a b. Show a => Text -> Either a b -> b
leftError Text
"Dead code" (Either RefineException (Refined (SizeEqualTo n) [a])
 -> Refined (SizeEqualTo n) [a])
-> ([a] -> Either RefineException (Refined (SizeEqualTo n) [a]))
-> [a]
-> Refined (SizeEqualTo n) [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Either RefineException (Refined (SizeEqualTo n) [a])
forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine ([a] -> Refined (SizeEqualTo n) [a])
-> Gen [a] -> Gen (Refined (SizeEqualTo n) [a])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    Int -> Gen a -> Gen [a]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ Proxy n -> Nat
forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n)) Gen a
forall a. Arbitrary a => Gen a
arbitrary

  shrink :: Refined (SizeEqualTo n) [a] -> [Refined (SizeEqualTo n) [a]]
shrink = [Either RefineException (Refined (SizeEqualTo n) [a])]
-> [Refined (SizeEqualTo n) [a]]
forall a b. [Either a b] -> [b]
rights ([Either RefineException (Refined (SizeEqualTo n) [a])]
 -> [Refined (SizeEqualTo n) [a]])
-> (Refined (SizeEqualTo n) [a]
    -> [Either RefineException (Refined (SizeEqualTo n) [a])])
-> Refined (SizeEqualTo n) [a]
-> [Refined (SizeEqualTo n) [a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> Either RefineException (Refined (SizeEqualTo n) [a]))
-> [[a]] -> [Either RefineException (Refined (SizeEqualTo n) [a])]
forall a b. (a -> b) -> [a] -> [b]
map [a] -> Either RefineException (Refined (SizeEqualTo n) [a])
forall {k} (p :: k) x.
Predicate p x =>
x -> Either RefineException (Refined p x)
refine ([[a]] -> [Either RefineException (Refined (SizeEqualTo n) [a])])
-> (Refined (SizeEqualTo n) [a] -> [[a]])
-> Refined (SizeEqualTo n) [a]
-> [Either RefineException (Refined (SizeEqualTo n) [a])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [[a]]
forall a. Arbitrary a => a -> [a]
shrink ([a] -> [[a]])
-> (Refined (SizeEqualTo n) [a] -> [a])
-> Refined (SizeEqualTo n) [a]
-> [[a]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined (SizeEqualTo n) [a] -> [a]
forall {k} (p :: k) x. Refined p x -> x
unrefine