From 7c0cc3111a24946fc110fe7eecfd0bf2664a3ad5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 May 2014 12:23:07 -0700 Subject: [PATCH] fix(kernel/type_checker): we must use different caches for infer_type and check The new test tc4.lua exposes the problem being fixed. We need separate caches otherwise we may mistakenly assume that an expression was already checked by the type checker, while only its type was inferred. Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 8 ++++---- tests/lua/tc4.lua | 17 +++++++++++++++++ 2 files changed, 21 insertions(+), 4 deletions(-) create mode 100644 tests/lua/tc4.lua diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index b573ab6180..ce9c663890 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -64,7 +64,7 @@ struct type_checker::imp { // Examples: // The type of (lambda x : A, t) is (Pi x : A, typeof(t)) // The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t)) - expr_bi_struct_map m_infer_type_cache; + expr_bi_struct_map m_infer_type_cache[2]; converter_context m_conv_ctx; type_checker_context m_tc_ctx; bool m_memoize; @@ -280,8 +280,8 @@ struct type_checker::imp { check_system("type checker"); if (m_memoize) { - auto it = m_infer_type_cache.find(e); - if (it != m_infer_type_cache.end()) + auto it = m_infer_type_cache[infer_only].find(e); + if (it != m_infer_type_cache[infer_only].end()) return it->second; } @@ -378,7 +378,7 @@ struct type_checker::imp { } if (m_memoize) - m_infer_type_cache.insert(mk_pair(e, r)); + m_infer_type_cache[infer_only].insert(mk_pair(e, r)); return r; } diff --git a/tests/lua/tc4.lua b/tests/lua/tc4.lua new file mode 100644 index 0000000000..cba4c235ef --- /dev/null +++ b/tests/lua/tc4.lua @@ -0,0 +1,17 @@ +local env = empty_environment() +env = add_decl(env, mk_var_decl("or", mk_arrow(Bool, Bool, Bool))) +env = add_decl(env, mk_var_decl("A", Bool)) +local Or = Const("or") +local A = Const("A") +local B = Const("B") +local tc = type_checker(env) +local F = Or(A, B) +assert(tc:infer(F) == Bool) +assert(not pcall(function() + -- The following test must fail since B is not + -- declared in env. + -- This test make sure that infer and check are + -- not sharing the same cache. + print(tc:check(F)) + end +))