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

refactor: clean up & delay registering parser aliases

Browse source
This commit is contained in:
Sebastian Ullrich 2020-12-04 17:22:16 +01:00
parent 878f32b662
commit 92cbe27810
5 changed files with 64 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/Lean/Parser.lean
View file

@ -13,6 +13,35 @@ import Lean.Parser.Syntax
import Lean.Parser.Do
namespace Lean
namespace Parser
builtin_initialize
registerAlias "ws" checkWsBefore
registerAlias "noWs" checkNoWsBefore
registerAlias "num" numLit
registerAlias "str" strLit
registerAlias "char" charLit
registerAlias "name" nameLit
registerAlias "ident" ident
registerAlias "colGt" checkColGt
registerAlias "colGe" checkColGe
registerAlias "lookahead" lookahead
registerAlias "atomic" atomic
registerAlias "many" many
registerAlias "many1" many1
registerAlias "notFollowedBy" (notFollowedBy · "element")
registerAlias "optional" optional
registerAlias "withPosition" withPosition
registerAlias "interpolatedStr" interpolatedStr
registerAlias "sepBy" sepBy
registerAlias "sepBy1" sepBy1
registerAlias "orelse" orelse
registerAlias "andthen" andthen
registerAlias "sepByT" (sepBy (allowTrailingSep := true))
registerAlias "sepBy1T" (sepBy1 (allowTrailingSep := true))
end Parser
namespace PrettyPrinter
namespace Parenthesizer

25
src/Lean/Parser/Extension.lean
View file

@ -268,31 +268,6 @@ def ensureBinaryParserAlias (aliasName : Name) : IO Unit :=
def ensureConstantParserAlias (aliasName : Name) : IO Unit :=
discard $ getConstAlias parserAliasesRef aliasName
builtin_initialize
registerAlias "ws" checkWsBefore
registerAlias "noWs" checkNoWsBefore
registerAlias "num" numLit
registerAlias "str" strLit
registerAlias "char" charLit
registerAlias "name" nameLit
registerAlias "ident" ident
registerAlias "colGt" checkColGt
registerAlias "colGe" checkColGe
registerAlias "lookahead" lookahead
registerAlias "atomic" atomic
registerAlias "many" many
registerAlias "many1" many1
registerAlias "notFollowedBy" (notFollowedBy · "element")
registerAlias "optional" optional
registerAlias "withPosition" withPosition
registerAlias "interpolatedStr" interpolatedStr
registerAlias "sepBy" sepBy
registerAlias "sepBy1" sepBy1
registerAlias "orelse" orelse
registerAlias "andthen" andthen
registerAlias "sepByT" (sepBy (allowTrailingSep := true))
registerAlias "sepBy1T" (sepBy1 (allowTrailingSep := true))
partial def compileParserDescr (categories : ParserCategories) (d : ParserDescr) : ImportM Parser :=
let rec visit : ParserDescr → ImportM Parser
| ParserDescr.const n => getConstAlias parserAliasesRef n

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

@ -82,4 +82,39 @@ builtin_initialize
registerParserAlias! "ppDedent" ppDedent
end Parser
open Parser
open PrettyPrinter.Parenthesizer (registerAlias) in
builtin_initialize
registerAlias "num" numLit.parenthesizer
registerAlias "scientific" scientificLit.parenthesizer
registerAlias "str" strLit.parenthesizer
registerAlias "char" charLit.parenthesizer
registerAlias "name" nameLit.parenthesizer
registerAlias "ident" ident.parenthesizer
registerAlias "many" many.parenthesizer
registerAlias "many1" many1.parenthesizer
registerAlias "optional" optional.parenthesizer
registerAlias "sepBy" sepBy.parenthesizer
registerAlias "sepBy1" sepBy1.parenthesizer
registerAlias "sepByT" sepBy.parenthesizer
registerAlias "sepBy1T" sepBy1.parenthesizer
open PrettyPrinter.Formatter (registerAlias) in
builtin_initialize
registerAlias "num" numLit.formatter
registerAlias "scientific" scientificLit.formatter
registerAlias "str" strLit.formatter
registerAlias "char" charLit.formatter
registerAlias "name" nameLit.formatter
registerAlias "ident" ident.formatter
registerAlias "many" many.formatter
registerAlias "many1" many1.formatter
registerAlias "optional" optional.formatter
registerAlias "sepBy" sepBy.formatter
registerAlias "sepBy1" sepBy1.formatter
registerAlias "sepByT" sepBy.formatter
registerAlias "sepBy1T" sepBy1.formatter
end Lean

13
src/Lean/PrettyPrinter/Formatter.lean
View file

@ -445,28 +445,15 @@ instance : Coe (Formatter → Formatter → Formatter) FormatterAliasValue := {
builtin_initialize
registerAlias "ws" checkWsBefore.formatter
registerAlias "noWs" checkNoWsBefore.formatter
registerAlias "num" (withAntiquot.formatter (mkAntiquot.formatter' "numLit" `numLit) numLitNoAntiquot.formatter)
registerAlias "scientific" (withAntiquot.formatter (mkAntiquot.formatter' "scientificLit" `scientificLit) scientificLitNoAntiquot.formatter)
registerAlias "str" (withAntiquot.formatter (mkAntiquot.formatter' "strLit" `strLit) strLitNoAntiquot.formatter)
registerAlias "char" (withAntiquot.formatter (mkAntiquot.formatter' "charLit" `charLit) charLitNoAntiquot.formatter)
registerAlias "name" (withAntiquot.formatter (mkAntiquot.formatter' "nameLit" `nameLit) nameLitNoAntiquot.formatter)
registerAlias "ident" (withAntiquot.formatter (mkAntiquot.formatter' "ident" `ident) identNoAntiquot.formatter)
registerAlias "colGt" checkColGt.formatter
registerAlias "colGe" checkColGe.formatter
registerAlias "lookahead" lookahead.formatter
registerAlias "atomic" atomic.formatter
registerAlias "many" many.formatter
registerAlias "many1" many1.formatter
registerAlias "notFollowedBy" notFollowedBy.formatter
registerAlias "optional" optional.formatter
registerAlias "withPosition" withPosition.formatter
registerAlias "interpolatedStr" interpolatedStr.formatter
registerAlias "sepBy" sepBy.formatter
registerAlias "sepBy1" sepBy1.formatter
registerAlias "orelse" orelse.formatter
registerAlias "andthen" andthen.formatter
registerAlias "sepByT" sepBy.formatter
registerAlias "sepBy1T" sepBy1.formatter
@[export lean_pretty_printer_formatter_interpret_parser_descr]
unsafe def interpretParserDescr : ParserDescr → CoreM Formatter

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

@ -500,28 +500,15 @@ instance : Coe (Parenthesizer → Parenthesizer → Parenthesizer) Parenthesizer
builtin_initialize
registerAlias "ws" checkWsBefore.parenthesizer
registerAlias "noWs" checkNoWsBefore.parenthesizer
registerAlias "num" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer)
registerAlias "scientific" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "scientificLit" `scientificLit) scientificLitNoAntiquot.parenthesizer)
registerAlias "str" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.parenthesizer)
registerAlias "char" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer)
registerAlias "name" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer)
registerAlias "ident" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer)
registerAlias "colGt" checkColGt.parenthesizer
registerAlias "colGe" checkColGe.parenthesizer
registerAlias "lookahead" lookahead.parenthesizer
registerAlias "atomic" atomic.parenthesizer
registerAlias "many" many.parenthesizer
registerAlias "many1" many1.parenthesizer
registerAlias "notFollowedBy" notFollowedBy.parenthesizer
registerAlias "optional" optional.parenthesizer
registerAlias "withPosition" withPosition.parenthesizer
registerAlias "interpolatedStr" interpolatedStr.parenthesizer
registerAlias "sepBy" sepBy.parenthesizer
registerAlias "sepBy1" sepBy1.parenthesizer
registerAlias "orelse" orelse.parenthesizer
registerAlias "andthen" andthen.parenthesizer
registerAlias "sepByT" sepBy.parenthesizer
registerAlias "sepBy1T" sepBy1.parenthesizer
@[export lean_pretty_printer_parenthesizer_interpret_parser_descr]
unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer