From 0f7745a3e0cf00f5a7c4e6f007cc96d835259b7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Oct 2018 16:33:10 -0700 Subject: [PATCH] feat(library/init/lean/parser/parsec): mark `whitespace` and `num` with `[noinline]` 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. --- library/init/lean/parser/parsec.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index a0cec2f8b0..0c17fce496 100644 --- a/library/init/lean/parser/parsec.lean +++ b/library/init/lean/parser/parsec.lean @@ -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. -/