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

refactor: remove redundancy from common register_parser_alias case

Browse source 
/cc @leodemoura
This commit is contained in:
Sebastian Ullrich 2021-09-20 13:19:36 +02:00
parent 83c2e8bf75
commit 585fba69e8
6 changed files with 40 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/Lean/Parser.lean
View file

@ -26,21 +26,21 @@ builtin_initialize
register_parser_alias "str" strLit
register_parser_alias "char" charLit
register_parser_alias "name" nameLit
register_parser_alias "ident" ident
register_parser_alias ident
register_parser_alias "colGt" checkColGt
register_parser_alias "colGe" checkColGe
register_parser_alias "lookahead" lookahead
register_parser_alias "atomic" atomic
register_parser_alias "many" many
register_parser_alias "many1" many1
register_parser_alias "manyIndent" manyIndent
register_parser_alias "many1Indent" many1Indent
register_parser_alias "optional" optional
register_parser_alias "withPosition" withPosition
register_parser_alias "interpolatedStr" interpolatedStr
register_parser_alias "orelse" orelse
register_parser_alias "andthen" andthen
register_parser_alias "incQuotDepth" incQuotDepth
register_parser_alias lookahead
register_parser_alias atomic
register_parser_alias many
register_parser_alias many1
register_parser_alias manyIndent
register_parser_alias many1Indent
register_parser_alias optional
register_parser_alias withPosition
register_parser_alias interpolatedStr
register_parser_alias orelse
register_parser_alias andthen
register_parser_alias incQuotDepth
registerAlias "notFollowedBy" (notFollowedBy · "element")
Parenthesizer.registerAlias "notFollowedBy" notFollowedBy.parenthesizer

10
src/Lean/Parser/Command.lean
View file

@ -116,11 +116,11 @@ def openDecl := openHiding <|> openRenaming <|> openOnly <|> openSimple
builtin_initialize
register_parser_alias "declModifiers" declModifiersF
register_parser_alias "nestedDeclModifiers" declModifiersT
register_parser_alias "declId" declId
register_parser_alias "declSig" declSig
register_parser_alias "declVal" declVal
register_parser_alias "optDeclSig" optDeclSig
register_parser_alias "openDecl" openDecl
register_parser_alias declId
register_parser_alias declSig
register_parser_alias declVal
register_parser_alias optDeclSig
register_parser_alias openDecl
end Command

4
src/Lean/Parser/Do.lean
View file

@ -28,8 +28,8 @@ def termBeforeDo := withForbidden "do" termParser
attribute [runBuiltinParserAttributeHooks] doSeq termBeforeDo
builtin_initialize
register_parser_alias "doSeq" doSeq
register_parser_alias "termBeforeDo" termBeforeDo
register_parser_alias doSeq
register_parser_alias termBeforeDo
def notFollowedByRedefinedTermToken :=
-- Remark: we don't currently support `open` and `set_option` in `do`-blocks, but we include them in the following list to fix the ambiguity

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

@ -98,19 +98,20 @@ namespace Parser
attribute [runBuiltinParserAttributeHooks]
ppHardSpace ppSpace ppLine ppGroup ppIndent ppDedent
macro "register_parser_alias" aliasName:strLit declName:ident : term =>
macro "register_parser_alias" aliasName?:optional(strLit) declName:ident : term =>
let aliasName := aliasName?.getD (Syntax.mkStrLit declName.getId.toString)
`(do Parser.registerAlias $aliasName $declName
PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter))
PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))
builtin_initialize
register_parser_alias "group" group
register_parser_alias "ppHardSpace" ppHardSpace
register_parser_alias "ppSpace" ppSpace
register_parser_alias "ppLine" ppLine
register_parser_alias "ppGroup" ppGroup
register_parser_alias "ppIndent" ppIndent
register_parser_alias "ppDedent" ppDedent
register_parser_alias group
register_parser_alias ppHardSpace
register_parser_alias ppSpace
register_parser_alias ppLine
register_parser_alias ppGroup
register_parser_alias ppIndent
register_parser_alias ppDedent
end Parser

2
src/Lean/Parser/Tactic.lean
View file

@ -10,7 +10,7 @@ namespace Parser
namespace Tactic
builtin_initialize
register_parser_alias "tacticSeq" tacticSeq
register_parser_alias tacticSeq
@[builtinTacticParser] def «unknown» := leading_parser withPosition (ident >> errorAtSavedPos "unknown tactic" true)
@[builtinTacticParser] def nestedTactic := tacticSeqBracketed

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

@ -269,16 +269,17 @@ end Term
@[builtinTermParser] def Level.quot : Parser := leading_parser "`(level|" >> incQuotDepth levelParser >> ")"
open Term in
builtin_initialize
register_parser_alias "letDecl" Term.letDecl
register_parser_alias "haveDecl" Term.haveDecl
register_parser_alias "sufficesDecl" Term.sufficesDecl
register_parser_alias "letRecDecls" Term.letRecDecls
register_parser_alias "hole" Term.hole
register_parser_alias "syntheticHole" Term.syntheticHole
register_parser_alias "matchDiscr" Term.matchDiscr
register_parser_alias "bracketedBinder" Term.bracketedBinder
register_parser_alias "attrKind" Term.attrKind
register_parser_alias letDecl
register_parser_alias haveDecl
register_parser_alias sufficesDecl
register_parser_alias letRecDecls
register_parser_alias hole
register_parser_alias syntheticHole
register_parser_alias matchDiscr
register_parser_alias bracketedBinder
register_parser_alias attrKind
end Parser
end Lean