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

fix(library/class_instance_resolution): bugs in new type class resolution procedure

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-17 13:53:38 -07:00
parent bf17440f31
commit 6a36bffe4b
12 changed files with 199 additions and 686 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -39,7 +39,7 @@ Author: Leonardo de Moura
#include "library/choice_iterator.h"
#include "library/projection.h"
#include "library/pp_options.h"
#include "library/class_instance_synth.h"
#include "library/class_instance_resolution.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/error_handling/error_handling.h"
#include "library/definitional/equations.h"
@ -293,7 +293,7 @@ expr elaborator::mk_placeholder_meta(optional<name> const & suffix, optional<exp
if (is_inst_implicit && !m_ctx.m_ignore_instances) {
auto ec = mk_class_instance_elaborator(
env(), ios(), m_context, m_ngen.next(), suffix,
use_local_instances(), is_strict, type, g, m_unifier_config, m_ctx.m_pos_provider);
use_local_instances(), is_strict, type, g, m_ctx.m_pos_provider);
register_meta(ec.first);
cs += ec.second;
return ec.first;

18
src/library/CMakeLists.txt
View file

@ -1,8 +1,8 @@
add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
kernel_bindings.cpp io_state_stream.cpp bin_app.cpp constants.cpp
resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
normalize.cpp shared_environment.cpp module.cpp coercion.cpp
private.cpp placeholder.cpp aliases.cpp level_names.cpp
add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
occurs.cpp kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
constants.cpp resolve_macro.cpp kernel_serializer.cpp
max_sharing.cpp normalize.cpp shared_environment.cpp module.cpp
coercion.cpp private.cpp placeholder.cpp aliases.cpp level_names.cpp
update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
standard_kernel.cpp sorry.cpp replace_visitor.cpp unifier.cpp
unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp
@ -13,7 +13,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp
local_context.cpp choice_iterator.cpp pp_options.cpp
unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
relation_manager.cpp export.cpp user_recursors.cpp
class_instance_synth.cpp idx_metavar.cpp composition_manager.cpp
tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp
decl_stats.cpp meng_paulson.cpp)
relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp
composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp
norm_num.cpp class_instance_resolution.cpp)

214
src/library/class_instance_resolution.cpp
View file

@ -8,20 +8,19 @@ Author: Leonardo de Moura
#include "util/interrupt.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/instantiate.h"
#include "kernel/metavar.h"
#include "kernel/abstract.h"
#include "kernel/for_each_fn.h"
#include "library/normalize.h"
#include "library/reducible.h"
#include "library/class.h"
#include "library/local_context.h"
#include "library/generic_exception.h"
#include "library/io_state_stream.h"
#include "library/replace_visitor.h"
#include "library/constants.h"
#include "library/class_instance_resolution.h"
#ifndef LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES
#define LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES false
#endif
#ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES
#define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false
#endif
@ -40,7 +39,6 @@ namespace lean {
typedef std::shared_ptr<ci_type_inference> ci_type_inference_ptr;
static name * g_class_unique_class_instances = nullptr;
static name * g_class_trace_instances = nullptr;
static name * g_class_instance_max_depth = nullptr;
static name * g_class_trans_instances = nullptr;
@ -52,10 +50,6 @@ static ci_type_inference_factory * g_default_factory = nullptr;
LEAN_THREAD_PTR(ci_type_inference_factory, g_factory);
LEAN_THREAD_PTR(io_state, g_ios);
bool get_class_unique_class_instances(options const & o) {
return o.get_bool(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES);
}
bool get_class_trace_instances(options const & o) {
return o.get_bool(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES);
}
@ -85,6 +79,8 @@ public:
}
};
ci_type_inference_factory::~ci_type_inference_factory() {}
std::shared_ptr<ci_type_inference> ci_type_inference_factory::operator()(environment const & env) const {
return std::shared_ptr<ci_type_inference>(new default_ci_type_inference(env));
}
@ -108,8 +104,8 @@ struct cienv {
list<expr> m_ctx;
buffer<pair<name, expr>> m_local_instances;
unsigned m_next_uvar;
unsigned m_next_mvar;
unsigned m_next_uvar_idx;
unsigned m_next_mvar_idx;
struct state {
list<expr> m_stack; // stack of meta-variables that need to be synthesized;
@ -134,15 +130,14 @@ struct cienv {
bool m_displayed_trace_header;
// configuration
bool m_unique_instances;
unsigned m_max_depth;
bool m_trans_instances;
bool m_trace_instances;
cienv(bool multiple_instances = false):
m_ngen(*g_prefix2),
m_next_uvar(0),
m_next_mvar(0),
m_next_uvar_idx(0),
m_next_mvar_idx(0),
m_multiple_instances(multiple_instances) {}
bool is_not_reducible(name const & n) const {
@ -176,18 +171,15 @@ struct cienv {
}
void set_options(options const & o) {
bool unique_instances = get_class_unique_class_instances(o);
unsigned max_depth = get_class_instance_max_depth(o);
bool trans_instances = get_class_trans_instances(o);
bool trace_instances = get_class_trace_instances(o);
if (m_unique_instances != unique_instances ||
m_max_depth != max_depth ||
if (m_max_depth != max_depth ||
m_trans_instances != trans_instances ||
m_trace_instances != trace_instances) {
reset_cache();
}
m_unique_instances = unique_instances;
m_max_depth = max_depth;
m_trans_instances = trans_instances;
m_trace_instances = trace_instances;
@ -251,7 +243,7 @@ struct cienv {
if (!is_constant(f))
return optional<name>();
return constant_is_class(f);
}
}
}
/** \brief Partial/Quick test for is_class. Result
@ -355,8 +347,8 @@ struct cienv {
// Create an internal universal metavariable
level mk_uvar() {
unsigned idx = m_next_uvar;
m_next_uvar++;
unsigned idx = m_next_uvar_idx;
m_next_uvar_idx++;
return mk_meta_univ(name(*g_prefix2, idx));
}
@ -394,8 +386,8 @@ struct cienv {
// Create an internal metavariable.
expr mk_mvar(expr const & type) {
unsigned idx = m_next_mvar;
m_next_mvar++;
unsigned idx = m_next_mvar_idx;
m_next_mvar_idx++;
return mk_metavar(name(*g_prefix2, idx), type);
}
@ -422,6 +414,7 @@ struct cienv {
void update_assignment(expr const & m, expr const & v) {
m_state.m_eassignment.insert(mvar_idx(m), v);
lean_assert(is_assigned(m));
}
// Assign \c v to the metavariable \c m.
@ -625,7 +618,7 @@ struct cienv {
}
virtual expr visit(expr const & e) {
if (!has_expr_metavar(e) || !has_univ_metavar(e))
if (!has_expr_metavar(e) && !has_univ_metavar(e))
return e;
else
return replace_visitor::visit(e);
@ -933,11 +926,6 @@ struct cienv {
return empty(m_state.m_stack);
}
expr const & next_mvar() const {
lean_assert(!is_done());
return head(m_state.m_stack);
}
bool mk_choice_point(expr const & mvar) {
lean_assert(is_mvar(mvar));
if (m_choices.size() > m_max_depth) {
@ -966,45 +954,46 @@ struct cienv {
return true;
}
bool process_next_alt_core(list<expr> & insts) {
bool process_next_alt_core(expr const & mvar, list<expr> & insts) {
while (!empty(insts)) {
expr inst = head(insts);
insts = tail(insts);
expr inst_type = infer_type(inst);
if (try_instance(next_mvar(), inst, inst_type))
if (try_instance(mvar, inst, inst_type))
return true;
}
return false;
}
bool process_next_alt_core(list<name> & inst_names) {
bool process_next_alt_core(expr const & mvar, list<name> & inst_names) {
while (!empty(inst_names)) {
name inst_name = head(inst_names);
inst_names = tail(inst_names);
if (try_instance(next_mvar(), inst_name))
if (try_instance(mvar, inst_name))
return true;
}
return false;
}
bool process_next_alt() {
bool process_next_alt(expr const & mvar) {
lean_assert(!m_choices.empty());
choice & c = m_choices.back();
if (process_next_alt_core(c.m_local_instances))
if (process_next_alt_core(mvar, c.m_local_instances))
return true;
if (process_next_alt_core(c.m_trans_instances))
if (process_next_alt_core(mvar, c.m_trans_instances))
return true;
if (process_next_alt_core(c.m_instances))
if (process_next_alt_core(mvar, c.m_instances))
return true;
return false;
}
bool process_next_mvar() {
lean_assert(!is_done());
expr mvar = next_mvar();
expr mvar = head(m_state.m_stack);
if (!mk_choice_point(mvar))
return false;
return process_next_alt();
m_state.m_stack = tail(m_state.m_stack);
return process_next_alt(mvar);
}
bool backtrack() {
@ -1013,8 +1002,10 @@ struct cienv {
m_choices.pop_back();
if (m_choices.empty())
return false;
m_state = m_choices.back().m_state;
if (process_next_alt())
m_state = m_choices.back().m_state;
expr mvar = head(m_state.m_stack);
m_state.m_stack = tail(m_state.m_stack);
if (process_next_alt(mvar))
return true;
}
}
@ -1029,6 +1020,20 @@ struct cienv {
return some_expr(instantiate_uvars_mvars(m_main_mvar));
}
optional<expr> next_solution() {
if (m_choices.empty())
return none_expr();
m_state = m_choices.back().m_state;
expr mvar = head(m_state.m_stack);
m_state.m_stack = tail(m_state.m_stack);
if (process_next_alt(mvar))
return search();
else if (backtrack())
return search();
else
return none_expr();
}
void init_search(expr const & type) {
m_state = state();
m_main_mvar = mk_mvar(type);
@ -1036,37 +1041,42 @@ struct cienv {
m_displayed_trace_header = false;
}
optional<expr> ensure_no_meta(optional<expr> r) {
while (true) {
if (!r)
return none_expr();
if (!has_expr_metavar_relaxed(*r)) {
cache_result(mlocal_type(m_main_mvar), *r);
return r;
}
r = next_solution();
}
}
optional<expr> operator()(environment const & env, options const & o, pos_info_provider const * pip, list<expr> const & ctx, expr const & type) {
set_env(env);
set_options(o);
set_ctx(ctx);
set_pos_info(pip, type);
if (auto r = check_cache(type))
if (auto r = check_cache(type)) {
if (m_trace_instances) {
auto out = diagnostic(m_env, *g_ios);
out << "cached instance for " << type << "\n" << *r << "\n";
}
return r;
}
init_search(type);
if (auto r = search()) {
cache_result(type, *r);
return r;
} else {
return none_expr();
}
auto r = search();
return ensure_no_meta(r);
}
optional<expr> next() {
if (!m_multiple_instances)
return none_expr();
if (m_choices.empty())
return none_expr();
m_state = m_choices.back().m_state;
if (process_next_alt())
return search();
else if (backtrack())
return search();
else
return none_expr();
auto r = next_solution();
return ensure_no_meta(r);
}
};
@ -1087,27 +1097,100 @@ ci_type_inference_factory_scope::~ci_type_inference_factory_scope() {
g_factory = m_old;
}
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & e, pos_info_provider * pip) {
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & e, pos_info_provider const * pip) {
flet<io_state*> set_ios(g_ios, const_cast<io_state*>(&ios));
return get_cienv()(env, ios.get_options(), pip, ctx, e);
}
optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx, expr const & e, pos_info_provider * pip) {
optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx, expr const & e, pos_info_provider const * pip) {
return mk_class_instance(env, get_dummy_ios(), ctx, e, pip);
}
static constraint mk_class_instance_root_cnstr(environment const & env, io_state const & ios, local_context const & _ctx, expr const & m, bool is_strict,
bool use_local_instances, pos_info_provider const * pip) {
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator &&) {
cienv & cenv = get_cienv();
cenv.set_env(env);
auto cls_name = cenv.is_class(meta_type);
if (!cls_name) {
// do nothing, since type is not a class.
return lazy_list<constraints>(constraints());
}
bool multiple_insts = try_multiple_instances(env, *cls_name);
local_context ctx;
if (use_local_instances)
ctx = _ctx.instantiate(substitution(s));
pair<expr, justification> mj = update_meta(meta, s);
expr new_meta = mj.first;
justification new_j = mj.second;
if (multiple_insts) {
// TODO(Leo)
return lazy_list<constraints>();
} else {
if (auto r = mk_class_instance(env, ios, ctx.get_data(), meta_type, pip)) {
constraint c = mk_eq_cnstr(new_meta, *r, new_j);
return lazy_list<constraints>(constraints(c));
} else if (is_strict) {
return lazy_list<constraints>();
} else {
return lazy_list<constraints>(constraints());
}
}
};
bool owner = false;
delay_factor factor;
return mk_choice_cnstr(m, choice_fn, factor, owner, j);
}
/** \brief Create a metavariable, and attach choice constraint for generating
solutions using class-instances
*/
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, pos_info_provider const * pip) {
name_generator ngen(prefix);
expr m = ctx.mk_meta(ngen, suffix, type, g);
constraint c = mk_class_instance_root_cnstr(env, ios, ctx, m, is_strict,
use_local_instances, pip);
return mk_pair(m, c);
}
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances) {
if (use_local_instances)
return mk_class_instance(env, ios, ctx.get_data(), type, nullptr);
else
return mk_class_instance(env, ios, list<expr>(), type, nullptr);
}
optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type) {
return mk_class_instance(env, ctx.get_data(), type, nullptr);
}
optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
level lvl = sort_level(tc.ensure_type(type).first);
expr is_hset = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first;
return mk_class_instance(tc.env(), ios, ctx, is_hset);
}
optional<expr> mk_subsingleton_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
level lvl = sort_level(tc.ensure_type(type).first);
expr subsingleton;
if (is_standard(tc.env()))
subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type);
else
subsingleton = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type)).first;
return mk_class_instance(tc.env(), ios, ctx, subsingleton);
}
void initialize_class_instance_resolution() {
g_prefix1 = new name(name::mk_internal_unique_name());
g_prefix2 = new name(name::mk_internal_unique_name());
g_class_unique_class_instances = new name{"class", "unique_instances"};
g_class_trace_instances = new name{"class", "trace_instances"};
g_class_instance_max_depth = new name{"class", "instance_max_depth"};
g_class_trans_instances = new name{"class", "trans_instances"};
register_bool_option(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES,
"(class) generate an error if there is more than one solution "
"for a class-instance resolution problem");
register_bool_option(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES,
"(class) display messages showing the class-instances resolution execution trace");
@ -1124,7 +1207,6 @@ void finalize_class_instance_resolution() {
delete g_default_factory;
delete g_prefix1;
delete g_prefix2;
delete g_class_unique_class_instances;
delete g_class_trace_instances;
delete g_class_instance_max_depth;
delete g_class_trans_instances;

27
src/library/class_instance_resolution.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <memory>
#include "kernel/environment.h"
#include "library/io_state.h"
#include "library/local_context.h"
namespace lean {
class ci_type_inference {
@ -32,6 +33,32 @@ public:
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx, expr const & e, pos_info_provider const * pip = nullptr);
optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx, expr const & e, pos_info_provider const * pip = nullptr);
// Old API
/** \brief Create a metavariable, and attach choice constraint for generating
solutions using class-instances.
\param ctx Local context where placeholder is located
\param prefix Prefix for metavariables that will be created by this procedure
\param suffix If provided, then it is added to the main metavariable created by this procedure.
\param use_local_instances If instances in the local context should be used
in the class-instance resolution
\param is_strict True if constraint should fail if not solution is found,
False if empty solution should be returned if there is no solution
\param type Expected type for the placeholder (if known)
\param tag To be associated with new metavariables and expressions (for error localization).
*/
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, pos_info_provider const * pip);
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx, expr const & type, bool use_local_instances);
optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type);
optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
optional<expr> mk_subsingleton_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
void initialize_class_instance_resolution();
void finalize_class_instance_resolution();
}

539
src/library/class_instance_synth.cpp
View file

@ -1,539 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/lazy_list_fn.h"
#include "util/flet.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/instantiate.h"
#include "kernel/for_each_fn.h"
#include "kernel/abstract.h"
#include "kernel/error_msgs.h"
#include "library/unifier.h"
#include "library/reducible.h"
#include "library/metavar_closure.h"
#include "library/error_handling/error_handling.h"
#include "library/class.h"
#include "library/local_context.h"
#include "library/choice_iterator.h"
#include "library/pp_options.h"
#include "library/generic_exception.h"
#include "library/util.h"
#include "library/constants.h"
#include "library/class_instance_synth.h"
#ifndef LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES
#define LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES false
#endif
#ifndef LEAN_DEFAULT_CLASS_TRACE_INSTANCES
#define LEAN_DEFAULT_CLASS_TRACE_INSTANCES false
#endif
#ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH
#define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32
#endif
#ifndef LEAN_DEFAULT_CLASS_CONSERVATIVE
#define LEAN_DEFAULT_CLASS_CONSERVATIVE true
#endif
#ifndef LEAN_DEFAULT_CLASS_TRANS_INSTANCES
#define LEAN_DEFAULT_CLASS_TRANS_INSTANCES true
#endif
namespace lean {
static name * g_tmp_prefix = nullptr;
static name * g_class_unique_class_instances = nullptr;
static name * g_class_trace_instances = nullptr;
static name * g_class_instance_max_depth = nullptr;
static name * g_class_conservative = nullptr;
static name * g_class_trans_instances = nullptr;
[[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
[[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); }
void initialize_class_instance_elaborator() {
g_tmp_prefix = new name(name::mk_internal_unique_name());
g_class_unique_class_instances = new name{"class", "unique_instances"};
g_class_trace_instances = new name{"class", "trace_instances"};
g_class_instance_max_depth = new name{"class", "instance_max_depth"};
g_class_conservative = new name{"class", "conservative"};
g_class_trans_instances = new name{"class", "trans_instances"};
register_bool_option(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES,
"(class) generate an error if there is more than one solution "
"for a class-instance resolution problem");
register_bool_option(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES,
"(class) display messages showing the class-instances resolution execution trace");
register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH,
"(class) max allowed depth in class-instance resolution");
register_bool_option(*g_class_conservative, LEAN_DEFAULT_CLASS_CONSERVATIVE,
"(class) use conservative unification (only unfold reducible definitions, and avoid delta-delta case splits)");
register_bool_option(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES,
"(class) use automatically derived instances from the transitive closure of the structure instance graph");
}
void finalize_class_instance_elaborator() {
delete g_tmp_prefix;
delete g_class_unique_class_instances;
delete g_class_trace_instances;
delete g_class_instance_max_depth;
delete g_class_conservative;
delete g_class_trans_instances;
}
bool get_class_unique_class_instances(options const & o) {
return o.get_bool(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES);
}
bool get_class_trace_instances(options const & o) {
return o.get_bool(*g_class_trace_instances, LEAN_DEFAULT_CLASS_TRACE_INSTANCES);
}
unsigned get_class_instance_max_depth(options const & o) {
return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH);
}
bool get_class_conservative(options const & o) {
return o.get_bool(*g_class_conservative, LEAN_DEFAULT_CLASS_CONSERVATIVE);
}
bool get_class_trans_instances(options const & o) {
return o.get_bool(*g_class_trans_instances, LEAN_DEFAULT_CLASS_TRANS_INSTANCES);
}
/** \brief Context for handling class-instance metavariable choice constraint */
struct class_instance_context {
io_state m_ios;
name_generator m_ngen;
type_checker_ptr m_tc;
expr m_main_meta;
bool m_use_local_instances;
bool m_trace_instances;
bool m_conservative;
unsigned m_max_depth;
bool m_trans_instances;
char const * m_fname;
optional<pos_info> m_pos;
class_instance_context(environment const & env, io_state const & ios,
name const & prefix, bool use_local_instances):
m_ios(ios),
m_ngen(prefix),
m_use_local_instances(use_local_instances) {
m_fname = nullptr;
m_trace_instances = get_class_trace_instances(ios.get_options());
m_max_depth = get_class_instance_max_depth(ios.get_options());
m_conservative = get_class_conservative(ios.get_options());
m_trans_instances = get_class_trans_instances(ios.get_options());
m_tc = mk_class_type_checker(env, m_ngen.mk_child(), m_conservative);
options opts = m_ios.get_options();
opts = opts.update_if_undef(get_pp_purify_metavars_name(), false);
opts = opts.update_if_undef(get_pp_implicit_name(), true);
m_ios.set_options(opts);
}
environment const & env() const { return m_tc->env(); }
io_state const & ios() const { return m_ios; }
bool use_local_instances() const { return m_use_local_instances; }
type_checker & tc() const { return *m_tc; }
bool trace_instances() const { return m_trace_instances; }
void set_main_meta(expr const & meta) { m_main_meta = meta; }
expr const & get_main_meta() const { return m_main_meta; }
void set_pos(char const * fname, optional<pos_info> const & pos) {
m_fname = fname;
m_pos = pos;
}
optional<pos_info> const & get_pos() const { return m_pos; }
char const * get_file_name() const { return m_fname; }
unsigned get_max_depth() const { return m_max_depth; }
bool use_trans_instances() const { return m_trans_instances; }
};
static pair<expr, constraint> mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
optional<expr> const & type, tag g, unsigned depth, bool use_globals);
/** \brief Choice function \c fn for synthesizing class instances.
The function \c fn produces a stream of alternative solutions for ?m.
In this case, \c fn will do the following:
1) if the elaborated type of ?m is a 'class' C, then the stream will start with
a) all local instances of class C (if elaborator.local_instances == true)
b) all global instances of class C
*/
struct class_instance_elaborator : public choice_iterator {
std::shared_ptr<class_instance_context> m_C;
local_context m_ctx;
expr m_meta;
// elaborated type of the metavariable
expr m_meta_type;
// local instances that should also be included in the
// class-instance resolution.
// This information is retrieved from the local context
list<expr> m_local_instances;
// global declaration names that are class instances.
// This information is retrieved using #get_class_instances.
list<name> m_trans_instances;
list<name> m_instances;
justification m_jst;
unsigned m_depth;
bool m_displayed_trace_header;
class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
expr const & meta, expr const & meta_type,
list<expr> const & local_insts, list<name> const & trans_insts, list<name> const & instances,
justification const & j, unsigned depth):
choice_iterator(), m_C(C), m_ctx(ctx), m_meta(meta), m_meta_type(meta_type),
m_local_instances(local_insts), m_trans_instances(trans_insts), m_instances(instances), m_jst(j), m_depth(depth) {
if (m_depth > m_C->get_max_depth()) {
throw_class_exception("maximum class-instance resolution depth has been reached "
"(the limit can be increased by setting option 'class.instance_max_depth') "
"(the class-instance resolution trace can be visualized by setting option 'class.trace_instances')",
C->get_main_meta());
}
m_displayed_trace_header = false;
}
constraints mk_constraints(constraint const & c, buffer<constraint> const & cs) {
return cons(c, to_list(cs.begin(), cs.end()));
}
void trace(expr const & t, expr const & r) {
if (!m_C->trace_instances())
return;
auto out = diagnostic(m_C->env(), m_C->ios());
if (!m_displayed_trace_header && m_depth == 0) {
if (auto fname = m_C->get_file_name()) {
out << fname << ":";
}
if (auto pos = m_C->get_pos()) {
out << pos->first << ":" << pos->second << ":";
}
out << " class-instance resolution trace" << endl;
m_displayed_trace_header = true;
}
for (unsigned i = 0; i < m_depth; i++)
out << " ";
if (m_depth > 0)
out << "[" << m_depth << "] ";
out << m_meta << " : " << t << " := " << r << endl;
}
optional<constraints> try_instance(expr const & inst, expr const & inst_type, bool use_globals) {
type_checker & tc = m_C->tc();
name_generator & ngen = m_C->m_ngen;
tag g = inst.get_tag();
try {
flet<local_context> scope(m_ctx, m_ctx);
buffer<expr> locals;
expr meta_type = m_meta_type;
while (true) {
meta_type = tc.whnf(meta_type).first;
if (!is_pi(meta_type))
break;
expr local = mk_local(ngen.next(), binding_name(meta_type),
binding_domain(meta_type), binding_info(meta_type));
m_ctx.add_local(local);
locals.push_back(local);
meta_type = instantiate(binding_body(meta_type), local);
}
expr type = inst_type;
expr r = inst;
buffer<constraint> cs;
while (true) {
type = tc.whnf(type).first;
if (!is_pi(type))
break;
expr arg;
if (binding_info(type).is_inst_implicit()) {
pair<expr, constraint> ac = mk_class_instance_elaborator(m_C, m_ctx, some_expr(binding_domain(type)),
g, m_depth+1, use_globals);
arg = ac.first;
cs.push_back(ac.second);
} else {
arg = m_ctx.mk_meta(m_C->m_ngen, some_expr(binding_domain(type)), g);
}
r = mk_app(r, arg, g);
type = instantiate(binding_body(type), arg);
}
r = Fun(locals, r);
trace(meta_type, r);
constraint c = mk_eq_cnstr(m_meta, r, m_jst);
return optional<constraints>(mk_constraints(c, cs));
} catch (exception &) {
return optional<constraints>();
}
}
optional<constraints> try_instance(name const & inst, bool use_globals) {
environment const & env = m_C->env();
if (auto decl = env.find(inst)) {
name_generator & ngen = m_C->m_ngen;
buffer<level> ls_buffer;
unsigned num_univ_ps = decl->get_num_univ_params();
for (unsigned i = 0; i < num_univ_ps; i++)
ls_buffer.push_back(mk_meta_univ(ngen.next()));
levels ls = to_list(ls_buffer.begin(), ls_buffer.end());
expr inst_cnst = copy_tag(m_meta, mk_constant(inst, ls));
expr inst_type = instantiate_type_univ_params(*decl, ls);
return try_instance(inst_cnst, inst_type, use_globals);
} else {
return optional<constraints>();
}
}
virtual optional<constraints> next() {
while (!empty(m_local_instances)) {
expr inst = head(m_local_instances);
m_local_instances = tail(m_local_instances);
if (!is_local(inst))
continue;
bool use_globals = true;
if (auto r = try_instance(inst, mlocal_type(inst), use_globals))
return r;
}
while (!empty(m_trans_instances)) {
bool use_globals = false;
name inst = head(m_trans_instances);
m_trans_instances = tail(m_trans_instances);
if (auto cs = try_instance(inst, use_globals))
return cs;
}
while (!empty(m_instances)) {
bool use_globals = true;
name inst = head(m_instances);
m_instances = tail(m_instances);
if (auto cs = try_instance(inst, use_globals))
return cs;
}
return optional<constraints>();
}
};
// Remarks:
// - we only use get_class_instances and get_class_derived_trans_instances when use_globals is true
static constraint mk_class_instance_cnstr(std::shared_ptr<class_instance_context> const & C, local_context const & ctx, expr const & m, unsigned depth, bool use_globals) {
environment const & env = C->env();
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const &, name_generator const &) {
if (auto cls_name_it = is_ext_class(C->tc(), meta_type)) {
name cls_name = *cls_name_it;
list<expr> const & ctx_lst = ctx.get_data();
list<expr> local_insts;
if (C->use_local_instances())
local_insts = get_local_instances(C->tc(), ctx_lst, cls_name);
list<name> trans_insts, insts;
if (use_globals) {
if (depth == 0 && C->use_trans_instances())
trans_insts = get_class_derived_trans_instances(env, cls_name);
insts = get_class_instances(env, cls_name);
}
if (empty(local_insts) && empty(insts))
return lazy_list<constraints>(); // nothing to be done
// we are always strict with placeholders associated with classes
return choose(std::make_shared<class_instance_elaborator>(C, ctx, meta, meta_type, local_insts, trans_insts, insts, j, depth));
} else {
// do nothing, type is not a class...
return lazy_list<constraints>(constraints());
}
};
bool owner = false;
return mk_choice_cnstr(m, choice_fn, to_delay_factor(cnstr_group::Basic), owner, j);
}
static pair<expr, constraint> mk_class_instance_elaborator(std::shared_ptr<class_instance_context> const & C, local_context const & ctx,
optional<expr> const & type, tag g, unsigned depth, bool use_globals) {
expr m = ctx.mk_meta(C->m_ngen, type, g);
constraint c = mk_class_instance_cnstr(C, ctx, m, depth, use_globals);
return mk_pair(m, c);
}
static constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_context> const & C, local_context const & _ctx,
expr const & m, bool is_strict, unifier_config const & cfg, delay_factor const & factor) {
environment const & env = C->env();
justification j = mk_failed_to_synthesize_jst(env, m);
auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s,
name_generator && ngen) {
environment const & env = C->env();
auto cls_name_it = is_ext_class(C->tc(), meta_type);
if (!cls_name_it) {
// do nothing, since type is not a class.
return lazy_list<constraints>(constraints());
}
local_context ctx = _ctx.instantiate(substitution(s));
pair<expr, justification> mj = update_meta(meta, s);
expr new_meta = mj.first;
justification new_j = mj.second;
unsigned depth = 0;
bool use_globals = true;
constraint c = mk_class_instance_cnstr(C, ctx, new_meta, depth, use_globals);
unifier_config new_cfg(cfg);
new_cfg.m_discard = false;
new_cfg.m_use_exceptions = false;
new_cfg.m_pattern = true;
new_cfg.m_kind = C->m_conservative ? unifier_kind::VeryConservative : unifier_kind::Liberal;
auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) -> constraints {
substitution new_s = subst;
// some constraints may have been postponed (example: universe level constraints)
constraints postponed = map(cnstrs,
[&](constraint const & c) {
// we erase internal justifications
return update_justification(c, mk_composite1(j, new_j));
});
metavar_closure cls(new_meta);
cls.add(meta_type);
constraints cs = cls.mk_constraints(new_s, new_j);
return append(cs, postponed);
};
auto no_solution_fn = [=]() {
if (is_strict)
return lazy_list<constraints>();
else
return lazy_list<constraints>(constraints());
};
unify_result_seq seq1 = unify(env, 1, &c, std::move(ngen), substitution(), new_cfg);
unify_result_seq seq2 = filter(seq1, [=](pair<substitution, constraints> const & p) {
substitution new_s = p.first;
expr result = new_s.instantiate(new_meta);
// We only keep complete solutions (modulo universe metavariables)
return !has_expr_metavar_relaxed(result);
});
if (get_class_unique_class_instances(C->m_ios.get_options())) {
optional<expr> solution;
substitution subst;
constraints cnstrs;
for_each(seq2, [&](pair<substitution, constraints> const & p) {
subst = p.first;
cnstrs = p.second;
expr next_solution = subst.instantiate(new_meta);
if (solution) {
throw_class_exception(m, [=](formatter const & fmt) {
format r = format("ambiguous class-instance resolution, "
"there is more than one solution");
r += pp_indent_expr(fmt, *solution);
r += compose(line(), format("and"));
r += pp_indent_expr(fmt, next_solution);
return r;
});
} else {
solution = next_solution;
}
});
if (!solution) {
return no_solution_fn();
} else {
// some constraints may have been postponed (example: universe level constraints)
return lazy_list<constraints>(to_cnstrs_fn(subst, cnstrs));
}
} else {
if (try_multiple_instances(env, *cls_name_it)) {
lazy_list<constraints> seq3 = map2<constraints>(seq2, [=](pair<substitution, constraints> const & p) {
return to_cnstrs_fn(p.first, p.second);
});
if (is_strict) {
return seq3;
} else {
// make sure it does not fail by appending empty set of constraints
return append(seq3, lazy_list<constraints>(constraints()));
}
} else {
auto p = seq2.pull();
if (!p)
return no_solution_fn();
else
return lazy_list<constraints>(to_cnstrs_fn(p->first.first, p->first.second));
}
}
};
bool owner = false;
return mk_choice_cnstr(m, choice_fn, factor, owner, j);
}
/** \brief Create a metavariable, and attach choice constraint for generating
solutions using class-instances
*/
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg,
pos_info_provider const * pip) {
auto C = std::make_shared<class_instance_context>(env, ios, prefix, use_local_instances);
expr m = ctx.mk_meta(C->m_ngen, suffix, type, g);
C->set_main_meta(m);
if (pip)
C->set_pos(pip->get_file_name(), pip->get_pos_info(m));
constraint c = mk_class_instance_root_cnstr(C, ctx, m, is_strict, cfg, delay_factor());
return mk_pair(m, c);
}
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, expr const & type, bool use_local_instances,
unifier_config const & cfg) {
auto C = std::make_shared<class_instance_context>(env, ios, prefix, use_local_instances);
if (!is_ext_class(C->tc(), type))
return none_expr();
expr meta = ctx.mk_meta(C->m_ngen, some_expr(type), type.get_tag());
unsigned depth = 0;
bool use_globals = true;
constraint c = mk_class_instance_cnstr(C, ctx, meta, depth, use_globals);
unifier_config new_cfg(cfg);
new_cfg.m_discard = true;
new_cfg.m_use_exceptions = true;
new_cfg.m_pattern = true;
new_cfg.m_kind = C->m_conservative ? unifier_kind::VeryConservative : unifier_kind::Liberal;
try {
auto seq = unify(env, 1, &c, C->m_ngen.mk_child(), substitution(), new_cfg);
while (true) {
auto p = seq.pull();
lean_assert(p);
substitution s = p->first.first;
expr r = s.instantiate_all(meta);
expr new_type = s.instantiate_all(type);
if (!has_expr_metavar_relaxed(r) && new_type == type)
return some_expr(r);
seq = p->second;
}
} catch (exception &) {
return none_expr();
}
}
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx,
name const & prefix, expr const & type, bool use_local_instances,
unifier_config const & cfg) {
local_context lctx(ctx);
return mk_class_instance(env, ios, lctx, prefix, type, use_local_instances, cfg);
}
optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type) {
return mk_class_instance(env, get_dummy_ios(), ctx, *g_tmp_prefix, type);
}
optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
level lvl = sort_level(tc.ensure_type(type).first);
expr is_hset = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hset_name(), {lvl}), type)).first;
return mk_class_instance(tc.env(), ios, ctx, tc.mk_fresh_name(), is_hset);
}
optional<expr> mk_subsingleton_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type) {
level lvl = sort_level(tc.ensure_type(type).first);
expr subsingleton;
if (is_standard(tc.env()))
subsingleton = mk_app(mk_constant(get_subsingleton_name(), {lvl}), type);
else
subsingleton = tc.whnf(mk_app(mk_constant(get_is_trunc_is_hprop_name(), {lvl}), type)).first;
return mk_class_instance(tc.env(), ios, ctx, tc.mk_fresh_name(), subsingleton);
}
}

55
src/library/class_instance_synth.h
View file

@ -1,55 +0,0 @@
/*
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
#include "library/io_state.h"
#include "library/unifier.h"
namespace lean {
class local_context;
class type_checker;
/** \brief Create a metavariable, and attach choice constraint for generating
solutions using class-instances.
\param ctx Local context where placeholder is located
\param prefix Prefix for metavariables that will be created by this procedure
\param suffix If provided, then it is added to the main metavariable created by this procedure.
\param use_local_instances If instances in the local context should be used
in the class-instance resolution
\param is_strict True if constraint should fail if not solution is found,
False if empty solution should be returned if there is no solution
\param type Expected type for the placeholder (if known)
\param tag To be associated with new metavariables and expressions (for error localization).
*/
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g, unifier_config const & cfg,
pos_info_provider const * pip);
/** \brief Create/synthesize a term of the class instance \c type. */
optional<expr> mk_class_instance(environment const & env, io_state const & ios, local_context const & ctx,
name const & prefix, expr const & type, bool use_local_instances = true,
unifier_config const & cfg = unifier_config());
optional<expr> mk_class_instance(environment const & env, io_state const & ios, list<expr> const & ctx,
name const & prefix, expr const & type, bool use_local_instances = true,
unifier_config const & cfg = unifier_config());
optional<expr> mk_class_instance(environment const & env, local_context const & ctx, expr const & type);
/** \brief Try to synthesize an inhabitant for (is_hset type) using class instance resolution */
optional<expr> mk_hset_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
/** \brief Try to synthesize an inhabitant for (subsingleton type in the standard library, and hprop in the HoTT library)
using class instance resolution */
optional<expr> mk_subsingleton_instance(type_checker & tc, io_state const & ios, list<expr> const & ctx, expr const & type);
void initialize_class_instance_elaborator();
void finalize_class_instance_elaborator();
}

9
src/library/init_module.cpp
View file

@ -37,13 +37,14 @@ Author: Leonardo de Moura
#include "library/abbreviation.h"
#include "library/relation_manager.h"
#include "library/user_recursors.h"
#include "library/class_instance_synth.h"
#include "library/class_instance_resolution.h"
#include "library/composition_manager.h"
#include "library/noncomputable.h"
#include "library/aux_recursors.h"
#include "library/decl_stats.h"
#include "library/meng_paulson.h"
#include "library/norm_num.h"
#include "library/class_instance_resolution.h"
namespace lean {
void initialize_library_module() {
@ -80,22 +81,23 @@ void initialize_library_module() {
initialize_abbreviation();
initialize_relation_manager();
initialize_user_recursors();
initialize_class_instance_elaborator();
initialize_composition_manager();
initialize_noncomputable();
initialize_aux_recursors();
initialize_decl_stats();
initialize_meng_paulson();
initialize_norm_num();
initialize_class_instance_resolution();
}
void finalize_library_module() {
finalize_class_instance_resolution();
finalize_norm_num();
finalize_meng_paulson();
finalize_decl_stats();
finalize_aux_recursors();
finalize_noncomputable();
finalize_composition_manager();
finalize_class_instance_elaborator();
finalize_user_recursors();
finalize_relation_manager();
finalize_abbreviation();
@ -129,6 +131,5 @@ void finalize_library_module() {
finalize_print();
finalize_fingerprint();
finalize_constants();
finalize_norm_num();
}
}

4
src/library/tactic/apply_tactic.cpp
View file

@ -22,7 +22,7 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/type_util.h"
#include "library/local_context.h"
#include "library/class_instance_synth.h"
#include "library/class_instance_resolution.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/apply_tactic.h"
@ -119,7 +119,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const
auto mc = mk_class_instance_elaborator(
env, ios, ctx, ngen.next(), optional<name>(),
use_local_insts, is_strict,
some_expr(head_beta_reduce(binding_domain(e_t))), e.get_tag(), cfg, nullptr);
some_expr(head_beta_reduce(binding_domain(e_t))), e.get_tag(), nullptr);
meta = mc.first;
cs.push_back(mc.second);
} else {

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

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "library/locals.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/class_instance_synth.h"
#include "library/class_instance_resolution.h"
#include "library/tactic/util.h"
#include "library/tactic/intros_tactic.h"
#include "library/tactic/subst_tactic.h"

5
src/library/tactic/induction_tactic.cpp
View file

@ -13,7 +13,7 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/reducible.h"
#include "library/locals.h"
#include "library/class_instance_synth.h"
#include "library/class_instance_resolution.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/generalize_tactic.h"
@ -66,11 +66,10 @@ class induction_tac {
bool use_local_insts = true;
bool is_strict = false;
local_context ctx = g.to_local_context();
unifier_config cfg(m_ios.get_options());
auto mc = mk_class_instance_elaborator(
m_env, m_ios, ctx, m_ngen.next(), optional<name>(),
use_local_insts, is_strict,
some_expr(type), m_ref.get_tag(), cfg, nullptr);
some_expr(type), m_ref.get_tag(), nullptr);
m_cs += mc.second;
return mc.first;
}

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

@ -15,7 +15,7 @@ Author: Leonardo de Moura
#include "library/util.h"
#include "library/constants.h"
#include "library/reducible.h"
#include "library/class_instance_synth.h"
#include "library/class_instance_resolution.h"
#include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h"
#include "library/tactic/inversion_tactic.h"

6
src/library/tactic/rewrite_tactic.cpp
View file

@ -32,7 +32,7 @@ Author: Leonardo de Moura
#include "library/constants.h"
#include "library/unfold_macros.h"
#include "library/generic_exception.h"
#include "library/class_instance_synth.h"
#include "library/class_instance_resolution.h"
#include "library/num.h"
#include "library/tactic/clear_tactic.h"
#include "library/tactic/trace_tactic.h"
@ -1040,13 +1040,11 @@ class rewrite_fn {
}
pair<expr, constraint> mk_class_instance_elaborator(expr const & type) {
unifier_config cfg;
cfg.m_kind = unifier_kind::VeryConservative;
bool use_local_instances = true;
bool is_strict = false;
return ::lean::mk_class_instance_elaborator(m_env, m_ios, m_ctx, m_ngen.next(), optional<name>(),
use_local_instances, is_strict,
some_expr(type), m_expr_loc.get_tag(), cfg, nullptr);
some_expr(type), m_expr_loc.get_tag(), nullptr);
}
// target, new_target, H : represents the rewrite (H : target = new_target) for hypothesis