michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(kernel/converter): do not cache easy cases

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-12 05:39:14 +01:00
parent 391e5e2bc2
commit 80d1a6b993
1 changed files with 8 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/converter.cpp
View file

@ -255,6 +255,14 @@ struct default_converter : public converter {
/** \brief Put expression \c t in weak head normal form */
virtual expr whnf(expr const & e_prime, type_checker & c) {
// Do not cache easy cases
switch (e_prime.kind()) {
case expr_kind::Var: case expr_kind::Sort: case expr_kind::Meta: case expr_kind::Local: case expr_kind::Pi:
return e_prime;
case expr_kind::Lambda: case expr_kind::Macro: case expr_kind::App: case expr_kind::Constant:
break;
}
expr e = e_prime;
// check cache
if (m_memoize) {