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

Fix nontermination problem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-30 17:18:39 -07:00
parent 4c27530930
commit 793468072b
2 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/elaborator.cpp
View file

@ -51,9 +51,11 @@ class elaborator::imp {
expr m_type;
expr m_mvar;
context m_ctx;
bool m_mark; // for implementing occurs check
bool m_mark; // for implementing occurs check
bool m_type_cnstr; // true when type constraint was already generated
metavar_info() {
m_mark = false;
m_type_cnstr = false;
}
};
@ -452,9 +454,10 @@ class elaborator::imp {
unsolved_midx = midx;
cont = true; // must continue
} else {
if (m_metavars[midx].m_type) {
if (m_metavars[midx].m_type && !m_metavars[midx].m_type_cnstr) {
try {
expr t = infer(m_metavars[midx].m_assignment, m_metavars[midx].m_ctx);
m_metavars[midx].m_type_cnstr = true;
m_constraints.push_back(constraint(m_metavars[midx].m_type, t, m_metavars[midx].m_ctx,
m_metavars[midx].m_mvar, m_metavars[midx].m_ctx, static_cast<unsigned>(-1)));
progress = true;
@ -537,4 +540,5 @@ void elaborator::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
void elaborator::clear() { m_ptr->clear(); }
environment const & elaborator::get_environment() const { return m_ptr->get_environment(); }
void elaborator::display(std::ostream & out) const { m_ptr->display(out); }
void elaborator::print(imp * ptr) { ptr->display(std::cout); }
}

1
src/library/elaborator.h
View file

@ -17,6 +17,7 @@ namespace lean {
class elaborator {
class imp;
std::shared_ptr<imp> m_ptr;
static void print(imp * ptr);
public:
explicit elaborator(environment const & env);
~elaborator();