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

fix: macro command syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-09 13:54:50 -07:00
parent a4f19aac32
commit 7ec23f9401
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Elab/Syntax.lean
View file

@ -375,7 +375,7 @@ else
@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro :=
fun stx => do
let prec := stx.getArg 1;
let prec := (stx.getArg 1).getArgs;
let head := stx.getArg 2;
let args := (stx.getArg 3).getArgs;
let cat := stx.getArg 5;
@ -391,11 +391,11 @@ fun stx => do
if stx.getArgs.size == 8 then
-- `stx` is of the form `macro $head $args* : $cat => term`
let rhs := stx.getArg 7;
`(syntax $prec [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => $rhs)
`(syntax $prec* [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => $rhs)
else
-- `stx` is of the form `macro $head $args* : $cat => `( $body )`
let rhsBody := stx.getArg 8;
`(syntax $prec [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
`(syntax $prec* [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.syntax;

2
src/Lean/Parser/Syntax.lean
View file

@ -64,7 +64,7 @@ def optKind : Parser := optional ("[" >> ident >> "]")
@[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> optKind >> Term.matchAlts
@[builtinCommandParser] def «syntax» := parser! "syntax " >> optPrecedence >> optKind >> many1 syntaxParser >> " : " >> ident
@[builtinCommandParser] def syntaxCat := parser! "declare_syntax_cat " >> ident
def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> ident
def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> (ident >> optPrecedence)
def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
def macroArg := try strLit <|> try macroArgSimple
def macroHead := macroArg <|> try ident