From d0e9e0e21ce87b723e3c39f624e5b12bf6fd12d0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Jan 2015 20:58:40 -0800 Subject: [PATCH] feat(library/definitional/projection): add auxiliary function for simplifying expressions containing projections and constructors --- src/frontends/lean/structure_cmd.cpp | 13 ---- src/library/definitional/projection.cpp | 85 +++++++++++++++++++++++++ src/library/definitional/projection.h | 7 ++ 3 files changed, 92 insertions(+), 13 deletions(-) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 3ed0b34c4..3080471f5 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -62,19 +62,6 @@ static name * g_gen_proj_mk = nullptr; bool get_structure_eta_thm(options const & o) { return o.get_bool(*g_gen_eta, LEAN_DEFAULT_STRUCTURE_ETA); } bool get_structure_proj_mk_thm(options const & o) { return o.get_bool(*g_gen_proj_mk, LEAN_DEFAULT_STRUCTURE_ETA); } -/** \brief Return true iff the type named \c S can be viewed as - a structure in the given environment. - - If not, generate an error message using \c pos. -*/ -bool is_structure(environment const & env, name const & S) { - optional idecls = inductive::is_inductive_decl(env, S); - if (!idecls || length(std::get<2>(*idecls)) != 1) - return false; - inductive::inductive_decl decl = head(std::get<2>(*idecls)); - return length(inductive::inductive_decl_intros(decl)) == 1 && *inductive::get_num_indices(env, S) == 0; -} - /** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure \pre is_structure(env, S) diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp index 5e241b8e8..dda40848b 100644 --- a/src/library/definitional/projection.cpp +++ b/src/library/definitional/projection.cpp @@ -77,6 +77,91 @@ void finalize_projection() { delete g_ext; } +/** \brief Return true iff the type named \c S can be viewed as + a structure in the given environment. + + If not, generate an error message using \c pos. +*/ +bool is_structure(environment const & env, name const & S) { + optional idecls = inductive::is_inductive_decl(env, S); + if (!idecls || length(std::get<2>(*idecls)) != 1) + return false; + inductive::inductive_decl decl = head(std::get<2>(*idecls)); + return length(inductive::inductive_decl_intros(decl)) == 1 && *inductive::get_num_indices(env, S) == 0; +} + +/** \brief If \c is a constructor application, then return the name of the constructor. + Otherwise, return none. +*/ +optional is_constructor_app(environment const & env, expr const & e) { + expr const & fn = get_app_fn(e); + if (is_constant(fn)) + if (auto I = inductive::is_intro_rule(env, const_name(fn))) + return optional(const_name(fn)); + return optional(); +} + +/** \brief If \c d is the name of a definition of the form + Fun (a : A), t + where t is a constructor application, then return the name of the constructor. +*/ +optional is_constructor_app_def(environment const & env, name const & d) { + if (auto decl = env.find(d)) { + expr const * it = &decl->get_value(); + while (is_lambda(*it)) + it = &binding_body(*it); + return is_constructor_app(env, *it); + } + return optional(); +} + +/** \brief Return the name of constructor and projection functions iff \c e is of the form + + (mk ... (pr ...) ...) + + where \c mk is a constructor of a structure, and at least of the arguments is a projection \c pr + where \c pr is not necessarily a projection associated with \c mk. + In this case, the name of \c pr is returned. Otherwise, none is returned. +*/ +optional> is_constructor_of_projections(environment const & env, expr const & e) { + expr const & fn = get_app_fn(e); + if (is_constant(fn)) { + if (auto I = inductive::is_intro_rule(env, const_name(fn))) { + if (is_structure(env, *I)) { + expr const * it = &e; + while (is_app(*it)) { + expr const & arg = app_arg(*it); + expr const & pr = get_app_fn(arg); + if (is_constant(pr)) { + if (auto info = get_projection_info(env, const_name(pr))) { + if (info->m_nparams + 1 == get_app_num_args(arg)) + return some(mk_pair(const_name(pr), const_name(pr))); + } + } + it = &app_fn(*it); + } + } + } + } + return optional>(); +} + +/** \brief Return the name of constructor and projection functions iff \c d is the name of a definition of the form + + Fun (a : A), t + + where is_constructor_of_projections(env, t) + */ +optional> is_constructor_of_projections_def(environment const & env, name const & d) { + if (auto decl = env.find(d)) { + expr const * it = &decl->get_value(); + while (is_lambda(*it)) + it = &binding_body(*it); + return is_constructor_of_projections(env, *it); + } + return optional>(); +} + [[ noreturn ]] static void throw_ill_formed(name const & n) { throw exception(sstream() << "projection generation, '" << n << "' is an ill-formed inductive datatype"); } diff --git a/src/library/definitional/projection.h b/src/library/definitional/projection.h index cbe2d4c60..81726b8bc 100644 --- a/src/library/definitional/projection.h +++ b/src/library/definitional/projection.h @@ -11,6 +11,13 @@ namespace lean { environment mk_projections(environment const & env, name const & n, buffer const & proj_names, bool inst_implicit = false); environment mk_projections(environment const & env, name const & n, bool inst_implicit = false); +/** \brief Return true iff the type named \c S can be viewed as + a structure in the given environment. + + If not, generate an error message using \c pos. +*/ +bool is_structure(environment const & env, name const & S); + /** \brief Auxiliary information attached to projections. This information is used to simplify projection over constructor (efficiently)