be841a7cad
@Kha I marked the corresponding methods as `protected`. I currently can't stand `throw_error`, and I am optimistic about server highlighting feature you are working on :)
55 lines
1.9 KiB
Text
55 lines
1.9 KiB
Text
/-
|
||
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
|