From fbeed99ff7c3760de6f1d4256f63b43d14dbb800 Mon Sep 17 00:00:00 2001
From: Nicolas Biri <nicolas@biri.name>
Date: Thu, 18 Dec 2025 23:35:34 +0100
Subject: [PATCH] Add a few comments and minor refactoring

---
 src/Replica/Command/Help.idr |  9 ++++-----
 src/Replica/Command/Run.idr  | 12 ++++++++++++
 src/Replica/Option/Types.idr | 32 +++++++++++++++++++++++++-------
 3 files changed, 41 insertions(+), 12 deletions(-)

diff --git a/src/Replica/Command/Help.idr b/src/Replica/Command/Help.idr
index e4e5329..ad82bc8 100644
--- a/src/Replica/Command/Help.idr
+++ b/src/Replica/Command/Help.idr
@@ -25,9 +25,10 @@ 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
@@ -35,8 +36,6 @@ parseHelp' help xs@(name:::ys) = maybe
              (\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
diff --git a/src/Replica/Command/Run.idr b/src/Replica/Command/Run.idr
index df7293a..4b17041 100644
--- a/src/Replica/Command/Run.idr
+++ b/src/Replica/Command/Run.idr
@@ -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)
@@ -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
@@ -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']
@@ -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']
@@ -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']
@@ -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"]) []
@@ -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
@@ -162,6 +169,7 @@ optParseRun =
        (embed global (\x => {global := x}) optParseGlobal)
     |]
 
+||| Default option for the `RunCommand`
 defaultRun : Default RunCommand'
 defaultRun = MkRunCommand
        (defaultPart workingDirPart)
@@ -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
@@ -186,6 +196,7 @@ 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'}
@@ -193,6 +204,7 @@ helpRun = commandHelp {b = Builder RunCommand'}
   optParseRun
   (Just "JSON_TEST_FILE(S)")
 
+||| Help for `replica test` command
 export
 helpTest : Help
 helpTest = commandHelp {b = Builder RunCommand'}
diff --git a/src/Replica/Option/Types.idr b/src/Replica/Option/Types.idr
index a73e9c5..9823203 100644
--- a/src/Replica/Option/Types.idr
+++ b/src/Replica/Option/Types.idr
@@ -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
@@ -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
@@ -46,6 +50,7 @@ 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
@@ -53,6 +58,7 @@ record Option b a where
   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)
@@ -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
@@ -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
@@ -100,10 +110,12 @@ 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
@@ -111,9 +123,11 @@ 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
@@ -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)
@@ -174,6 +191,7 @@ namespace Parser
     InvalidMix reason >>= f = InvalidMix reason
     Done x >>= f = f x
 
+  ||| Parse a CLI call
   export
   parse :
     Help ->
@@ -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
 
@@ -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