max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add [parserAttributeHook] attribute

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-18 14:41:36 +02:00
parent 5e48d2bb7d
commit dab53c4986
1 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/Lean/Parser/Extension.lean
View file

@ -338,6 +338,25 @@ if s.hasError then
else
Except.ok s.stxStack.back
structure ParserAttributeHook :=
/- Called after a parser attribute is applied to a declaration. -/
(postAdd : forall (attr catName : Name) (env : Environment) (declName : Name) (builtin : Bool), IO Environment)
def mkParserAttributeHooks : IO (IO.Ref (List ParserAttributeHook)) := IO.mkRef {}
@[init mkParserAttributeHooks] constant parserAttributeHooks : IO.Ref (List ParserAttributeHook) := arbitrary _
unsafe def mkParserAttributeHookAttribute : IO (KeyedDeclsAttribute ParserAttributeHook) :=
KeyedDeclsAttribute.init {
builtinName := `builtinParserAttributeHook,
name := `parserAttributeHook,
descr := "Add a hook of type `ParserAttributeHook`, which is executed whenever a parser attribute is applied.",
valueTypeName := `Lean.PrettyPrinter.ParserAttributeHook,
evalKey := fun builtin env args => do
when args.hasArgs $ throw "invalid attribute 'parserAttributeHook', unexpected argument";
pure ""
} `Lean.Parser.parserAttributeHookAttribute
@[init mkParserAttributeHookAttribute] constant parserAttributeHookAttribute : KeyedDeclsAttribute ParserAttributeHook := arbitrary _
def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) : IO Environment :=
let name := `_regBuiltinParser ++ declName;
let type := mkApp (mkConst `IO) (mkConst `Unit);