From ebeec844af348d1a53ae245d88caea6563ad0575 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 4 Oct 2018 18:36:39 -0700 Subject: [PATCH] perf(library/init/lean/parser): minor performance tweaks --- library/init/lean/parser/basic.lean | 1 + library/init/lean/parser/token.lean | 6 +++--- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index 5879480e4a..67cf4305bc 100644 --- a/library/init/lean/parser/basic.lean +++ b/library/init/lean/parser/basic.lean @@ -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 diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index 71cc43b88d..9556ae97cd 100644 --- a/library/init/lean/parser/token.lean +++ b/library/init/lean/parser/token.lean @@ -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⟩]⟩