From ac664505e6587f6ef3775d4d1160616d18f406af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Dec 2014 21:12:39 -0800 Subject: [PATCH] refactor(library): move class management to library module --- src/frontends/lean/builtin_cmds.cpp | 1 + src/frontends/lean/class.cpp | 280 +---------------- src/frontends/lean/class.h | 22 -- src/frontends/lean/decl_cmds.cpp | 3 +- src/frontends/lean/inductive_cmd.cpp | 2 +- src/frontends/lean/init_module.cpp | 3 - src/frontends/lean/placeholder_elaborator.cpp | 2 +- src/frontends/lean/structure_cmd.cpp | 2 +- src/library/CMakeLists.txt | 2 +- src/library/class.cpp | 289 ++++++++++++++++++ src/library/class.h | 32 ++ src/library/init_module.cpp | 3 + 12 files changed, 332 insertions(+), 309 deletions(-) create mode 100644 src/library/class.cpp create mode 100644 src/library/class.h diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 3c889682a..47acb6398 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/normalize.h" #include "library/print.h" +#include "library/class.h" #include "library/flycheck.h" #include "library/definitional/projection.h" #include "library/definitional/util.h" diff --git a/src/frontends/lean/class.cpp b/src/frontends/lean/class.cpp index 574689f90..01532cf1e 100644 --- a/src/frontends/lean/class.cpp +++ b/src/frontends/lean/class.cpp @@ -5,183 +5,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include -#include "util/lbool.h" -#include "util/sstream.h" -#include "kernel/instantiate.h" -#include "library/scoped_ext.h" -#include "library/kernel_serializer.h" -#include "library/reducible.h" #include "library/num.h" #include "library/normalize.h" -#include "library/aliases.h" +#include "library/class.h" #include "frontends/lean/parser.h" #include "frontends/lean/util.h" #include "frontends/lean/tokens.h" -#ifndef LEAN_INSTANCE_DEFAULT_PRIORITY -#define LEAN_INSTANCE_DEFAULT_PRIORITY 1000 -#endif - namespace lean { -struct class_entry { - bool m_class_cmd; - name m_class; - name m_instance; // only relevant if m_class_cmd == false - unsigned m_priority; // only relevant if m_class_cmd == false - class_entry():m_class_cmd(false), m_priority(0) {} - explicit class_entry(name const & c):m_class_cmd(true), m_class(c), m_priority(0) {} - class_entry(name const & c, name const & i, unsigned p): - m_class_cmd(false), m_class(c), m_instance(i), m_priority(p) {} -}; - -struct class_state { - typedef name_map> class_instances; - typedef name_map instance_priorities; - class_instances m_instances; - instance_priorities m_priorities; - - unsigned get_priority(name const & i) const { - if (auto it = m_priorities.find(i)) - return *it; - else - return LEAN_INSTANCE_DEFAULT_PRIORITY; - } - - list insert(name const & inst, unsigned priority, list const & insts) const { - if (!insts) - return to_list(inst); - else if (priority >= get_priority(head(insts))) - return list(inst, insts); - else - return list(head(insts), insert(inst, priority, tail(insts))); - } - - void add_class(name const & c) { - auto it = m_instances.find(c); - if (!it) - m_instances.insert(c, list()); - } - - void add_instance(name const & c, name const & i, unsigned p) { - auto it = m_instances.find(c); - if (!it) { - m_instances.insert(c, to_list(i)); - } else { - auto lst = filter(*it, [&](name const & i1) { return i1 != i; }); - m_instances.insert(c, insert(i, p, lst)); - } - if (p != LEAN_INSTANCE_DEFAULT_PRIORITY) - m_priorities.insert(i, p); - } -}; - -static name * g_class_name = nullptr; -static std::string * g_key = nullptr; - -struct class_config { - typedef class_state state; - typedef class_entry entry; - static void add_entry(environment const &, io_state const &, state & s, entry const & e) { - if (e.m_class_cmd) - s.add_class(e.m_class); - else - s.add_instance(e.m_class, e.m_instance, e.m_priority); - } - static name const & get_class_name() { - return *g_class_name; - } - static std::string const & get_serialization_key() { - return *g_key; - } - static void write_entry(serializer & s, entry const & e) { - if (e.m_class_cmd) - s << true << e.m_class; - else - s << false << e.m_class << e.m_instance << e.m_priority; - } - static entry read_entry(deserializer & d) { - entry e; - d >> e.m_class_cmd; - if (e.m_class_cmd) - d >> e.m_class; - else - d >> e.m_class >> e.m_instance >> e.m_priority; - return e; - } - static optional get_fingerprint(entry const & e) { - if (e.m_class_cmd) - return some(e.m_class.hash()); - else - return some(hash(hash(e.m_class.hash(), e.m_instance.hash()), e.m_priority)); - } -}; - -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"); -} - -static void check_is_class(environment const & env, name const & c_name) { - class_state const & s = class_ext::get_state(env); - if (!s.m_instances.contains(c_name)) - throw exception(sstream() << "'" << c_name << "' is not a class"); -} - -name get_class_name(environment const & env, expr const & e) { - if (!is_constant(e)) - throw exception("class expected, expression is not a constant"); - name const & c_name = const_name(e); - check_is_class(env, c_name); - return c_name; -} - -environment add_class(environment const & env, name const & n, bool persistent) { - check_class(env, n); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(n), persistent); -} - -void get_classes(environment const & env, buffer & classes) { - class_state const & s = class_ext::get_state(env); - s.m_instances.for_each([&](name const & c, list const &) { - classes.push_back(c); - }); -} - -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, false); - while (true) { - type = tc->whnf(type).first; - if (!is_pi(type)) - break; - type = instantiate(binding_body(type), mk_local(ngen.next(), binding_domain(type))); - } - name c = get_class_name(env, get_app_fn(type)); - check_is_class(env, c); - return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n, priority), persistent); -} - -environment add_instance(environment const & env, name const & n, bool persistent) { - return add_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, persistent); -} - -bool is_class(environment const & env, name const & c) { - class_state const & s = class_ext::get_state(env); - return s.m_instances.contains(c); -} - -list get_class_instances(environment const & env, name const & c) { - class_state const & s = class_ext::get_state(env); - return ptr_to_list(s.m_instances.find(c)); -} - optional parse_instance_priority(parser & p) { if (p.curr_is_token(get_priority_tk())) { p.next(); @@ -242,113 +73,4 @@ void register_class_cmds(cmd_table & r) { add_cmd(r, cmd_info("instance", "add a new instance", add_instance_cmd)); add_cmd(r, cmd_info("class", "add a new class", add_class_cmd)); } - -/** \brief If the constant \c e is a class, return its name */ -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); - } else { - return optional(); - } -} - -/** \brief Partial/Quick test for is_ext_class. Result - l_true: \c type is a class, and the name of the class is stored in \c result. - 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) { - environment const & env = tc.env(); - expr const * it = &type; - while (true) { - switch (it->kind()) { - case expr_kind::Var: case expr_kind::Sort: case expr_kind::Local: - case expr_kind::Meta: case expr_kind::Lambda: - return l_false; - case expr_kind::Macro: - return l_undef; - case expr_kind::Constant: - if (auto r = constant_is_ext_class(env, *it)) { - result = *r; - return l_true; - } else if (tc.is_opaque(*it)) { - return l_false; - } else { - return l_undef; - } - case expr_kind::App: { - expr const & f = get_app_fn(*it); - if (is_constant(f)) { - if (auto r = constant_is_ext_class(env, f)) { - result = *r; - return l_true; - } else if (tc.is_opaque(f)) { - return l_false; - } else { - return l_undef; - } - } else if (is_lambda(f) || is_macro(f)) { - return l_undef; - } else { - return l_false; - } - } - case expr_kind::Pi: - it = &binding_body(*it); - break; - } - } -} - -/** \brief Full/Expensive test for \c is_ext_class */ -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)))); - } else { - expr f = get_app_fn(type); - if (!is_constant(f)) - return optional(); - return constant_is_ext_class(tc.env(), f); - } -} - -/** \brief Return true iff \c type is a class or Pi that produces a class. */ -optional is_ext_class(type_checker & tc, expr const & type) { - name result; - switch (is_quick_ext_class(tc, type, result)) { - case l_true: return optional(result); - case l_false: return optional(); - case l_undef: break; - } - return is_full_ext_class(tc, type); -} - -/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */ -list get_local_instances(type_checker & tc, list const & ctx, name const & cls_name) { - buffer buffer; - for (auto const & l : ctx) { - if (!is_local(l)) - continue; - expr inst_type = mlocal_type(l); - if (auto it = is_ext_class(tc, inst_type)) - if (*it == cls_name) - buffer.push_back(l); - } - return to_list(buffer.begin(), buffer.end()); -} -void initialize_class() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); - g_class_name = new name("class"); - g_key = new std::string("class"); - class_ext::initialize(); -} - -void finalize_class() { - class_ext::finalize(); - delete g_key; - delete g_class_name; - delete g_tmp_prefix; -} } diff --git a/src/frontends/lean/class.h b/src/frontends/lean/class.h index ac632bd3a..7c4ba6184 100644 --- a/src/frontends/lean/class.h +++ b/src/frontends/lean/class.h @@ -11,29 +11,7 @@ Author: Leonardo de Moura #include "frontends/lean/cmd_table.h" namespace lean { -/** \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. */ -environment add_instance(environment const & env, name const & n, bool persistent = true); -/** \brief Add a new 'class instance' to the environment. */ -environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent); -/** \brief Return true iff \c c was declared with \c add_class . */ -bool is_class(environment const & env, name const & c); -/** \brief Return the instances of the given class. */ -list get_class_instances(environment const & env, name const & c); -/** \brief Return the classes in the given environment. */ -void get_classes(environment const & env, buffer & classes); -name get_class_name(environment const & env, expr const & e); /** \brief Parse priority for an class instance */ optional parse_instance_priority(parser & p); void register_class_cmds(cmd_table & r); - -/** \brief Return true iff \c type is a class or Pi that produces a class. */ -optional is_ext_class(type_checker & tc, expr const & type); - -/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */ -list get_local_instances(type_checker & tc, list const & ctx, name const & cls_name); - -void initialize_class(); -void finalize_class(); } diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 4105d6d2b..56d2e66f0 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -18,10 +18,11 @@ Author: Leonardo de Moura #include "library/explicit.h" #include "library/reducible.h" #include "library/coercion.h" +#include "library/class.h" #include "library/definitional/equations.h" #include "frontends/lean/parser.h" -#include "frontends/lean/util.h" #include "frontends/lean/class.h" +#include "frontends/lean/util.h" #include "frontends/lean/tokens.h" namespace lean { diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 5e7c624cd..40780125e 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -21,6 +21,7 @@ Author: Leonardo de Moura #include "library/protected.h" #include "library/explicit.h" #include "library/reducible.h" +#include "library/class.h" #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" #include "library/definitional/cases_on.h" @@ -29,7 +30,6 @@ Author: Leonardo de Moura #include "library/definitional/util.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/util.h" -#include "frontends/lean/class.h" #include "frontends/lean/parser.h" #include "frontends/lean/tokens.h" #include "frontends/lean/type_util.h" diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index 0c288a71e..60d804c23 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -11,7 +11,6 @@ Author: Leonardo de Moura #include "frontends/lean/parser.h" #include "frontends/lean/info_annotation.h" #include "frontends/lean/tactic_hint.h" -#include "frontends/lean/class.h" #include "frontends/lean/parser_config.h" #include "frontends/lean/calc.h" #include "frontends/lean/begin_end_ext.h" @@ -44,7 +43,6 @@ void initialize_frontend_lean_module() { initialize_scanner(); initialize_parser(); initialize_tactic_hint(); - initialize_class(); initialize_parser_config(); initialize_calc(); initialize_begin_end_ext(); @@ -71,7 +69,6 @@ void finalize_frontend_lean_module() { finalize_begin_end_ext(); finalize_calc(); finalize_parser_config(); - finalize_class(); finalize_tactic_hint(); finalize_parser(); finalize_scanner(); diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 32052bd46..ff964e819 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -15,8 +15,8 @@ Author: Leonardo de Moura #include "library/reducible.h" #include "library/metavar_closure.h" #include "library/error_handling/error_handling.h" +#include "library/class.h" #include "frontends/lean/util.h" -#include "frontends/lean/class.h" #include "frontends/lean/local_context.h" #include "frontends/lean/choice_iterator.h" #include "frontends/lean/elaborator_exception.h" diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 4960244b7..1278a7d87 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -26,6 +26,7 @@ Author: Leonardo de Moura #include "library/coercion.h" #include "library/explicit.h" #include "library/protected.h" +#include "library/class.h" #include "library/definitional/rec_on.h" #include "library/definitional/induction_on.h" #include "library/definitional/cases_on.h" @@ -38,7 +39,6 @@ Author: Leonardo de Moura #include "frontends/lean/tokens.h" #include "frontends/lean/elaborator_exception.h" #include "frontends/lean/type_util.h" -#include "frontends/lean/class.h" #ifndef LEAN_DEFAULT_STRUCTURE_INTRO #define LEAN_DEFAULT_STRUCTURE_INTRO "mk" diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 514c84097..084548a23 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -7,7 +7,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp standard_kernel.cpp sorry.cpp replace_visitor.cpp unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp explicit.cpp num.cpp string.cpp head_map.cpp match.cpp - definition_cache.cpp declaration_index.cpp + definition_cache.cpp declaration_index.cpp class.cpp print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp) diff --git a/src/library/class.cpp b/src/library/class.cpp new file mode 100644 index 000000000..893b1c1cd --- /dev/null +++ b/src/library/class.cpp @@ -0,0 +1,289 @@ +/* +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 +#include "util/lbool.h" +#include "util/sstream.h" +#include "kernel/instantiate.h" +#include "library/scoped_ext.h" +#include "library/kernel_serializer.h" +#include "library/reducible.h" +#include "library/aliases.h" + +#ifndef LEAN_INSTANCE_DEFAULT_PRIORITY +#define LEAN_INSTANCE_DEFAULT_PRIORITY 1000 +#endif + +namespace lean { +struct class_entry { + bool m_class_cmd; + name m_class; + name m_instance; // only relevant if m_class_cmd == false + unsigned m_priority; // only relevant if m_class_cmd == false + class_entry():m_class_cmd(false), m_priority(0) {} + explicit class_entry(name const & c):m_class_cmd(true), m_class(c), m_priority(0) {} + class_entry(name const & c, name const & i, unsigned p): + m_class_cmd(false), m_class(c), m_instance(i), m_priority(p) {} +}; + +struct class_state { + typedef name_map> class_instances; + typedef name_map instance_priorities; + class_instances m_instances; + instance_priorities m_priorities; + + unsigned get_priority(name const & i) const { + if (auto it = m_priorities.find(i)) + return *it; + else + return LEAN_INSTANCE_DEFAULT_PRIORITY; + } + + list insert(name const & inst, unsigned priority, list const & insts) const { + if (!insts) + return to_list(inst); + else if (priority >= get_priority(head(insts))) + return list(inst, insts); + else + return list(head(insts), insert(inst, priority, tail(insts))); + } + + void add_class(name const & c) { + auto it = m_instances.find(c); + if (!it) + m_instances.insert(c, list()); + } + + void add_instance(name const & c, name const & i, unsigned p) { + auto it = m_instances.find(c); + if (!it) { + m_instances.insert(c, to_list(i)); + } else { + auto lst = filter(*it, [&](name const & i1) { return i1 != i; }); + m_instances.insert(c, insert(i, p, lst)); + } + if (p != LEAN_INSTANCE_DEFAULT_PRIORITY) + m_priorities.insert(i, p); + } +}; + +static name * g_class_name = nullptr; +static std::string * g_key = nullptr; + +struct class_config { + typedef class_state state; + typedef class_entry entry; + static void add_entry(environment const &, io_state const &, state & s, entry const & e) { + if (e.m_class_cmd) + s.add_class(e.m_class); + else + s.add_instance(e.m_class, e.m_instance, e.m_priority); + } + static name const & get_class_name() { + return *g_class_name; + } + static std::string const & get_serialization_key() { + return *g_key; + } + static void write_entry(serializer & s, entry const & e) { + if (e.m_class_cmd) + s << true << e.m_class; + else + s << false << e.m_class << e.m_instance << e.m_priority; + } + static entry read_entry(deserializer & d) { + entry e; + d >> e.m_class_cmd; + if (e.m_class_cmd) + d >> e.m_class; + else + d >> e.m_class >> e.m_instance >> e.m_priority; + return e; + } + static optional get_fingerprint(entry const & e) { + if (e.m_class_cmd) + return some(e.m_class.hash()); + else + return some(hash(hash(e.m_class.hash(), e.m_instance.hash()), e.m_priority)); + } +}; + +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"); +} + +static void check_is_class(environment const & env, name const & c_name) { + class_state const & s = class_ext::get_state(env); + if (!s.m_instances.contains(c_name)) + throw exception(sstream() << "'" << c_name << "' is not a class"); +} + +name get_class_name(environment const & env, expr const & e) { + if (!is_constant(e)) + throw exception("class expected, expression is not a constant"); + name const & c_name = const_name(e); + check_is_class(env, c_name); + return c_name; +} + +environment add_class(environment const & env, name const & n, bool persistent) { + check_class(env, n); + return class_ext::add_entry(env, get_dummy_ios(), class_entry(n), persistent); +} + +void get_classes(environment const & env, buffer & classes) { + class_state const & s = class_ext::get_state(env); + s.m_instances.for_each([&](name const & c, list const &) { + classes.push_back(c); + }); +} + +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, false); + while (true) { + type = tc->whnf(type).first; + if (!is_pi(type)) + break; + type = instantiate(binding_body(type), mk_local(ngen.next(), binding_domain(type))); + } + name c = get_class_name(env, get_app_fn(type)); + check_is_class(env, c); + return class_ext::add_entry(env, get_dummy_ios(), class_entry(c, n, priority), persistent); +} + +environment add_instance(environment const & env, name const & n, bool persistent) { + return add_instance(env, n, LEAN_INSTANCE_DEFAULT_PRIORITY, persistent); +} + +bool is_class(environment const & env, name const & c) { + class_state const & s = class_ext::get_state(env); + return s.m_instances.contains(c); +} + +list get_class_instances(environment const & env, name const & c) { + class_state const & s = class_ext::get_state(env); + return ptr_to_list(s.m_instances.find(c)); +} + +/** \brief If the constant \c e is a class, return its name */ +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); + } else { + return optional(); + } +} + +/** \brief Partial/Quick test for is_ext_class. Result + l_true: \c type is a class, and the name of the class is stored in \c result. + 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) { + environment const & env = tc.env(); + expr const * it = &type; + while (true) { + switch (it->kind()) { + case expr_kind::Var: case expr_kind::Sort: case expr_kind::Local: + case expr_kind::Meta: case expr_kind::Lambda: + return l_false; + case expr_kind::Macro: + return l_undef; + case expr_kind::Constant: + if (auto r = constant_is_ext_class(env, *it)) { + result = *r; + return l_true; + } else if (tc.is_opaque(*it)) { + return l_false; + } else { + return l_undef; + } + case expr_kind::App: { + expr const & f = get_app_fn(*it); + if (is_constant(f)) { + if (auto r = constant_is_ext_class(env, f)) { + result = *r; + return l_true; + } else if (tc.is_opaque(f)) { + return l_false; + } else { + return l_undef; + } + } else if (is_lambda(f) || is_macro(f)) { + return l_undef; + } else { + return l_false; + } + } + case expr_kind::Pi: + it = &binding_body(*it); + break; + } + } +} + +/** \brief Full/Expensive test for \c is_ext_class */ +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)))); + } else { + expr f = get_app_fn(type); + if (!is_constant(f)) + return optional(); + return constant_is_ext_class(tc.env(), f); + } +} + +/** \brief Return true iff \c type is a class or Pi that produces a class. */ +optional is_ext_class(type_checker & tc, expr const & type) { + name result; + switch (is_quick_ext_class(tc, type, result)) { + case l_true: return optional(result); + case l_false: return optional(); + case l_undef: break; + } + return is_full_ext_class(tc, type); +} + +/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */ +list get_local_instances(type_checker & tc, list const & ctx, name const & cls_name) { + buffer buffer; + for (auto const & l : ctx) { + if (!is_local(l)) + continue; + expr inst_type = mlocal_type(l); + if (auto it = is_ext_class(tc, inst_type)) + if (*it == cls_name) + buffer.push_back(l); + } + return to_list(buffer.begin(), buffer.end()); +} + +void initialize_class() { + g_tmp_prefix = new name(name::mk_internal_unique_name()); + g_class_name = new name("class"); + g_key = new std::string("class"); + class_ext::initialize(); +} + +void finalize_class() { + class_ext::finalize(); + delete g_key; + delete g_class_name; + delete g_tmp_prefix; +} +} diff --git a/src/library/class.h b/src/library/class.h new file mode 100644 index 000000000..c17996b6e --- /dev/null +++ b/src/library/class.h @@ -0,0 +1,32 @@ +/* +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 + +namespace lean { +/** \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. */ +environment add_instance(environment const & env, name const & n, bool persistent = true); +/** \brief Add a new 'class instance' to the environment. */ +environment add_instance(environment const & env, name const & n, unsigned priority, bool persistent); +/** \brief Return true iff \c c was declared with \c add_class . */ +bool is_class(environment const & env, name const & c); +/** \brief Return the instances of the given class. */ +list get_class_instances(environment const & env, name const & c); +/** \brief Return the classes in the given environment. */ +void get_classes(environment const & env, buffer & classes); +name get_class_name(environment const & env, expr const & e); + +/** \brief Return true iff \c type is a class or Pi that produces a class. */ +optional is_ext_class(type_checker & tc, expr const & type); + +/** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */ +list get_local_instances(type_checker & tc, list const & ctx, name const & cls_name); + +void initialize_class(); +void finalize_class(); +} diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 70dd99377..00dedd85e 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include "library/let.h" #include "library/typed_expr.h" #include "library/choice.h" +#include "library/class.h" #include "library/string.h" #include "library/num.h" #include "library/resolve_macro.h" @@ -57,9 +58,11 @@ void initialize_library_module() { initialize_coercion(); initialize_unifier_plugin(); initialize_sorry(); + initialize_class(); } void finalize_library_module() { + finalize_class(); finalize_sorry(); finalize_unifier_plugin(); finalize_coercion();