refactor: register parenthesizer compiler as hook

/cc @leodemoura

src/Lean/Parser/Extension.lean

@@ -7,7 +7,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 /-! Extensible parsing via attributes -/
 
 import Lean.Parser.Basic
-import Lean.PrettyPrinter.Parenthesizer
+import Lean.KeyedDeclsAttribute
 
 namespace Lean
 namespace Parser
@@ -223,6 +223,16 @@ partial def compileParserDescr (env : Environment) (categories : ParserCategorie
 def mkParserOfConstant (env : Environment) (categories : ParserCategories) (constName : Name) : Except String (Bool × Parser) :=
 mkParserOfConstantAux env categories constName (compileParserDescr env categories)
 
+structure ParserAttributeHook :=
+/- Called after a parser attribute is applied to a declaration. -/
+(postAdd : forall (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 _
+
+def registerParserAttributeHook (hook : ParserAttributeHook) : IO Unit := do
+parserAttributeHooks.modify fun hooks => hook::hooks
+
 private def ParserExtension.addImported (env : Environment) (es : Array (Array ParserExtensionOleanEntry)) : IO ParserExtensionState := do
 s ← ParserExtension.mkInitial;
 es.foldlM
@@ -241,8 +251,9 @@ es.foldlM
        | ParserExtensionOleanEntry.parser catName declName => do
          p ← IO.ofExcept $ mkParserOfConstant env s.categories declName;
          categories ← IO.ofExcept $ addParser s.categories catName declName p.1 p.2;
-         -- discard result env; all imported parenthesizers should already be compiled
-         _ ← PrettyPrinter.Parenthesizer.addParenthesizerFromConstant env declName;
+         hooks ← parserAttributeHooks.get;
+         -- discard result env; all environment side effects should already have happened when the parser was declared initially
+         _ ← hooks.foldlM (fun env hook => hook.postAdd catName env declName /- builtin -/ false) env;
          pure { s with categories := categories })
       s)
   s
@@ -260,7 +271,6 @@ registerPersistentEnvExtension {
 @[init mkParserExtension]
 constant parserExtension : ParserExtension := arbitrary _
 
-@[export lean_is_parser_category]
 def isParserCategory (env : Environment) (catName : Name) : Bool :=
 (parserExtension.getState env).categories.contains catName
 
@@ -301,7 +311,6 @@ pure $ parserExtension.addEntry env $ ParserExtensionEntry.token tk
 def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
 parserExtension.addEntry env $ ParserExtensionEntry.kind k
 
-@[export lean_is_valid_syntax_node_kind]
 def isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool :=
 let kinds := (parserExtension.getState env).kinds;
 kinds.contains k
@@ -338,16 +347,6 @@ 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 _
-
-def registerParserAttributeHook (hook : ParserAttributeHook) : IO Unit := do
-parserAttributeHooks.modify fun hooks => hook::hooks
-
 def declareBuiltinParser (env : Environment) (addFnName : Name) (catName : Name) (declName : Name) : IO Environment :=
 let name := `_regBuiltinParser ++ declName;
 let type := mkApp (mkConst `IO) (mkConst `Unit);
@@ -378,7 +377,8 @@ env ← match env.find? declName with
    declareLeadingBuiltinParser env catName declName
  | _ =>
    throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"));
-PrettyPrinter.Parenthesizer.compileParser env declName /- builtin -/ true
+hooks ← parserAttributeHooks.get;
+hooks.foldlM (fun env hook => hook.postAdd catName env declName /- builtin -/ true) env
 
 /-
 The parsing tables for builtin parsers are "stored" in the extracted source code.
@@ -412,7 +412,8 @@ match mkParserOfConstant env categories declName with
   env ← match addParser categories catName declName leading parser with
   | Except.ok _     => pure $ parserExtension.addEntry env $ ParserExtensionEntry.parser catName declName leading parser
   | Except.error ex => throw (IO.userError ex);
-  PrettyPrinter.Parenthesizer.addParenthesizerFromConstant env declName
+  hooks ← parserAttributeHooks.get;
+  hooks.foldlM (fun env hook => hook.postAdd catName env declName /- builtin -/ false) env
 
 def mkParserAttributeImpl (attrName : Name) (catName : Name) : AttributeImpl :=
 { name            := attrName,

src/Lean/Parser/Level.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Parser.Extension
+import Lean.PrettyPrinter.Parenthesizer  -- necessary for auto-generation
 
 namespace Lean
 namespace Parser

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -74,7 +74,7 @@ import Lean.Util.ReplaceExpr
 import Lean.Meta.Basic
 import Lean.Meta.WHNF
 import Lean.KeyedDeclsAttribute
-import Lean.Parser.Basic
+import Lean.Parser.Extension
 import Lean.ParserCompiler
 
 namespace Lean
@@ -103,9 +103,6 @@ abbrev ParenthesizerM := ReaderT Parenthesizer.Context $ StateT Parenthesizer.St
 
 abbrev Parenthesizer := ParenthesizerM Unit
 
-@[extern "lean_is_valid_syntax_node_kind"]
-constant isValidSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Bool := arbitrary _
-
 unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) :=
 KeyedDeclsAttribute.init {
   builtinName := `builtinParenthesizer,
@@ -118,7 +115,7 @@ KeyedDeclsAttribute.init {
     | some id =>
       -- `isValidSyntaxNodeKind` is updated only in the next stage for new `[builtin*Parser]`s, but we try to
       -- synthesize a parenthesizer for it immediately, so we just check for a declaration in this case
-      if (builtin && (env.find? id).isSome) || isValidSyntaxNodeKind env id then pure id
+      if (builtin && (env.find? id).isSome) || Parser.isValidSyntaxNodeKind env id then pure id
       else throw ("invalid [parenthesizer] argument, unknown syntax kind '" ++ toString id ++ "'")
     | none    => throw "invalid [parenthesizer] argument, expected identifier"
 } `Lean.PrettyPrinter.parenthesizerAttribute
@@ -126,9 +123,6 @@ KeyedDeclsAttribute.init {
 
 abbrev CategoryParenthesizer := forall (prec : Nat), Parenthesizer
 
-@[extern "lean_is_parser_category"]
-constant isParserCategory (env : Environment) (k : SyntaxNodeKind) : Bool := arbitrary _
-
 unsafe def mkCategoryParenthesizerAttribute : IO (KeyedDeclsAttribute CategoryParenthesizer) :=
 KeyedDeclsAttribute.init {
   builtinName := `builtinCategoryParenthesizer,
@@ -142,7 +136,7 @@ parenthesized, but still be traversed for parenthesizing nested categories.",
   valueTypeName := `Lean.PrettyPrinter.CategoryParenthesizer,
   evalKey := fun _ env args => match attrParamSyntaxToIdentifier args with
     | some id =>
-      if isParserCategory env id then pure id
+      if Parser.isParserCategory env id then pure id
       else throw ("invalid [parenthesizer] argument, unknown parser category '" ++ toString id ++ "'")
     | none    => throw "invalid [parenthesizer] argument, expected identifier"
 } `Lean.PrettyPrinter.categoryParenthesizerAttribute
@@ -592,6 +586,13 @@ def parenthesizeCommand := parenthesize $ categoryParser.parenthesizer `command
 
 @[init] private def regTraceClasses : IO Unit := do
 registerTraceClass `PrettyPrinter.parenthesize;
+Parser.registerParserAttributeHook {
+  postAdd := fun catName env declName builtin =>
+    if builtin then
+      compileParser env declName builtin
+    else
+      addParenthesizerFromConstant env declName
+};
 pure ()
 
 end PrettyPrinter