-
Notifications
You must be signed in to change notification settings - Fork 350
/
MacroArgUtil.lean
80 lines (77 loc) · 3.9 KB
/
MacroArgUtil.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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Elab.Syntax
namespace Lean.Elab.Command
open Lean.Syntax
open Lean.Parser.Term hiding macroArg
open Lean.Parser.Command
/-- Convert `macro` arg into a `syntax` command item and a pattern element -/
partial def expandMacroArg (stx : TSyntax ``macroArg) : CommandElabM (TSyntax `stx × Term) := do
let (id?, id, stx) ← match (← liftMacroM <| expandMacros stx) with
| `(macroArg| $id:ident:$stx) => pure (some id, (id : Term), stx)
| `(macroArg| $stx:stx) => pure (none, (← `(x)), stx)
| _ => throwUnsupportedSyntax
mkSyntaxAndPat id? id stx
where
mkSyntaxAndPat (id? : Option Ident) (id : Term) (stx : TSyntax `stx) := do
let pat ← match stx with
| `(stx| $s:str)
| `(stx| &$s:str) => pure ⟨mkNode `token_antiquot #[← liftMacroM <| strLitToPattern s, mkAtom "%", mkAtom "$", id]⟩
| `(stx| optional($stx)) => mkSplicePat `optional stx id "?"
| `(stx| many($stx))
| `(stx| many1($stx)) => mkSplicePat `many stx id "*"
| `(stx| sepBy($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?))
| `(stx| sepBy1($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
mkSplicePat `sepBy stx id ((isStrLit? sep).get! ++ "*")
-- NOTE: all `interpolatedStr(·)` reuse the same node kind
| `(stx| interpolatedStr(term)) => pure ⟨Syntax.mkAntiquotNode interpolatedStrKind id⟩
-- bind through withPosition
| `(stx| withPosition($stx)) =>
let (stx, pat) ← mkSyntaxAndPat id? id stx
let stx ← `(stx| withPosition($stx))
return (stx, pat)
| _ => match id? with
-- if there is a binding, we assume the user knows what they are doing
| some id => mkAntiquotNode stx id
-- otherwise `group` the syntax to enforce arity 1, e.g. for `noWs`
| none => return (← `(stx| group($stx)), (← mkAntiquotNode stx id))
pure (stx, pat)
mkSplicePat (kind : SyntaxNodeKind) (stx : TSyntax `stx) (id : Term) (suffix : String) : CommandElabM Term :=
return ⟨mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix]⟩
mkAntiquotNode : TSyntax `stx → Term → CommandElabM Term
| `(stx| $id:ident$[:$_]?), term => do
match (← liftTermElabM do Elab.Term.elabParserName? id) with
| some (.parser n _) =>
let kind := match n with
| ``Parser.ident => identKind
| ``Parser.Term.ident => identKind
| ``Parser.strLit => strLitKind
| _ => n -- assume kind == decl name
return ⟨Syntax.mkAntiquotNode kind term⟩
| some (.category cat) =>
return ⟨Syntax.mkAntiquotNode cat term (isPseudoKind := true)⟩
| none =>
let id := id.getId.eraseMacroScopes
if (← Parser.isParserAlias id) then
let kind := (← Parser.getSyntaxKindOfParserAlias? id).getD Name.anonymous
return ⟨Syntax.mkAntiquotNode kind term⟩
else
throwError "unknown parser declaration/category/alias '{id}'"
| stx, term => do
-- can't match against `` `(stx| ($stxs*)) `` as `*` is interpreted as the `stx` operator
if stx.raw.isOfKind ``Parser.Syntax.paren then
-- translate argument `v:(p1 ... pn)` where all but one `pi` produce zero nodes to
-- `v:pi` using that single `pi`
let nonNullaryNodes ← stx.raw[1].getArgs.filterM fun
| `(stx| $id:ident$[:$_]?) | `(stx| $id:ident($_)) => do
let info ← Parser.getParserAliasInfo id.getId
return info.stackSz? != some 0
| _ => return true
if let #[stx] := nonNullaryNodes then
return (← mkAntiquotNode ⟨stx⟩ term)
pure ⟨Syntax.mkAntiquotNode Name.anonymous term (isPseudoKind := true)⟩
end Lean.Elab.Command