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

refactor(library/unifier): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-01 21:55:45 -08:00
parent e6672b958f
commit 19d14678ef
2 changed files with 2 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/library/unifier.cpp
View file

@ -266,15 +266,6 @@ static unsigned g_cnstr_group_first_index[g_num_groups] = { 0, g_group_size, 2*g
static unsigned get_group_first_index(cnstr_group g) { static unsigned get_group_first_index(cnstr_group g) {
return g_cnstr_group_first_index[static_cast<unsigned>(g)]; return g_cnstr_group_first_index[static_cast<unsigned>(g)];
} }
static unsigned get_group_last_index(cnstr_group g) {
unsigned g_idx = static_cast<unsigned>(g);
if (g_idx + 1 < g_num_groups) {
lean_assert(g_cnstr_group_first_index[g_idx+1] != 0);
return g_cnstr_group_first_index[g_idx+1]-1;
} else {
return std::numeric_limits<unsigned>::max();
}
}
static cnstr_group to_cnstr_group(unsigned d) { static cnstr_group to_cnstr_group(unsigned d) {
if (d >= g_num_groups) if (d >= g_num_groups)
d = g_num_groups-1; d = g_num_groups-1;
@ -518,13 +509,7 @@ struct unifier_fn {
/** \brief Add constraint to the constraint queue */ /** \brief Add constraint to the constraint queue */
unsigned add_cnstr(constraint const & c, cnstr_group g) { unsigned add_cnstr(constraint const & c, cnstr_group g) {
unsigned cidx; unsigned cidx = m_next_cidx + get_group_first_index(g);
if (g == cnstr_group::ClassInstance) {
// we use a stack discipline for solving class instances
cidx = get_group_last_index(g) - m_next_cidx;
} else {
cidx = m_next_cidx + get_group_first_index(g);
}
m_cnstrs.insert(cnstr(c, cidx)); m_cnstrs.insert(cnstr(c, cidx));
m_next_cidx++; m_next_cidx++;
return cidx; return cidx;

2
tests/lean/unique_instances.lean.expected.out
View file

@ -1,4 +1,4 @@
unique_instances.lean:6:0: error: ambiguous class-instance resolution, there is more than one solution unique_instances.lean:6:0: error: ambiguous class-instance resolution, there is more than one solution
prod.is_inhabited H₂ H₂ prod.is_inhabited H₂ H₂
and and
prod.is_inhabited H₁ H₂ prod.is_inhabited H₂ H₁