From 1bd1f94542c524015919460d6f38e6f1773b8752 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Feb 2015 12:12:52 -0800 Subject: [PATCH] feat(library/normalize): add "unfold-c" hint to normalizer This hint will also be used in the simplifier --- src/library/init_module.cpp | 3 ++ src/library/normalize.cpp | 86 +++++++++++++++++++++++++++++++++++++ src/library/normalize.h | 24 +++++++++++ 3 files changed, 113 insertions(+) diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index ead8cb2e3..1713f6e25 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -34,6 +34,7 @@ Author: Leonardo de Moura #include "library/util.h" #include "library/pp_options.h" #include "library/projection.h" +#include "library/normalize.h" namespace lean { void initialize_library_module() { @@ -67,9 +68,11 @@ void initialize_library_module() { initialize_library_util(); initialize_pp_options(); initialize_projection(); + initialize_normalize(); } void finalize_library_module() { + finalize_normalize(); finalize_projection(); finalize_pp_options(); finalize_library_util(); diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index 3c9ffda8c..008d4c029 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -11,8 +11,82 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/inductive/inductive.h" #include "library/reducible.h" +#include "library/util.h" +#include "library/scoped_ext.h" +#include "library/kernel_serializer.h" namespace lean { +/** + \brief c_unfold hint instructs the normalizer (and simplifier) that + a function application (f a_1 ... a_i ... a_n) should be unfolded + when argument a_i is a constructor. +*/ +struct unfold_c_hint_entry { + name m_decl_name; + optional m_arg_idx; + unfold_c_hint_entry() {} + unfold_c_hint_entry(name const & n, optional const & idx):m_decl_name(n), m_arg_idx(idx) {} +}; + +static name * g_unfold_c_hint_name = nullptr; +static std::string * g_key = nullptr; + +struct unfold_c_hint_config { + typedef name_map state; + typedef unfold_c_hint_entry entry; + + static void add_entry(environment const &, io_state const &, state & s, entry const & e) { + if (e.m_arg_idx) + s.insert(e.m_decl_name, *e.m_arg_idx); + else + s.erase(e.m_decl_name); + } + static name const & get_class_name() { + return *g_unfold_c_hint_name; + } + static std::string const & get_serialization_key() { + return *g_key; + } + static void write_entry(serializer & s, entry const & e) { + s << e.m_decl_name << e.m_arg_idx; + } + static entry read_entry(deserializer & d) { + entry e; + d >> e.m_decl_name >> e.m_arg_idx; + return e; + } + static optional get_fingerprint(entry const & e) { + return some(e.m_decl_name.hash()); + } +}; + +template class scoped_ext; +typedef scoped_ext unfold_c_hint_ext; + +environment add_unfold_c_hint(environment const & env, name const & n, optional idx, bool persistent) { + return unfold_c_hint_ext::add_entry(env, get_dummy_ios(), unfold_c_hint_entry(n, idx), persistent); +} + +optional has_unfold_c_hint(environment const & env, name const & d) { + name_map const & s = unfold_c_hint_ext::get_state(env); + if (auto it = s.find(d)) + return optional(*it); + else + return optional(); +} + +void initialize_normalize() { + g_unfold_c_hint_name = new name("c-unfold"); + g_key = new std::string("c-unfold"); + unfold_c_hint_ext::initialize(); +} + +void finalize_normalize() { + unfold_c_hint_ext::finalize(); + delete g_unfold_c_hint_name; + delete g_key; +} + class normalize_fn { type_checker & m_tc; name_generator m_ngen; @@ -27,6 +101,12 @@ class normalize_fn { return update_binding(e, d, b); } + optional has_unfold_c_hint(expr const & f) { + if (!is_constant(f)) + return optional(); + return ::lean::has_unfold_c_hint(m_tc.env(), const_name(f)); + } + expr normalize_app(expr const & e) { buffer args; bool modified = false; @@ -37,6 +117,12 @@ class normalize_fn { modified = true; a = new_a; } + if (auto idx = has_unfold_c_hint(f)) { + if (*idx < args.size() && is_constructor_app(m_tc.env(), args[args.size() - *idx - 1])) { + if (optional r = unfold_app(m_tc.env(), mk_rev_app(f, args))) + return normalize(*r); + } + } if (!modified) return e; expr r = mk_rev_app(f, args); diff --git a/src/library/normalize.h b/src/library/normalize.h index af44fbc2b..afed47253 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -30,4 +30,28 @@ expr normalize(type_checker & tc, expr const & e, constraint_seq & cs); */ expr normalize(type_checker & tc, expr const & e, std::function const & pred, // NOLINT constraint_seq & cs); + +/** \brief c_unfold hint instructs the normalizer (and simplifier) that + a function application (f a_1 ... a_i ... a_n) should be unfolded + when argument a_i is a constructor. + + The constant will be unfolded even if it the whnf procedure did not unfolded it. + + Of course, kernel opaque constants are not unfolded. + + \remark If idx is none, then the hint is removed. +*/ +environment add_unfold_c_hint(environment const & env, name const & n, optional idx, bool persistent = true); +inline environment add_unfold_c_hint(environment const & env, name const & n, unsigned idx, bool persistent = true) { + return add_unfold_c_hint(env, n, optional(idx), persistent); +} +inline environment erase_unfold_c_hint(environment const & env, name const & n, bool persistent = true) { + return add_unfold_c_hint(env, n, optional(), persistent); +} + +/** \brief Retrieve the hint added with the procedure add_unfold_c_hint. */ +optional has_unfold_c_hint(environment const & env, name const & d); + +void initialize_normalize(); +void finalize_normalize(); }