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

feat(library/init/lean/parser/parsec): mark whitespace and num with [noinline]

Browse source 
We want them to be specialized for a given monad stack, but not
inlined. If we inline them, then every occurrence of `whitespace` and
`num` will specialize the nested `take_while?` application.
This is bad since we don't cache them.
This commit is contained in:
Leonardo de Moura 2018-10-18 16:33:10 -07:00
parent 677864dee5
commit 0f7745a3e0
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
library/init/lean/parser/parsec.lean
View file

@ -438,7 +438,7 @@ lift $ λ it, take_while_aux' p it.remaining ff it
satisfy p *> take_while' p
/-- Consume zero or more whitespaces. -/
def whitespace : m unit :=
@[noinline] def whitespace : m unit :=
take_while' char.is_whitespace
/-- Shorthand for `p <* whitespace` -/
@ -446,7 +446,7 @@ take_while' char.is_whitespace
p <* whitespace
/-- Parse a numeral in decimal. -/
def num : m nat :=
@[noinline] def num : m nat :=
string.to_nat <$> (take_while1 char.is_digit)
/-- Succeed only if there are at least `n` characters left. -/