From 34cba1ec2eecba1f956ec5363de4cd4b8489bf0f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Nov 2020 06:42:25 -0800 Subject: [PATCH] feat: add `withPosition` and `checkCol` constructors --- src/Init/LeanInit.lean | 2 ++ src/Lean/Parser/Extension.lean | 2 ++ src/Lean/ParserCompiler.lean | 2 ++ src/Lean/PrettyPrinter/Formatter.lean | 2 ++ src/Lean/PrettyPrinter/Parenthesizer.lean | 2 ++ 5 files changed, 10 insertions(+) diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index d5bb9d0eec..35105f3eec 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -191,6 +191,8 @@ inductive ParserDescr | cat : Name → Nat → ParserDescr | parser : Name → ParserDescr | notFollowedBy : ParserDescr → ParserDescr + | withPosition : ParserDescr → ParserDescr + | checkCol : Bool → ParserDescr instance : Inhabited ParserDescr := ⟨ParserDescr.symbol ""⟩ abbrev TrailingParserDescr := ParserDescr diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index ebea0bb433..429c5da0e1 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -214,6 +214,8 @@ partial def compileParserDescr (env : Environment) (opts : Options) (categories | ParserDescr.nameLit => pure $ nameLit | ParserDescr.interpolatedStr d => interpolatedStr <$> visit d | ParserDescr.ident => pure $ ident + | ParserDescr.checkCol strict => pure $ if strict then checkColGt else checkColGe + | ParserDescr.withPosition d => withPosition <$> visit d | ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol tk includeIdent | ParserDescr.parser constName => do let (_, p) ← mkParserOfConstantAux env opts categories constName visit; diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 9635809846..1bf8c54e09 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -129,6 +129,8 @@ def compileEmbeddedParsers : ParserDescr → MetaM Unit | ParserDescr.node k prec d => compileEmbeddedParsers d | ParserDescr.trailingNode k prec d => compileEmbeddedParsers d | ParserDescr.interpolatedStr d => compileEmbeddedParsers d + | ParserDescr.withPosition d => compileEmbeddedParsers d + | ParserDescr.checkCol _ => pure () | ParserDescr.symbol tk => pure () | ParserDescr.numLit => pure () | ParserDescr.strLit => pure () diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 52f4cfca43..06bb67afb7 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -423,6 +423,8 @@ unsafe def interpretParserDescr : ParserDescr → CoreM Formatter | ParserDescr.interpolatedStr d => interpolatedStr.formatter <$> interpretParserDescr d | ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol.formatter tk | ParserDescr.noWs => pure $ checkNoWsBefore.formatter + | ParserDescr.withPosition d => withPosition.formatter <$> interpretParserDescr d + | ParserDescr.checkCol strict => pure $ if strict then checkColGt.formatter else checkColGe.formatter | ParserDescr.parser constName => combinatorFormatterAttribute.runDeclFor constName | ParserDescr.cat catName prec => pure $ categoryParser.formatter catName diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean index 77330b305a..0b2e0ed363 100644 --- a/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -500,6 +500,8 @@ unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer | ParserDescr.interpolatedStr d => interpolatedStr.parenthesizer <$> interpretParserDescr d | ParserDescr.nonReservedSymbol tk includeIdent => pure $ nonReservedSymbol.parenthesizer tk includeIdent | ParserDescr.noWs => pure $ checkNoWsBefore.parenthesizer + | ParserDescr.checkCol strict => pure $ if strict then checkColGt.parenthesizer else checkColGe.parenthesizer + | ParserDescr.withPosition d => withPosition.parenthesizer <$> interpretParserDescr d | ParserDescr.parser constName => combinatorParenthesizerAttribute.runDeclFor constName | ParserDescr.cat catName prec => pure $ categoryParser.parenthesizer catName prec