-
Notifications
You must be signed in to change notification settings - Fork 345
/
Util.lean
48 lines (41 loc) · 1.86 KB
/
Util.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
/-
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Ullrich
-/
prelude
import Lean.Elab.Term
namespace Lean.Elab.Term.Quotation
open Lean.Syntax
register_builtin_option hygiene : Bool := {
defValue := true
descr := "Annotate identifiers in quotations such that they are resolved relative to the scope at their declaration, not that at their eventual use/expansion, to avoid accidental capturing. Note that quotations/notations already defined are unaffected."
}
def getAntiquotationIds (stx : Syntax) : TermElabM (Array Ident) := do
let mut ids := #[]
for stx in stx.topDown (firstChoiceOnly := true) do
if (isAntiquot stx || isTokenAntiquot stx) && !isEscapedAntiquot stx then
let anti := getAntiquotTerm stx
if anti.isIdent then ids := ids.push ⟨anti⟩
else if anti.isOfKind ``Parser.Term.hole then pure ()
else throwErrorAt stx "complex antiquotation not allowed here"
return ids
/-- Get all pattern vars (as `Syntax.ident`s) in `stx` -/
partial def getPatternVars (stx : Syntax) : TermElabM (Array Syntax) :=
if stx.isQuot then
getAntiquotationIds stx
else match stx with
| `(_) => return #[]
| `($id:ident) => return #[id]
| `($id:ident@$e) => return (← getPatternVars e).push id
| _ => throwErrorAt stx "unsupported pattern in syntax match{indentD stx}"
def getPatternsVars (pats : Array Syntax) : TermElabM (Array Syntax) :=
pats.foldlM (fun vars pat => do return vars ++ (← getPatternVars pat)) #[]
/--
Given an antiquotation like `$e:term` (i.e. `Syntax.antiquotKind?` returns `some`),
returns the `"term"` atom if present.
-/
def getAntiquotKindSpec? (antiquot : Syntax) : Option Syntax :=
let name := antiquot[3][1]
if name.isMissing then none else some name
end Lean.Elab.Term.Quotation