perf(library/init/lean/parser/parsec): optimize str and raw_str
Both `str` amd `raw_str` are used with string literals. This commit makes sure we don't need to recompute the nested term `dlist.singleton (repr s)`. This modification saves .2 secs when parsing `core.lean` on my MacBook. cc @kha
This commit is contained in:
parent
eaeb0a40a5
commit
0dfeb8a79c
2 changed files with 6 additions and 3 deletions
|
|
@ -362,11 +362,14 @@ This parser consumes no input if it fails (even if a partial match).
|
|||
Note: The behaviour of this parser is different to that the `string` parser in the Parsec_t Μ M Haskell library,
|
||||
as this one is all-or-nothing.
|
||||
-/
|
||||
def str (s : string) : m string :=
|
||||
def str_core (s : string) (ex : dlist string) : m string :=
|
||||
if s.is_empty then pure ""
|
||||
else lift $ λ it, match str_aux s.length s.mk_iterator it with
|
||||
| some it' := result.ok s it' none
|
||||
| none := result.error { it := it, expected := dlist.singleton (repr s), custom := none } ff
|
||||
| none := result.error { it := it, expected := ex, custom := none } ff
|
||||
|
||||
@[inline] def str (s : string) : m string :=
|
||||
str_core s (dlist.singleton (repr s))
|
||||
|
||||
private def take_aux : nat → string → iterator → result μ string
|
||||
| 0 r it := result.ok r it none
|
||||
|
|
|
|||
|
|
@ -107,7 +107,7 @@ instance raw.view {α} (p : m α) (t) : parser.has_view (option syntax_atom) (ra
|
|||
review := λ a, (syntax.atom <$> a).get_or_else syntax.missing }
|
||||
|
||||
/-- Like `raw (str s)`, but default to `s` in views. -/
|
||||
@[derive has_tokens has_view]
|
||||
@[inline, derive has_tokens has_view]
|
||||
def raw_str (s : string) (trailing_ws := ff) : parser :=
|
||||
raw (str s) trailing_ws
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue