Skip to content

Commit 9e52c83

Browse files
mhuisimhuisi
committed
fix: varargs (#52)
This PR fixes the vararg syntax after it was accidentally broken by the introduction of polymorphic range syntax in core and attempts to make the grammar a bit more robust against future changes by only accepting strings or identifiers in several places where it accepted arbitrary terms before and limiting sub-commands to identifiers. Notably, this PR contains a **breaking change**: Multi-line flag and argument descriptions can now not contain inline-uses of `++` anymore. It is advised to use [string gaps](https://lean-lang.org/doc/reference/latest//Basic-Types/Strings/#string-literals) instead. This breakage unfortunately wasn't noticed in time due to our current build setup excluding `Tests.lean` and `Example.lean`, which will be fixed in a future PR. Fixes #51.
1 parent c682c91 commit 9e52c83

File tree

3 files changed

+73
-64
lines changed

3 files changed

+73
-64
lines changed

‎Cli/Basic.lean‎

Lines changed: 31 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1006,31 +1006,36 @@ end Configuration
10061006
section Macro
10071007
open Lean
10081008

1009-
syntax literalIdent := term
1009+
syntax nameableStringArg := str <|> ident
10101010

1011-
syntax runFun := (" VIA " term) <|> " NOOP"
1011+
syntax literalIdent := str <|> ident
10121012

1013-
syntax positionalArg := colGe literalIdent " : " term "; " term
1013+
syntax runFun := (" VIA " ident) <|> " NOOP"
10141014

1015-
syntax variableArg := colGe "..." literalIdent " : " term "; " term
1015+
syntax positionalArg := colGe literalIdent " : " term "; " nameableStringArg
10161016

1017-
syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " term
1017+
syntax variableArg := colGe "..." literalIdent " : " term "; " nameableStringArg
1018+
1019+
syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " nameableStringArg
10181020

10191021
syntax "`[Cli|\n"
1020-
literalIdent runFun "; " ("[" term "]")?
1021-
term
1022+
literalIdent runFun "; " ("[" nameableStringArg "]")?
1023+
nameableStringArg
10221024
("FLAGS:\n" withPosition((flag)*))?
10231025
("ARGS:\n" withPosition((positionalArg)* (variableArg)?))?
1024-
("SUBCOMMANDS: " sepBy(term, ";", "; "))?
1026+
("SUBCOMMANDS: " sepBy(ident, ";", "; "))?
10251027
("EXTENSIONS: " sepBy(term, ";", "; "))?
10261028
"\n]" : term
10271029

1028-
def expandIdentLiterally (t : Term) : Term :=
1029-
match t with
1030-
| `($i:ident) =>
1031-
quote i.getId.toString
1032-
| `($t:term) =>
1033-
t
1030+
def expandNameableStringArg (t : TSyntax `Cli.nameableStringArg) : MacroM Term :=
1031+
pure ⟨t.raw[0]⟩
1032+
1033+
def expandLiteralIdent (t : TSyntax `Cli.literalIdent) : MacroM Term :=
1034+
let s := t.raw[0]
1035+
if s.getKind == identKind then
1036+
pure <| quote s.getId.toString
1037+
else
1038+
pure ⟨s⟩
10341039

10351040
def expandRunFun (runFun : TSyntax `Cli.runFun) : MacroM Term :=
10361041
match runFun with
@@ -1041,33 +1046,33 @@ section Macro
10411046
| _ => Macro.throwUnsupported
10421047

10431048
def expandPositionalArg (positionalArg : TSyntax `Cli.positionalArg) : MacroM Term := do
1044-
let `(Cli.positionalArg| $name:term : $type; $description) := positionalArg
1049+
let `(Cli.positionalArg| $name : $type; $description) := positionalArg
10451050
| Macro.throwUnsupported
1046-
`(Arg.mk $(expandIdentLiterally name) $description $type)
1051+
`(Arg.mk $(← expandLiteralIdent name) $(← expandNameableStringArg description) $type)
10471052

10481053
def expandVariableArg (variableArg : TSyntax `Cli.variableArg) : MacroM Term := do
1049-
let `(Cli.variableArg| ...$name:term : $type; $description) := variableArg
1054+
let `(Cli.variableArg| ...$name : $type; $description) := variableArg
10501055
| Macro.throwUnsupported
1051-
`(Arg.mk $(expandIdentLiterally name) $description $type)
1056+
`(Arg.mk $(← expandLiteralIdent name) $(← expandNameableStringArg description) $type)
10521057

10531058
def expandFlag (flag : TSyntax `Cli.flag) : MacroM Term := do
1054-
let `(Cli.flag| $flagName1:term $[, $flagName2:term]? $[ : $type]?; $description) := flag
1059+
let `(Cli.flag| $flagName1 $[, $flagName2]? $[ : $type]?; $description) := flag
10551060
| Macro.throwUnsupported
10561061
let mut shortName := quote (none : Option String)
10571062
let mut longName := flagName1
10581063
if let some flagName2 := flagName2 then
1059-
shortName ← `(some $(expandIdentLiterally flagName1))
1064+
shortName ← `(some $(← expandLiteralIdent flagName1))
10601065
longName := flagName2
10611066
let unitType : Term ← `(Unit)
10621067
let type :=
10631068
match type with
10641069
| none => unitType
10651070
| some type => type
1066-
`(Flag.mk $shortName $(expandIdentLiterally longName) $description $type)
1071+
`(Flag.mk $shortName $(← expandLiteralIdent longName) $(← expandNameableStringArg description) $type)
10671072

10681073
macro_rules
10691074
| `(`[Cli|
1070-
$name:term $run:runFun; $[[$version]]?
1075+
$name $run:runFun; $[[$version?]]?
10711076
$description
10721077
$[FLAGS:
10731078
$flags*
@@ -1080,14 +1085,14 @@ section Macro
10801085
$[EXTENSIONS: $extensions;*]?
10811086
]) => do
10821087
`(Cmd.mk
1083-
(name := $(expandIdentLiterally name))
1084-
(version? := $(quote version))
1085-
(description := $description)
1088+
(name := $(← expandLiteralIdent name))
1089+
(version? := $(quote (← version?.mapM expandNameableStringArg)))
1090+
(description := $(← expandNameableStringArg description))
10861091
(flags := $(quote (← flags.getD #[] |>.mapM expandFlag)))
10871092
(positionalArgs := $(quote (← positionalArgs.getD #[] |>.mapM expandPositionalArg)))
10881093
(variableArg? := $(quote (← (Option.join variableArg).mapM expandVariableArg)))
10891094
(run := $(← expandRunFun run))
1090-
(subCmds := $(quote (subCommands.getD ⟨#[]⟩).getElems))
1095+
(subCmds := $(quote ((subCommands.getD ⟨#[]⟩).getElems : TSyntaxArray `term)))
10911096
(extension? := some <| Array.foldl Extension.then { : Extension } <| Array.qsort
10921097
$(quote (extensions.getD ⟨#[]⟩).getElems) (·.priority > ·.priority)))
10931098
end Macro

‎Cli/Example.lean‎

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,8 @@ def runExampleCmd (p : Parsed) : IO UInt32 := do
2828

2929
def installCmd := `[Cli|
3030
installCmd NOOP;
31-
"installCmd provides an example for a subcommand without flags or arguments that does nothing. " ++
32-
"Versions can be omitted."
31+
"installCmd provides an example for a subcommand without flags or arguments that does nothing. \
32+
Versions can be omitted."
3333
]
3434

3535
def testCmd := `[Cli|
@@ -45,20 +45,20 @@ def exampleCmd : Cmd := `[Cli|
4545
verbose; "Declares a flag `--verbose`. This is the description of the flag."
4646
i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
4747
o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
48-
p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` " ++
49-
"that takes an argument of type `Nat`."
50-
module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` " ++
51-
"which can be used to reference Lean modules like `Init.Data.Array` " ++
52-
"or Lean files using a relative path like `Init/Data/Array.lean`."
53-
"set-paths" : Array String; "Declares a flag `--set-paths` " ++
54-
"that takes an argument of type `Array Nat`. " ++
55-
"Quotation marks allow the use of hyphens."
48+
p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
49+
that takes an argument of type `Nat`."
50+
module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
51+
which can be used to reference Lean modules like `Init.Data.Array` \
52+
or Lean files using a relative path like `Init/Data/Array.lean`."
53+
"set-paths" : Array String; "Declares a flag `--set-paths` \
54+
that takes an argument of type `Array Nat`. \
55+
Quotation marks allow the use of hyphens."
5656

5757
ARGS:
58-
input : String; "Declares a positional argument <input> " ++
59-
"that takes an argument of type `String`."
60-
...outputs : String; "Declares a variable argument <output>... " ++
61-
"that takes an arbitrary amount of arguments of type `String`."
58+
input : String; "Declares a positional argument <input> \
59+
that takes an argument of type `String`."
60+
...outputs : String; "Declares a variable argument <output>... \
61+
that takes an arbitrary amount of arguments of type `String`."
6262

6363
SUBCOMMANDS:
6464
installCmd;
@@ -149,4 +149,4 @@ Yields:
149149
arguments that does nothing. Versions can be omitted.
150150
testCmd testCmd provides another example for a subcommand without flags
151151
or arguments that does nothing.
152-
-/
152+
-/

‎README.md‎

Lines changed: 27 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,8 @@ open Cli
1212
1313
def installCmd := `[Cli|
1414
installCmd NOOP;
15-
"installCmd provides an example for a subcommand without flags or arguments that does nothing. " ++
16-
"Versions can be omitted."
15+
"installCmd provides an example for a subcommand without flags or arguments that does nothing. \
16+
Versions can be omitted."
1717
]
1818
1919
def testCmd := `[Cli|
@@ -29,20 +29,20 @@ def exampleCmd : Cmd := `[Cli|
2929
verbose; "Declares a flag `--verbose`. This is the description of the flag."
3030
i, invert; "Declares a flag `--invert` with an associated short alias `-i`."
3131
o, optimize; "Declares a flag `--optimize` with an associated short alias `-o`."
32-
p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` " ++
33-
"that takes an argument of type `Nat`."
34-
module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` " ++
35-
"which be can used to reference Lean modules like `Init.Data.Array` " ++
36-
"or Lean files using a relative path like `Init/Data/Array.lean`."
37-
"set-paths" : Array String; "Declares a flag `--set-paths` " ++
38-
"that takes an argument of type `Array String`. " ++
39-
"Quotation marks allow the use of hyphens."
32+
p, priority : Nat; "Declares a flag `--priority` with an associated short alias `-p` \
33+
that takes an argument of type `Nat`."
34+
module : ModuleName; "Declares a flag `--module` that takes an argument of type `ModuleName` \
35+
which can be used to reference Lean modules like `Init.Data.Array` \
36+
or Lean files using a relative path like `Init/Data/Array.lean`."
37+
"set-paths" : Array String; "Declares a flag `--set-paths` \
38+
that takes an argument of type `Array Nat`. \
39+
Quotation marks allow the use of hyphens."
4040
4141
ARGS:
42-
input : String; "Declares a positional argument <input> " ++
43-
"that takes an argument of type `String`."
44-
...outputs : String; "Declares a variable argument <output>... " ++
45-
"that takes an arbitrary amount of arguments of type `String`."
42+
input : String; "Declares a positional argument <input> \
43+
that takes an argument of type `String`."
44+
...outputs : String; "Declares a variable argument <output>... \
45+
that takes an arbitrary amount of arguments of type `String`."
4646
4747
SUBCOMMANDS:
4848
installCmd;
@@ -176,23 +176,27 @@ The full example can be found under `./Cli/Example.lean`.
176176
This section documents only the most common features of the library. For the full documentation, peek into `./Cli/Basic.lean` and `./Cli/Extensions.lean`! All definitions below live in the `Cli` namespace.
177177

178178
```Lean
179-
-- In a literalIdent, identifiers are expanded as `String`s.
180-
syntax literalIdent := term
179+
-- In a `nameableStringArg`, string literals can either be used directly or an identifier can be
180+
-- supplied that references a string value.
181+
syntax nameableStringArg := str <|> ident
181182
182-
syntax runFun := (" VIA " term) <|> " NOOP"
183+
-- In a `literalIdent`, identifiers are expanded as `String`s.
184+
syntax literalIdent := str <|> ident
183185
184-
syntax positionalArg := colGe literalIdent " : " term "; " term
186+
syntax runFun := (" VIA " ident) <|> " NOOP"
185187
186-
syntax variableArg := colGe "..." literalIdent " : " term "; " term
188+
syntax positionalArg := colGe literalIdent " : " term "; " nameableStringArg
187189
188-
syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " term
190+
syntax variableArg := colGe "..." literalIdent " : " term "; " nameableStringArg
191+
192+
syntax flag := colGe literalIdent ("," literalIdent)? (" : " term)? "; " nameableStringArg
189193
190194
syntax "`[Cli|\n"
191-
literalIdent runFun "; " ("[" term "]")?
192-
term
195+
literalIdent runFun "; " ("[" nameableStringArg "]")?
196+
nameableStringArg
193197
("FLAGS:\n" withPosition((flag)*))?
194198
("ARGS:\n" withPosition((positionalArg)* (variableArg)?))?
195-
("SUBCOMMANDS: " sepBy(term, ";", "; "))?
199+
("SUBCOMMANDS: " sepBy(ident, ";", "; "))?
196200
("EXTENSIONS: " sepBy(term, ";", "; "))?
197201
"\n]" : term
198202
```

0 commit comments

Comments
 (0)