diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 812917d548..a7fce0cc59 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -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 diff --git a/src/Lean/Parser/Extra.lean b/src/Lean/Parser/Extra.lean index d0dd8f88c0..20464de76f 100644 --- a/src/Lean/Parser/Extra.lean +++ b/src/Lean/Parser/Extra.lean @@ -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 diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean index e584d5f6a8..98a0687fc1 100644 --- a/src/Lean/Parser/Level.lean +++ b/src/Lean/Parser/Level.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 diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 8bb47e05ae..fa880fadc5 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -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 diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index a81ec748d1..d33ad8cf7e 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -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