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

chore: add parser aliases

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-17 11:11:40 -08:00
parent 1d93eefada
commit 3ad2d6c4e1
2 changed files with 27 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/Lean/Parser/Extra.lean
View file

@ -48,20 +48,18 @@ attribute [runBuiltinParserAttributeHooks]
end Parser
namespace PrettyPrinter
namespace Formatter
section
open PrettyPrinter
@[combinatorFormatter Lean.Parser.ppHardSpace] def ppHardSpace.formatter : Formatter := push " "
@[combinatorFormatter Lean.Parser.ppSpace] def ppSpace.formatter : Formatter := pushLine
@[combinatorFormatter Lean.Parser.ppLine] def ppLine.formatter : Formatter := push "\n"
@[combinatorFormatter Lean.Parser.ppGroup] def ppGroup.formatter (p : Formatter) : Formatter := group $ indent p
@[combinatorFormatter Lean.Parser.ppIndent] def ppIndent.formatter (p : Formatter) : Formatter := indent p
@[combinatorFormatter Lean.Parser.ppHardSpace] def ppHardSpace.formatter : Formatter := Formatter.push " "
@[combinatorFormatter Lean.Parser.ppSpace] def ppSpace.formatter : Formatter := Formatter.pushLine
@[combinatorFormatter Lean.Parser.ppLine] def ppLine.formatter : Formatter := Formatter.push "\n"
@[combinatorFormatter Lean.Parser.ppGroup] def ppGroup.formatter (p : Formatter) : Formatter := Formatter.group $ Formatter.indent p
@[combinatorFormatter Lean.Parser.ppIndent] def ppIndent.formatter (p : Formatter) : Formatter := Formatter.indent p
@[combinatorFormatter Lean.Parser.ppDedent] def ppDedent.formatter (p : Formatter) : Formatter := do
let opts ← getOptions
indent p (some (0 - Format.getIndent opts))
end Formatter
end PrettyPrinter
Formatter.indent p (some (0 - Format.getIndent opts))
end
namespace Parser
@ -74,5 +72,15 @@ macro "registerParserAlias!" aliasName:strLit declName:ident : term =>
PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter))
PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))
open PrettyPrinter in
builtin_initialize
registerParserAlias! "group" group
registerParserAlias! "ppHardSpace" ppHardSpace
registerParserAlias! "ppSpace" ppSpace
registerParserAlias! "ppLine" ppLine
registerParserAlias! "ppGroup" ppGroup
registerParserAlias! "ppIndent" ppIndent
registerParserAlias! "ppDedent" ppDedent
end Parser
end Lean

8
src/Lean/Parser/Term.lean
View file

@ -211,5 +211,13 @@ end Term
@[builtinTermParser] def Level.quot : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"
builtin_initialize
registerParserAlias! "letDecl" Term.letDecl
registerParserAlias! "haveDecl" Term.haveDecl
registerParserAlias! "sufficesDecl" Term.sufficesDecl
registerParserAlias! "letRecDecls" Term.letRecDecls
registerParserAlias! "hole" Term.hole
registerParserAlias! "syntheticHole" Term.syntheticHole
end Parser
end Lean