diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index 99b2348bdc..a1408d1761 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -1823,13 +1823,12 @@ es.foldlM | ParserExtensionOleanEntry.category catName leadingIdentAsSymbol => do categories ← IO.ofExcept (addParserCategoryCore s.categories catName { tables := {}, leadingIdentAsSymbol := leadingIdentAsSymbol}); pure { s with categories := categories } - | ParserExtensionOleanEntry.parser catName declName => - match mkParserOfConstant env s.categories declName with - | Except.ok p => - match addParser s.categories catName declName p.1 p.2 with - | Except.ok categories => pure { s with categories := categories } - | Except.error ex => throw (IO.userError ex) - | Except.error ex => throw (IO.userError ex)) + | 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; + pure { s with categories := categories }) s) s @@ -1986,7 +1985,7 @@ 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.compile env declName /- builtin -/ false + PrettyPrinter.Parenthesizer.addParenthesizerFromConstant env declName def mkParserAttributeImpl (attrName : Name) (catName : Name) : AttributeImpl := { name := attrName, diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 0358fce812..731ae7d267 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -266,6 +266,10 @@ maybeParenthesize (fun stx => Unhygienic.run `(level|($stx))) prec $ def try.parenthesizer (p : Parenthesizer) : Parenthesizer := p +@[combinatorParenthesizer Lean.Parser.lookahead] +def lookahead.parenthesizer (p : Parenthesizer) : Parenthesizer := +p + @[combinatorParenthesizer Lean.Parser.andthen] def andthen.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p2 *> p1 @@ -470,6 +474,53 @@ env ← env.addAttribute parenthesizerDeclName (if builtin then `builtinParenthe -- call them at compile time but only reference them). env.addAttribute parenthesizerDeclName `combinatorParenthesizer (mkNullNode #[mkIdent declName]) +unsafe def mkParenthesizerOfConstantUnsafe (constName : Name) (compileParenthesizerDescr : ParserDescr → StateT Environment IO Parenthesizer) + : StateT Environment IO Parenthesizer := +fun env => match env.find? constName with +| none => throw $ IO.userError ("unknow constant '" ++ toString constName ++ "'") +| some info => + if info.type.isConstOf `Lean.Parser.TrailingParser || info.type.isConstOf `Lean.Parser.Parser then + match parenthesizerAttribute.getValues env constName with + | p::_ => pure (p, env) + | _ => do + env ← compile env constName /- builtin -/ false; + pure (parenthesizerForKind constName, env) + else do + d ← IO.ofExcept $ env.evalConst TrailingParserDescr constName; + compileParenthesizerDescr d env + +@[implementedBy mkParenthesizerOfConstantUnsafe] +constant mkParenthesizerOfConstantAux (constName : Name) (compileParenthesizerDescr : ParserDescr → StateT Environment IO Parenthesizer) + : StateT Environment IO Parenthesizer := +arbitrary _ + +partial def compileParenthesizerDescr : ParserDescr → StateT Environment IO Parenthesizer +| ParserDescr.andthen d₁ d₂ => andthen.parenthesizer <$> compileParenthesizerDescr d₁ <*> compileParenthesizerDescr d₂ +| ParserDescr.orelse d₁ d₂ => orelse.parenthesizer <$> compileParenthesizerDescr d₁ <*> compileParenthesizerDescr d₂ +| ParserDescr.optional d => optional.parenthesizer <$> compileParenthesizerDescr d +| ParserDescr.lookahead d => lookahead.parenthesizer <$> compileParenthesizerDescr d +| ParserDescr.try d => try.parenthesizer <$> compileParenthesizerDescr d +| ParserDescr.many d => many.parenthesizer <$> compileParenthesizerDescr d +| ParserDescr.many1 d => many1.parenthesizer <$> compileParenthesizerDescr d +| ParserDescr.sepBy d₁ d₂ => sepBy.parenthesizer <$> compileParenthesizerDescr d₁ <*> compileParenthesizerDescr d₂ +| ParserDescr.sepBy1 d₁ d₂ => sepBy1.parenthesizer <$> compileParenthesizerDescr d₁ <*> compileParenthesizerDescr d₂ +| ParserDescr.node k prec d => leadingNode.parenthesizer k prec <$> compileParenthesizerDescr d +| ParserDescr.trailingNode k prec d => trailingNode.parenthesizer k prec <$> compileParenthesizerDescr d +| ParserDescr.symbol tk => pure $ symbol.parenthesizer +| ParserDescr.numLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer +| ParserDescr.strLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.parenthesizer +| ParserDescr.charLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer +| ParserDescr.nameLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer +| ParserDescr.ident => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer +| ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol.parenthesizer +| ParserDescr.parser constName => mkParenthesizerOfConstantAux constName compileParenthesizerDescr +| ParserDescr.cat catName prec => pure $ categoryParser.parenthesizer catName prec + +def addParenthesizerFromConstant (env : Environment) (constName : Name) : IO Environment := do +(p, env) ← mkParenthesizerOfConstantAux constName compileParenthesizerDescr env; +parenthesizerAttribute.addBuiltin constName p; +pure env + end Parenthesizer open Parenthesizer