-
Notifications
You must be signed in to change notification settings - Fork 329
/
Macro.lean
40 lines (37 loc) · 1.65 KB
/
Macro.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.MacroArgUtil
namespace Lean.Elab.Command
open Lean.Syntax
open Lean.Parser.Term hiding macroArg
open Lean.Parser.Command
@[builtinMacro Lean.Parser.Command.macro] def expandMacro : Macro
| `($[$doc?:docComment]? $attrKind:attrKind
macro%$tk$[:$prec?]? $[(name := $name?)]? $[(priority := $prio?)]? $args:macroArg* :
$cat => $rhs) => do
let prio ← evalOptPrio prio?
let (stxParts, patArgs) := (← args.mapM expandMacroArg).unzip
-- name
let name ← match name? with
| some name => pure name.getId
| none => mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
/- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
let pat := mkNode ((← Macro.getCurrNamespace) ++ name) patArgs
let stxCmd ← `($[$doc?:docComment]? $attrKind:attrKind
syntax%$tk$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat)
let macroRulesCmd ←
if rhs.getArgs.size == 1 then
-- `rhs` is a `term`
let rhs := rhs[0]
`($[$doc?:docComment]? macro_rules%$tk | `($pat) => $rhs)
else
-- `rhs` is of the form `` `( $body ) ``
let rhsBody := rhs[1]
`($[$doc?:docComment]? macro_rules%$tk | `($pat) => `($rhsBody))
return mkNullNode #[stxCmd, macroRulesCmd]
| _ => Macro.throwUnsupported
end Lean.Elab.Command