feat(library/init/lean/parser/token): cache hit statistics

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 :=

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]

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
    )
 

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 {