Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 4 additions & 5 deletions src/Replica/Command/Help.idr
Original file line number Diff line number Diff line change
Expand Up @@ -25,18 +25,17 @@ help = MkHelp
}

parseHelp' : Help -> List1 String -> ParseResult Help
parseHelp' help xs@(name:::ys) = maybe
(InvalidOption (pure help) xs)
( const $ case ys of
parseHelp' help xs@(name:::ys) =
if name /= help.name
then InvalidOption (pure help) xs
else case ys of
[] => Done help
(next::ys') => let
subs = foldMap (forget . snd) help.chapter
in foldl
(\res, h => res <+> parseHelp' h (assert_smaller xs (next:::ys')))
(InvalidOption (pure help) $ pure "Cannot find help for '\{unwords ys}'")
subs
)
$ guard $ name == help.name

export
parseHelp : List1 String -> ParseResult Help
Expand Down
12 changes: 12 additions & 0 deletions src/Replica/Command/Run.idr
Original file line number Diff line number Diff line change
Expand Up @@ -67,6 +67,7 @@ Show RunCommand where
, show x.global
]

||| `Run` option that handle if we run in interactive mode
interactivePart : Part (Builder RunCommand') Bool
interactivePart = inj $ MkOption
(singleton $ MkMod (singleton "interactive") ['i'] (Left True)
Expand All @@ -79,6 +80,7 @@ interactivePart = inj $ MkOption
(\x => {interactive := Right x})
(const $ const "Contradictory values for interactive")

||| `Run` option that handle if we display execution time
timingPart : Part (Builder RunCommand') Bool
timingPart = inj $ MkOption
(toList1
Expand All @@ -96,6 +98,7 @@ timingPart = inj $ MkOption
(\x => {timing := Right x})
(const $ const "Contradictory values for timing")

||| `Run` option that define the working directory for the tests
workingDirPart : Part (Builder RunCommand') String
workingDirPart = inj $ MkOption
(singleton $ MkMod ("working-dir" ::: ["wdir"]) ['w']
Expand All @@ -110,6 +113,7 @@ workingDirPart = inj $ MkOption
(\x, y => "More than one working directony were given: \{y}, \{x}")


||| `Run` option for the parralelism level
threadsPart : Part (Builder RunCommand') Nat
threadsPart = inj $ MkOption
(singleton $ MkMod (singleton "threads") ['x']
Expand All @@ -123,6 +127,7 @@ threadsPart = inj $ MkOption
(\x => {threads := Right x})
(\x, y => "More than one threads values were given: \{show y}, \{show x}")

||| `Run` option to decide if we stop execution on the first failure
punitivePart : Part (Builder RunCommand') Bool
punitivePart = inj $ MkOption
(singleton $ MkMod ("punitive" ::: ["fail-fast"]) ['p']
Expand All @@ -136,6 +141,7 @@ punitivePart = inj $ MkOption
(\x => {punitive := Right x})
(const $ const "Contradictory values for punitive mode")

||| `Run` option to decide if we hide successful tests in the report
hideSuccessPart : Part (Builder RunCommand') Bool
hideSuccessPart = inj $ MkOption
(singleton $ MkMod (toList1 ["hide-success", "fail-only"]) []
Expand All @@ -149,6 +155,7 @@ hideSuccessPart = inj $ MkOption
(\x => {hideSuccess := Right x})
(const $ const "Contradictory values for hide success mode")

||| `RunCommand` option parser
optParseRun : OptParse (Builder RunCommand') RunCommand
optParseRun =
[| MkRunCommand
Expand All @@ -162,6 +169,7 @@ optParseRun =
(embed global (\x => {global := x}) optParseGlobal)
|]

||| Default option for the `RunCommand`
defaultRun : Default RunCommand'
defaultRun = MkRunCommand
(defaultPart workingDirPart)
Expand All @@ -173,10 +181,12 @@ defaultRun = MkRunCommand
defaultFilter
defaultGlobal

||| Add Global config to a RunCommand config
withGivenGlobal : Default RunCommand' -> Default Global' -> Default RunCommand'
withGivenGlobal x g = {global := g <+> defaultGlobal} x


||| Parser for `replica run` command
parseRun' : Help -> Default Global' -> List String -> ParseResult RunCommand
parseRun' help g xs = do
builder <- parse
Expand All @@ -186,13 +196,15 @@ parseRun' help g xs = do
xs
maybe (InvalidMix "No test file given") Done $ build builder

||| Help for `replica run` command
export
helpRun : Help
helpRun = commandHelp {b = Builder RunCommand'}
(pure "replica") "run" "Run tests from a Replica JSON file"
optParseRun
(Just "JSON_TEST_FILE(S)")

||| Help for `replica test` command
export
helpTest : Help
helpTest = commandHelp {b = Builder RunCommand'}
Expand Down
32 changes: 25 additions & 7 deletions src/Replica/Option/Types.idr
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,17 @@ import public Replica.Other.Free
%default total


||| Transform a string into a CLI long option
export
prefixLongOption : String -> String
prefixLongOption : (optionName : String) -> String
prefixLongOption = ("--" <+>)

||| Transform a char into a CLI short option
export
prefixShortOption : Char -> String
prefixShortOption : (optionChar : Char) -> String
prefixShortOption x = pack ['-',x]

||| Name and parsing of a CLI option
public export
record Value a where
constructor MkValue
Expand All @@ -32,6 +35,7 @@ export
Functor Value where
map func x = MkValue x.name (map func . x.parser)

||| Describe a modifiers of an option
public export
record Mod a where
constructor MkMod
Expand All @@ -46,13 +50,15 @@ Functor Mod where
(bimap func (map func) x.param)
x.description

||| An option has a list of modifiers, a default value and a setter
public export
record Option b a where
constructor MkOption
mods : List1 (Mod a)
defaultValue : a
setter : a -> b -> Either String b

||| Reuse an existing option in a different context
export
embedOption : (c -> b) -> (b -> c -> c) -> Option b a -> Option c a
embedOption f g x = MkOption x.mods x.defaultValue (embed f g x.setter)
Expand All @@ -62,6 +68,7 @@ embedOption f g x = MkOption x.mods x.defaultValue (embed f g x.setter)

namespace Param

||| A `Param` is the description of a parameter
public export
record Param b a where
constructor MkParam
Expand All @@ -88,10 +95,13 @@ namespace Param

namespace Parts

||| A `Part` can be a Param or an option
||| It's used to list indifferently options and parameters as a part of a command.
public export
Part : Type -> Type -> Type
Part b a = Union (\p => p b a) [Param, Option]

||| Reuse a generic `Part` in a specific setting
export
embedPart : (c -> b) -> (b -> c -> c) -> Part b a -> Part c a
embedPart get set x = let
Expand All @@ -100,20 +110,24 @@ namespace Parts
v = decomp0 x1
in inj $ embedOption get set v

||| A Free applicative of Parts
public export
OptParse : Type -> Type -> Type
OptParse = Ap . Part

||| Reuse a generic `OptParse` in a specific setting
export
embed : (c -> b) -> (b -> c -> c) -> OptParse b a -> OptParse c a
embed get set (Pure x) = Pure x
embed get set (MkAp x y) = MkAp (embedPart get set x) $ embed get set y

namespace Parser

||| Generic parser type
Parser : (a : Type) -> Type
Parser a = List String -> Maybe (List String, a)

||| Parse a` `Mod`
modParser : Mod a -> Parser a
modParser m [] = Nothing
modParser m (x::xs) = let
Expand All @@ -127,22 +141,25 @@ namespace Parser
[] => Nothing
(y::ys) => MkPair ys <$> v.parser y

||| Parse a whole `Option`
optionParser : Option b a -> Parser (b -> Either String b)
optionParser x xs = map x.setter <$> choiceMap (flip modParser xs) x.mods

||| Parse a `Part`
partParser : Part b a -> Parser (b -> Either String b)
partParser x xs = let
Left x1 = decomp x
| Right v => MkPair [] . v.setter <$> v.parser xs
in optionParser (decomp0 x1) xs

||| Explain why a CLI call is invalid
public export
data ParseResult a
-- = InvalidCommand (List1 String)
= InvalidOption (Maybe Help) (List1 String)
| InvalidMix String -- reason
| Done a

||| Explain why a specific option is invalid
public export
data ParsingFailure : ParseResult a -> Type where
OptionFailure : ParsingFailure (InvalidOption help xs)
Expand Down Expand Up @@ -174,6 +191,7 @@ namespace Parser
InvalidMix reason >>= f = InvalidMix reason
Done x >>= f = f x

||| Parse a CLI call
export
parse :
Help ->
Expand Down Expand Up @@ -204,9 +222,9 @@ namespace Default
defaultPart : Part b a -> Maybe a
defaultPart x = let
Left x1 = decomp x
| Right v => defaultParam v
v = decomp0 x1
in defaultOption v
| Right param => defaultParam param
option = decomp0 x1
in defaultOption option

namespace Help

Expand All @@ -215,7 +233,7 @@ namespace Help
optionName long short param =
either (flip const) (\v => (++ " \{v.name}")) param $
(concat $ intersperse ", " $
map ("--" ++) long ++ map (\c => pack ['-',c]) short)
map prefixLongOption long ++ map prefixShortOption short)

modHelp : Mod a -> Help
modHelp x = MkHelp
Expand Down