From eeaf20080c76c08126ee384426e34e360e22fd70 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 18 Aug 2020 16:01:55 +0200 Subject: [PATCH] refactor: register parenthesizer compiler as hook /cc @leodemoura --- src/Lean/Parser/Extension.lean | 35 ++++++++++++----------- src/Lean/Parser/Level.lean | 1 + src/Lean/PrettyPrinter/Parenthesizer.lean | 19 ++++++------ 3 files changed, 29 insertions(+), 26 deletions(-) diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 85ed1bfd53..ab8f93cb8b 100644 --- a/src/Lean/Parser/Extension.lean +++ b/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, diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean index dce2614d13..a92094d3fd 100644 --- a/src/Lean/Parser/Level.lean +++ b/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 diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 37487bf03a..d3e208a7c6 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/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