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

fix: macro command

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

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

@ -341,18 +341,17 @@ if k == `Lean.Parser.Command.macroArgSimple then
| 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]
| _ => Macro.throwUnsupported
else if k == `Lean.Parser.Command.strLitPrec then
pure $ Syntax.node `Lean.Parser.Syntax.atom stx.getArgs
else if k == strLitKind then
pure $ Syntax.node `Lean.Parser.Syntax.atom #[stx]
else
Macro.throwUnsupported
/- Convert `macro` head into a `syntax` command item -/
def expandMacroHeadIntoSyntaxItem (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind;
if k == `Lean.Parser.Command.identPrec then
if stx.isIdent then
let info := stx.getHeadInfo.getD {};
let id := (stx.getArg 0).getId;
pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info, stx.getArg 1]
let id := stx.getId;
pure $ Syntax.node `Lean.Parser.Syntax.atom #[mkStxStrLit (toString id) info]
else
expandMacroArgIntoSyntaxItem stx
@ -362,25 +361,24 @@ let k := stx.getKind;
if k == `Lean.Parser.Command.macroArgSimple then
let item := stx.getArg 0;
pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, item, mkNullNode, mkNullNode]
else if k == `Lean.Parser.Command.strLit then
else if k == strLitKind then
strLitToPattern stx
else
Macro.throwUnsupported
/- Convert `macro` head into a pattern element -/
def expandMacroHeadIntoPattern (stx : Syntax) : MacroM Syntax :=
let k := stx.getKind;
if k == `Lean.Parser.Command.identPrec then
let str := toString (stx.getArg 0).getId;
pure $ mkAtomFrom stx str
if stx.isIdent then
pure $ mkAtomFrom stx (toString stx.getId)
else
expandMacroArgIntoPattern stx
@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro :=
fun stx => do
let head := stx.getArg 1;
let args := (stx.getArg 2).getArgs;
let cat := stx.getArg 4;
let prec := stx.getArg 1;
let head := stx.getArg 2;
let args := (stx.getArg 3).getArgs;
let cat := stx.getArg 5;
kind ← Macro.mkFreshKind (cat.getId).eraseMacroScopes;
-- build parser
stxPart ← expandMacroHeadIntoSyntaxItem head;
@ -390,14 +388,14 @@ fun stx => do
patHead ← expandMacroHeadIntoPattern head;
patArgs ← args.mapM expandMacroArgIntoPattern;
let pat := Syntax.node kind (#[patHead] ++ patArgs);
if stx.getArgs.size == 7 then
if stx.getArgs.size == 8 then
-- `stx` is of the form `macro $head $args* : $cat => term`
let rhs := stx.getArg 6;
`(syntax [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => $rhs)
let rhs := stx.getArg 7;
`(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 7;
`(syntax [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
let rhsBody := stx.getArg 8;
`(syntax $prec [$(mkIdentFrom stx kind)] $stxParts* : $cat macro_rules | `($pat) => `($rhsBody))
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.syntax;

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

@ -67,12 +67,12 @@ def optKind : Parser := optional ("[" >> ident >> "]")
def macroArgType := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|> nonReservedSymbol "str" <|> nonReservedSymbol "char" <|> ident
def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
def macroArg := try strLit <|> try macroArgSimple
def macroHead := macroArg <|> try identPrec
def macroHead := macroArg <|> try ident
def macroTailTactic : Parser := try (" : " >> identEq "tactic") >> darrow >> "`(" >> sepBy1 tacticParser "; " true true >> ")"
def macroTailCommand : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"
def macroTailDefault : Parser := try (" : " >> ident) >> darrow >> (("`(" >> categoryParserOfStack 2 >> ")") <|> termParser)
def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
@[builtinCommandParser] def «macro» := parser! "macro " >> optPrecedence <|> macroHead >> many macroArg >> macroTail
@[builtinCommandParser] def «macro» := parser! "macro " >> optPrecedence >> macroHead >> many macroArg >> macroTail
end Command