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

feat(library/class_instance_synth): add helper mk_class_instance procedure

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-08 13:09:54 -07:00
parent 2c7d245bbe
commit ce6e1c9694
2 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/class_instance_synth.cpp
View file

@ -45,6 +45,7 @@ Author: Leonardo de Moura
#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;
@ -55,6 +56,7 @@ static name * g_class_trans_instances = nullptr;
[[ 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"};
@ -79,6 +81,7 @@ void initialize_class_instance_elaborator() {
}
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;
@ -514,6 +517,10 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
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;

2
src/library/class_instance_synth.h
View file

@ -41,6 +41,8 @@ optional<expr> mk_class_instance(environment const & env, io_state const & ios,
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);