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

fix(kernel/type_checker): we must use different caches for infer_type and check

Browse source 
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 <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 12:23:07 -07:00
parent 687639a599
commit 7c0cc3111a
2 changed files with 21 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/kernel/type_checker.cpp
View file

@ -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<expr> m_infer_type_cache;
expr_bi_struct_map<expr> 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;
}

17
tests/lua/tc4.lua Normal file
View file

@ -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
))