perf(library/init/lean/parser): minor performance tweaks

This commit is contained in:
Sebastian Ullrich 2018-10-04 18:36:39 -07:00
parent d1b6b9721a
commit ebeec844af
2 changed files with 4 additions and 3 deletions

View file

@ -60,6 +60,7 @@ state_t parser_state $ parsec_t syntax $ state_t parser_cache $ m
@[derive monad alternative monad_reader monad_state monad_parsec monad_except]
def parser_t (ρ : Type) (m : Type → Type) [monad m] := reader_t ρ $ parser_core_t m
@[derive monad alternative monad_reader monad_state monad_parsec monad_except]
abbreviation basic_parser_m := parser_t parser_config id
abbreviation basic_parser := basic_parser_m syntax
abbreviation monad_basic_parser := has_monad_lift_t basic_parser_m

View file

@ -186,11 +186,11 @@ def symbol (sym : string) (lbp := 0) : parser :=
let sym := sym.trim in
lift $ try $ do {
it ← left_over,
stx@(syntax.atom ⟨_, sym'⟩) ← token | error "" (dlist.singleton (repr sym)) it,
stx@(syntax.atom ⟨_, sym'⟩) ← token | error "" (dlist.singleton sym) it,
when (sym ≠ sym') $
error ("token " ++ repr sym') (dlist.singleton (repr sym)) it,
error ("token " ++ sym') (dlist.singleton sym) it,
pure stx
} <?> repr sym
} <?> sym
instance symbol.tokens (sym lbp) : parser.has_tokens (symbol sym lbp : parser) :=
⟨[⟨sym.trim, lbp, none⟩]⟩