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

feat: support interpreting parenthesizers from ParserDescr

Browse source
This commit is contained in:
Sebastian Ullrich 2020-08-11 18:36:33 +02:00 • committed by Leonardo de Moura
parent 1f4cc130b7
commit f4e59070c4
2 changed files with 58 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Parser/Parser.lean
View file

@ -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,

51
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -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