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

feat: update macro_rules

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-25 18:19:16 -08:00
parent c2d2fd98ba
commit 32b36f0ea3
1 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -180,16 +180,18 @@ fun stx => do
trace `Elab stx $ fun _ => d;
withMacroExpansion stx d $ elabCommand d
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
adaptExpander $ fun stx => match_syntax stx with
| `(macro_rules $alts*) => do
-- TODO: clean up with matchAlt quotation
k ← match_syntax ((alts.get! 0).getArg 1).getArg 0 with
def elabMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
k ← match_syntax ((alts.get! 0).getArg 0).getArg 0 with
| `(`($quot)) => pure quot.getKind
| stx => throwUnsupportedSyntax;
-- TODO: meaningful, unhygienic def name for selective macro `open`ing?
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
| _ => throwUnsupportedSyntax
-- TODO: meaningful, unhygienic def name for selective macro `open`ing?
`(@[macro $(Lean.mkIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
adaptExpander $ fun stx => match_syntax stx with
| `(macro_rules $alts:matchAlt*) => elabMacroRulesAux alts
| `(macro_rules | $alts:matchAlt*) => elabMacroRulesAux alts
| _ => throwUnsupportedSyntax
/- We just ignore Lean3 notation declaration commands. -/
@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()