feat: add macro registerParserAlias!
It register the parser, parenthesizer, and formatter.
This commit is contained in:
Leonardo de Moura
parent
d30e96bc7d
commit
0510f746fc
5 changed files with 95 additions and 84 deletions
|
|
@ -198,7 +198,7 @@ inductive AliasValue (α : Type)
|
|||
|
||||
abbrev AliasTable (α) := NameMap (AliasValue α)
|
||||
|
||||
def registerAlias {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) (value : AliasValue α) : IO Unit := do
|
||||
def registerAliasCore {α} (mapRef : IO.Ref (AliasTable α)) (aliasName : Name) (value : AliasValue α) : IO Unit := do
|
||||
unless (← IO.initializing) do throw ↑"aliases can only be registered during initialization"
|
||||
if (← mapRef.get).contains aliasName then
|
||||
throw ↑s!"alias '{aliasName}' has already been declared"
|
||||
|
|
@ -229,34 +229,38 @@ abbrev ParserAliasValue := AliasValue Parser
|
|||
|
||||
builtin_initialize parserAliasesRef : IO.Ref (NameMap ParserAliasValue) ← IO.mkRef {}
|
||||
|
||||
-- Later, we define registerParserAlias which registers a parser, formatter and parenthesizer
|
||||
def registerParserAliasCore (aliasName : Name) (p : ParserAliasValue) : IO Unit := do
|
||||
registerAlias parserAliasesRef aliasName p
|
||||
-- Later, we define macro registerParserAlias! which registers a parser, formatter and parenthesizer
|
||||
def registerAlias (aliasName : Name) (p : ParserAliasValue) : IO Unit := do
|
||||
registerAliasCore parserAliasesRef aliasName p
|
||||
|
||||
instance : Coe Parser ParserAliasValue := { coe := AliasValue.const }
|
||||
instance : Coe (Parser → Parser) ParserAliasValue := { coe := AliasValue.unary }
|
||||
instance : Coe (Parser → Parser → Parser) ParserAliasValue := { coe := AliasValue.binary }
|
||||
|
||||
builtin_initialize
|
||||
registerParserAliasCore "ws" (AliasValue.const checkWsBefore)
|
||||
registerParserAliasCore "noWs" (AliasValue.const checkNoWsBefore)
|
||||
registerParserAliasCore "num" (AliasValue.const numLit)
|
||||
registerParserAliasCore "str" (AliasValue.const strLit)
|
||||
registerParserAliasCore "char" (AliasValue.const charLit)
|
||||
registerParserAliasCore "name" (AliasValue.const nameLit)
|
||||
registerParserAliasCore "ident" (AliasValue.const ident)
|
||||
registerParserAliasCore "colGt" (AliasValue.const checkColGt)
|
||||
registerParserAliasCore "colGe" (AliasValue.const checkColGe)
|
||||
registerParserAliasCore "lookahead" (AliasValue.unary lookahead)
|
||||
registerParserAliasCore "try" (AliasValue.unary «try»)
|
||||
registerParserAliasCore "many" (AliasValue.unary many)
|
||||
registerParserAliasCore "many1" (AliasValue.unary many1)
|
||||
registerParserAliasCore "notFollowedBy" (AliasValue.unary (notFollowedBy · "element"))
|
||||
registerParserAliasCore "optional" (AliasValue.unary optional)
|
||||
registerParserAliasCore "withPosition" (AliasValue.unary withPosition)
|
||||
registerParserAliasCore "interpolatedStr" (AliasValue.unary interpolatedStr)
|
||||
registerParserAliasCore "sepBy" (AliasValue.binary sepBy)
|
||||
registerParserAliasCore "sepBy1" (AliasValue.binary sepBy1)
|
||||
registerParserAliasCore "orelse" (AliasValue.binary orelse)
|
||||
registerParserAliasCore "andthen" (AliasValue.binary andthen)
|
||||
registerParserAliasCore "sepByT" (AliasValue.binary (sepBy (allowTrailingSep := true)))
|
||||
registerParserAliasCore "sepBy1T" (AliasValue.binary (sepBy1 (allowTrailingSep := true)))
|
||||
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 "try" «try»
|
||||
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
|
||||
|
|
|
|||
|
|
@ -3,9 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura, Sebastian Ullrich
|
||||
-/
|
||||
|
||||
import Lean.Parser.Basic
|
||||
|
||||
import Lean.Parser.Extension
|
||||
-- necessary for auto-generation
|
||||
import Lean.PrettyPrinter.Parenthesizer
|
||||
import Lean.PrettyPrinter.Formatter
|
||||
|
|
@ -71,5 +69,10 @@ namespace Parser
|
|||
attribute [runBuiltinParserAttributeHooks]
|
||||
ppHardSpace ppSpace ppLine ppGroup ppIndent ppDedent
|
||||
|
||||
macro "registerParserAlias!" aliasName:strLit declName:ident : term =>
|
||||
`(do Parser.registerAlias $aliasName $declName
|
||||
PrettyPrinter.Formatter.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `formatter))
|
||||
PrettyPrinter.Parenthesizer.registerAlias $aliasName $(mkIdentFrom declName (declName.getId ++ `parenthesizer)))
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -5,10 +5,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
|
|||
-/
|
||||
import Lean.Parser.Extra
|
||||
|
||||
-- necessary for auto-generation
|
||||
import Lean.PrettyPrinter.Parenthesizer
|
||||
import Lean.PrettyPrinter.Formatter
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
|
|
|
|||
|
|
@ -404,33 +404,37 @@ abbrev FormatterAliasValue := AliasValue Formatter
|
|||
|
||||
builtin_initialize formatterAliasesRef : IO.Ref (NameMap FormatterAliasValue) ← IO.mkRef {}
|
||||
|
||||
def registerFormatterAlias (aliasName : Name) (v : FormatterAliasValue) : IO Unit := do
|
||||
registerAlias formatterAliasesRef aliasName v
|
||||
def registerAlias (aliasName : Name) (v : FormatterAliasValue) : IO Unit := do
|
||||
Parser.registerAliasCore formatterAliasesRef aliasName v
|
||||
|
||||
instance : Coe Formatter FormatterAliasValue := { coe := AliasValue.const }
|
||||
instance : Coe (Formatter → Formatter) FormatterAliasValue := { coe := AliasValue.unary }
|
||||
instance : Coe (Formatter → Formatter → Formatter) FormatterAliasValue := { coe := AliasValue.binary }
|
||||
|
||||
builtin_initialize
|
||||
registerFormatterAlias "ws" (AliasValue.const checkWsBefore.formatter)
|
||||
registerFormatterAlias "noWs" (AliasValue.const checkNoWsBefore.formatter)
|
||||
registerFormatterAlias "num" (AliasValue.const $ withAntiquot.formatter (mkAntiquot.formatter' "numLit" `numLit) numLitNoAntiquot.formatter)
|
||||
registerFormatterAlias "str" (AliasValue.const $ withAntiquot.formatter (mkAntiquot.formatter' "strLit" `strLit) strLitNoAntiquot.formatter)
|
||||
registerFormatterAlias "char" (AliasValue.const $ withAntiquot.formatter (mkAntiquot.formatter' "charLit" `charLit) charLitNoAntiquot.formatter)
|
||||
registerFormatterAlias "name" (AliasValue.const $ withAntiquot.formatter (mkAntiquot.formatter' "nameLit" `nameLit) nameLitNoAntiquot.formatter)
|
||||
registerFormatterAlias "ident" (AliasValue.const $ withAntiquot.formatter (mkAntiquot.formatter' "ident" `ident) identNoAntiquot.formatter)
|
||||
registerFormatterAlias "colGt" (AliasValue.const checkColGt.formatter)
|
||||
registerFormatterAlias "colGe" (AliasValue.const checkColGe.formatter)
|
||||
registerFormatterAlias "lookahead" (AliasValue.unary lookahead.formatter)
|
||||
registerFormatterAlias "try" (AliasValue.unary try.formatter)
|
||||
registerFormatterAlias "many" (AliasValue.unary many.formatter)
|
||||
registerFormatterAlias "many1" (AliasValue.unary many1.formatter)
|
||||
registerFormatterAlias "notFollowedBy" (AliasValue.unary notFollowedBy.formatter)
|
||||
registerFormatterAlias "optional" (AliasValue.unary optional.formatter)
|
||||
registerFormatterAlias "withPosition" (AliasValue.unary withPosition.formatter)
|
||||
registerFormatterAlias "interpolatedStr" (AliasValue.unary interpolatedStr.formatter)
|
||||
registerFormatterAlias "sepBy" (AliasValue.binary sepBy.formatter)
|
||||
registerFormatterAlias "sepBy1" (AliasValue.binary sepBy1.formatter)
|
||||
registerFormatterAlias "orelse" (AliasValue.binary orelse.formatter)
|
||||
registerFormatterAlias "andthen" (AliasValue.binary andthen.formatter)
|
||||
registerFormatterAlias "sepByT" (AliasValue.binary sepBy.formatter)
|
||||
registerFormatterAlias "sepBy1T" (AliasValue.binary sepBy1.formatter)
|
||||
registerAlias "ws" checkWsBefore.formatter
|
||||
registerAlias "noWs" checkNoWsBefore.formatter
|
||||
registerAlias "num" (withAntiquot.formatter (mkAntiquot.formatter' "numLit" `numLit) numLitNoAntiquot.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 "try" try.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
|
||||
|
|
|
|||
|
|
@ -483,33 +483,37 @@ abbrev ParenthesizerAliasValue := AliasValue Parenthesizer
|
|||
|
||||
builtin_initialize parenthesizerAliasesRef : IO.Ref (NameMap ParenthesizerAliasValue) ← IO.mkRef {}
|
||||
|
||||
def registerParenthesizerAlias (aliasName : Name) (v : ParenthesizerAliasValue) : IO Unit := do
|
||||
registerAlias parenthesizerAliasesRef aliasName v
|
||||
def registerAlias (aliasName : Name) (v : ParenthesizerAliasValue) : IO Unit := do
|
||||
Parser.registerAliasCore parenthesizerAliasesRef aliasName v
|
||||
|
||||
instance : Coe Parenthesizer ParenthesizerAliasValue := { coe := AliasValue.const }
|
||||
instance : Coe (Parenthesizer → Parenthesizer) ParenthesizerAliasValue := { coe := AliasValue.unary }
|
||||
instance : Coe (Parenthesizer → Parenthesizer → Parenthesizer) ParenthesizerAliasValue := { coe := AliasValue.binary }
|
||||
|
||||
builtin_initialize
|
||||
registerParenthesizerAlias "ws" (AliasValue.const checkWsBefore.parenthesizer)
|
||||
registerParenthesizerAlias "noWs" (AliasValue.const checkNoWsBefore.parenthesizer)
|
||||
registerParenthesizerAlias "num" (AliasValue.const $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.parenthesizer)
|
||||
registerParenthesizerAlias "str" (AliasValue.const $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "strLit" `strLit) strLitNoAntiquot.parenthesizer)
|
||||
registerParenthesizerAlias "char" (AliasValue.const $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer)
|
||||
registerParenthesizerAlias "name" (AliasValue.const $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer)
|
||||
registerParenthesizerAlias "ident" (AliasValue.const $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer)
|
||||
registerParenthesizerAlias "colGt" (AliasValue.const checkColGt.parenthesizer)
|
||||
registerParenthesizerAlias "colGe" (AliasValue.const checkColGe.parenthesizer)
|
||||
registerParenthesizerAlias "lookahead" (AliasValue.unary lookahead.parenthesizer)
|
||||
registerParenthesizerAlias "try" (AliasValue.unary try.parenthesizer)
|
||||
registerParenthesizerAlias "many" (AliasValue.unary many.parenthesizer)
|
||||
registerParenthesizerAlias "many1" (AliasValue.unary many1.parenthesizer)
|
||||
registerParenthesizerAlias "notFollowedBy" (AliasValue.unary notFollowedBy.parenthesizer)
|
||||
registerParenthesizerAlias "optional" (AliasValue.unary optional.parenthesizer)
|
||||
registerParenthesizerAlias "withPosition" (AliasValue.unary withPosition.parenthesizer)
|
||||
registerParenthesizerAlias "interpolatedStr" (AliasValue.unary interpolatedStr.parenthesizer)
|
||||
registerParenthesizerAlias "sepBy" (AliasValue.binary sepBy.parenthesizer)
|
||||
registerParenthesizerAlias "sepBy1" (AliasValue.binary sepBy1.parenthesizer)
|
||||
registerParenthesizerAlias "orelse" (AliasValue.binary orelse.parenthesizer)
|
||||
registerParenthesizerAlias "andthen" (AliasValue.binary andthen.parenthesizer)
|
||||
registerParenthesizerAlias "sepByT" (AliasValue.binary sepBy.parenthesizer)
|
||||
registerParenthesizerAlias "sepBy1T" (AliasValue.binary sepBy1.parenthesizer)
|
||||
registerAlias "ws" checkWsBefore.parenthesizer
|
||||
registerAlias "noWs" checkNoWsBefore.parenthesizer
|
||||
registerAlias "num" (withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "numLit" `numLit) numLitNoAntiquot.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 "try" try.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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue