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

refactor(library/class): remove attribute [multiple_instances] and old type class resolution procedure

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-03 13:58:22 -08:00
parent 4a43e33d45
commit d7de521126
5 changed files with 9 additions and 476 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/library/class.cpp
View file

@ -19,7 +19,7 @@ Author: Leonardo de Moura
#include "library/attribute_manager.h"
namespace lean {
enum class class_entry_kind { Class, Multi, Instance, TransInstance, DerivedTransInstance };
enum class class_entry_kind { Class, Instance, TransInstance, DerivedTransInstance };
struct class_entry {
class_entry_kind m_kind;
name m_class;
@ -35,8 +35,6 @@ struct class_entry {
class_entry(name const & src, name const & tgt, name const & i):
m_kind(class_entry_kind::DerivedTransInstance), m_class(tgt), m_instance(i),
m_priority(0), m_source(src) {}
class_entry(name const & c, bool):
m_kind(class_entry_kind::Multi), m_class(c) {}
static class_entry mk_trans_inst(name const & src, name const & tgt, name const & i, unsigned p) {
return class_entry(src, tgt, i, p);
@ -53,7 +51,6 @@ struct class_state {
class_instances m_derived_trans_instances;
instance_priorities m_priorities;
name_set m_derived_trans_instance_set;
name_set m_multiple; // set of classes that allow multiple solutions/instances
tc_multigraph m_mgraph;
class_state():m_mgraph("transitive instance") {}
@ -73,10 +70,6 @@ struct class_state {
return m_derived_trans_instance_set.contains(i);
}
bool try_multiple_instances(name const & c) const {
return m_multiple.contains(c);
}
list<name> insert(name const & inst, unsigned priority, list<name> const & insts) const {
if (!insts)
return to_list(inst);
@ -119,11 +112,6 @@ struct class_state {
m_derived_trans_instance_set.insert(i);
m_mgraph.add1(env, src, i, tgt);
}
void add_multiple(name const & c) {
add_class(c);
m_multiple.insert(c);
}
};
static name * g_class_name = nullptr;
@ -137,9 +125,6 @@ struct class_config {
case class_entry_kind::Class:
s.add_class(e.m_class);
break;
case class_entry_kind::Multi:
s.add_multiple(e.m_class);
break;
case class_entry_kind::Instance:
s.add_instance(e.m_class, e.m_instance, e.m_priority);
break;
@ -161,7 +146,6 @@ struct class_config {
s << static_cast<char>(e.m_kind);
switch (e.m_kind) {
case class_entry_kind::Class:
case class_entry_kind::Multi:
s << e.m_class;
break;
case class_entry_kind::Instance:
@ -181,7 +165,6 @@ struct class_config {
e.m_kind = static_cast<class_entry_kind>(k);
switch (e.m_kind) {
case class_entry_kind::Class:
case class_entry_kind::Multi:
d >> e.m_class;
break;
case class_entry_kind::Instance:
@ -199,7 +182,6 @@ struct class_config {
static optional<unsigned> get_fingerprint(entry const & e) {
switch (e.m_kind) {
case class_entry_kind::Class:
case class_entry_kind::Multi:
return some(e.m_class.hash());
case class_entry_kind::Instance:
case class_entry_kind::TransInstance:
@ -325,16 +307,6 @@ environment add_trans_instance(environment const & env, name const & n, unsigned
return new_env;
}
environment mark_multiple_instances(environment const & env, name const & n, name const & ns, bool persistent) {
check_class(env, n);
return class_ext::add_entry(env, get_dummy_ios(), class_entry(n, true), ns, persistent);
}
bool try_multiple_instances(environment const & env, name const & n) {
class_state const & s = class_ext::get_state(env);
return s.try_multiple_instances(n);
}
bool is_instance(environment const & env, name const & i) {
class_state const & s = class_ext::get_state(env);
return s.is_instance(i);
@ -484,12 +456,6 @@ void initialize_class() {
},
is_class);
register_attribute("multiple_instances", "a type class where elaborator should consider multiple solutions",
[](environment const & env, io_state const &, name const & d, name const & ns, bool persistent) {
return mark_multiple_instances(env, d, ns, persistent);
},
try_multiple_instances);
register_prio_attribute("instance", "type class instance",
[](environment const & env, io_state const &, name const & d, unsigned prio,
name const & ns, bool persistent) {

5
src/library/class.h
View file

@ -33,11 +33,6 @@ list<name> get_class_derived_trans_instances(environment const & env, name const
void get_classes(environment const & env, buffer<name> & classes);
name get_class_name(environment const & env, expr const & e);
/** \brief Mark that multiple instances of class \c n must be explored. */
environment mark_multiple_instances(environment const & env, name const & n, name const & ns, bool persistent);
/** \brief Return true iff multiple instances of class \c n must be explored. */
bool try_multiple_instances(environment const & env, name const & n);
/** \brief Return true iff \c type is a class or Pi that produces a class. */
optional<name> is_ext_class(type_checker & tc, expr const & type);

425
src/library/class_instance_resolution.cpp
View file

@ -25,10 +25,6 @@ Author: Leonardo de Moura
#include "library/choice_iterator.h"
#include "library/type_context.h"
#include "library/class_instance_resolution.h"
// The following include files are need by the old type class resolution procedure
#include "util/lazy_list_fn.h"
#include "library/unifier.h"
#include "library/metavar_closure.h"
namespace lean {
[[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); }
@ -86,47 +82,6 @@ optional<expr> mk_class_instance(environment const & env, list<expr> const & ctx
return mk_class_instance(env, options(), ctx, e, pip);
}
// Auxiliary class for generating a lazy-stream of instances.
class class_multi_instance_iterator : public choice_iterator {
io_state m_ios;
default_type_context m_ti;
type_context::scope_pos_info m_scope_pos_info;
expr m_new_meta;
justification m_new_j;
optional<expr> m_first;
public:
class_multi_instance_iterator(environment const & env, io_state const & ios, list<expr> const & ctx,
expr const & e, pos_info_provider const * pip, expr const & pos_ref,
expr const & new_meta, justification const & new_j,
bool is_strict):
choice_iterator(!is_strict),
m_ios(ios),
m_ti(env, ios.get_options(), ctx, true),
m_scope_pos_info(m_ti, pip, pos_ref),
m_new_meta(new_meta),
m_new_j(new_j) {
m_first = m_ti.mk_class_instance(e);
}
virtual ~class_multi_instance_iterator() {}
virtual optional<constraints> next() {
optional<expr> r;
if (m_first) {
r = m_first;
m_first = none_expr();
} else {
r = m_ti.next_class_instance();
}
if (r) {
constraint c = mk_eq_cnstr(m_new_meta, *r, m_new_j);
return optional<constraints>(constraints(c));
} else {
return optional<constraints>();
}
}
};
static constraint mk_class_instance_root_cnstr(environment const & env, io_state const & ios, old_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);
@ -141,23 +96,16 @@ static constraint mk_class_instance_root_cnstr(environment const & env, io_state
// do nothing, since type is not a class.
return lazy_list<constraints>(constraints());
}
bool multiple_insts = try_multiple_instances(env, *cls_name);
pair<expr, justification> mj = update_meta(meta, s);
expr new_meta = mj.first;
justification new_j = mj.second;
if (multiple_insts) {
return choose(std::shared_ptr<choice_iterator>(new class_multi_instance_iterator(env, ios, ctx.get_data(),
meta_type, pip, meta,
new_meta, new_j, is_strict)));
if (auto r = mk_class_instance(env, ios.get_options(), ctx.get_data(), meta_type, pip, meta)) {
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 {
if (auto r = mk_class_instance(env, ios.get_options(), ctx.get_data(), meta_type, pip, meta)) {
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());
}
return lazy_list<constraints>(constraints());
}
};
bool owner = false;
@ -212,369 +160,12 @@ void finalize_class_instance_resolution() {
delete g_class_force_new;
}
/*
The rest of this module implements the old more powerful and *expensive* type class
resolution procedure. We still have it because the HoTT library contains
type class instances that require full-higher order unification to be solved.
Example:
definition is_equiv_tr [instance] [constructor] {A : Type} (P : A → Type) {x y : A}
(p : x = y) : (is_equiv (transport P p)) := ...
*/
static bool get_class_trace_instances(options const & o) {
return o.get_bool(name("trace", "class_instances"), false);
}
/** \brief Context for handling class-instance metavariable choice constraint */
struct class_instance_context {
io_state m_ios;
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,
bool use_local_instances):
m_ios(ios),
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 = true; // We removed the option class.conservative
m_trans_instances = get_class_trans_instances(ios.get_options());
m_tc = mk_class_type_checker(env, 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, old_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;
old_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, old_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(), m_C->m_tc->get_type_context());
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();
tag g = inst.get_tag();
try {
flet<old_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(mk_fresh_name(), 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(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)) {
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(mk_fresh_name()));
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,
old_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 &) {
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, old_local_context const & ctx,
optional<expr> const & type, tag g, unsigned depth, bool use_globals) {
expr m = ctx.mk_meta(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, old_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) {
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());
}
old_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::Conservative : 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, 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 (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_old_class_instance_elaborator(
environment const & env, io_state const & ios, old_local_context const & ctx,
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, use_local_instances);
expr m = ctx.mk_meta(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);
}
pair<expr, constraint> mk_class_instance_elaborator(
environment const & env, io_state const & ios, old_local_context const & ctx,
optional<name> const & suffix, bool use_local_instances,
bool is_strict, optional<expr> const & type, tag g,
pos_info_provider const * pip) {
if (is_standard(env) || get_class_force_new(ios.get_options())) {
return mk_new_class_instance_elaborator(env, ios, ctx, suffix, use_local_instances,
is_strict, type, g, pip);
} else {
unifier_config cfg(ios.get_options(), true /* use exceptions */, true /* discard */);
return mk_old_class_instance_elaborator(env, ios, ctx, suffix, use_local_instances,
is_strict, type, g, cfg, pip);
}
return mk_new_class_instance_elaborator(env, ios, ctx, suffix, use_local_instances,
is_strict, type, g, pip);
}
}

2
tests/lean/run/div2.lean
View file

@ -49,8 +49,6 @@ definition rec_measure {dom codom : Type} (default : codom) (measure : dom →
(rec_val : dom → (dom → codom) → codom) (x : dom) : codom :=
rec_measure_aux default measure rec_val (succ (measure x)) x
attribute decidable [multiple_instances]
theorem rec_measure_aux_spec {dom codom : Type} (default : codom) (measure : dom → ℕ)
(rec_val : dom → (dom → codom) → codom)
(rec_decreasing : ∀g1 g2 x, (∀z, measure z < measure x → g1 z = g2 z) →

17
tests/lean/run/mult.lean
View file

@ -1,17 +0,0 @@
structure C [class] :=
(val : nat)
attribute C [multiple_instances]
definition c1 [instance] : C := C.mk 1
definition c2 [instance] : C := C.mk 2
set_option trace.class_instances true
definition f [s : C] : nat := C.val
definition tst1 : f = 1 :=
rfl
definition tst2 : f = 2 :=
rfl