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

feat: add interpolatedStr to ParserDescr and Syntax

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-09 14:04:53 -07:00
parent 1b5bf34e1e
commit 7013ea4098
6 changed files with 22 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/LeanInit.lean
View file

@ -172,6 +172,7 @@ inductive ParserDescr
| strLit : ParserDescr
| charLit : ParserDescr
| nameLit : ParserDescr
| interpolatedStr : ParserDescr → ParserDescr -- interpolated string
| ident : ParserDescr
| cat : Name → Nat → ParserDescr
| parser : Name → ParserDescr

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

@ -7,6 +7,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
/-! Extensible parsing via attributes -/
import Lean.Parser.Basic
import Lean.Parser.StrInterpolation
import Lean.KeyedDeclsAttribute
namespace Lean
@ -214,6 +215,7 @@ partial def compileParserDescr (env : Environment) (categories : ParserCategorie
| ParserDescr.strLit => pure $ strLit
| ParserDescr.charLit => pure $ charLit
| ParserDescr.nameLit => pure $ nameLit
| ParserDescr.interpolatedStr d => interpolatedStr <$> compileParserDescr d
| ParserDescr.ident => pure $ ident
| ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol tk includeIdent
| ParserDescr.parser constName => do

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

@ -26,23 +26,24 @@ def «precedence» := parser! ":" >> precedenceLit
def optPrecedence := optional (try «precedence»)
namespace Syntax
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat := parser! ident >> optPrecedence
@[builtinSyntaxParser] def atom := parser! strLit
@[builtinSyntaxParser] def num := parser! nonReservedSymbol "num"
@[builtinSyntaxParser] def str := parser! nonReservedSymbol "str"
@[builtinSyntaxParser] def char := parser! nonReservedSymbol "char"
@[builtinSyntaxParser] def ident := parser! nonReservedSymbol "ident"
@[builtinSyntaxParser] def try := parser! nonReservedSymbol "try " >> syntaxParser maxPrec
@[builtinSyntaxParser] def lookahead := parser! nonReservedSymbol "lookahead " >> syntaxParser maxPrec
@[builtinSyntaxParser] def sepBy := parser! nonReservedSymbol "sepBy " >> syntaxParser maxPrec >> syntaxParser maxPrec
@[builtinSyntaxParser] def sepBy1 := parser! nonReservedSymbol "sepBy1 " >> syntaxParser maxPrec >> syntaxParser maxPrec
@[builtinSyntaxParser] def notFollowedBy := parser! nonReservedSymbol "notFollowedBy " >> syntaxParser maxPrec
@[builtinSyntaxParser] def paren := parser! "(" >> many1 syntaxParser >> ")"
@[builtinSyntaxParser] def cat := parser! ident >> optPrecedence
@[builtinSyntaxParser] def atom := parser! strLit
@[builtinSyntaxParser] def num := parser! nonReservedSymbol "num"
@[builtinSyntaxParser] def str := parser! nonReservedSymbol "str"
@[builtinSyntaxParser] def char := parser! nonReservedSymbol "char"
@[builtinSyntaxParser] def ident := parser! nonReservedSymbol "ident"
@[builtinSyntaxParser] def interpolatedStr := parser! nonReservedSymbol "interpolatedStr " >> syntaxParser maxPrec
@[builtinSyntaxParser] def try := parser! nonReservedSymbol "try " >> syntaxParser maxPrec
@[builtinSyntaxParser] def lookahead := parser! nonReservedSymbol "lookahead " >> syntaxParser maxPrec
@[builtinSyntaxParser] def sepBy := parser! nonReservedSymbol "sepBy " >> syntaxParser maxPrec >> syntaxParser maxPrec
@[builtinSyntaxParser] def sepBy1 := parser! nonReservedSymbol "sepBy1 " >> syntaxParser maxPrec >> syntaxParser maxPrec
@[builtinSyntaxParser] def notFollowedBy := parser! nonReservedSymbol "notFollowedBy " >> syntaxParser maxPrec
@[builtinSyntaxParser] def optional := tparser! "?"
@[builtinSyntaxParser] def many := tparser! "*"
@[builtinSyntaxParser] def many1 := tparser! "+"
@[builtinSyntaxParser] def orelse := tparser!:2 " <|> " >> syntaxParser 1
@[builtinSyntaxParser] def optional := tparser! "?"
@[builtinSyntaxParser] def many := tparser! "*"
@[builtinSyntaxParser] def many1 := tparser! "+"
@[builtinSyntaxParser] def orelse := tparser!:2 " <|> " >> syntaxParser 1
end Syntax

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

@ -15,7 +15,6 @@ already know the text following it and can decide whether or not whitespace betw
import Lean.CoreM
import Lean.Parser.Extension
import Lean.Parser.StrInterpolation
import Lean.KeyedDeclsAttribute
import Lean.ParserCompiler.Attribute
import Lean.PrettyPrinter.Backtrack

2
src/Lean/PrettyPrinter/Meta.lean
View file

@ -41,6 +41,7 @@ unsafe def interpretParserDescr : ParserDescr → AttrM Parenthesizer
| ParserDescr.charLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "charLit" `charLit) charLitNoAntiquot.parenthesizer
| ParserDescr.nameLit => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "nameLit" `nameLit) nameLitNoAntiquot.parenthesizer
| ParserDescr.ident => pure $ withAntiquot.parenthesizer (mkAntiquot.parenthesizer' "ident" `ident) identNoAntiquot.parenthesizer
| ParserDescr.interpolatedStr d => interpolatedStr.parenthesizer <$> interpretParserDescr d
| ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol.parenthesizer
| ParserDescr.parser constName => interpretParser (ctx interpretParserDescr) constName
| ParserDescr.cat catName prec => pure $ categoryParser.parenthesizer catName prec
@ -73,6 +74,7 @@ unsafe def interpretParserDescr : ParserDescr → AttrM Formatter
| ParserDescr.strLit => pure $ withAntiquot.formatter (mkAntiquot.formatter' "strLit" `strLit) strLitNoAntiquot.formatter
| ParserDescr.charLit => pure $ withAntiquot.formatter (mkAntiquot.formatter' "charLit" `charLit) charLitNoAntiquot.formatter
| ParserDescr.nameLit => pure $ withAntiquot.formatter (mkAntiquot.formatter' "nameLit" `nameLit) nameLitNoAntiquot.formatter
| ParserDescr.interpolatedStr d => interpolatedStr.formatter <$> interpretParserDescr d
| ParserDescr.ident => pure $ withAntiquot.formatter (mkAntiquot.formatter' "ident" `ident) identNoAntiquot.formatter
| ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol.formatter tk
| ParserDescr.parser constName => interpretParser (ctx interpretParserDescr) constName

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

@ -74,7 +74,6 @@ node).
import Lean.CoreM
import Lean.KeyedDeclsAttribute
import Lean.Parser.Extension
import Lean.Parser.StrInterpolation
import Lean.ParserCompiler.Attribute
import Lean.PrettyPrinter.Backtrack