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

feat(library/simplifier): make sure the simplifier can handle meta-variables

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-28 20:30:47 -08:00
parent ee4344076e
commit 24452289dd
7 changed files with 68 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/kernel/free_vars.cpp
View file

@ -365,7 +365,12 @@ bool has_free_var(context_entry const & e, unsigned low, unsigned high, ro_metav
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, 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, 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, optional<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<ro_metavar_env> const & DEBUG_CODE(menv)) {

1
src/kernel/free_vars.h
View file

@ -64,6 +64,7 @@ bool has_free_var(context_entry const & e, unsigned low, unsigned high, ro_metav
occur in a metavariable.
*/
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, optional<ro_metavar_env> const & menv);
bool has_free_var_ge(expr const & e, unsigned low);
/**

30
src/library/hop_match.cpp
View file

@ -21,6 +21,7 @@ class hop_match_fn {
buffer<optional<expr>> & m_subst;
buffer<expr> m_vars;
optional<ro_environment> m_env;
optional<ro_metavar_env> m_menv;
name_map<name> * m_name_subst;
bool is_free_var(expr const & x, unsigned ctx_size) const {
@ -31,6 +32,13 @@ class hop_match_fn {
return is_var(x) && var_idx(x) < ctx_size;
}
expr lift_free_vars(expr const & e, unsigned d) const { return ::lean::lift_free_vars(e, d, m_menv); }
expr lower_free_vars(expr const & e, unsigned s, unsigned d) const { return ::lean::lower_free_vars(e, s, d, m_menv); }
bool has_free_var(expr const & e, unsigned i) const { return ::lean::has_free_var(e, i, m_menv); }
bool has_free_var(expr const & e, unsigned low, unsigned high) const { return ::lean::has_free_var(e, low, high, m_menv); }
expr apply_beta(expr f, unsigned num_args, expr const * args) const { return ::lean::apply_beta(f, num_args, args, m_menv); }
bool has_free_var_ge(expr const & e, unsigned low) const { return ::lean::has_free_var_ge(e, low, m_menv); }
optional<expr> get_subst(expr const & x, unsigned ctx_size) const {
lean_assert(is_free_var(x, ctx_size));
unsigned vidx = var_idx(x) - ctx_size;
@ -180,7 +188,7 @@ class hop_match_fn {
for_each(p, [&](expr const & v, unsigned offset) {
if (!result)
return false;
if (is_var(v) && is_free_var(v, ctx_size + offset) && !get_subst(v, ctx_size + offset)) {
if (is_var(v) && this->is_free_var(v, ctx_size + offset) && !get_subst(v, ctx_size + offset)) {
result = false;
}
return true;
@ -201,7 +209,7 @@ class hop_match_fn {
if (m_ref.is_free_var(x, real_ctx_sz)) {
optional<expr> r = m_ref.get_subst(x, real_ctx_sz);
lean_assert(r);
return lift_free_vars(*r, real_ctx_sz);
return m_ref.lift_free_vars(*r, real_ctx_sz);
} else {
return x;
}
@ -215,7 +223,7 @@ class hop_match_fn {
for (unsigned i = 0; i < num_args(e); i++)
new_args.push_back(visit(arg(e, i), ctx));
if (is_lambda(new_args[0]))
return apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
return m_ref.apply_beta(new_args[0], new_args.size() - 1, new_args.data() + 1);
else
return mk_app(new_args);
} else {
@ -310,7 +318,8 @@ class hop_match_fn {
}
public:
hop_match_fn(buffer<optional<expr>> & subst, optional<ro_environment> const & env,
name_map<name> * name_subst):m_subst(subst), m_env(env), m_name_subst(name_subst) {}
optional<ro_metavar_env> const & menv, name_map<name> * name_subst):
m_subst(subst), m_env(env), m_menv(menv), m_name_subst(name_subst) {}
bool operator()(expr const & p, expr const & t) {
return match(p, t, context(), 0);
@ -318,8 +327,8 @@ public:
};
bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst, optional<ro_environment> const & env,
name_map<name> * name_subst) {
return hop_match_fn(subst, env, name_subst)(p, t);
optional<ro_metavar_env> const & menv, name_map<name> * name_subst) {
return hop_match_fn(subst, env, menv, name_subst)(p, t);
}
static int hop_match_core(lua_State * L, optional<ro_environment> const & env) {
@ -327,8 +336,11 @@ static int hop_match_core(lua_State * L, optional<ro_environment> const & env) {
expr p = to_expr(L, 1);
expr t = to_expr(L, 2);
int k = 0;
if (nargs >= 4) {
k = luaL_checkinteger(L, 4);
optional<ro_metavar_env> menv;
if (nargs >= 4 && !lua_isnil(L, 4))
menv = to_metavar_env(L, 4);
if (nargs >= 5) {
k = luaL_checkinteger(L, 5);
if (k < 0)
throw exception("hop_match, arg #4 must be non-negative");
} else {
@ -336,7 +348,7 @@ static int hop_match_core(lua_State * L, optional<ro_environment> const & env) {
}
buffer<optional<expr>> subst;
subst.resize(k);
if (hop_match(p, t, subst, env)) {
if (hop_match(p, t, subst, env, menv)) {
lua_newtable(L);
int i = 1;
for (auto s : subst) {

4
src/library/hop_match.h
View file

@ -29,12 +29,16 @@ namespace lean {
If an environment is provided, then a constant \c c matches a term \c t if
\c c is definitionally equal to \c t.
If a metavariable environment is provided, then it is provided to lift/lower
free variables procedures to be able to minimize the size of the local context.
If name_subst is different from nullptr, then the procedure stores in name_subst
a mapping for binder names. It maps the binder names used in the pattern \c p into
the binder names used in \c t.
*/
bool hop_match(expr const & p, expr const & t, buffer<optional<expr>> & subst,
optional<ro_environment> const & env = optional<ro_environment>(),
optional<ro_metavar_env> const & menv = optional<ro_metavar_env>(),
name_map<name> * name_subst = nullptr);
void open_hop_match(lua_State * L);
}

54
src/library/simplifier/simplifier.cpp
View file

@ -156,6 +156,7 @@ class simplifier_cell::imp {
unsigned m_num_steps; // number of steps performed
unsigned m_depth; // recursion depth
name_map<name> m_name_subst;
cached_ro_metavar_env m_menv;
std::shared_ptr<simplifier_monitor> m_monitor;
// Configuration
@ -214,30 +215,22 @@ class simplifier_cell::imp {
return mk_lambda(abst_name(abst), abst_domain(abst), new_body);
}
bool is_proposition(expr const & e) {
return m_tc.is_proposition(e, m_ctx);
}
bool is_convertible(expr const & t1, expr const & t2) {
return m_tc.is_convertible(t1, t2, m_ctx);
}
bool is_proposition(expr const & e) { return m_tc.is_proposition(e, m_ctx, m_menv.to_some_menv()); }
bool is_convertible(expr const & t1, expr const & t2) { return m_tc.is_convertible(t1, t2, m_ctx, m_menv.to_some_menv()); }
bool is_definitionally_equal(expr const & t1, expr const & t2) {
return m_tc.is_definitionally_equal(t1, t2, m_ctx);
return m_tc.is_definitionally_equal(t1, t2, m_ctx, m_menv.to_some_menv());
}
expr infer_type(expr const & e) {
return m_tc.infer_type(e, m_ctx);
}
expr ensure_pi(expr const & e) {
return m_tc.ensure_pi(e, m_ctx);
}
expr infer_type(expr const & e) { return m_tc.infer_type(e, m_ctx, m_menv.to_some_menv()); }
expr ensure_pi(expr const & e) { return m_tc.ensure_pi(e, m_ctx, m_menv.to_some_menv()); }
expr normalize(expr const & e) {
normalizer & proc = m_tc.get_normalizer();
return proc(e, m_ctx, true);
return proc(e, m_ctx, m_menv.to_some_menv(), true);
}
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 lower_free_vars(expr const & e, unsigned s, unsigned d) { return ::lean::lower_free_vars(e, s, d, m_menv.to_some_menv()); }
expr instantiate(expr const & e, expr const & s) { return ::lean::instantiate(e, s, m_menv.to_some_menv()); }
expr instantiate(expr const & e, unsigned n, expr const * s) { return ::lean::instantiate(e, n, s, m_menv.to_some_menv()); }
expr head_beta_reduce(expr const & t) { return ::lean::head_beta_reduce(t, m_menv.to_some_menv()); }
expr mk_fresh_const(expr const & type) {
m_next_idx++;
@ -892,7 +885,8 @@ class simplifier_cell::imp {
subst.clear();
subst.resize(num);
m_name_subst.clear();
if (hop_match(rule.get_lhs(), target, subst, optional<ro_environment>(m_env), &m_name_subst)) {
if (hop_match(rule.get_lhs(), target, subst, optional<ro_environment>(m_env),
m_menv.to_some_menv(), &m_name_subst)) {
new_args.clear();
new_args.resize(num+1);
if (found_all_args(num, subst, new_args)) {
@ -1508,8 +1502,10 @@ public:
m_next_idx = 0;
}
expr_pair operator()(expr const & e, context const & ctx) {
expr_pair operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
set_ctx(ctx);
if (m_menv.update(menv))
m_cache.clear();
m_num_steps = 0;
m_depth = 0;
try {
@ -1526,7 +1522,9 @@ simplifier_cell::simplifier_cell(ro_environment const & env, options const & o,
m_ptr(new imp(env, o, num_rs, rs, monitor)) {
}
expr_pair simplifier_cell::operator()(expr const & e, context const & ctx) { return m_ptr->operator()(e, ctx); }
expr_pair simplifier_cell::operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
return m_ptr->operator()(e, ctx, menv);
}
void simplifier_cell::clear() { return m_ptr->m_cache.clear(); }
unsigned simplifier_cell::get_depth() const { return m_ptr->m_depth; }
context const & simplifier_cell::get_context() const { return m_ptr->m_ctx; }
@ -1551,17 +1549,19 @@ ro_simplifier::ro_simplifier(weak_ref const & r) {
expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_rs, rewrite_rule_set const * rs,
optional<ro_metavar_env> const & menv,
std::shared_ptr<simplifier_monitor> const & monitor) {
return simplifier(env, opts, num_rs, rs, monitor)(e, ctx);
return simplifier(env, opts, num_rs, rs, monitor)(e, ctx, menv);
}
expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_ns, name const * ns,
optional<ro_metavar_env> const & menv,
std::shared_ptr<simplifier_monitor> const & monitor) {
buffer<rewrite_rule_set> rules;
for (unsigned i = 0; i < num_ns; i++)
rules.push_back(get_rewrite_rule_set(env, ns[i]));
return simplify(e, env, ctx, opts, num_ns, rules.data(), monitor);
return simplify(e, env, ctx, opts, num_ns, rules.data(), menv, monitor);
}
simplifier_stack_space_exception::simplifier_stack_space_exception():stack_space_exception("simplifier") {}
@ -1738,9 +1738,11 @@ static int simplifier_apply(lua_State * L) {
int nargs = lua_gettop(L);
expr_pair r;
if (nargs == 2)
r = to_simplifier(L, 1)(to_expr(L, 2), context());
r = to_simplifier(L, 1)(to_expr(L, 2), context(), none_ro_menv());
else if (nargs == 3)
r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3), none_ro_menv());
else
r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3));
r = to_simplifier(L, 1)(to_expr(L, 2), to_context(L, 3), some_ro_menv(to_metavar_env(L, 4)));
push_expr(L, r.first);
push_expr(L, r.second);
return 2;

9
src/library/simplifier/simplifier.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <memory>
#include "util/lua.h"
#include "kernel/environment.h"
#include "kernel/metavar.h"
#include "library/expr_pair.h"
#include "library/simplifier/rewrite_rule_set.h"
@ -23,7 +24,7 @@ public:
simplifier_cell(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs,
std::shared_ptr<simplifier_monitor> const & monitor);
expr_pair operator()(expr const & e, context const & ctx);
expr_pair operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv);
void clear();
unsigned get_depth() const;
@ -41,7 +42,9 @@ public:
std::shared_ptr<simplifier_monitor> const & monitor);
simplifier_cell * operator->() const { return m_ptr.get(); }
simplifier_cell & operator*() const { return *(m_ptr.get()); }
expr_pair operator()(expr const & e, context const & ctx) { return (*m_ptr)(e, ctx); }
expr_pair operator()(expr const & e, context const & ctx, optional<ro_metavar_env> const & menv) {
return (*m_ptr)(e, ctx, menv);
}
};
/** \brief Read only reference to simplifier object */
@ -115,9 +118,11 @@ public:
expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & pts,
unsigned num_rs, rewrite_rule_set const * rs,
optional<ro_metavar_env> const & menv = none_ro_menv(),
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
expr_pair simplify(expr const & e, ro_environment const & env, context const & ctx, options const & opts,
unsigned num_ns, name const * ns,
optional<ro_metavar_env> const & menv = none_ro_menv(),
std::shared_ptr<simplifier_monitor> const & monitor = std::shared_ptr<simplifier_monitor>());
void open_simplifier(lua_State * L);
}

2
src/library/tactic/simplify_tactic.cpp
View file

@ -52,7 +52,7 @@ static optional<proof_state> simplify_tactic(ro_environment const & env, io_stat
}
expr conclusion = g.get_conclusion();
auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data());
auto r = simplify(conclusion, env, context(), opts, rule_sets.size(), rule_sets.data(), some_ro_menv(menv));
expr new_conclusion = r.first;
expr eq_proof = r.second;
if (new_conclusion == g.get_conclusion())