module System.Process.Quick.Predicate.InFile where

import Control.Monad.Writer.Strict
import System.Process.Quick.Predicate
import System.Process.Quick.Prelude
import System.Process.Quick.TdfaToSbvRegex as P
import System.Process.Quick.Sbv.Arbitrary
import System.Process.Quick.CallArgument (NeList)
import Text.Regex.TDFA ((=~))
import Type.Reflection qualified as R
import Type.Reflection ((:~:)(Refl))
import Data.Typeable (eqT)


data InFile (ext :: Symbol) deriving (Typeable (InFile ext)
Typeable (InFile ext) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> InFile ext -> c (InFile ext))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (InFile ext))
-> (InFile ext -> Constr)
-> (InFile ext -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (InFile ext)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (InFile ext)))
-> ((forall b. Data b => b -> b) -> InFile ext -> InFile ext)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> InFile ext -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> InFile ext -> r)
-> (forall u. (forall d. Data d => d -> u) -> InFile ext -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> InFile ext -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext))
-> Data (InFile ext)
InFile ext -> Constr
InFile ext -> DataType
(forall b. Data b => b -> b) -> InFile ext -> InFile ext
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> InFile ext -> u
forall u. (forall d. Data d => d -> u) -> InFile ext -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InFile ext -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InFile ext -> r
forall (ext :: Symbol). KnownSymbol ext => Typeable (InFile ext)
forall (ext :: Symbol). KnownSymbol ext => InFile ext -> Constr
forall (ext :: Symbol). KnownSymbol ext => InFile ext -> DataType
forall (ext :: Symbol).
KnownSymbol ext =>
(forall b. Data b => b -> b) -> InFile ext -> InFile ext
forall (ext :: Symbol) u.
KnownSymbol ext =>
Int -> (forall d. Data d => d -> u) -> InFile ext -> u
forall (ext :: Symbol) u.
KnownSymbol ext =>
(forall d. Data d => d -> u) -> InFile ext -> [u]
forall (ext :: Symbol) r r'.
KnownSymbol ext =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InFile ext -> r
forall (ext :: Symbol) r r'.
KnownSymbol ext =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InFile ext -> r
forall (ext :: Symbol) (m :: * -> *).
(KnownSymbol ext, Monad m) =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
forall (ext :: Symbol) (m :: * -> *).
(KnownSymbol ext, MonadPlus m) =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
forall (ext :: Symbol) (c :: * -> *).
KnownSymbol ext =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InFile ext)
forall (ext :: Symbol) (c :: * -> *).
KnownSymbol ext =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InFile ext -> c (InFile ext)
forall (ext :: Symbol) (t :: * -> *) (c :: * -> *).
(KnownSymbol ext, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (InFile ext))
forall (ext :: Symbol) (t :: * -> * -> *) (c :: * -> *).
(KnownSymbol ext, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InFile ext))
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InFile ext)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InFile ext -> c (InFile ext)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (InFile ext))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InFile ext))
$cgfoldl :: forall (ext :: Symbol) (c :: * -> *).
KnownSymbol ext =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InFile ext -> c (InFile ext)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> InFile ext -> c (InFile ext)
$cgunfold :: forall (ext :: Symbol) (c :: * -> *).
KnownSymbol ext =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InFile ext)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (InFile ext)
$ctoConstr :: forall (ext :: Symbol). KnownSymbol ext => InFile ext -> Constr
toConstr :: InFile ext -> Constr
$cdataTypeOf :: forall (ext :: Symbol). KnownSymbol ext => InFile ext -> DataType
dataTypeOf :: InFile ext -> DataType
$cdataCast1 :: forall (ext :: Symbol) (t :: * -> *) (c :: * -> *).
(KnownSymbol ext, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (InFile ext))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (InFile ext))
$cdataCast2 :: forall (ext :: Symbol) (t :: * -> * -> *) (c :: * -> *).
(KnownSymbol ext, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InFile ext))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (InFile ext))
$cgmapT :: forall (ext :: Symbol).
KnownSymbol ext =>
(forall b. Data b => b -> b) -> InFile ext -> InFile ext
gmapT :: (forall b. Data b => b -> b) -> InFile ext -> InFile ext
$cgmapQl :: forall (ext :: Symbol) r r'.
KnownSymbol ext =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InFile ext -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> InFile ext -> r
$cgmapQr :: forall (ext :: Symbol) r r'.
KnownSymbol ext =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InFile ext -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> InFile ext -> r
$cgmapQ :: forall (ext :: Symbol) u.
KnownSymbol ext =>
(forall d. Data d => d -> u) -> InFile ext -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> InFile ext -> [u]
$cgmapQi :: forall (ext :: Symbol) u.
KnownSymbol ext =>
Int -> (forall d. Data d => d -> u) -> InFile ext -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> InFile ext -> u
$cgmapM :: forall (ext :: Symbol) (m :: * -> *).
(KnownSymbol ext, Monad m) =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
$cgmapMp :: forall (ext :: Symbol) (m :: * -> *).
(KnownSymbol ext, MonadPlus m) =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
$cgmapMo :: forall (ext :: Symbol) (m :: * -> *).
(KnownSymbol ext, MonadPlus m) =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> InFile ext -> m (InFile ext)
Data, Int -> InFile ext -> ShowS
[InFile ext] -> ShowS
InFile ext -> String
(Int -> InFile ext -> ShowS)
-> (InFile ext -> String)
-> ([InFile ext] -> ShowS)
-> Show (InFile ext)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (ext :: Symbol). Int -> InFile ext -> ShowS
forall (ext :: Symbol). [InFile ext] -> ShowS
forall (ext :: Symbol). InFile ext -> String
$cshowsPrec :: forall (ext :: Symbol). Int -> InFile ext -> ShowS
showsPrec :: Int -> InFile ext -> ShowS
$cshow :: forall (ext :: Symbol). InFile ext -> String
show :: InFile ext -> String
$cshowList :: forall (ext :: Symbol). [InFile ext] -> ShowS
showList :: [InFile ext] -> ShowS
Show, InFile ext -> InFile ext -> Bool
(InFile ext -> InFile ext -> Bool)
-> (InFile ext -> InFile ext -> Bool) -> Eq (InFile ext)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (ext :: Symbol). InFile ext -> InFile ext -> Bool
$c== :: forall (ext :: Symbol). InFile ext -> InFile ext -> Bool
== :: InFile ext -> InFile ext -> Bool
$c/= :: forall (ext :: Symbol). InFile ext -> InFile ext -> Bool
/= :: InFile ext -> InFile ext -> Bool
Eq, (forall x. InFile ext -> Rep (InFile ext) x)
-> (forall x. Rep (InFile ext) x -> InFile ext)
-> Generic (InFile ext)
forall x. Rep (InFile ext) x -> InFile ext
forall x. InFile ext -> Rep (InFile ext) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (ext :: Symbol) x. Rep (InFile ext) x -> InFile ext
forall (ext :: Symbol) x. InFile ext -> Rep (InFile ext) x
$cfrom :: forall (ext :: Symbol) x. InFile ext -> Rep (InFile ext) x
from :: forall x. InFile ext -> Rep (InFile ext) x
$cto :: forall (ext :: Symbol) x. Rep (InFile ext) x -> InFile ext
to :: forall x. Rep (InFile ext) x -> InFile ext
Generic)

instance KnownSymbol e => Predicate (InFile e) String where
  validate :: Proxy (InFile e) -> String -> Maybe RefineException
validate Proxy (InFile e)
p String
x =
    let ext :: String
ext = Proxy e -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @e) in
      if String
ext String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"*"
      then
        if String
x String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~  (String
"^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*$" :: String)
        then Maybe RefineException
forall a. Maybe a
Nothing
        else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (InFile e) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (InFile e)
p) (Text -> Maybe RefineException) -> Text -> Maybe RefineException
forall a b. (a -> b) -> a -> b
$ Text
"Bad FilePath " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. ToText a => a -> Text
toText String
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"
      else
        if String
x String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ (String
"^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*[.]" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
ext String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"$")
        then Maybe RefineException
forall a. Maybe a
Nothing
        else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (InFile e) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (InFile e)
p) (Text -> Maybe RefineException) -> Text -> Maybe RefineException
forall a b. (a -> b) -> a -> b
$ Text
"Bad FilePath " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. ToText a => a -> Text
toText String
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"

instance Predicate (InFile e) String => Predicate (InFile e) [String] where
  validate :: Proxy (InFile e) -> [String] -> Maybe RefineException
validate Proxy (InFile e)
p = [RefineException] -> Maybe RefineException
forall a. [a] -> Maybe a
listToMaybe ([RefineException] -> Maybe RefineException)
-> ([String] -> [RefineException])
-> [String]
-> Maybe RefineException
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Maybe RefineException) -> [String] -> [RefineException]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Proxy (InFile e) -> String -> Maybe RefineException
forall k (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate Proxy (InFile e)
p)
instance Predicate (InFile e) String => Predicate (InFile e) (NeList String) where
  validate :: Proxy (InFile e) -> NeList String -> Maybe RefineException
validate Proxy (InFile e)
p = [RefineException] -> Maybe RefineException
forall a. [a] -> Maybe a
listToMaybe ([RefineException] -> Maybe RefineException)
-> (NeList String -> [RefineException])
-> NeList String
-> Maybe RefineException
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Maybe RefineException) -> [String] -> [RefineException]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Proxy (InFile e) -> String -> Maybe RefineException
forall k (p :: k) x.
Predicate p x =>
Proxy p -> x -> Maybe RefineException
validate Proxy (InFile e)
p) ([String] -> [RefineException])
-> (NeList String -> [String])
-> NeList String
-> [RefineException]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NeList String -> [String]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList

genFilePathBy :: forall e. KnownSymbol e => Proxy e -> Gen FilePath
genFilePathBy :: forall (e :: Symbol). KnownSymbol e => Proxy e -> Gen String
genFilePathBy Proxy e
_ =
  let ext :: String
ext = Proxy e -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @e) in
    RegExp -> Gen String
forall b. SymVal b => RegExp -> Gen b
findStringByRegex
      (String -> RegExp
parse (String -> RegExp) -> String -> RegExp
forall a b. (a -> b) -> a -> b
$ if String
ext String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"*"
        then String
"^[^/\x0000-\x001F]+([.][a-z]{1,4})?$"
        else String
"^[^/\x0000-\x001F]+[.]" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
ext String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"$")

instance {-# OVERLAPPING #-}
  KnownSymbol e => Arbitrary (Refined (InFile e) FilePath) where
  arbitrary :: Gen (Refined (InFile e) String)
arbitrary =
    Proxy e -> Gen String
forall (e :: Symbol). KnownSymbol e => Proxy e -> Gen String
genFilePathBy (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @e) Gen String
-> (String -> Gen (Refined (InFile e) String))
-> Gen (Refined (InFile e) String)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Refined (InFile e) String -> Gen (Refined (InFile e) String)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Refined (InFile e) String -> Gen (Refined (InFile e) String))
-> (String -> Refined (InFile e) String)
-> String
-> Gen (Refined (InFile e) String)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Refined (InFile e) String
forall {k} (p :: k) a. (Predicate p a, Show a) => a -> Refined p a
refinErr

instance {-# OVERLAPPING #-}
  KnownSymbol e => Arbitrary (Refined (InFile e) [FilePath]) where
  arbitrary :: Gen (Refined (InFile e) [String])
arbitrary =
    (Int -> Gen (Refined (InFile e) [String]))
-> Gen (Refined (InFile e) [String])
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (Refined (InFile e) [String]))
 -> Gen (Refined (InFile e) [String]))
-> (Int -> Gen (Refined (InFile e) [String]))
-> Gen (Refined (InFile e) [String])
forall a b. (a -> b) -> a -> b
$ \Int
n -> [String] -> Refined (InFile e) [String]
forall {k} (p :: k) a. (Predicate p a, Show a) => a -> Refined p a
refinErr ([String] -> Refined (InFile e) [String])
-> Gen [String] -> Gen (Refined (InFile e) [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Gen String) -> [Int] -> Gen [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Int
_ -> Proxy e -> Gen String
forall (e :: Symbol). KnownSymbol e => Proxy e -> Gen String
genFilePathBy (Proxy e -> Gen String) -> Proxy e -> Gen String
forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @e) (Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
n [Int
1::Int ..])

instance {-# OVERLAPPING #-}
  KnownSymbol e => Arbitrary (Refined (InFile e) (NeList FilePath)) where
  arbitrary :: Gen (Refined (InFile e) (NeList String))
arbitrary =
    (Int -> Gen (Refined (InFile e) (NeList String)))
-> Gen (Refined (InFile e) (NeList String))
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen (Refined (InFile e) (NeList String)))
 -> Gen (Refined (InFile e) (NeList String)))
-> (Int -> Gen (Refined (InFile e) (NeList String)))
-> Gen (Refined (InFile e) (NeList String))
forall a b. (a -> b) -> a -> b
$ \Int
n -> NeList String -> Refined (InFile e) (NeList String)
forall {k} (p :: k) a. (Predicate p a, Show a) => a -> Refined p a
refinErr (NeList String -> Refined (InFile e) (NeList String))
-> Gen (NeList String) -> Gen (Refined (InFile e) (NeList String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Gen String) -> NonEmpty Int -> Gen (NeList String)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> NonEmpty a -> m (NonEmpty b)
mapM (\Int
_ -> Proxy e -> Gen String
forall (e :: Symbol). KnownSymbol e => Proxy e -> Gen String
genFilePathBy (Proxy e -> Gen String) -> Proxy e -> Gen String
forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @e) (Int
0 Int -> [Int] -> NonEmpty Int
forall a. a -> [a] -> NonEmpty a
:| Int -> [Int] -> [Int]
forall a. Int -> [a] -> [a]
take Int
n [Int
1::Int ..])

data OutFile (ext :: Symbol)

instance KnownSymbol e => Predicate (OutFile e) String where
  validate :: Proxy (OutFile e) -> String -> Maybe RefineException
validate Proxy (OutFile e)
p String
x =
    let ext :: String
ext = Proxy e -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @e) in
      if String
ext String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"*"
      then
        if String
x String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~  (String
"^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*$" :: String)
        then Maybe RefineException
forall a. Maybe a
Nothing
        else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (OutFile e) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (OutFile e)
p) (Text -> Maybe RefineException) -> Text -> Maybe RefineException
forall a b. (a -> b) -> a -> b
$ Text
"Bad FilePath " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. ToText a => a -> Text
toText String
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"
      else
        if String
x String -> String -> Bool
forall source source1 target.
(RegexMaker Regex CompOption ExecOption source,
 RegexContext Regex source1 target) =>
source1 -> source -> target
=~ (String
"^([.~]?[/])?[^/\x0000-\x001F]+([/][^/\x0000-\x001F]+)*[.]" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
ext String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"$")
        then Maybe RefineException
forall a. Maybe a
Nothing
        else TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (OutFile e) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (OutFile e)
p) (Text -> Maybe RefineException) -> Text -> Maybe RefineException
forall a b. (a -> b) -> a -> b
$ Text
"Bad FilePath " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall a. ToText a => a -> Text
toText String
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"

instance {-# OVERLAPPING #-}
  KnownSymbol e => Arbitrary (Refined (OutFile e) FilePath) where
  arbitrary :: Gen (Refined (OutFile e) String)
arbitrary =
    let ext :: String
ext = Proxy e -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @e) in do
      sv <- RegExp -> Gen String
forall b. SymVal b => RegExp -> Gen b
findStringByRegex
        (String -> RegExp
parse (String -> RegExp) -> String -> RegExp
forall a b. (a -> b) -> a -> b
$ if String
ext String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"*"
          then String
"^[^/\x0000-\x001F]+([.][a-z]{1,4})?$"
          else String
"^[^/\x0000-\x001F]+[.]" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
ext String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"$")
      case refine sv of
        Left RefineException
e -> Text -> Gen (Refined (OutFile e) String)
forall a t. (HasCallStack, IsText t) => t -> a
error (Text -> Gen (Refined (OutFile e) String))
-> Text -> Gen (Refined (OutFile e) String)
forall a b. (a -> b) -> a -> b
$ Text
"Satisfing value [" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
forall b a. (Show a, IsString b) => a -> b
show String
sv Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"] is no valid: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RefineException -> Text
forall b a. (Show a, IsString b) => a -> b
show RefineException
e
        Right Refined (OutFile e) String
vv -> Refined (OutFile e) String -> Gen (Refined (OutFile e) String)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Refined (OutFile e) String
vv

findRefinedStrings :: forall v p m x.
  ( Typeable p
  , MonadWriter [FilePath] m
  , MonadIO m
  , Typeable x
  , Typeable v
  , Data x
  ) => Proxy p -> (v -> [String]) -> x -> m x
findRefinedStrings :: forall {k} v (p :: k) (m :: * -> *) x.
(Typeable p, MonadWriter [String] m, MonadIO m, Typeable x,
 Typeable v, Data x) =>
Proxy p -> (v -> [String]) -> x -> m x
findRefinedStrings Proxy p
_ v -> [String]
f x
x
  | TypeRep a
_rRefined `R.App` rif :: TypeRep b
rif@(R.TypeRep @tif) `R.App` TypeRep b
_rString <- forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.TypeRep @x
  , TypeRep k1
R.TypeRep <- TypeRep b -> TypeRep k1
forall k (a :: k). TypeRep a -> TypeRep k
R.typeRepKind TypeRep b
rif
  , Just x :~: Refined b v
Refl <- forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
forall a b. (Typeable a, Typeable b) => Maybe (a :~: b)
eqT @x @(Refined tif v)
  , TypeRep a
rInFile `R.App` TypeRep b
_rExt <- forall (a :: k1). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
R.TypeRep @tif
  , Just a :~~: p
R.HRefl <- TypeRep a -> TypeRep p -> Maybe (a :~~: p)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
R.eqTypeRep  TypeRep a
rInFile (TypeRep p
forall {k} (a :: k). Typeable a => TypeRep a
R.typeRep :: R.TypeRep p)
  = let fp :: v
fp = Refined (p b) v -> v
forall {k} (p :: k) x. Refined p x -> x
unrefine x
Refined (p b) v
x in [String] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (v -> [String]
f v
fp) m () -> m x -> m x
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure x
x
  | Bool
otherwise = x -> m x
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure x
x

instance RefinedInArgLocator (Refined (InFile e) FilePath) where
  locateRefinedInArg :: forall (m :: * -> *).
Proxy (Refined (InFile e) String) -> ArgCollector m
locateRefinedInArg Proxy (Refined (InFile e) String)
_ = Proxy InFile -> (String -> [String]) -> v -> m v
forall {k} v (p :: k) (m :: * -> *) x.
(Typeable p, MonadWriter [String] m, MonadIO m, Typeable x,
 Typeable v, Data x) =>
Proxy p -> (v -> [String]) -> x -> m x
findRefinedStrings (forall {k} (t :: k). Proxy t
forall (t :: Symbol -> *). Proxy t
Proxy @InFile) String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure
instance RefinedInArgLocator (Refined (InFile e) (NeList FilePath)) where
  locateRefinedInArg :: forall (m :: * -> *).
Proxy (Refined (InFile e) (NeList String)) -> ArgCollector m
locateRefinedInArg Proxy (Refined (InFile e) (NeList String))
_ = forall {k} v (p :: k) (m :: * -> *) x.
(Typeable p, MonadWriter [String] m, MonadIO m, Typeable x,
 Typeable v, Data x) =>
Proxy p -> (v -> [String]) -> x -> m x
forall v (p :: Symbol -> *) (m :: * -> *) x.
(Typeable p, MonadWriter [String] m, MonadIO m, Typeable x,
 Typeable v, Data x) =>
Proxy p -> (v -> [String]) -> x -> m x
findRefinedStrings @(NeList FilePath) (forall {k} (t :: k). Proxy t
forall (t :: Symbol -> *). Proxy t
Proxy @InFile) NeList String -> [String]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList
instance RefinedInArgLocator (Refined (InFile e) [FilePath]) where
  locateRefinedInArg :: forall (m :: * -> *).
Proxy (Refined (InFile e) [String]) -> ArgCollector m
locateRefinedInArg Proxy (Refined (InFile e) [String])
_ = Proxy InFile -> ([String] -> [String]) -> v -> m v
forall {k} v (p :: k) (m :: * -> *) x.
(Typeable p, MonadWriter [String] m, MonadIO m, Typeable x,
 Typeable v, Data x) =>
Proxy p -> (v -> [String]) -> x -> m x
findRefinedStrings (forall {k} (t :: k). Proxy t
forall (t :: Symbol -> *). Proxy t
Proxy @InFile) [String] -> [String]
forall a. a -> a
id
instance RefinedOutArgLocator (Refined (OutFile e) FilePath) where
  locateRefinedOutArg :: forall (m :: * -> *).
Proxy (Refined (OutFile e) String) -> ArgCollector m
locateRefinedOutArg Proxy (Refined (OutFile e) String)
_ = Proxy OutFile -> (String -> [String]) -> v -> m v
forall {k} v (p :: k) (m :: * -> *) x.
(Typeable p, MonadWriter [String] m, MonadIO m, Typeable x,
 Typeable v, Data x) =>
Proxy p -> (v -> [String]) -> x -> m x
findRefinedStrings (forall {k} (t :: k). Proxy t
forall (t :: Symbol -> *). Proxy t
Proxy @OutFile) String -> [String]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure