max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(frontends/lean/elaborator): allow elaborator to add auxiliary definitions

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-10 08:31:00 -07:00
parent e5cf12e2ad
commit 8498bbaeff
6 changed files with 20 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/elaborator.cpp
View file

@ -1738,13 +1738,14 @@ elaborate(environment const & env, options const & opts,
return p;
}
expr nested_elaborate(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
expr nested_elaborate(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
expr const & e, bool relaxed) {
elaborator elab(env, opts, mctx, lctx);
expr r = elab(translate(env, lctx, e));
if (!relaxed)
elab.ensure_no_unassigned_metavars();
mctx = elab.mctx();
env = elab.env();
return r;
}

3
src/frontends/lean/elaborator.h
View file

@ -201,13 +201,14 @@ public:
expr operator()(expr const & e);
pair<expr, level_param_names> finalize(expr const & e, bool check_unassigned, bool to_simple_metavar);
void ensure_no_unassigned_metavars();
environment const & env() const { return m_env; }
};
pair<expr, level_param_names> elaborate(environment const & env, options const & opts,
metavar_context & mctx, local_context const & lctx,
expr const & e, bool check_unassigend);
expr nested_elaborate(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
expr nested_elaborate(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
expr const & e, bool relaxed);
void initialize_elaborator();

7
src/library/tactic/elaborate.cpp
View file

@ -37,7 +37,8 @@ vm_obj tactic_to_expr_core(vm_obj const & relaxed, vm_obj const & qe, vm_obj con
}
metavar_context mctx = s.mctx();
try {
expr r = (*g_elaborate)(s.env(), s.get_options(), mctx, g->get_context(), to_expr(qe), to_bool(relaxed));
environment env = s.env();
expr r = (*g_elaborate)(env, s.get_options(), mctx, g->get_context(), to_expr(qe), to_bool(relaxed));
r = mctx.instantiate_mvars(r);
if (relaxed && has_expr_metavar(r)) {
buffer<expr> new_goals;
@ -52,9 +53,9 @@ vm_obj tactic_to_expr_core(vm_obj const & relaxed, vm_obj const & qe, vm_obj con
return true;
});
list<expr> new_gs = cons(head(s.goals()), to_list(new_goals.begin(), new_goals.end(), tail(s.goals())));
return mk_tactic_success(to_obj(r), set_mctx_goals(s, mctx, new_gs));
return mk_tactic_success(to_obj(r), set_env_mctx_goals(s, env, mctx, new_gs));
} else {
return mk_tactic_success(to_obj(r), set_mctx(s, mctx));
return mk_tactic_success(to_obj(r), set_env_mctx(s, env, mctx));
}
} catch (exception & ex) {
return mk_tactic_exception(ex, s);

2
src/library/tactic/elaborate.h
View file

@ -16,7 +16,7 @@ expr const & get_by_arg(expr const & e);
/* Elaboration function.
\remark The boolean flag indicates whether metavariables should be tolerated in the result or not.
\remark The metavariable context is input/output. */
typedef std::function<expr(environment const &, options const &, metavar_context &, local_context const &, expr const &, bool)> elaborate_fn;
typedef std::function<expr(environment &, options const &, metavar_context &, local_context const &, expr const &, bool)> elaborate_fn;
/** \brief Auxiliary function for setting the thread local elaboration
procedure used by the tactic framework. */

9
src/library/tactic/tactic_state.cpp
View file

@ -67,6 +67,10 @@ tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx) {
return tactic_state(s.env(), s.get_options(), mctx, s.goals(), s.main());
}
tactic_state set_env_mctx(tactic_state const & s, environment const & env, metavar_context const & mctx) {
return tactic_state(env, s.get_options(), mctx, s.goals(), s.main());
}
static list<expr> consume_solved_prefix(metavar_context const & mctx, list<expr> const & gs) {
if (empty(gs))
return gs;
@ -84,6 +88,11 @@ tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx
return tactic_state(s.env(), s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main());
}
tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env,
metavar_context const & mctx, list<expr> const & gs) {
return tactic_state(env, s.get_options(), mctx, consume_solved_prefix(mctx, gs), s.main());
}
format tactic_state::pp_expr(formatter_factory const & fmtf, expr const & e) const {
type_context ctx = mk_type_context_for(*this, transparency_mode::All);
formatter fmt = fmtf(env(), get_options(), ctx);

2
src/library/tactic/tactic_state.h
View file

@ -81,8 +81,10 @@ tactic_state mk_tactic_state_for(environment const & env, options const & opts,
tactic_state set_options(tactic_state const & s, options const & o);
tactic_state set_env(tactic_state const & s, environment const & env);
tactic_state set_mctx(tactic_state const & s, metavar_context const & mctx);
tactic_state set_env_mctx(tactic_state const & s, environment const & env, metavar_context const & mctx);
tactic_state set_goals(tactic_state const & s, list<expr> const & gs);
tactic_state set_mctx_goals(tactic_state const & s, metavar_context const & mctx, list<expr> const & gs);
tactic_state set_env_mctx_goals(tactic_state const & s, environment const & env, metavar_context const & mctx, list<expr> const & gs);
tactic_state const & to_tactic_state(vm_obj const & o);
vm_obj to_obj(tactic_state const & s);