From 468ac814a761a4894de4b8e56d600b63d296a6bc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 13 Sep 2018 17:54:40 -0700 Subject: [PATCH] perf(library/init/lean/parser/token): move `number'` out of `longest_match` call --- library/init/lean/parser/parsec.lean | 2 +- library/init/lean/parser/token.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/parser/parsec.lean b/library/init/lean/parser/parsec.lean index 3918b25c17..abca4ab3b3 100644 --- a/library/init/lean/parser/parsec.lean +++ b/library/init/lean/parser/parsec.lean @@ -221,7 +221,7 @@ def not_followed_by (p : parsec' α) (msg : string := "input") : parsec' unit := def dbg (label : string) (p : parsec_t μ m α) : parsec_t μ m α := λ it, do r ← p it, - pure $ trace ("DBG " ++ label ++ ": '" ++ (it.extract (it.nextn 40)).get_or_else "" ++ "'") $ match r : _ → result μ α with + pure $ trace ("DBG " ++ label ++ ": \"" ++ (it.extract (it.nextn 40)).get_or_else "" ++ "\"") $ match r : _ → result μ α with | ok a it' := trace ("consumed ok : '" ++ (it.extract it').get_or_else "" ++ "'") $ @ok μ α a it' | ok_eps a it' ex := trace ("empty ok : '" ++ (it.extract it').get_or_else "" ++ "'") $ @ok_eps μ α a it' ex | error msg tt := trace ("consumed error : '" ++ (it.extract msg.it).get_or_else "" ++ "'\n" ++ to_string msg) $ @error μ α msg tt diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index f3f27a1610..62f7706075 100644 --- a/library/init/lean/parser/token.lean +++ b/library/init/lean/parser/token.lean @@ -108,7 +108,7 @@ def token : basic_parser_m syntax := do (r, i) ← with_source_info $ do { -- NOTE the order: if a token is both a symbol and a valid identifier (i.e. a keyword), -- we want it to be recognized as a symbol - f::_ ← longest_match [symbol', ident', number'] | failure, + f::_ ← longest_match [symbol', ident'] <|> list.ret <$> number' | failure, pure f }, pure (r i)