/
Basic.lean
29 lines (25 loc) · 1.05 KB
/
Basic.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
/-
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.KeyedDeclsAttribute
namespace Lean
namespace PrettyPrinter
/- Auxiliary internal exception for backtracking the pretty printer.
See `orelse.parenthesizer` for example -/
builtin_initialize backtrackExceptionId : InternalExceptionId ← registerInternalExceptionId `backtrackFormatter
unsafe def runForNodeKind {α} (attr : KeyedDeclsAttribute α) (k : SyntaxNodeKind) (interp : ParserDescr → CoreM α) : CoreM α := do
match attr.getValues (← getEnv) k with
| p::_ => pure p
| _ =>
-- assume `k` is from a `ParserDescr`, in which case we assume it's also the declaration name
let info ← getConstInfo k
if info.type.isConstOf ``ParserDescr || info.type.isConstOf ``TrailingParserDescr then
let d ← evalConst ParserDescr k
interp d
else
throwError "no declaration of attribute [{attr.defn.name}] found for '{k}'"
end PrettyPrinter
end Lean