max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: elaborate new macro argument types

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-18 19:41:17 -08:00
parent 781956e455
commit be571e8d42
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Lean/Elab/Syntax.lean
View file

@ -263,7 +263,14 @@ else
def expandMacroArgIntoSyntaxItem (stx : Syntax) : CommandElabM Syntax :=
let k := stx.getKind;
if k == `Lean.Parser.Command.macroArgSimple then
pure $ Syntax.node `Lean.Parser.Syntax.cat #[stx.getArg 2, stx.getArg 3]
let argType := stx.getArg 2;
match argType with
| Syntax.atom _ "ident" => pure $ Syntax.node `Lean.Parser.Syntax.ident #[argType]
| Syntax.atom _ "num" => pure $ Syntax.node `Lean.Parser.Syntax.num #[argType]
| Syntax.atom _ "str" => pure $ Syntax.node `Lean.Parser.Syntax.str #[argType]
| Syntax.atom _ "char" => pure $ Syntax.node `Lean.Parser.Syntax.char #[argType]
| Syntax.ident _ _ _ _ => pure $ Syntax.node `Lean.Parser.Syntax.cat #[stx.getArg 2, stx.getArg 3]
| _ => throwUnsupportedSyntax
else if k == `Lean.Parser.Command.strLitPrec then
pure $ Syntax.node `Lean.Parser.Syntax.atom stx.getArgs
else