chore: remove nodeSepBy1Unbox combinator

This commit is contained in:
Leonardo de Moura 2020-10-06 07:43:30 -07:00
parent e635196f32
commit 5c74c408ae
3 changed files with 0 additions and 23 deletions

View file

@ -604,13 +604,6 @@ fun c s =>
@[inline] def many1Unbox (p : Parser) : Parser :=
withResultOf (many1 p) fun stx => if stx.getNumArgs == 1 then stx.getArg 0 else stx
@[inline] def nodeSepBy1Unbox (k : SyntaxNodeKind) (p sep : Parser) (allowTrailingSep := false) : Parser :=
withResultOf (node k (sepBy1 p sep allowTrailingSep)) fun stx =>
if (stx.getArg 0).getNumArgs < 2 then
(stx.getArg 0).getArg 0
else
stx
@[specialize] partial def satisfyFn (p : Char → Bool) (errorMsg : String := "unexpected character") : ParserFn
| c, s =>
let i := s.pos;

View file

@ -357,14 +357,6 @@ concatArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0
@[combinatorFormatter sepBy1] def sepBy1.formatter := sepBy.formatter
@[combinatorFormatter Parser.nodeSepBy1Unbox]
def nodeSepBy1Unbox.formatter (k : SyntaxNodeKind) (p sep : Formatter) : Formatter := do
stx ← getCur;
if stx.getKind == k then do
node.formatter k $ sepBy.formatter p sep
else
p
@[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := do
p
@[combinatorFormatter Lean.Parser.withoutPosition] def withoutPosition.formatter (p : Formatter) : Formatter := do

View file

@ -422,14 +422,6 @@ visitArgs $ (List.range stx.getArgs.size).reverse.forM $ fun i => if i % 2 == 0
@[combinatorParenthesizer Lean.Parser.sepBy1] def sepBy1.parenthesizer := sepBy.parenthesizer
@[combinatorParenthesizer Lean.Parser.nodeSepBy1Unbox]
def nodeSepBy1Unbox.parenthesizer (k : SyntaxNodeKind) (p pSep : Parenthesizer) : Parenthesizer := do
stx ← getCur;
if stx.getKind == k then
node.parenthesizer k $ sepBy.parenthesizer p pSep
else
p
@[combinatorParenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
p
@[combinatorParenthesizer Lean.Parser.withoutPosition] def withoutPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do