diff --git a/library/init/lean/parser/basic.lean b/library/init/lean/parser/basic.lean index d47790c2c3..456d67c523 100644 --- a/library/init/lean/parser/basic.lean +++ b/library/init/lean/parser/basic.lean @@ -54,6 +54,8 @@ structure token_cache_entry := -- Non-backtrackable state structure parser_cache := (token_cache : option token_cache_entry := none) +-- for profiling +(hit miss : nat := 0) /- Remark: if we have a node in the trie with `some token_config`, the string induced by the path is equal to the `token_config.prefix`. -/ structure parser_config := diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean index d41b4bccaf..2a1d27b7a8 100644 --- a/library/init/lean/parser/module.lean +++ b/library/init/lean/parser/module.lean @@ -28,6 +28,8 @@ instance module_parser_config_coe : has_coe module_parser_config command_parser_ structure module_parser_output := (cmd : syntax) (messages : message_log) +-- to access the profile data inside +(cache : parser_cache) section local attribute [reducible] parser_core_t @@ -54,7 +56,8 @@ end namespace module def yield_command (cmd : syntax) : module_parser_m unit := do st ← get, - yield {cmd := cmd, messages := st.messages}, + cache ← monad_lift get_cache, + yield {cmd := cmd, messages := st.messages, cache := cache}, put {st with messages := message_log.empty} @[derive parser.has_view parser.has_tokens] diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index f402074370..f3d4a15512 100644 --- a/library/init/lean/parser/token.lean +++ b/library/init/lean/parser/token.lean @@ -164,6 +164,7 @@ do it ← left_over, guard (it.offset = tkc.start_it.offset), -- hackishly update parsec position monad_parsec.lift (λ it, parsec.result.ok () tkc.stop_it none), + put_cache {cache with hit := cache.hit + 1}, pure tkc.tk ) (λ _, do -- cache failed, update cache @@ -186,7 +187,7 @@ do it ← left_over, | none, except.error _ := number' <|> string_lit', tk ← with_trailing tk, new_it ← left_over, - put_cache {cache with token_cache := some ⟨it, new_it, tk⟩}, + put_cache {cache with token_cache := some ⟨it, new_it, tk⟩, miss := cache.miss + 1}, pure tk ) diff --git a/tests/lean/parser1.lean b/tests/lean/parser1.lean index 8967e175ef..f100aa5d6c 100644 --- a/tests/lean/parser1.lean +++ b/tests/lean/parser1.lean @@ -115,6 +115,8 @@ def run_frontend (input : string) : except_t string io unit := do when ¬(cmd'.is_of_kind module.eoi) $ io.println "elaborator died!!", msgs.to_list.mfor $ λ e, io.println e.text, + io.println $ "parser cache hit rate: " ++ to_string out.cache.hit ++ "/" ++ + to_string (out.cache.hit + out.cache.miss), pure $ sum.inr (out::outs).reverse } | coroutine_result_core.yielded elab_out elab_k := do {