From 24647cb7cb7182bbd47ffac3a4ce81aaacd87c26 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Jun 2019 09:01:20 -0700 Subject: [PATCH] fix(library/init/lean/parser/parser): better representation for many1 Syntax node --- library/init/lean/parser/parser.lean | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index bf783eb495..135ec8aa16 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -302,8 +302,15 @@ instance hashOrelse {k : ParserKind} : HasOrelse (Parser k) := { info := noFirstTokenInfo p.info, fn := manyFn p.fn } +@[inline] def many1Fn {k : ParserKind} (p : ParserFn k) : ParserFn k := +λ a c s, + let iniSz := s.stackSize; + let s := andthenFn p (manyAux p) a c s; + s.mkNode nullKind iniSz + @[inline] def many1 {k : ParserKind} (p : Parser k) : Parser k := -andthen p (many p) +{ info := p.info, + fn := many1Fn p.fn } @[specialize] private partial def sepByFnAux {k : ParserKind} (p : ParserFn k) (sep : ParserFn k) (allowTrailingSep : Bool) (iniSz : Nat) : Bool → ParserFn k | pOpt a c s :=