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

refactor: move prioParser to Term.lean

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-14 17:33:38 -08:00
parent c0b90e9341
commit 69e8385f8d
2 changed files with 13 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

14
src/Lean/Parser/Syntax.lean
View file

@ -17,16 +17,9 @@ builtin_initialize
registerBuiltinParserAttribute `builtinPrecParser `prec (leadingIdentAsSymbol := true)
registerBuiltinDynamicParserAttribute `precParser `prec
builtin_initialize
registerBuiltinParserAttribute `builtinPrioParser `prio (leadingIdentAsSymbol := true)
registerBuiltinDynamicParserAttribute `prioParser `prio
@[inline] def precedenceParser (rbp : Nat := 0) : Parser :=
categoryParser `prec rbp
@[inline] def priorityParser (rbp : Nat := 0) : Parser :=
categoryParser `prio rbp
@[inline] def syntaxParser (rbp : Nat := 0) : Parser :=
categoryParser `stx rbp
@ -36,9 +29,6 @@ def optPrecedence := optional (atomic «precedence»)
namespace Syntax
@[builtinPrecParser] def numPrec := checkPrec maxPrec >> numLit
@[builtinPrioParser] def numPrio := checkPrec maxPrec >> numLit
@[builtinPrioParser] def highPrio := parser!:maxPrec nonReservedSymbol "high"
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat := parser! ident >> optPrecedence
@[builtinSyntaxParser] def unary := parser! ident >> checkNoWsBefore >> "(" >> many1 syntaxParser >> ")"
@ -58,10 +48,6 @@ namespace Term
end Term
namespace AttrParam
@[builtinAttrParamParser] def prio := parser!:maxPrec "priority: " >> priorityParser maxPrec
end AttrParam
namespace Command
def optPrio := optional ("[" >> priorityParser >> "]")

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

@ -13,6 +13,10 @@ builtin_initialize
registerBuiltinParserAttribute `builtinTacticParser `tactic (leadingIdentAsSymbol := true)
registerBuiltinDynamicParserAttribute `tacticParser `tactic
builtin_initialize
registerBuiltinParserAttribute `builtinPrioParser `prio (leadingIdentAsSymbol := true)
registerBuiltinDynamicParserAttribute `prioParser `prio
builtin_initialize
registerBuiltinParserAttribute `builtinAttrParamParser `attrParam (leadingIdentAsSymbol := true)
registerBuiltinDynamicParserAttribute `attrParamParser `attrParam
@ -20,6 +24,9 @@ builtin_initialize
@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
categoryParser `tactic rbp
@[inline] def priorityParser (rbp : Nat := 0) : Parser :=
categoryParser `prio rbp
@[inline] def attrParamParser (rbp : Nat := 0) : Parser :=
categoryParser `attrParam rbp
@ -40,10 +47,16 @@ end Tactic
def darrow : Parser := " => "
namespace Priority
@[builtinPrioParser] def numPrio := checkPrec maxPrec >> numLit
@[builtinPrioParser] def highPrio := parser!:maxPrec nonReservedSymbol "high"
end Priority
namespace AttrParam
@[builtinAttrParamParser] def ident := checkPrec maxPrec >> Parser.ident
@[builtinAttrParamParser] def str := checkPrec maxPrec >> strLit
@[builtinAttrParamParser] def num := checkPrec maxPrec >> numLit
@[builtinAttrParamParser] def prio := parser!:maxPrec "priority: " >> priorityParser maxPrec
end AttrParam
namespace Term