From ce8f2a16741fe0049b745a64105d329c4f9d191a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Jun 2015 16:21:38 -0700 Subject: [PATCH] feat(library/class): allow any constant to be marked as a class closes #679 --- src/frontends/lean/decl_attributes.cpp | 2 -- src/library/class.cpp | 30 +++++++++++++++----------- src/library/class.h | 4 +++- src/library/class_instance_synth.cpp | 5 +---- tests/lean/bad_class.lean.expected.out | 2 -- tests/lean/run/679a.lean | 22 +++++++++++++++++++ tests/lean/run/679b.lean | 22 +++++++++++++++++++ 7 files changed, 66 insertions(+), 21 deletions(-) create mode 100644 tests/lean/run/679a.lean create mode 100644 tests/lean/run/679b.lean diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp index f05fe22c0..480d07486 100644 --- a/src/frontends/lean/decl_attributes.cpp +++ b/src/frontends/lean/decl_attributes.cpp @@ -114,8 +114,6 @@ void decl_attributes::parse(buffer const & ns, parser & p) { m_is_quasireducible = true; p.next(); } else if (p.curr_is_token(get_class_tk())) { - if (m_def_only) - throw parser_error("invalid '[class]' attribute, definitions cannot be marked as classes", pos); m_is_class = true; p.next(); } else if (p.curr_is_token(get_multiple_instances_tk())) { diff --git a/src/library/class.cpp b/src/library/class.cpp index 74f464453..e51056163 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -151,9 +151,7 @@ template class scoped_ext; typedef scoped_ext class_ext; static void check_class(environment const & env, name const & c_name) { - declaration c_d = env.get(c_name); - if (c_d.is_definition()) - throw exception(sstream() << "invalid class, '" << c_name << "' is a definition"); + env.get(c_name); } static void check_is_class(environment const & env, name const & c_name) { @@ -182,12 +180,25 @@ void get_classes(environment const & env, buffer & classes) { }); } +bool is_class(environment const & env, name const & c) { + class_state const & s = class_ext::get_state(env); + return s.m_instances.contains(c); +} + +type_checker_ptr mk_class_type_checker(environment const & env, name_generator && ngen, bool conservative) { + auto pred = conservative ? mk_not_reducible_pred(env) : mk_irreducible_pred(env); + class_state s = class_ext::get_state(env); + return mk_type_checker(env, std::move(ngen), [=](name const & n) { + return s.m_instances.contains(n) || pred(n); + }); +} + static name * g_tmp_prefix = nullptr; environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent) { declaration d = env.get(n); expr type = d.get_type(); name_generator ngen(*g_tmp_prefix); - auto tc = mk_type_checker(env, ngen.mk_child()); + auto tc = mk_class_type_checker(env, ngen.mk_child(), false); while (true) { type = tc->whnf(type).first; if (!is_pi(type)) @@ -213,11 +224,6 @@ bool try_multiple_instances(environment const & env, name const & n) { return s.try_multiple_instances(n); } -bool is_class(environment const & env, name const & c) { - class_state const & s = class_ext::get_state(env); - return s.m_instances.contains(c); -} - bool is_instance(environment const & env, name const & i) { class_state const & s = class_ext::get_state(env); return s.is_instance(i); @@ -229,7 +235,7 @@ list get_class_instances(environment const & env, name const & c) { } /** \brief If the constant \c e is a class, return its name */ -optional constant_is_ext_class(environment const & env, expr const & e) { +static optional constant_is_ext_class(environment const & env, expr const & e) { name const & cls_name = const_name(e); if (is_class(env, cls_name)) { return optional(cls_name); @@ -243,7 +249,7 @@ optional constant_is_ext_class(environment const & env, expr const & e) { l_false: \c type is not a class. l_undef: procedure did not establish whether \c type is a class or not. */ -lbool is_quick_ext_class(type_checker const & tc, expr const & type, name & result) { +static lbool is_quick_ext_class(type_checker const & tc, expr const & type, name & result) { environment const & env = tc.env(); expr const * it = &type; while (true) { @@ -287,7 +293,7 @@ lbool is_quick_ext_class(type_checker const & tc, expr const & type, name & resu } /** \brief Full/Expensive test for \c is_ext_class */ -optional is_full_ext_class(type_checker & tc, expr type) { +static optional is_full_ext_class(type_checker & tc, expr type) { type = tc.whnf(type).first; if (is_pi(type)) { return is_full_ext_class(tc, instantiate(binding_body(type), mk_local(tc.mk_fresh_name(), binding_domain(type)))); diff --git a/src/library/class.h b/src/library/class.h index 7149f0327..fb67ae289 100644 --- a/src/library/class.h +++ b/src/library/class.h @@ -5,8 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once - +#include "library/util.h" namespace lean { +/** \brief Create type checker that treats classes as opaque constants */ +type_checker_ptr mk_class_type_checker(environment const & env, name_generator && ngen, bool conservative); /** \brief Add a new 'class' to the environment (if it is not already declared) */ environment add_class(environment const & env, name const & n, bool persistent = true); /** \brief Add a new 'class instance' to the environment with default priority. */ diff --git a/src/library/class_instance_synth.cpp b/src/library/class_instance_synth.cpp index 79f73b9e7..f89bc7472 100644 --- a/src/library/class_instance_synth.cpp +++ b/src/library/class_instance_synth.cpp @@ -113,10 +113,7 @@ struct class_instance_context { 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()); - if (m_conservative) - m_tc = mk_type_checker(env, m_ngen.mk_child(), UnfoldReducible); - else - m_tc = mk_type_checker(env, m_ngen.mk_child()); + 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); diff --git a/tests/lean/bad_class.lean.expected.out b/tests/lean/bad_class.lean.expected.out index 7c8f87591..e69de29bb 100644 --- a/tests/lean/bad_class.lean.expected.out +++ b/tests/lean/bad_class.lean.expected.out @@ -1,2 +0,0 @@ -bad_class.lean:4:0: error: invalid class, 'foo.subsingleton' is a definition -bad_class.lean:6:0: error: 'eq' is not a class diff --git a/tests/lean/run/679a.lean b/tests/lean/run/679a.lean new file mode 100644 index 000000000..89f28a518 --- /dev/null +++ b/tests/lean/run/679a.lean @@ -0,0 +1,22 @@ +import data.finset +open bool nat list finset + +attribute finset [class] + +definition fin_nat [instance] : finset nat := +to_finset [0] + +definition fin_bool [instance] : finset bool := +to_finset [tt, ff] + +definition tst (A : Type) [s : finset A] : finset A := +s + +example : tst nat = to_finset [0] := +rfl + +example : tst bool = to_finset [ff, tt] := +dec_trivial + +example : tst bool = to_finset [tt, ff] := +rfl diff --git a/tests/lean/run/679b.lean b/tests/lean/run/679b.lean new file mode 100644 index 000000000..c43356af9 --- /dev/null +++ b/tests/lean/run/679b.lean @@ -0,0 +1,22 @@ +import data.finset +open bool nat list finset + +definition fset [class] (A : Type) := finset A + +definition fin_nat [instance] : fset nat := +to_finset [0] + +definition fin_bool [instance] : fset bool := +to_finset [tt, ff] + +definition tst (A : Type) [s : fset A] : finset A := +s + +example : tst nat = to_finset [0] := +rfl + +example : tst bool = to_finset [ff, tt] := +dec_trivial + +example : tst bool = to_finset [tt, ff] := +rfl