From 321105099fc22197923b9a7b4641cdee17b75baa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Feb 2017 20:17:25 -0800 Subject: [PATCH] feat(library/type_context): add compilation flag for disabling type inference cache --- src/CMakeLists.txt | 5 +++++ src/library/type_context.cpp | 4 ++++ tmp/perf.info | 26 ++++++++++++++++++++++++++ 3 files changed, 35 insertions(+) create mode 100644 tmp/perf.info diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index acfb595301..95d5f05704 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -40,6 +40,7 @@ option(FREE_VAR_RANGE_OPT "FREE_VAR_RANGE_OPT" ON) option(HAS_LOCAL_OPT "HAS_LOCAL_OPT" ON) option(ABSTRACTION_CACHE "ABSTRACTION_CACHE" ON) option(TYPE_CLASS_CACHE "TYPE_CLASS_CACHE" ON) +option(TYPE_INFER_CACHE "TYPE_INFER_CACHE" ON) # emacs site-lisp dir set(EMACS_LISP_DIR "share/emacs/site-lisp/lean" CACHE STRING "emacs site-lisp dir") @@ -64,6 +65,10 @@ if (NOT("${TYPE_CLASS_CACHE}" MATCHES "ON")) set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_NO_TYPE_CLASS_CACHE") endif() +if (NOT("${TYPE_INFER_CACHE}" MATCHES "ON")) + set(LEAN_EXTRA_CXX_FLAGS "${LEAN_EXTRA_CXX_FLAGS} -D LEAN_NO_TYPE_INFER_CACHE") +endif() + message(STATUS "Lean emacs-mode will be installed at " "${CMAKE_INSTALL_PREFIX}/${EMACS_LISP_DIR}") message(STATUS "Lean library will be installed at " diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index cd1b75f2d4..aac60b21b2 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -859,11 +859,13 @@ expr type_context::infer_core(expr const & e) { lean_assert(!is_var(e)); lean_assert(closed(e)); +#ifndef LEAN_NO_TYPE_INFER_CACHE auto & cache = m_cache->m_infer_cache; unsigned postponed_sz = m_postponed.size(); auto it = cache.find(e); if (it != cache.end()) return it->second; +#endif reset_used_assignment reset(*this); @@ -900,8 +902,10 @@ expr type_context::infer_core(expr const & e) { break; } +#ifndef LEAN_NO_TYPE_INFER_CACHE if (!m_used_assignment && postponed_sz == m_postponed.size()) cache.insert(mk_pair(e, r)); +#endif return r; } diff --git a/tmp/perf.info b/tmp/perf.info new file mode 100644 index 0000000000..27baf525d0 --- /dev/null +++ b/tmp/perf.info @@ -0,0 +1,26 @@ +NO FREE VAR OPT base + +../../library/init/algebra/ordered_field.lean 2.64 2.00 +../../library/init/algebra/ordered_group.lean 1.76 1.55 +../../library/init/data/list/lemmas.lean 1.18 1.16 + + +NO HAS LOCAL + +../../library/init/algebra/ordered_field.lean 2.00 2.00 +../../library/init/algebra/ordered_group.lean 1.55 1.55 +../../library/init/data/list/lemmas.lean 1.18 1.16 + +NO TYPE CLASS CACHE + +../../library/init/algebra/ordered_field.lean 2.20 2.00 +../../library/init/algebra/ordered_group.lean 1.58 1.55 +../../library/init/data/list/lemmas.lean 1.22 1.16 +../../perf/bench30.lean 1.08 (0.62) 0.74 (0.30 elab) (over 2300 type class resolution problems) + +NO TYPE INFERENCE CACHE + +../../library/init/algebra/ordered_field.lean 2.14 2.00 +../../library/init/algebra/ordered_group.lean 1.57 1.55 +../../library/init/data/list/lemmas.lean 1.17 1.16 +../../perf/bench30.lean 1.30 (0.83) 0.74 (0.30 elab) (over 2300 type class resolution problems)