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

fix(library/init/lean/parser/parser): better representation for many1 Syntax node

Browse source
This commit is contained in:
Leonardo de Moura 2019-06-30 09:01:20 -07:00
parent 531ef5d700
commit 24647cb7cb
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
library/init/lean/parser/parser.lean
View file

@ -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 :=