{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Options.Harg.Subcommands
( Subcommands (..),
)
where
import qualified Barbies as B
import Data.Functor.Compose (Compose (..))
import Data.Kind (Type)
import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import qualified Options.Applicative as Optparse
import Options.Harg.Cmdline (mkOptparseParser)
import Options.Harg.Het.All (All)
import Options.Harg.Het.HList (AssocListF (..))
import Options.Harg.Het.Nat
import Options.Harg.Het.Proofs (Proof (..), hgcastWith, type (++))
import Options.Harg.Het.Variant (InjectPosF (..), VariantF)
import Options.Harg.Sources (accumSourceResults)
import Options.Harg.Sources.Types
import Options.Harg.Types
class
Subcommands
(ts :: [Symbol])
(xs :: [(Type -> Type) -> Type])
where
mapSubcommand ::
( All (RunSource s) xs,
Applicative f
) =>
s ->
AssocListF ts xs (Compose Opt f) ->
([SourceRunError], [Optparse.Mod Optparse.CommandFields (VariantF xs f)])
instance ExplSubcommands Z ts xs '[] => Subcommands ts xs where
mapSubcommand :: s
-> AssocListF ts xs (Compose Opt f)
-> ([SourceRunError], [Mod CommandFields (VariantF xs f)])
mapSubcommand = SNat 'Z
-> s
-> AssocListF ts xs (Compose Opt f)
-> ([SourceRunError], [Mod CommandFields (VariantF ('[] ++ xs) f)])
forall (n :: Nat) (ts :: [Symbol]) (xs :: [(* -> *) -> *])
(acc :: [(* -> *) -> *]) s (f :: * -> *).
(ExplSubcommands n ts xs acc, All (RunSource s) xs,
Applicative f) =>
SNat n
-> s
-> AssocListF ts xs (Compose Opt f)
-> ([SourceRunError], [Mod CommandFields (VariantF (acc ++ xs) f)])
explMapSubcommand @Z @ts @xs @'[] SNat 'Z
SZ
class
ExplSubcommands
(n :: Nat)
(ts :: [Symbol])
(xs :: [(Type -> Type) -> Type])
(acc :: [(Type -> Type) -> Type])
where
explMapSubcommand ::
( All (RunSource s) xs,
Applicative f
) =>
SNat n ->
s ->
AssocListF ts xs (Compose Opt f) ->
([SourceRunError], [Optparse.Mod Optparse.CommandFields (VariantF (acc ++ xs) f)])
instance ExplSubcommands n '[] '[] acc where
explMapSubcommand :: SNat n
-> s
-> AssocListF '[] '[] (Compose Opt f)
-> ([SourceRunError],
[Mod CommandFields (VariantF (acc ++ '[]) f)])
explMapSubcommand _ _ _ = ([], [])
instance
( ExplSubcommands (S n) ts xs (as ++ '[x]),
InjectPosF n x (as ++ (x ': xs)),
B.TraversableB x,
B.ApplicativeB x,
KnownSymbol t,
Proof as x xs
) =>
ExplSubcommands n (t ': ts) (x ': xs) as
where
explMapSubcommand :: SNat n
-> s
-> AssocListF (t : ts) (x : xs) (Compose Opt f)
-> ([SourceRunError],
[Mod CommandFields (VariantF (as ++ (x : xs)) f)])
explMapSubcommand n :: SNat n
n srcs :: s
srcs (ACons opt :: x (Compose Opt f)
opt opts :: AssocListF ts xs (Compose Opt f)
opts) =
([SourceRunError]
thisErr [SourceRunError] -> [SourceRunError] -> [SourceRunError]
forall a. [a] -> [a] -> [a]
++ [SourceRunError]
restErr, Mod CommandFields (VariantF (as ++ (x : xs)) f)
sc Mod CommandFields (VariantF (as ++ (x : xs)) f)
-> [Mod CommandFields (VariantF (as ++ (x : xs)) f)]
-> [Mod CommandFields (VariantF (as ++ (x : xs)) f)]
forall a. a -> [a] -> [a]
: [Mod CommandFields (VariantF (as ++ (x : xs)) f)]
rest)
where
(thisErr :: [SourceRunError]
thisErr, sc :: Mod CommandFields (VariantF (as ++ (x : xs)) f)
sc) =
([SourceRunError], Mod CommandFields (VariantF (as ++ (x : xs)) f))
subcommand
(restErr :: [SourceRunError]
restErr, rest :: [Mod CommandFields (VariantF (as ++ (x : xs)) f)]
rest) =
((as ++ (x : xs)) :~~: ((as ++ '[x]) ++ xs))
-> (((as ++ (x : xs)) ~~ ((as ++ '[x]) ++ xs)) =>
([SourceRunError],
[Mod CommandFields (VariantF (as ++ (x : xs)) f)]))
-> ([SourceRunError],
[Mod CommandFields (VariantF (as ++ (x : xs)) f)])
forall k k' (a :: k) (b :: k') r.
(a :~~: b) -> ((a ~~ b) => r) -> r
hgcastWith (Proof as x xs => (as ++ (x : xs)) :~~: ((as ++ '[x]) ++ xs)
forall k (xs :: [k]) (y :: k) (zs :: [k]).
Proof xs y zs =>
(xs ++ (y : zs)) :~~: ((xs ++ '[y]) ++ zs)
proof @as @x @xs) ((((as ++ (x : xs)) ~~ ((as ++ '[x]) ++ xs)) =>
([SourceRunError],
[Mod CommandFields (VariantF (as ++ (x : xs)) f)]))
-> ([SourceRunError],
[Mod CommandFields (VariantF (as ++ (x : xs)) f)]))
-> (((as ++ (x : xs)) ~~ ((as ++ '[x]) ++ xs)) =>
([SourceRunError],
[Mod CommandFields (VariantF (as ++ (x : xs)) f)]))
-> ([SourceRunError],
[Mod CommandFields (VariantF (as ++ (x : xs)) f)])
forall a b. (a -> b) -> a -> b
$
SNat ('S n)
-> s
-> AssocListF ts xs (Compose Opt f)
-> ([SourceRunError],
[Mod CommandFields (VariantF ((as ++ '[x]) ++ xs) f)])
forall (n :: Nat) (ts :: [Symbol]) (xs :: [(* -> *) -> *])
(acc :: [(* -> *) -> *]) s (f :: * -> *).
(ExplSubcommands n ts xs acc, All (RunSource s) xs,
Applicative f) =>
SNat n
-> s
-> AssocListF ts xs (Compose Opt f)
-> ([SourceRunError], [Mod CommandFields (VariantF (acc ++ xs) f)])
explMapSubcommand
@(S n)
@ts
@xs
@(as ++ '[x])
(SNat n -> SNat ('S n)
forall (n :: Nat). SNat n -> SNat ('S n)
SS SNat n
n)
s
srcs
AssocListF ts xs (Compose Opt f)
AssocListF ts xs (Compose Opt f)
opts
subcommand :: ([SourceRunError], Mod CommandFields (VariantF (as ++ (x : xs)) f))
subcommand =
let (errs :: [SourceRunError]
errs, src :: [x (Compose Maybe f)]
src) =
[Either SourceRunError (x (Compose SourceRunResult f))]
-> ([SourceRunError], [x (Compose Maybe f)])
forall (a :: (* -> *) -> *) (f :: * -> *).
TraversableB a =>
[Either SourceRunError (a (Compose SourceRunResult f))]
-> ([SourceRunError], [a (Compose Maybe f)])
accumSourceResults ([Either SourceRunError (x (Compose SourceRunResult f))]
-> ([SourceRunError], [x (Compose Maybe f)]))
-> [Either SourceRunError (x (Compose SourceRunResult f))]
-> ([SourceRunError], [x (Compose Maybe f)])
forall a b. (a -> b) -> a -> b
$ s
-> x (Compose Opt f)
-> [Either SourceRunError (x (Compose SourceRunResult f))]
forall s (a :: (* -> *) -> *) (f :: * -> *).
(RunSource s a, Applicative f) =>
s
-> a (Compose Opt f)
-> [Either SourceRunError (a (Compose SourceRunResult f))]
runSource s
srcs x (Compose Opt f)
opt
parser :: Parser (x f)
parser =
[x (Compose Maybe f)] -> x (Compose Opt f) -> Parser (x f)
forall (f :: * -> *) (a :: (* -> *) -> *).
(Applicative f, TraversableB a, ApplicativeB a) =>
[a (Compose Maybe f)] -> a (Compose Opt f) -> Parser (a f)
mkOptparseParser [x (Compose Maybe f)]
src x (Compose Opt f)
opt
tag :: String
tag =
Proxy t -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Proxy t
forall k (t :: k). Proxy t
Proxy :: Proxy t)
cmd :: Mod CommandFields (VariantF (as ++ (x : xs)) f)
cmd =
String
-> ParserInfo (VariantF (as ++ (x : xs)) f)
-> Mod CommandFields (VariantF (as ++ (x : xs)) f)
forall a. String -> ParserInfo a -> Mod CommandFields a
Optparse.command String
tag (ParserInfo (VariantF (as ++ (x : xs)) f)
-> Mod CommandFields (VariantF (as ++ (x : xs)) f))
-> ParserInfo (VariantF (as ++ (x : xs)) f)
-> Mod CommandFields (VariantF (as ++ (x : xs)) f)
forall a b. (a -> b) -> a -> b
$
SNat n -> x f -> VariantF (as ++ (x : xs)) f
forall (n :: Nat) (x :: (* -> *) -> *) (xs :: [(* -> *) -> *])
(f :: * -> *).
InjectPosF n x xs =>
SNat n -> x f -> VariantF xs f
injectPosF SNat n
n
(x f -> VariantF (as ++ (x : xs)) f)
-> ParserInfo (x f) -> ParserInfo (VariantF (as ++ (x : xs)) f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (x f) -> InfoMod (x f) -> ParserInfo (x f)
forall a. Parser a -> InfoMod a -> ParserInfo a
Optparse.info (Parser (x f -> x f)
forall a. Parser (a -> a)
Optparse.helper Parser (x f -> x f) -> Parser (x f) -> Parser (x f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (x f)
parser) InfoMod (x f)
forall a. Monoid a => a
mempty
in ([SourceRunError]
errs, Mod CommandFields (VariantF (as ++ (x : xs)) f)
cmd)