f97c260b0b
The environment object is a "smart-pointer".
Before this commit, the use of "const &" for environment objects was broken.
For example, suppose we have a function f that should not modify the input environment.
Before this commit, its signature would be
void f(environment const & env)
This is broken, f's implementation can easilty convert it to a read-write pointer by using
the copy constructor.
environment rw_env(env);
Now, f can use rw_env to update env.
To fix this issue, we now have ro_environment. It is a shared *const* pointer.
We can convert an environment into a ro_environment, but not the other way around.
ro_environment can also be seen as a form of documentation.
For example, now it is clear that type_inferer is not updating the environment, since its constructor takes a ro_environment.
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
154 lines
6.6 KiB
C++
154 lines
6.6 KiB
C++
/*
|
|
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
Author: Leonardo de Moura
|
|
*/
|
|
#include <utility>
|
|
#include <algorithm>
|
|
#include "kernel/environment.h"
|
|
#include "kernel/instantiate.h"
|
|
#include "library/fo_unify.h"
|
|
#include "library/kernel_bindings.h"
|
|
#include "library/type_inferer.h"
|
|
#include "library/tactic/goal.h"
|
|
#include "library/tactic/proof_builder.h"
|
|
#include "library/tactic/proof_state.h"
|
|
#include "library/tactic/tactic.h"
|
|
#include "library/tactic/apply_tactic.h"
|
|
|
|
namespace lean {
|
|
static name g_tmp_mvar_name = name::mk_internal_unique_name();
|
|
|
|
static optional<proof_state> apply_tactic(ro_environment const & env, proof_state const & s,
|
|
expr const & th, expr const & th_type, bool all) {
|
|
precision prec = s.get_precision();
|
|
if (prec != precision::Precise && prec != precision::Over) {
|
|
// it is pointless to apply this tactic, since it will produce UnderOver
|
|
return none_proof_state();
|
|
}
|
|
unsigned num = 0;
|
|
expr th_type_c = th_type;
|
|
while (is_pi(th_type_c)) {
|
|
num++;
|
|
th_type_c = abst_body(th_type_c);
|
|
}
|
|
buffer<expr> mvars;
|
|
for (unsigned i = 0; i < num; i++)
|
|
mvars.push_back(mk_metavar(name(g_tmp_mvar_name, i)));
|
|
th_type_c = instantiate_with_closed_relaxed(th_type_c, mvars.size(), mvars.data());
|
|
bool found = false;
|
|
buffer<std::pair<name, goal>> new_goals_buf;
|
|
// The proof is based on an application of th.
|
|
// There are two kinds of arguments:
|
|
// 1) regular arguments computed using unification.
|
|
// 2) propostions that generate new subgoals.
|
|
// We use a pair to simulate this "union" type.
|
|
typedef list<std::pair<optional<expr>, name>> arg_list;
|
|
// We may solve more than one goal.
|
|
// We store the solved goals using a list of pairs
|
|
// name, args. Where the 'name' is the name of the solved goal.
|
|
type_inferer inferer(env);
|
|
metavar_env new_menv = s.get_menv();
|
|
list<std::pair<name, arg_list>> proof_info;
|
|
for (auto const & p : s.get_goals()) {
|
|
check_interrupted();
|
|
if (all || !found) {
|
|
name const & gname = p.first;
|
|
goal const & g = p.second;
|
|
expr const & c = g.get_conclusion();
|
|
optional<substitution> subst = fo_unify(th_type_c, c);
|
|
if (subst) {
|
|
found = true;
|
|
th_type_c = th_type;
|
|
arg_list l;
|
|
unsigned new_goal_idx = 1;
|
|
for (auto const & mvar : mvars) {
|
|
expr mvar_sol = apply(*subst, mvar);
|
|
if (mvar_sol != mvar) {
|
|
l = cons(mk_pair(some_expr(mvar_sol), name()), l);
|
|
th_type_c = instantiate(abst_body(th_type_c), mvar_sol);
|
|
} else {
|
|
if (inferer.is_proposition(abst_domain(th_type_c), context(), &new_menv)) {
|
|
name new_gname(gname, new_goal_idx);
|
|
new_goal_idx++;
|
|
l = cons(mk_pair(none_expr(), new_gname), l);
|
|
new_goals_buf.emplace_back(new_gname, update(g, abst_domain(th_type_c)));
|
|
th_type_c = instantiate(abst_body(th_type_c), mk_constant(new_gname, abst_domain(th_type_c)));
|
|
} else {
|
|
// we have to create a new metavar in menv
|
|
// since we do not have a substitution for mvar, and
|
|
// it is not a proposition
|
|
expr new_m = new_menv.mk_metavar(context(), some_expr(abst_domain(th_type_c)));
|
|
l = cons(mk_pair(some_expr(new_m), name()), l);
|
|
// we use instantiate_with_closed_relaxed because we do not want
|
|
// to introduce a lift operator in the new_m
|
|
th_type_c = instantiate_with_closed_relaxed(abst_body(th_type_c), 1, &new_m);
|
|
}
|
|
}
|
|
}
|
|
proof_info.emplace_front(gname, l);
|
|
} else {
|
|
new_goals_buf.push_back(p);
|
|
}
|
|
} else {
|
|
new_goals_buf.push_back(p);
|
|
}
|
|
}
|
|
if (found) {
|
|
proof_builder pb = s.get_proof_builder();
|
|
proof_builder new_pb = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
|
|
proof_map new_m(m);
|
|
for (auto const & p1 : proof_info) {
|
|
name const & gname = p1.first;
|
|
arg_list const & l = p1.second;
|
|
buffer<expr> args;
|
|
args.push_back(th);
|
|
for (auto const & p2 : l) {
|
|
optional<expr> const & arg = p2.first;
|
|
if (arg) {
|
|
// TODO(Leo): decide if we instantiate the metavars in the end or not.
|
|
args.push_back(*arg);
|
|
} else {
|
|
name const & subgoal_name = p2.second;
|
|
args.push_back(find(m, subgoal_name));
|
|
new_m.erase(subgoal_name);
|
|
}
|
|
}
|
|
std::reverse(args.begin() + 1, args.end());
|
|
new_m.insert(gname, mk_app(args));
|
|
}
|
|
return pb(new_m, a);
|
|
});
|
|
goals new_gs = to_list(new_goals_buf.begin(), new_goals_buf.end());
|
|
return some(proof_state(precision::Over, new_gs, new_menv, new_pb, s.get_cex_builder()));
|
|
} else {
|
|
return none_proof_state();
|
|
}
|
|
}
|
|
|
|
tactic apply_tactic(expr const & th, expr const & th_type, bool all) {
|
|
return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
|
|
return apply_tactic(env, s, th, th_type, all);
|
|
});
|
|
}
|
|
|
|
tactic apply_tactic(name const & th_name, bool all) {
|
|
return mk_tactic01([=](ro_environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
|
|
optional<object> obj = env->find_object(th_name);
|
|
if (obj && (obj->is_theorem() || obj->is_axiom()))
|
|
return apply_tactic(env, s, mk_constant(th_name), obj->get_type(), all);
|
|
else
|
|
return none_proof_state();
|
|
});
|
|
}
|
|
|
|
int mk_apply_tactic(lua_State * L) {
|
|
int nargs = lua_gettop(L);
|
|
return push_tactic(L, apply_tactic(to_name_ext(L, 1), nargs >= 2 ? lua_toboolean(L, 2) : true));
|
|
}
|
|
|
|
void open_apply_tactic(lua_State * L) {
|
|
SET_GLOBAL_FUN(mk_apply_tactic, "apply_tac");
|
|
}
|
|
}
|