feat(library/head_map): a simple indexing datastructure
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
2fa2589220
commit
33cb2db5b5
5 changed files with 150 additions and 1 deletions
|
@ -6,7 +6,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
|
|||
update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
|
||||
standard_kernel.cpp hott_kernel.cpp
|
||||
unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
|
||||
explicit.cpp num.cpp string.cpp opaque_hints.cpp)
|
||||
explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp)
|
||||
# hop_match.cpp)
|
||||
|
||||
target_link_libraries(library ${LEAN_LIBS})
|
||||
|
|
23
src/library/head_map.cpp
Normal file
23
src/library/head_map.cpp
Normal file
|
@ -0,0 +1,23 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "library/head_map.h"
|
||||
|
||||
namespace lean {
|
||||
head_index::head_index(expr const & e) {
|
||||
expr const & f = get_app_fn(e);
|
||||
m_kind = f.kind();
|
||||
if (is_constant(f))
|
||||
m_const_name = const_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)
|
||||
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);
|
||||
}
|
||||
}
|
64
src/library/head_map.h
Normal file
64
src/library/head_map.h
Normal file
|
@ -0,0 +1,64 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#pragma once
|
||||
#include "util/rb_map.h"
|
||||
#include "util/list.h"
|
||||
#include "kernel/expr.h"
|
||||
|
||||
namespace lean {
|
||||
struct head_index {
|
||||
expr_kind m_kind;
|
||||
name m_const_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) {}
|
||||
head_index(expr const & e);
|
||||
|
||||
struct cmp {
|
||||
int operator()(head_index const & i1, head_index const & i2) const;
|
||||
};
|
||||
};
|
||||
|
||||
/**
|
||||
\brief Very simple indexing data-structure that allow us to map the head symbol of an expression to
|
||||
a list of values.
|
||||
|
||||
The index is the expression kind and a name (if it is a constant).
|
||||
|
||||
This index is very naive, but it is effective for many applications.
|
||||
*/
|
||||
template<typename V>
|
||||
class head_map {
|
||||
rb_map<head_index, list<V>, head_index::cmp> m_map;
|
||||
public:
|
||||
bool empty() const { return m_map.empty(); }
|
||||
bool contains(head_index const & h) const { return m_map.contains(h); }
|
||||
list<V> const * find(head_index const & h) const { return m_map.find(h); }
|
||||
void erase(head_index const & h) { m_map.erase(h); }
|
||||
void erase_entry(head_index const & h, V const & v) {
|
||||
if (auto it = m_map.find(h)) {
|
||||
auto new_vs = filter(*it, [&](V const & v2) { return v != v2; });
|
||||
if (!new_vs)
|
||||
m_map.erase(h);
|
||||
else
|
||||
m_map.insert(h, new_vs);
|
||||
}
|
||||
}
|
||||
void insert(head_index const & h, V const & v) {
|
||||
if (auto it = m_map.find(h))
|
||||
m_map.insert(h, cons(v, filter(*it, [&](V const & v2) { return v != v2; })));
|
||||
else
|
||||
m_map.insert(h, list<V>(v));
|
||||
}
|
||||
template<typename F> void for_each(F && f) const { m_map.for_each(f); }
|
||||
template<typename F> void for_each_entry(F && f) const {
|
||||
m_map.for_each([&](head_index const & h, list<V> const & vs) {
|
||||
for (V const & v : vs)
|
||||
f(h, v);
|
||||
});
|
||||
}
|
||||
};
|
||||
}
|
|
@ -10,3 +10,6 @@ add_test(occurs ${CMAKE_CURRENT_BINARY_DIR}/occurs)
|
|||
add_executable(unifier unifier.cpp)
|
||||
target_link_libraries(unifier ${EXTRA_LIBS})
|
||||
add_test(unifier ${CMAKE_CURRENT_BINARY_DIR}/unifier)
|
||||
add_executable(head_map head_map.cpp)
|
||||
target_link_libraries(head_map ${EXTRA_LIBS})
|
||||
add_test(head_map ${CMAKE_CURRENT_BINARY_DIR}/head_map)
|
||||
|
|
59
src/tests/library/head_map.cpp
Normal file
59
src/tests/library/head_map.cpp
Normal file
|
@ -0,0 +1,59 @@
|
|||
/*
|
||||
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
||||
Author: Leonardo de Moura
|
||||
*/
|
||||
#include "util/test.h"
|
||||
#include "kernel/abstract.h"
|
||||
#include "library/head_map.h"
|
||||
using namespace lean;
|
||||
|
||||
static void tst1() {
|
||||
head_map<expr> map;
|
||||
expr a = Const("a");
|
||||
expr f = Const("f");
|
||||
expr b = Const("b");
|
||||
expr x = Local("x", Bool);
|
||||
expr l1 = Fun(x, x);
|
||||
expr l2 = Fun(x, f(x));
|
||||
lean_assert(l1 != l2);
|
||||
lean_assert(map.empty());
|
||||
map.insert(a, a);
|
||||
lean_assert(map.contains(a));
|
||||
map.insert(a, b);
|
||||
lean_assert(map.contains(a));
|
||||
map.erase_entry(a, b);
|
||||
lean_assert(map.contains(a));
|
||||
map.erase_entry(a, a);
|
||||
lean_assert(!map.contains(a));
|
||||
lean_assert(map.empty());
|
||||
map.insert(l1, a);
|
||||
map.insert(l2, b);
|
||||
lean_assert(map.contains(l1));
|
||||
lean_assert(length(*map.find(l1)) == 2);
|
||||
auto size_fn = [](head_map<expr> const & m) {
|
||||
unsigned r = 0;
|
||||
m.for_each_entry([&](head_index const &, expr const &) { r++; });
|
||||
return r;
|
||||
};
|
||||
lean_assert(size_fn(map) == 2);
|
||||
map.insert(a, a);
|
||||
lean_assert(size_fn(map) == 3);
|
||||
map.erase(l1);
|
||||
lean_assert(size_fn(map) == 1);
|
||||
map.insert(a, b);
|
||||
lean_assert(size_fn(map) == 2);
|
||||
map.erase(a);
|
||||
lean_assert(size_fn(map) == 0);
|
||||
lean_assert(map.empty());
|
||||
map.insert(f(a), f(a));
|
||||
map.insert(f(b), f(b));
|
||||
lean_assert(length(*map.find(f(a))) == 2);
|
||||
}
|
||||
|
||||
int main() {
|
||||
save_stack_info();
|
||||
tst1();
|
||||
return has_violations() ? 1 : 0;
|
||||
}
|
Loading…
Reference in a new issue