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

refactor(frontends/lean): move some auxiliary procedures to library/tactic

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-19 15:17:42 -08:00
parent 07d7ea2f4e
commit a22dc773b7
4 changed files with 52 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/frontends/lean/util.cpp
View file

@ -357,27 +357,6 @@ expr univ_metavars_to_params(environment const & env, local_decls<level> const &
return univ_metavars_to_params_fn(env, lls, s, ps, new_ps)(e);
}
expr instantiate_meta(expr const & meta, substitution & subst) {
lean_assert(is_meta(meta));
buffer<expr> locals;
expr mvar = get_app_args(meta, locals);
mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
for (auto & local : locals)
local = subst.instantiate_all(local);
return mk_app(mvar, locals);
}
justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) {
return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
substitution tmp(subst);
expr new_m = instantiate_meta(m, tmp);
expr new_type = type_checker(env).infer(new_m).first;
bool relax_main_opaque = true; // this value doesn't really matter for pretty printing
proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"), relax_main_opaque);
return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
});
}
justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr const & t, expr const & src) {
return mk_justification(src, [=](formatter const & fmt, substitution const & subst) {
substitution s(subst);
@ -393,21 +372,6 @@ justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr con
});
}
pair<expr, justification> update_meta(expr const & meta, substitution s) {
buffer<expr> args;
expr mvar = get_app_args(meta, args);
justification j;
auto p = s.instantiate_metavars(mlocal_type(mvar));
mvar = update_mlocal(mvar, p.first);
j = p.second;
for (expr & arg : args) {
auto p = s.instantiate_metavars(mlocal_type(arg));
arg = update_mlocal(arg, p.first);
j = mk_composite1(j, p.second);
}
return mk_pair(mk_app(mvar, args), j);
}
std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
expr e = p.parse_expr();
list<expr> ctx = p.locals_to_context();

14
src/frontends/lean/util.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include "kernel/expr_sets.h"
#include "kernel/type_checker.h"
#include "library/util.h"
#include "library/tactic/util.h"
#include "frontends/lean/local_decls.h"
namespace lean {
@ -80,13 +81,6 @@ bool occurs(level const & u, level const & l);
expr univ_metavars_to_params(environment const & env, local_decls<level> const & lls, substitution & s,
name_set & ps, buffer<name> & new_ps, expr const & e);
/** \brief Instantiate metavariable application \c meta (?M ...) using \c subst */
expr instantiate_meta(expr const & meta, substitution & subst);
/** \brief Return a 'failed to synthesize placholder' justification for the given
metavariable application \c m of the form (?m l_1 ... l_k) */
justification mk_failed_to_synthesize_jst(environment const & env, expr const & m);
/** \brief Return a justification for \c v_type being definitionally equal to \c t,
<tt> v : v_type</tt>, the expressiong \c src is used to extract position information.
*/
@ -95,12 +89,6 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e
return mk_type_mismatch_jst(v, v_type, t, v);
}
/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of
?m and local constants l_i
Return the updated expression and a justification for all substitutions.
*/
pair<expr, justification> update_meta(expr const & meta, substitution s);
/** \brief Auxiliary function for check/eval/find_decl */
std::tuple<expr, level_param_names> parse_local_expr(parser & p);

38
src/library/tactic/util.cpp
View file

@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/type_checker.h"
#include "library/aliases.h"
#include "library/tactic/util.h"
#include "library/tactic/proof_state.h"
namespace lean {
bool is_tactic_namespace_open(environment const & env) {
@ -27,4 +29,40 @@ bool is_tactic_namespace_open(environment const & env) {
}
return false;
}
pair<expr, justification> update_meta(expr const & meta, substitution s) {
buffer<expr> args;
expr mvar = get_app_args(meta, args);
justification j;
auto p = s.instantiate_metavars(mlocal_type(mvar));
mvar = update_mlocal(mvar, p.first);
j = p.second;
for (expr & arg : args) {
auto p = s.instantiate_metavars(mlocal_type(arg));
arg = update_mlocal(arg, p.first);
j = mk_composite1(j, p.second);
}
return mk_pair(mk_app(mvar, args), j);
}
expr instantiate_meta(expr const & meta, substitution & subst) {
lean_assert(is_meta(meta));
buffer<expr> locals;
expr mvar = get_app_args(meta, locals);
mvar = update_mlocal(mvar, subst.instantiate_all(mlocal_type(mvar)));
for (auto & local : locals)
local = subst.instantiate_all(local);
return mk_app(mvar, locals);
}
justification mk_failed_to_synthesize_jst(environment const & env, expr const & m) {
return mk_justification(m, [=](formatter const & fmt, substitution const & subst) {
substitution tmp(subst);
expr new_m = instantiate_meta(m, tmp);
expr new_type = type_checker(env).infer(new_m).first;
bool relax_main_opaque = true; // this value doesn't really matter for pretty printing
proof_state ps = to_proof_state(new_m, new_type, name_generator("dontcare"), relax_main_opaque);
return format("failed to synthesize placeholder") + line() + ps.pp(fmt);
});
}
}

13
src/library/tactic/util.h
View file

@ -9,4 +9,17 @@ Author: Leonardo de Moura
namespace lean {
/** \brief Return true iff the tactic namespace is open in given environment. */
bool is_tactic_namespace_open(environment const & env);
/** \brief Instantiate metavariable application \c meta (?M ...) using \c subst */
expr instantiate_meta(expr const & meta, substitution & subst);
/** \brief Given a metavariable application (?m l_1 ... l_n), apply \c s to the types of
?m and local constants l_i
Return the updated expression and a justification for all substitutions.
*/
pair<expr, justification> update_meta(expr const & meta, substitution s);
/** \brief Return a 'failed to synthesize placholder' justification for the given
metavariable application \c m of the form (?m l_1 ... l_k) */
justification mk_failed_to_synthesize_jst(environment const & env, expr const & m);
}