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

refactor(kernel/metavar): separate substitution from their justifications

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-03 14:01:22 -07:00
parent abbd054b51
commit b49902807c
2 changed files with 31 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
src/kernel/metavar.cpp
View file

@ -14,54 +14,47 @@ Author: Leonardo de Moura
#include "kernel/level.h"
namespace lean {
substitution::substitution(expr_map const & em, level_map const & lm):
m_expr_subst(em), m_level_subst(lm) {}
substitution::substitution() {}
bool substitution::is_expr_assigned(name const & m) const {
return m_expr_subst.contains(m);
}
optional<std::pair<expr, justification>> substitution::get_expr_assignment(name const & m) const {
auto substitution::get_expr_assignment(name const & m) const -> opt_expr_jst {
auto it = m_expr_subst.find(m);
if (it)
return optional<std::pair<expr, justification>>(*it);
return opt_expr_jst(mk_pair(*it, get_expr_jst(m)));
else
return optional<std::pair<expr, justification>>();
return opt_expr_jst();
}
bool substitution::is_level_assigned(name const & m) const {
return m_level_subst.contains(m);
}
optional<std::pair<level, justification>> substitution::get_level_assignment(name const & m) const {
auto substitution::get_level_assignment(name const & m) const -> opt_level_jst {
auto it = m_level_subst.find(m);
if (it)
return opt_level_jst(*it);
return opt_level_jst(mk_pair(*it, get_level_jst(m)));
else
return opt_level_jst();
}
optional<expr> substitution::get_expr(name const & m) const {
auto it = m_expr_subst.find(m);
if (it)
return some_expr(it->first);
else
return none_expr();
return it ? some_expr(*it) : none_expr();
}
optional<level> substitution::get_level(name const & m) const {
auto it = m_level_subst.find(m);
if (it)
return some_level(it->first);
else
return none_level();
return it ? some_level(*it) : none_level();
}
void substitution::d_assign(name const & m, expr const & t, justification const & j) {
lean_assert(closed(t));
m_expr_subst.insert(m, mk_pair(t, j));
m_expr_subst.insert(m, t);
if (!j.is_none())
m_expr_jsts.insert(m, j);
}
void substitution::d_assign(name const & m, expr const & t) {
@ -69,7 +62,9 @@ void substitution::d_assign(name const & m, expr const & t) {
}
void substitution::d_assign(name const & m, level const & l, justification const & j) {
m_level_subst.insert(m, mk_pair(l, j));
m_level_subst.insert(m, l);
if (!j.is_none())
m_level_jsts.insert(m, j);
}
void substitution::d_assign(name const & m, level const & l) {
@ -77,8 +72,9 @@ void substitution::d_assign(name const & m, level const & l) {
}
substitution substitution::assign(name const & m, expr const & t, justification const & j) const {
lean_assert(closed(t));
return substitution(insert(m_expr_subst, m, mk_pair(t, j)), m_level_subst);
substitution s(*this);
s.d_assign(m, t, j);
return s;
}
substitution substitution::assign(name const & m, expr const & t) const {
@ -86,7 +82,9 @@ substitution substitution::assign(name const & m, expr const & t) const {
}
substitution substitution::assign(name const & m, level const & l, justification const & j) const {
return substitution(m_expr_subst, insert(m_level_subst, m, mk_pair(l, j)));
substitution s(*this);
s.d_assign(m, l, j);
return s;
}
substitution substitution::assign(name const & m, level const & l) const {

17
src/kernel/metavar.h
View file

@ -14,12 +14,15 @@ Author: Leonardo de Moura
namespace lean {
class substitution {
typedef rb_map<name, std::pair<expr, justification>, name_quick_cmp> expr_map;
typedef rb_map<name, std::pair<level, justification>, name_quick_cmp> level_map;
typedef rb_map<name, expr, name_quick_cmp> expr_map;
typedef rb_map<name, level, name_quick_cmp> level_map;
typedef rb_map<name, justification, name_quick_cmp> jst_map;
expr_map m_expr_subst;
level_map m_level_subst;
jst_map m_expr_jsts;
jst_map m_level_jsts;
substitution(expr_map const & em, level_map const & lm);
void d_assign(name const & m, expr const & t, justification const & j);
void d_assign(name const & m, expr const & t);
void d_assign(name const & m, level const & t, justification const & j);
@ -28,6 +31,10 @@ class substitution {
expr d_instantiate_metavars_wo_jst(expr const & e);
std::pair<level, justification> d_instantiate_metavars(level const & l, bool use_jst, bool updt, name_set * unassigned);
friend class instantiate_metavars_fn;
justification get_expr_jst(name const & m) const { if (auto it = m_expr_jsts.find(m)) return *it; else return justification(); }
justification get_level_jst(name const & m) const { if (auto it = m_level_jsts.find(m)) return *it; else return justification(); }
public:
substitution();
typedef optional<std::pair<expr, justification>> opt_expr_jst;
@ -50,12 +57,12 @@ public:
template<typename F>
void for_each_expr(F && fn) const {
for_each(m_expr_subst, [=](name const & n, std::pair<expr, justification> const & a) { fn(n, a.first, a.second); });
for_each(m_expr_subst, [=](name const & n, expr const & e) { fn(n, e, get_expr_jst(n)); });
}
template<typename F>
void for_each_level(F && fn) const {
for_each(m_level_subst, [=](name const & n, std::pair<level, justification> const & a) { fn(n, a.first, a.second); });
for_each(m_level_subst, [=](name const & n, level const & l) { fn(n, l, get_level_jst(n)); });
}
bool is_assigned(expr const & m) const { lean_assert(is_metavar(m)); return is_expr_assigned(mlocal_name(m)); }