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

feat(library/head_map): support local name in the head_map

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-10 20:02:31 -08:00
parent bd06bf9fb1
commit 41e14fddf8
2 changed files with 7 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/head_map.cpp
View file

@ -22,13 +22,15 @@ head_index::head_index(expr const & e) {
}
m_kind = f.kind();
if (is_constant(f))
m_const_name = const_name(f);
m_name = const_name(f);
else if (is_local(f))
m_name = mlocal_name(f);
}
int head_index::cmp::operator()(head_index const & i1, head_index const & i2) const {
if (i1.m_kind != i2.m_kind || i1.m_kind != expr_kind::Constant)
if (i1.m_kind != i2.m_kind || (i1.m_kind != expr_kind::Constant && i1.m_kind != expr_kind::Local))
return static_cast<int>(i1.m_kind) - static_cast<int>(i2.m_kind);
else
return quick_cmp(i1.m_const_name, i2.m_const_name);
return quick_cmp(i1.m_name, i2.m_name);
}
}

4
src/library/head_map.h
View file

@ -12,9 +12,9 @@ Author: Leonardo de Moura
namespace lean {
struct head_index {
expr_kind m_kind;
name m_const_name;
name m_name;
explicit head_index(expr_kind k = expr_kind::Var):m_kind(k) {}
explicit head_index(name const & c):m_kind(expr_kind::Constant), m_const_name(c) {}
explicit head_index(name const & c):m_kind(expr_kind::Constant), m_name(c) {}
head_index(expr const & e);
struct cmp {