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

perf(library/init/lean/parser/token): inline hot polymorphic functions

Browse source 
Decreases parser runtime by ~15%
This commit is contained in:
Sebastian Ullrich 2018-09-27 12:29:10 -07:00
parent 8556365e9c
commit e535cd92f7
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/parser/token.lean
View file

@ -60,7 +60,7 @@ hidden $ do
section
variables [monad m] [monad_parsec syntax m]
def as_substring {α : Type} (p : m α) : m substring :=
@[inline] def as_substring {α : Type} (p : m α) : m substring :=
do start ← left_over,
p,
stop ← left_over,
@ -68,7 +68,7 @@ do start ← left_over,
variables [monad_state parser_state m] [monad_basic_parser m]
def with_source_info {α : Type} (r : m α) (trailing_ws := tt) : m (α × source_info) :=
@[inline] def with_source_info {α : Type} (r : m α) (trailing_ws := tt) : m (α × source_info) :=
do it ← left_over,
let leading : substring := ⟨it, it⟩, -- NOTE: will be adjusted by `syntax.update_leading`
a ← r,
@ -79,7 +79,7 @@ do it ← left_over,
pure (a, ⟨leading, it.offset, trailing⟩)
/-- Match an arbitrary parser and return the consumed string in a `syntax.atom`. -/
def raw {α : Type} (p : m α) (trailing_ws := ff) : parser :=
@[inline] def raw {α : Type} (p : m α) (trailing_ws := ff) : parser :=
try $ do
(ss, info) ← with_source_info (as_substring p) trailing_ws,
pure $ syntax.atom ⟨info, ss.to_string⟩