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

Fix bug in has_free_vars_fn. Add optimization to type_checker.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-10 22:05:04 -07:00
parent 3a1514982f
commit 5c6ee647a9
3 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/free_vars.cpp
View file

@ -63,7 +63,7 @@ protected:
break; break;
} }
if (m_set_closed_flag && !result) if (m_set_closed_flag && !result && offset == 0)
e.raw()->set_closed(); e.raw()->set_closed();
return result; return result;

4
src/kernel/type_check.cpp
View file

@ -128,7 +128,9 @@ struct infer_type_fn {
buffer << "\nin context:\n" << ctx; buffer << "\nin context:\n" << ctx;
throw exception(buffer.str()); throw exception(buffer.str());
} }
if (closed(c)) if (closed(abst_body(f_t)))
f_t = abst_body(f_t);
else if (closed(c))
f_t = instantiate_with_closed(abst_body(f_t), c); f_t = instantiate_with_closed(abst_body(f_t), c);
else else
f_t = instantiate(abst_body(f_t), c); f_t = instantiate(abst_body(f_t), c);

2
src/tests/kernel/type_check.cpp
View file

@ -89,7 +89,7 @@ static void tst5() {
env.add_var("P", Bool); env.add_var("P", Bool);
expr P = Const("P"); expr P = Const("P");
expr H = Const("H"); expr H = Const("H");
unsigned n = 500; unsigned n = 4000;
expr prop = P; expr prop = P;
expr pr = H; expr pr = H;
for (unsigned i = 1; i < n; i++) { for (unsigned i = 1; i < n; i++) {