max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf(library/init/lean/ir/extract_cpp): use derive to speedup type class resolution

Browse source 
This modification reduced processing time for this file to 1.49 secs
from 2.30 secs on my office desktop.
This commit is contained in:
Leonardo de Moura 2018-10-12 12:27:08 -07:00
parent 17d6ef3abe
commit 5810418ddd
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/ir/extract_cpp.lean
View file

@ -42,7 +42,8 @@ structure extract_env :=
(cfg : extract_cpp_config)
(ctx : context := mk_context)
@[reducible] def extract_m := reader_t extract_env (except_t format (state_t string id))
@[derive monad monad_except monad_state monad_reader monad_run]
def extract_m := reader_t extract_env (except_t format (state_t string id))
def emit {α} [has_to_string α] (a : α) : extract_m unit :=
modify (++ (to_string a))
@ -378,11 +379,14 @@ match d with
when (need_uncurry d) (emit_uncurry d)
| _ := pure ()
section
local attribute [reducible] extract_m
def emit_def (d : decl) : extract_m unit :=
do env ← read,
ctx ← monad_lift $ infer_types d env.cfg.env,
adapt_reader (λ env : extract_env, {ctx := ctx, ..env}) $
emit_def_core d
end
def collect_used (d : list decl) : fnid_set :=
d.foldl (λ s d, match d with