Skip to content

Support accumulating repeatable flags #92

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mirryi wants to merge 1 commit into
base: main
Choose a base branch
from
+129 −68
Open

Support accumulating repeatable flags #92

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
28 changes: 23 additions & 5 deletions Cli/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -301,6 +301,9 @@ section Configuration
`Unit` is used to designate flags without a parameter.
-/
type : ParamType
/-- Whether the flag may be passed multiple times, accumulating its values.
Only meaningful for an `Array τ`-typed flag. -/
repeatable : Bool := false
deriving Inhabited, BEq, Repr

namespace Flag
Expand Down Expand Up @@ -1007,7 +1010,7 @@ section Macro

syntax variableArg := colGe "..." literalIdent " : " term "; " nameableStringArg

syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " nameableStringArg
syntax flag := colGe literalIdent ("," literalIdent)? "..."? (" : " term)? "; " nameableStringArg

syntax "`[Cli|\n"
literalIdent runFun "; " ("[" nameableStringArg "]")?
Expand Down Expand Up @@ -1047,8 +1050,13 @@ section Macro
`(Arg.mk $(← expandLiteralIdent name) $(← expandNameableStringArg description) $type)

meta def expandFlag (flag : TSyntax `Cli.flag) : MacroM Term := do
let `(Cli.flag| $flagName1 $[, $flagName2]? $[ : $type]?; $description) := flag
| Macro.throwUnsupported
let (flagName1, flagName2, type, description, repeatable) ←
match flag with
| `(Cli.flag| $flagName1 $[, $flagName2]? ... $[ : $type]?; $description) =>
pure (flagName1, flagName2, type, description, true)
| `(Cli.flag| $flagName1 $[, $flagName2]? $[ : $type]?; $description) =>
pure (flagName1, flagName2, type, description, false)
| _ => Macro.throwUnsupported
let mut shortName := quote (none : Option String)
let mut longName := flagName1
if let some flagName2 := flagName2 then
Expand All @@ -1059,7 +1067,7 @@ section Macro
match type with
| none => unitType
| some type => type
`(Flag.mk $shortName $(← expandLiteralIdent longName) $(← expandNameableStringArg description) $type)
`(Flag.mk $shortName $(← expandLiteralIdent longName) $(← expandNameableStringArg description) $type $(quote repeatable))

macro_rules
| `(`[Cli|
Expand Down Expand Up @@ -1155,7 +1163,10 @@ section Info
let columns : Array (String × String) := c.meta.flags.map fun flag =>
let shortName? : Option String := do return s!"-{← flag.shortName?}"
let names : String := optJoin #[optStr shortName?, s!"--{flag.longName}"] ", "
let type? : Option String := if ¬ flag.isParamless then s!": {flag.type.name}" else none
let type? : Option String :=
if ¬ flag.isParamless then
(s!": {flag.type.name}" ++ (if flag.repeatable then " ..." else "") : String)
else none
(line #[names, optStr type?], flag.description)
renderTable "FLAGS" columns (emptyTablePlaceholder? := "None")

Expand Down Expand Up @@ -1336,6 +1347,11 @@ section Parsing
private def setParent (c? : Option Cmd) : ParseM Unit := do
set { ← get with parent? := c? }
private def pushParsedFlag (parsedFlag : Parsed.Flag) : ParseM Unit := do
if parsedFlag.flag.repeatable then
if let some i := (← parsedFlags).findIdx? (·.flag.longName = parsedFlag.flag.longName) then
let merged := { parsedFlag with value := (← parsedFlags)[i]!.value ++ "," ++ parsedFlag.value }
set { ← get with parsedFlags := (← parsedFlags).set! i merged }
return
set { ← get with parsedFlags := (← parsedFlags).push parsedFlag }
private def pushParsedPositionalArg (parsedPositionalArg : Parsed.Arg) : ParseM Unit := do
set { ← get with parsedPositionalArgs := (← parsedPositionalArgs).push parsedPositionalArg }
Expand Down Expand Up @@ -1380,6 +1396,8 @@ section Parsing
return none

private def ensureFlagUnique (flag : Flag) (inputFlag : InputFlag) : ParseM Unit := do
if flag.repeatable then
return
if (← parsedFlags).find? (·.flag.longName = flag.longName) |>.isSome then
throw <| ← parseError <| duplicateFlag flag inputFlag

Expand Down
64 changes: 33 additions & 31 deletions CliTest/Example.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,17 +42,18 @@ def exampleCmd : Cmd := `[Cli|
"This string denotes the description of `exampleCmd`."

FLAGS:
verbose; "Declares a flag `--verbose`. This is the description of the flag."
i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
that takes an argument of type `Nat`."
module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
which can be used to reference Lean modules like `Init.Data.Array` \
or Lean files using a relative path like `Init/Data/Array.lean`."
"set-paths" : Array String; "Declares a flag `--set-paths` \
that takes an argument of type `Array Nat`. \
Quotation marks allow the use of hyphens."
verbose; "Declares a flag `--verbose`. This is the description of the flag."
i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
that takes an argument of type `Nat`."
module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
which can be used to reference Lean modules like `Init.Data.Array` \
or Lean files using a relative path like `Init/Data/Array.lean`."
"set-paths" ... : Array String; "Declares a flag `--set-paths` \
that takes an argument of type `Array String`. \
The trailing `...` makes it repeatable: passing it \
multiple times accumulates the values."

ARGS:
input : String; "Declares a positional argument <input> \
Expand All @@ -75,7 +76,7 @@ def exampleCmd : Cmd := `[Cli|
def main (args : List String) : IO UInt32 :=
exampleCmd.validate args

#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1,path2,path3 input output1 output2".splitOn " "
#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1 --set-paths=path2,path3 input output1 output2".splitOn " "
/-
Yields:
Input: input
Expand Down Expand Up @@ -118,25 +119,26 @@ Yields:
exampleCmd [SUBCOMMAND] [FLAGS] <input> <outputs>...

FLAGS:
-h, --help Prints this message.
--version Prints the version.
--verbose Declares a flag `--verbose`. This is the
description of the flag.
-i, --invert Declares a flag `--invert` with an associated
short alias `-i`.
-o, --optimize Declares a flag `--optimize` with an associated
short alias `-o`.
-p, --priority : Nat Declares a flag `--priority` with an associated
short alias `-p` that takes an argument of type
`Nat`. [Default: `0`]
--module : ModuleName Declares a flag `--module` that takes an
argument of type `ModuleName` which can be used
to reference Lean modules like `Init.Data.Array`
or Lean files using a relative path like
`Init/Data/Array.lean`.
--set-paths : Array String Declares a flag `--set-paths` that takes an
argument of type `Array Nat`. Quotation marks
allow the use of hyphens.
-h, --help Prints this message.
--version Prints the version.
--verbose Declares a flag `--verbose`. This is the
description of the flag.
-i, --invert Declares a flag `--invert` with an
associated short alias `-i`.
-o, --optimize Declares a flag `--optimize` with an
associated short alias `-o`.
-p, --priority : Nat Declares a flag `--priority` with an
associated short alias `-p` that takes an
argument of type `Nat`. [Default: `0`]
--module : ModuleName Declares a flag `--module` that takes an
argument of type `ModuleName` which can be
used to reference Lean modules like
`Init.Data.Array` or Lean files using a
relative path like `Init/Data/Array.lean`.
--set-paths : Array String ... Declares a flag `--set-paths` that takes an
argument of type `Array String`. The
trailing `...` makes it repeatable: passing
it multiple times accumulates the values.

ARGS:
input : String Declares a positional argument <input> that takes an
Expand Down
39 changes: 39 additions & 0 deletions CliTest/Tests.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,45 @@ def testCmd : Cmd := `[Cli|
require! #["typed1"]
]

def testRepeatedCmd : Cmd := `[Cli|
repeatedcommand VIA doNothing;
"tests repeatable flags"

FLAGS:
t, tag ... : Array String; "a repeatable flag"
f, other; "a normal flag"
]

/--
info: "cmd: repeatedcommand; flags: #[--tag=a]; positionalArgs: #[]; variableArgs: #[]"
-/
#guard_msgs in
#eval testRepeatedCmd.processParsed "-t a"

/--
info: "repeatedcommand\ntests repeatable flags\n\nUSAGE:\n repeatedcommand [FLAGS]\n\nFLAGS:\n -h, --help Prints this message.\n -t, --tag : Array String ... a repeatable flag\n -f, --other a normal flag"
-/
#guard_msgs in
#eval testRepeatedCmd.help

/--
info: "cmd: repeatedcommand; flags: #[--tag=a,b,c]; positionalArgs: #[]; variableArgs: #[]"
-/
#guard_msgs in
#eval testRepeatedCmd.processParsed "-t a -t b -t c"

/--
info: "cmd: repeatedcommand; flags: #[--tag=a,b,c]; positionalArgs: #[]; variableArgs: #[]"
-/
#guard_msgs in
#eval testRepeatedCmd.processParsed "-t a,b -t c"

/--
info: "cmd: repeatedcommand; flags: #[--tag=a,b, --other]; positionalArgs: #[]; variableArgs: #[]"
-/
#guard_msgs in
#eval testRepeatedCmd.processParsed "-t a -f -t b"

section ValidInputs

/--
Expand Down
66 changes: 34 additions & 32 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,17 +26,18 @@ def exampleCmd : Cmd := `[Cli|
"This string denotes the description of `exampleCmd`."

FLAGS:
verbose; "Declares a flag `--verbose`. This is the description of the flag."
i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
that takes an argument of type `Nat`."
module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
which can be used to reference Lean modules like `Init.Data.Array` \
or Lean files using a relative path like `Init/Data/Array.lean`."
"set-paths" : Array String; "Declares a flag `--set-paths` \
that takes an argument of type `Array Nat`. \
Quotation marks allow the use of hyphens."
verbose; "Declares a flag `--verbose`. This is the description of the flag."
i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
that takes an argument of type `Nat`."
module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
which can be used to reference Lean modules like `Init.Data.Array` \
or Lean files using a relative path like `Init/Data/Array.lean`."
"set-paths" ... : Array String; "Declares a flag `--set-paths` \
that takes an argument of type `Array String`. \
The trailing `...` makes it repeatable: passing it \
multiple times accumulates the values."

ARGS:
input : String; "Declares a positional argument <input> \
Expand Down Expand Up @@ -93,7 +94,7 @@ Below you can find some simple examples of how to pass user input to the Cli lib
def main (args : List String) : IO UInt32 :=
exampleCmd.validate args

#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1,path2,path3 input output1 output2".splitOn " "
#eval main <| "-i -o -p 1 --module=Lean.Compiler --set-paths=path1 --set-paths=path2,path3 input output1 output2".splitOn " "
/-
Yields:
Input: input
Expand Down Expand Up @@ -137,25 +138,26 @@ USAGE:
exampleCmd [SUBCOMMAND] [FLAGS] <input> <outputs>...

FLAGS:
-h, --help Prints this message.
--version Prints the version.
--verbose Declares a flag `--verbose`. This is the
description of the flag.
-i, --invert Declares a flag `--invert` with an associated
short alias `-i`.
-o, --optimize Declares a flag `--optimize` with an associated
short alias `-o`.
-p, --priority : Nat Declares a flag `--priority` with an associated
short alias `-p` that takes an argument of type
`Nat`. [Default: `0`]
--module : ModuleName Declares a flag `--module` that takes an
argument of type `ModuleName` which can be used
to reference Lean modules like `Init.Data.Array`
or Lean files using a relative path like
`Init/Data/Array.lean`.
--set-paths : Array String Declares a flag `--set-paths` that takes an
argument of type `Array String`. Quotation marks
allow the use of hyphens.
-h, --help Prints this message.
--version Prints the version.
--verbose Declares a flag `--verbose`. This is the
description of the flag.
-i, --invert Declares a flag `--invert` with an
associated short alias `-i`.
-o, --optimize Declares a flag `--optimize` with an
associated short alias `-o`.
-p, --priority : Nat Declares a flag `--priority` with an
associated short alias `-p` that takes an
argument of type `Nat`. [Default: `0`]
--module : ModuleName Declares a flag `--module` that takes an
argument of type `ModuleName` which can be
used to reference Lean modules like
`Init.Data.Array` or Lean files using a
relative path like `Init/Data/Array.lean`.
--set-paths : Array String ... Declares a flag `--set-paths` that takes an
argument of type `Array String`. The
trailing `...` makes it repeatable: passing
it multiple times accumulates the values.

ARGS:
input : String Declares a positional argument <input> that takes an
Expand Down Expand Up @@ -189,7 +191,7 @@ syntax positionalArg := colGe literalIdent " : " term "; " nameableStringArg

syntax variableArg := colGe "..." literalIdent " : " term "; " nameableStringArg

syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " nameableStringArg
syntax flag := colGe literalIdent ("," literalIdent)? "..."? (" : " term)? "; " nameableStringArg

syntax "`[Cli|\n"
literalIdent runFun "; " ("[" nameableStringArg "]")?
Expand Down