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

refactor(kernel): use ro_metavar_env instead of metavar_env in places where we only need to read the metavariable environment

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-27 16:44:43 -08:00
parent 7b88d68afb
commit 3b152d1a9e
10 changed files with 119 additions and 108 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
src/kernel/free_vars.cpp
View file

@ -111,7 +111,7 @@ bool has_free_vars(expr const & e) {
*/
class free_var_range_fn {
expr_map<unsigned> m_cached;
optional<metavar_env> const & m_menv;
optional<ro_metavar_env> const & m_menv;
static unsigned dec(unsigned s) { return (s == 0) ? 0 : s - 1; }
@ -215,19 +215,19 @@ class free_var_range_fn {
return result;
}
public:
free_var_range_fn(optional<metavar_env> const & menv):m_menv(menv) {}
free_var_range_fn(optional<ro_metavar_env> const & menv):m_menv(menv) {}
unsigned operator()(expr const & e) { return apply(e); }
};
unsigned free_var_range(expr const & e, metavar_env const & menv) {
unsigned free_var_range(expr const & e, ro_metavar_env const & menv) {
if (closed(e))
return 0;
else
return free_var_range_fn(some_menv(menv))(e);
return free_var_range_fn(some_ro_menv(menv))(e);
}
unsigned free_var_range(expr const & e) {
return free_var_range_fn(none_menv())(e);
return free_var_range_fn(none_ro_menv())(e);
}
/**
@ -338,7 +338,7 @@ protected:
return result;
}
public:
has_free_var_in_range_fn(unsigned low, unsigned high, optional<metavar_env> const & menv):
has_free_var_in_range_fn(unsigned low, unsigned high, optional<ro_metavar_env> const & menv):
m_low(low),
m_high(high) {
lean_assert(low < high);
@ -348,16 +348,16 @@ public:
bool operator()(expr const & e) { return apply(e, 0); }
};
bool has_free_var(expr const & e, unsigned low, unsigned high, optional<metavar_env> const & menv) {
bool has_free_var(expr const & e, unsigned low, unsigned high, optional<ro_metavar_env> const & menv) {
return high > low && !closed(e) && has_free_var_in_range_fn(low, high, menv)(e);
}
bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv) { return has_free_var(e, low, high, some_menv(menv)); }
bool has_free_var(expr const & e, unsigned low, unsigned high) { return has_free_var(e, low, high, none_menv()); }
bool has_free_var(expr const & e, unsigned i, optional<metavar_env> const & menv) { return has_free_var(e, i, i+1, menv); }
bool has_free_var(expr const & e, unsigned i, metavar_env const & menv) { return has_free_var(e, i, i+1, menv); }
bool has_free_var(expr const & e, unsigned low, unsigned high, ro_metavar_env const & menv) { return has_free_var(e, low, high, some_ro_menv(menv)); }
bool has_free_var(expr const & e, unsigned low, unsigned high) { return has_free_var(e, low, high, none_ro_menv()); }
bool has_free_var(expr const & e, unsigned i, optional<ro_metavar_env> const & menv) { return has_free_var(e, i, i+1, menv); }
bool has_free_var(expr const & e, unsigned i, ro_metavar_env const & menv) { return has_free_var(e, i, i+1, menv); }
bool has_free_var(expr const & e, unsigned i) { return has_free_var(e, i, i+1); }
bool has_free_var(context_entry const & e, unsigned low, unsigned high, metavar_env const & menv) {
bool has_free_var(context_entry const & e, unsigned low, unsigned high, ro_metavar_env const & menv) {
if (high <= low)
return false;
auto d = e.get_domain();
@ -365,10 +365,10 @@ bool has_free_var(context_entry const & e, unsigned low, unsigned high, metavar_
return (d && has_free_var(*d, low, high, menv)) || (b && has_free_var(*b, low, high, menv));
}
bool has_free_var_ge(expr const & e, unsigned low, metavar_env const & menv) { return has_free_var(e, low, std::numeric_limits<unsigned>::max(), menv); }
bool has_free_var_ge(expr const & e, unsigned low, ro_metavar_env const & menv) { return has_free_var(e, low, std::numeric_limits<unsigned>::max(), menv); }
bool has_free_var_ge(expr const & e, unsigned low) { return has_free_var(e, low, std::numeric_limits<unsigned>::max()); }
expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & DEBUG_CODE(menv)) {
expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<ro_metavar_env> const & DEBUG_CODE(menv)) {
if (d == 0 || closed(e))
return e;
lean_assert(s >= d);
@ -382,13 +382,13 @@ expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_en
}
});
}
expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lower_free_vars(e, s, d, some_menv(menv)); }
expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return lower_free_vars(e, s, d, none_menv()); }
expr lower_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv) { return lower_free_vars(e, d, d, menv); }
expr lower_free_vars(expr const & e, unsigned d, metavar_env const & menv) { return lower_free_vars(e, d, d, menv); }
expr lower_free_vars(expr const & e, unsigned s, unsigned d, ro_metavar_env const & menv) { return lower_free_vars(e, s, d, some_ro_menv(menv)); }
expr lower_free_vars(expr const & e, unsigned s, unsigned d) { return lower_free_vars(e, s, d, none_ro_menv()); }
expr lower_free_vars(expr const & e, unsigned d, optional<ro_metavar_env> const & menv) { return lower_free_vars(e, d, d, menv); }
expr lower_free_vars(expr const & e, unsigned d, ro_metavar_env const & menv) { return lower_free_vars(e, d, d, menv); }
expr lower_free_vars(expr const & e, unsigned d) { return lower_free_vars(e, d, d); }
context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, metavar_env const & menv) {
context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, ro_metavar_env const & menv) {
auto domain = e.get_domain();
auto body = e.get_body();
if (domain && body)
@ -399,7 +399,7 @@ context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, m
return context_entry(e.get_name(), none_expr(), lower_free_vars(*body, s, d, menv));
}
expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv) {
expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<ro_metavar_env> const & menv) {
if (d == 0 || closed(e))
return e;
return replace(e, [=](expr const & e, unsigned offset) -> expr {
@ -412,13 +412,13 @@ expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env
}
});
}
expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv) { return lift_free_vars(e, s, d, some_menv(menv)); }
expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return lift_free_vars(e, s, d, none_menv()); }
expr lift_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv) { return lift_free_vars(e, 0, d, menv); }
expr lift_free_vars(expr const & e, unsigned s, unsigned d, ro_metavar_env const & menv) { return lift_free_vars(e, s, d, some_ro_menv(menv)); }
expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return lift_free_vars(e, s, d, none_ro_menv()); }
expr lift_free_vars(expr const & e, unsigned d, optional<ro_metavar_env> const & menv) { return lift_free_vars(e, 0, d, menv); }
expr lift_free_vars(expr const & e, unsigned d) { return lift_free_vars(e, 0, d); }
expr lift_free_vars(expr const & e, unsigned d, metavar_env const & menv) { return lift_free_vars(e, 0, d, menv); }
expr lift_free_vars(expr const & e, unsigned d, ro_metavar_env const & menv) { return lift_free_vars(e, 0, d, menv); }
context_entry lift_free_vars(context_entry const & e, unsigned s, unsigned d, metavar_env const & menv) {
context_entry lift_free_vars(context_entry const & e, unsigned s, unsigned d, ro_metavar_env const & menv) {
auto domain = e.get_domain();
auto body = e.get_body();
if (domain && body)

34
src/kernel/free_vars.h
View file

@ -35,7 +35,7 @@ class metavar_env;
[inst:s v] R ===> if s >= R then R else max(R-1, range_of(v))
[lift:s:n] R ===> if s >= R then R else R + n
*/
unsigned free_var_range(expr const & e, metavar_env const & menv);
unsigned free_var_range(expr const & e, ro_metavar_env const & menv);
unsigned free_var_range(expr const & e);
/**
@ -45,17 +45,17 @@ unsigned free_var_range(expr const & e);
\remark If menv is not none, then we use \c free_var_range to compute the free variables that may
occur in a metavariable.
*/
bool has_free_var(expr const & e, unsigned low, unsigned high, optional<metavar_env> const & menv);
bool has_free_var(expr const & e, unsigned low, unsigned high, metavar_env const & menv);
bool has_free_var(expr const & e, unsigned low, unsigned high, optional<ro_metavar_env> const & menv);
bool has_free_var(expr const & e, unsigned low, unsigned high, ro_metavar_env const & menv);
bool has_free_var(expr const & e, unsigned low, unsigned high);
/**
\brief Return true iff \c e contains the free variable <tt>(var i)</tt>.
*/
bool has_free_var(expr const & e, unsigned i, optional<metavar_env> const & menv);
bool has_free_var(expr const & e, unsigned i, metavar_env const & menv);
bool has_free_var(expr const & e, unsigned i, optional<ro_metavar_env> const & menv);
bool has_free_var(expr const & e, unsigned i, ro_metavar_env const & menv);
bool has_free_var(expr const & e, unsigned i);
bool has_free_var(context_entry const & e, unsigned low, unsigned high, metavar_env const & menv);
bool has_free_var(context_entry const & e, unsigned low, unsigned high, ro_metavar_env const & menv);
/**
\brief Return true iff \c e contains a free variable >= low.
@ -63,7 +63,7 @@ bool has_free_var(context_entry const & e, unsigned low, unsigned high, metavar_
\remark If menv is provided, then we use \c free_var_range to compute the free variables that may
occur in a metavariable.
*/
bool has_free_var_ge(expr const & e, unsigned low, metavar_env const & menv);
bool has_free_var_ge(expr const & e, unsigned low, ro_metavar_env const & menv);
bool has_free_var_ge(expr const & e, unsigned low);
/**
@ -75,14 +75,14 @@ bool has_free_var_ge(expr const & e, unsigned low);
\remark The parameter menv is only used for debugging purposes
*/
expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv);
expr lower_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv);
expr lower_free_vars(expr const & e, unsigned s, unsigned d, optional<ro_metavar_env> const & menv);
expr lower_free_vars(expr const & e, unsigned s, unsigned d, ro_metavar_env const & menv);
expr lower_free_vars(expr const & e, unsigned s, unsigned d);
expr lower_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv);
expr lower_free_vars(expr const & e, unsigned d, metavar_env const & menv);
expr lower_free_vars(expr const & e, unsigned d, optional<ro_metavar_env> const & menv);
expr lower_free_vars(expr const & e, unsigned d, ro_metavar_env const & menv);
expr lower_free_vars(expr const & e, unsigned d);
context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, metavar_env const & menv);
context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, ro_metavar_env const & menv);
/**
\brief Lift free variables >= s in \c e by d.
@ -90,12 +90,12 @@ context_entry lower_free_vars(context_entry const & e, unsigned s, unsigned d, m
\remark When the parameter menv is not none, this function will minimize the use
of the local entry lift in metavariables occurring in \c e.
*/
expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<metavar_env> const & menv);
expr lift_free_vars(expr const & e, unsigned s, unsigned d, optional<ro_metavar_env> const & menv);
expr lift_free_vars(expr const & e, unsigned s, unsigned d);
expr lift_free_vars(expr const & e, unsigned s, unsigned d, metavar_env const & menv);
expr lift_free_vars(expr const & e, unsigned d, optional<metavar_env> const & menv);
expr lift_free_vars(expr const & e, unsigned d, metavar_env const & menv);
expr lift_free_vars(expr const & e, unsigned s, unsigned d, ro_metavar_env const & menv);
expr lift_free_vars(expr const & e, unsigned d, optional<ro_metavar_env> const & menv);
expr lift_free_vars(expr const & e, unsigned d, ro_metavar_env const & menv);
expr lift_free_vars(expr const & e, unsigned d);
context_entry lift_free_vars(context_entry const & e, unsigned s, unsigned d, metavar_env const & menv);
context_entry lift_free_vars(context_entry const & e, unsigned s, unsigned d, ro_metavar_env const & menv);
}

50
src/kernel/instantiate.cpp
View file

@ -13,7 +13,7 @@ Author: Leonardo de Moura
namespace lean {
template<bool ClosedSubst>
expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) {
expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst, optional<ro_metavar_env> const & menv) {
return replace(a, [=](expr const & m, unsigned offset) -> expr {
if (is_var(m)) {
unsigned vidx = var_idx(m);
@ -42,36 +42,36 @@ expr instantiate_core(expr const & a, unsigned s, unsigned n, expr const * subst
});
}
expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<metavar_env> const & menv) {
expr instantiate_with_closed(expr const & a, unsigned n, expr const * s, optional<ro_metavar_env> const & menv) {
lean_assert(std::all_of(s, s+n, [&](expr const & e) { return !has_free_var(e, 0, std::numeric_limits<unsigned>::max(), menv); }));
return instantiate_core<true>(a, 0, n, s, menv);
}
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_menv(menv)); }
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_menv()); }
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv) { return instantiate_with_closed(e, n, s, some_ro_menv(menv)); }
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s) { return instantiate_with_closed(e, n, s, none_ro_menv()); }
expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l) { return instantiate_with_closed(e, l.size(), l.begin()); }
expr instantiate_with_closed(expr const & e, expr const & s, optional<metavar_env> const & menv) { return instantiate_with_closed(e, 1, &s, menv); }
expr instantiate_with_closed(expr const & e, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate_with_closed(e, 1, &s, menv); }
expr instantiate_with_closed(expr const & e, expr const & s) { return instantiate_with_closed(e, 1, &s); }
expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv) { return instantiate_with_closed(e, s, some_menv(menv)); }
expr instantiate_with_closed(expr const & e, expr const & s, ro_metavar_env const & menv) { return instantiate_with_closed(e, s, some_ro_menv(menv)); }
expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<metavar_env> const & menv) {
expr instantiate(expr const & a, unsigned s, unsigned n, expr const * subst, optional<ro_metavar_env> const & menv) {
return instantiate_core<false>(a, s, n, subst, menv);
}
expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); }
expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv) { return instantiate(e, n, s, some_menv(menv)); }
expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, n, s, none_menv()); }
expr instantiate(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv) { return instantiate(e, 0, n, s, menv); }
expr instantiate(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv) { return instantiate(e, n, s, some_ro_menv(menv)); }
expr instantiate(expr const & e, unsigned n, expr const * s) { return instantiate(e, n, s, none_ro_menv()); }
expr instantiate(expr const & e, std::initializer_list<expr> const & l) { return instantiate(e, l.size(), l.begin()); }
expr instantiate(expr const & e, unsigned i, expr const & s, optional<metavar_env> const & menv) { return instantiate(e, i, 1, &s, menv); }
expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const & menv) { return instantiate(e, i, 1, &s, some_menv(menv)); }
expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s, none_menv()); }
expr instantiate(expr const & e, expr const & s, optional<metavar_env> const & menv) { return instantiate(e, 1, &s, menv); }
expr instantiate(expr const & e, expr const & s, metavar_env const & menv) { return instantiate(e, s, some_menv(menv)); }
expr instantiate(expr const & e, expr const & s) { return instantiate(e, s, none_menv()); }
expr instantiate(expr const & e, unsigned i, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate(e, i, 1, &s, menv); }
expr instantiate(expr const & e, unsigned i, expr const & s, ro_metavar_env const & menv) { return instantiate(e, i, 1, &s, some_ro_menv(menv)); }
expr instantiate(expr const & e, unsigned i, expr const & s) { return instantiate(e, i, 1, &s, none_ro_menv()); }
expr instantiate(expr const & e, expr const & s, optional<ro_metavar_env> const & menv) { return instantiate(e, 1, &s, menv); }
expr instantiate(expr const & e, expr const & s, ro_metavar_env const & menv) { return instantiate(e, s, some_ro_menv(menv)); }
expr instantiate(expr const & e, expr const & s) { return instantiate(e, s, none_ro_menv()); }
bool is_head_beta(expr const & t) {
return is_app(t) && is_lambda(arg(t, 0));
}
expr apply_beta(expr f, unsigned num_args, expr const * args, optional<metavar_env> const & menv) {
expr apply_beta(expr f, unsigned num_args, expr const * args, optional<ro_metavar_env> const & menv) {
if (!is_lambda(f)) {
buffer<expr> new_args;
new_args.push_back(f);
@ -96,20 +96,20 @@ expr apply_beta(expr f, unsigned num_args, expr const * args, optional<metavar_e
}
}
}
expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const & menv) { return apply_beta(f, num_args, args, some_menv(menv)); }
expr apply_beta(expr f, unsigned num_args, expr const * args) { return apply_beta(f, num_args, args, none_menv()); }
expr apply_beta(expr f, unsigned num_args, expr const * args, ro_metavar_env const & menv) { return apply_beta(f, num_args, args, some_ro_menv(menv)); }
expr apply_beta(expr f, unsigned num_args, expr const * args) { return apply_beta(f, num_args, args, none_ro_menv()); }
expr head_beta_reduce(expr const & t, optional<metavar_env> const & menv) {
expr head_beta_reduce(expr const & t, optional<ro_metavar_env> const & menv) {
if (!is_head_beta(t)) {
return t;
} else {
return apply_beta(arg(t, 0), num_args(t) - 1, &arg(t, 1), menv);
}
}
expr head_beta_reduce(expr const & t) { return head_beta_reduce(t, none_menv()); }
expr head_beta_reduce(expr const & t, metavar_env const & menv) { return head_beta_reduce(t, some_menv(menv)); }
expr head_beta_reduce(expr const & t) { return head_beta_reduce(t, none_ro_menv()); }
expr head_beta_reduce(expr const & t, ro_metavar_env const & menv) { return head_beta_reduce(t, some_ro_menv(menv)); }
expr beta_reduce(expr t, optional<metavar_env> const & menv) {
expr beta_reduce(expr t, optional<ro_metavar_env> const & menv) {
auto f = [=](expr const & m, unsigned) -> expr {
if (is_head_beta(m))
return head_beta_reduce(m, menv);
@ -124,6 +124,6 @@ expr beta_reduce(expr t, optional<metavar_env> const & menv) {
t = new_t;
}
}
expr beta_reduce(expr t, metavar_env const & menv) { return beta_reduce(t, some_menv(menv)); }
expr beta_reduce(expr t) { return beta_reduce(t, none_menv()); }
expr beta_reduce(expr t, ro_metavar_env const & menv) { return beta_reduce(t, some_ro_menv(menv)); }
expr beta_reduce(expr t) { return beta_reduce(t, none_ro_menv()); }
}

34
src/kernel/instantiate.h
View file

@ -8,7 +8,7 @@ Author: Leonardo de Moura
#include "kernel/expr.h"
namespace lean {
class metavar_env;
class ro_metavar_env;
/**
\brief Replace the free variables with indices 0, ..., n-1 with s[n-1], ..., s[0] in e.
@ -17,12 +17,12 @@ class metavar_env;
\remark When the parameter menv is not none, this function will minimize the use
of the local entry inst in metavariables occurring in \c e.
*/
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv);
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, metavar_env const & menv);
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv);
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv);
expr instantiate_with_closed(expr const & e, unsigned n, expr const * s);
expr instantiate_with_closed(expr const & e, std::initializer_list<expr> const & l);
expr instantiate_with_closed(expr const & e, expr const & s, optional<metavar_env> const & menv);
expr instantiate_with_closed(expr const & e, expr const & s, metavar_env const & menv);
expr instantiate_with_closed(expr const & e, expr const & s, optional<ro_metavar_env> const & menv);
expr instantiate_with_closed(expr const & e, expr const & s, ro_metavar_env const & menv);
expr instantiate_with_closed(expr const & e, expr const & s);
/**
@ -31,34 +31,34 @@ expr instantiate_with_closed(expr const & e, expr const & s);
\remark When the parameter menv is not none, this function will minimize the use
of the local entry inst in metavariables occurring in \c e.
*/
expr instantiate(expr const & e, unsigned n, expr const * s, optional<metavar_env> const & menv);
expr instantiate(expr const & e, unsigned n, expr const * s, metavar_env const & menv);
expr instantiate(expr const & e, unsigned n, expr const * s, optional<ro_metavar_env> const & menv);
expr instantiate(expr const & e, unsigned n, expr const * s, ro_metavar_env const & menv);
expr instantiate(expr const & e, unsigned n, expr const * s);
expr instantiate(expr const & e, std::initializer_list<expr> const & l);
/**
\brief Replace free variable \c i with \c s in \c e.
*/
expr instantiate(expr const & e, unsigned i, expr const & s, optional<metavar_env> const & menv);
expr instantiate(expr const & e, unsigned i, expr const & s, metavar_env const & menv);
expr instantiate(expr const & e, unsigned i, expr const & s, optional<ro_metavar_env> const & menv);
expr instantiate(expr const & e, unsigned i, expr const & s, ro_metavar_env const & menv);
expr instantiate(expr const & e, unsigned i, expr const & s);
/**
\brief Replace free variable \c 0 with \c s in \c e.
*/
expr instantiate(expr const & e, expr const & s, optional<metavar_env> const & menv);
expr instantiate(expr const & e, expr const & s, metavar_env const & menv);
expr instantiate(expr const & e, expr const & s, optional<ro_metavar_env> const & menv);
expr instantiate(expr const & e, expr const & s, ro_metavar_env const & menv);
expr instantiate(expr const & e, expr const & s);
expr apply_beta(expr f, unsigned num_args, expr const * args, optional<metavar_env> const & menv);
expr apply_beta(expr f, unsigned num_args, expr const * args, metavar_env const & menv);
expr apply_beta(expr f, unsigned num_args, expr const * args, optional<ro_metavar_env> const & menv);
expr apply_beta(expr f, unsigned num_args, expr const * args, ro_metavar_env const & menv);
expr apply_beta(expr f, unsigned num_args, expr const * args);
bool is_head_beta(expr const & t);
expr head_beta_reduce(expr const & t, optional<metavar_env> const & menv);
expr head_beta_reduce(expr const & t, metavar_env const & menv);
expr head_beta_reduce(expr const & t, optional<ro_metavar_env> const & menv);
expr head_beta_reduce(expr const & t, ro_metavar_env const & menv);
expr head_beta_reduce(expr const & t);
expr beta_reduce(expr t, optional<metavar_env> const & menv);
expr beta_reduce(expr t, metavar_env const & menv);
expr beta_reduce(expr t, optional<ro_metavar_env> const & menv);
expr beta_reduce(expr t, ro_metavar_env const & menv);
expr beta_reduce(expr t);
}

6
src/kernel/metavar.cpp
View file

@ -224,7 +224,7 @@ bool metavar_env_cell::assign(expr const & m, expr const & t) {
return assign(m, t, j);
}
expr apply_local_context(expr const & a, local_context const & lctx, optional<metavar_env> const & menv) {
expr apply_local_context(expr const & a, local_context const & lctx, optional<ro_metavar_env> const & menv) {
if (lctx) {
if (is_metavar(a)) {
return mk_metavar(metavar_name(a), append(lctx, metavar_lctx(a)));
@ -463,7 +463,7 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n) {
return cons(mk_lift(s, n), lctx);
}
expr add_lift(expr const & m, unsigned s, unsigned n, optional<metavar_env> const & menv) {
expr add_lift(expr const & m, unsigned s, unsigned n, optional<ro_metavar_env> const & menv) {
if (menv && s >= free_var_range(m, *menv))
return m;
return update_metavar(m, add_lift(metavar_lctx(m), s, n));
@ -487,7 +487,7 @@ local_context add_inst(local_context const & lctx, unsigned s, expr const & v) {
return cons(mk_inst(s, v), lctx);
}
expr add_inst(expr const & m, unsigned s, expr const & v, optional<metavar_env> const & menv) {
expr add_inst(expr const & m, unsigned s, expr const & v, optional<ro_metavar_env> const & menv) {
if (menv && s >= free_var_range(m, *menv))
return m;
return update_metavar(m, add_inst(metavar_lctx(m), s, v));

33
src/kernel/metavar.h
View file

@ -246,8 +246,10 @@ inline context instantiate_metavars(optional<metavar_env> const & menv, context
\brief Read-only reference to metavariable environment (cell).
*/
class ro_metavar_env {
friend class optional<ro_metavar_env>;
friend class metavar_env;
metavar_env_cell * m_ptr;
explicit ro_metavar_env(metavar_env_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
public:
ro_metavar_env():m_ptr(new metavar_env_cell()) { m_ptr->inc_ref(); }
ro_metavar_env(metavar_env const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
@ -259,8 +261,16 @@ public:
metavar_env_cell const * operator->() const { return m_ptr; }
metavar_env_cell const & operator*() const { return *m_ptr; }
metavar_env copy() const { return metavar_env(new metavar_env_cell(*m_ptr)); }
friend bool is_eqp(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return menv1.m_ptr == menv2.m_ptr; }
friend bool operator==(ro_metavar_env const & menv1, ro_metavar_env const & menv2) { return is_eqp(menv1, menv2); }
};
SPECIALIZE_OPTIONAL_FOR_SMART_PTR(ro_metavar_env)
inline optional<ro_metavar_env> none_ro_menv() { return optional<ro_metavar_env>(); }
inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env const & e) { return optional<ro_metavar_env>(e); }
inline optional<ro_metavar_env> some_ro_menv(ro_metavar_env && e) { return optional<ro_metavar_env>(std::forward<ro_metavar_env>(e)); }
inline optional<ro_metavar_env> const & to_ro_menv(optional<metavar_env> const & menv) { return reinterpret_cast<optional<ro_metavar_env> const &>(menv); }
/**
\brief A cached weak reference to a metavariable environment + timestamp at the time of
the caching. This object may also cache optional references.
@ -280,6 +290,7 @@ public:
bool update(metavar_env const & menv) { return update(some(menv)); }
explicit operator bool() const { return static_cast<bool>(m_menv); }
optional<metavar_env> const & to_some_menv() const { return m_menv; }
optional<ro_metavar_env> const & to_some_ro_menv() const { return to_ro_menv(m_menv); }
metavar_env operator*() const { return *m_menv; }
metavar_env_cell * operator->() const { lean_assert(m_menv); return (*m_menv).operator->(); }
};
@ -287,9 +298,9 @@ public:
/**
\brief Apply the changes in \c lctx to \c a.
*/
expr apply_local_context(expr const & a, local_context const & lctx, optional<metavar_env> const & menv);
inline expr apply_local_context(expr const & a, local_context const & lctx, metavar_env const & menv) { return apply_local_context(a, lctx, some_menv(menv)); }
inline expr apply_local_context(expr const & a, local_context const & lctx) { return apply_local_context(a, lctx, none_menv()); }
expr apply_local_context(expr const & a, local_context const & lctx, optional<ro_metavar_env> const & menv);
inline expr apply_local_context(expr const & a, local_context const & lctx, ro_metavar_env const & menv) { return apply_local_context(a, lctx, some_ro_menv(menv)); }
inline expr apply_local_context(expr const & a, local_context const & lctx) { return apply_local_context(a, lctx, none_ro_menv()); }
/**
\brief Extend the local context \c lctx with the entry <tt>lift:s:n</tt>
@ -305,9 +316,9 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n);
occur in \c m. If s > the maximum free variable that occurs in \c m, then
we do not add a lift local entry to the local context.
*/
expr add_lift(expr const & m, unsigned s, unsigned n, optional<metavar_env> const & menv);
inline expr add_lift(expr const & m, unsigned s, unsigned n) { return add_lift(m, s, n, none_menv()); }
inline expr add_lift(expr const & m, unsigned s, unsigned n, metavar_env const & menv) { return add_lift(m, s, n, some_menv(menv)); }
expr add_lift(expr const & m, unsigned s, unsigned n, optional<ro_metavar_env> const & menv);
inline expr add_lift(expr const & m, unsigned s, unsigned n) { return add_lift(m, s, n, none_ro_menv()); }
inline expr add_lift(expr const & m, unsigned s, unsigned n, ro_metavar_env const & menv) { return add_lift(m, s, n, some_ro_menv(menv)); }
/**
\brief Extend the local context \c lctx with the entry <tt>inst:s v</tt>
@ -323,9 +334,9 @@ local_context add_inst(local_context const & lctx, unsigned s, expr const & v);
occur in \c m. If s > the maximum free variable that occurs in \c m, then
we do not add an inst local entry to the local context.
*/
expr add_inst(expr const & m, unsigned s, expr const & v, optional<metavar_env> const & menv);
inline expr add_inst(expr const & m, unsigned s, expr const & v) { return add_inst(m, s, v, none_menv()); }
inline expr add_inst(expr const & m, unsigned s, expr const & v, metavar_env const & menv) { return add_inst(m, s, v, some_menv(menv)); }
expr add_inst(expr const & m, unsigned s, expr const & v, optional<ro_metavar_env> const & menv);
inline expr add_inst(expr const & m, unsigned s, expr const & v) { return add_inst(m, s, v, none_ro_menv()); }
inline expr add_inst(expr const & m, unsigned s, expr const & v, ro_metavar_env const & menv) { return add_inst(m, s, v, some_ro_menv(menv)); }
/**
\brief Return true iff the given metavariable has a non-empty
@ -346,7 +357,7 @@ expr pop_meta_context(expr const & m);
/**
\brief Return true iff \c e has a metavariable that is assigned in \c menv.
*/
bool has_assigned_metavar(expr const & e, metavar_env const & menv);
bool has_assigned_metavar(expr const & e, ro_metavar_env const & menv);
/**
\brief Return true iff \c e contains the metavariable \c m.
@ -354,5 +365,5 @@ bool has_assigned_metavar(expr const & e, metavar_env const & menv);
\brief is_metavar(m)
*/
bool has_metavar(expr const & e, expr const & m, metavar_env const & menv);
bool has_metavar(expr const & e, expr const & m, ro_metavar_env const & menv);
}

4
src/kernel/normalizer.cpp
View file

@ -87,11 +87,11 @@ class normalizer::imp {
ro_environment env() const { return ro_environment(m_env); }
expr instantiate(expr const & e, unsigned n, expr const * s) {
return ::lean::instantiate(e, n, s, m_menv.to_some_menv());
return ::lean::instantiate(e, n, s, m_menv.to_some_ro_menv());
}
expr add_lift(expr const & m, unsigned s, unsigned n) {
return ::lean::add_lift(m, s, n, m_menv.to_some_menv());
return ::lean::add_lift(m, s, n, m_menv.to_some_ro_menv());
}
expr lookup(value_stack const & s, unsigned i) {

10
src/kernel/type_checker.cpp
View file

@ -43,11 +43,11 @@ class type_checker::imp {
bool m_infer_only;
ro_environment env() const { return ro_environment(m_env); }
expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); }
expr lift_free_vars(expr const & e, unsigned d) { return ::lean::lift_free_vars(e, d, m_menv.to_some_menv()); }
expr lower_free_vars(expr const & e, unsigned s, unsigned n) { return ::lean::lower_free_vars(e, s, n, m_menv.to_some_menv()); }
expr instantiate_with_closed(expr const & e, expr const & v) { return ::lean::instantiate_with_closed(e, v, m_menv.to_some_menv()); }
expr instantiate(expr const & e, expr const & v) { return ::lean::instantiate(e, v, m_menv.to_some_menv()); }
expr lift_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lift_free_vars(e, s, d, m_menv.to_some_ro_menv()); }
expr lift_free_vars(expr const & e, unsigned d) { return ::lean::lift_free_vars(e, d, m_menv.to_some_ro_menv()); }
expr lower_free_vars(expr const & e, unsigned s, unsigned n) { return ::lean::lower_free_vars(e, s, n, m_menv.to_some_ro_menv()); }
expr instantiate_with_closed(expr const & e, expr const & v) { return ::lean::instantiate_with_closed(e, v, m_menv.to_some_ro_menv()); }
expr instantiate(expr const & e, expr const & v) { return ::lean::instantiate(e, v, m_menv.to_some_ro_menv()); }
expr normalize(expr const & e, context const & ctx, bool unfold_opaque) { return m_normalizer(e, ctx, m_menv.to_some_menv(), unfold_opaque); }
expr check_type(expr const & e, expr const & s, context const & ctx) {

2
src/library/substitution.cpp
View file

@ -23,7 +23,7 @@ expr find(substitution & s, expr e) {
}
}
expr apply(substitution & s, expr const & e, optional<metavar_env> const & menv) {
expr apply(substitution & s, expr const & e, optional<ro_metavar_env> const & menv) {
return replace(e, [&](expr const & e, unsigned) -> expr {
if (is_metavar(e)) {
expr r = find(s, e);

4
src/library/substitution.h
View file

@ -20,8 +20,8 @@ typedef splay_map<name, expr, name_quick_cmp> substitution;
/**
\brief Apply substitution \c s to \c e
*/
expr apply(substitution & s, expr const & e, optional<metavar_env> const & menv = none_menv());
inline expr apply(substitution & s, expr const & e, metavar_env const & menv) { return apply(s, e, some_menv(menv)); }
expr apply(substitution & s, expr const & e, optional<ro_metavar_env> const & menv = none_ro_menv());
inline expr apply(substitution & s, expr const & e, ro_metavar_env const & menv) { return apply(s, e, some_ro_menv(menv)); }
expr find(substitution & s, expr e);
UDATA_DEFS_CORE(substitution)