-
Notifications
You must be signed in to change notification settings - Fork 330
/
Attribute.lean
55 lines (45 loc) · 1.93 KB
/
Attribute.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
/-
Copyright (c) 2020 Sebastian Ullrich. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
import Lean.Attributes
import Lean.Compiler.InitAttr
import Lean.ToExpr
namespace Lean
namespace ParserCompiler
structure CombinatorAttribute where
impl : AttributeImpl
ext : SimplePersistentEnvExtension (Name × Name) (NameMap Name)
deriving Inhabited
-- TODO(Sebastian): We'll probably want priority support here at some point
def registerCombinatorAttribute (name : Name) (descr : String)
: IO CombinatorAttribute := do
let ext : SimplePersistentEnvExtension (Name × Name) (NameMap Name) ← registerSimplePersistentEnvExtension {
name := name,
addImportedFn := mkStateFromImportedEntries (fun s p => s.insert p.1 p.2) {},
addEntryFn := fun (s : NameMap Name) (p : Name × Name) => s.insert p.1 p.2,
}
let attrImpl : AttributeImpl := {
name := name,
descr := descr,
add := fun decl stx _ => do
let env ← getEnv
let parserDeclName ← Attribute.Builtin.getId stx
discard <| getConstInfo parserDeclName
setEnv <| ext.addEntry env (parserDeclName, decl)
}
registerBuiltinAttribute attrImpl
pure { impl := attrImpl, ext := ext }
namespace CombinatorAttribute
def getDeclFor? (attr : CombinatorAttribute) (env : Environment) (parserDecl : Name) : Option Name :=
(attr.ext.getState env).find? parserDecl
def setDeclFor (attr : CombinatorAttribute) (env : Environment) (parserDecl : Name) (decl : Name) : Environment :=
attr.ext.addEntry env (parserDecl, decl)
unsafe def runDeclFor {α} (attr : CombinatorAttribute) (parserDecl : Name) : CoreM α := do
match attr.getDeclFor? (← getEnv) parserDecl with
| some d => evalConst α d
| _ => throwError "no declaration of attribute [{attr.impl.name}] found for '{parserDecl}'"
end CombinatorAttribute
end ParserCompiler
end Lean