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

feat(library/tactic/class_instance_synth): add mk_class_instance procedures

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-19 20:09:09 -08:00
parent 4421069e34
commit d6f79423e9
2 changed files with 38 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/library/tactic/class_instance_synth.cpp
View file

@ -426,4 +426,33 @@ pair<expr, constraint> mk_class_instance_elaborator(
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 relax_opaque, bool use_local_instances,
unifier_config const & cfg) {
auto C = std::make_shared<class_instance_context>(env, ios, prefix, relax_opaque, 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;
constraint c = mk_class_instance_cnstr(C, ctx, meta, depth);
unifier_config new_cfg(cfg);
new_cfg.m_discard = true;
new_cfg.m_use_exceptions = true;
try {
auto p = unify(env, 1, &c, C->m_ngen.mk_child(), substitution(), new_cfg).pull();
lean_assert(p);
substitution s = p->first.first;
return some_expr(s.instantiate_all(meta));
} 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 relax_opaque, bool use_local_instances,
unifier_config const & cfg) {
local_context lctx(ctx);
return mk_class_instance(env, ios, lctx, prefix, type, relax_opaque, use_local_instances, cfg);
}
}

9
src/library/tactic/class_instance_synth.h
View file

@ -33,6 +33,15 @@ pair<expr, constraint> mk_class_instance_elaborator(
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 relax_opaque = true, 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 relax_opaque = true, bool use_local_instances = true,
unifier_config const & cfg = unifier_config());
void initialize_class_instance_elaborator();
void finalize_class_instance_elaborator();
}