From 05f27b8f0e92e8ea01118bad62ab7c7514d22635 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Dec 2014 12:40:09 -0800 Subject: [PATCH] feat(frontends/lean/structure): add option for controlling whether we automatically generate eta and projection-over-intro theorems for structures It seems most of the time these theorems are not used at all. They are just polluting the namespace. Signed-off-by: Leonardo de Moura --- library/data/subtype.lean | 2 ++ library/init/datatypes.lean | 3 +++ src/frontends/lean/structure_cmd.cpp | 37 ++++++++++++++++++++++++++-- tests/lean/run/record4.lean | 2 ++ 4 files changed, 42 insertions(+), 2 deletions(-) diff --git a/library/data/subtype.lean b/library/data/subtype.lean index dbceffb92..d13ba25de 100644 --- a/library/data/subtype.lean +++ b/library/data/subtype.lean @@ -3,6 +3,8 @@ -- Author: Leonardo de Moura, Jeremy Avigad open decidable +set_option structure.proj_mk_thm true + structure subtype {A : Type} (P : A → Prop) := tag :: (elt_of : A) (has_property : P elt_of) diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 8dda9cca0..1404ab5f3 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -14,6 +14,9 @@ notation `Type₁` := Type.{1} notation `Type₂` := Type.{2} notation `Type₃` := Type.{3} +set_option structure.eta_thm true +set_option structure.proj_mk_thm true + inductive unit.{l} : Type.{l} := star : unit diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 3a47a5461..4960244b7 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include #include "util/sstream.h" +#include "util/sexpr/option_declarations.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" @@ -43,17 +44,38 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_STRUCTURE_INTRO "mk" #endif +#ifndef LEAN_DEFAULT_STRUCTURE_ETA +#define LEAN_DEFAULT_STRUCTURE_ETA false +#endif + +#ifndef LEAN_DEFAULT_STRUCTURE_PROJ_MK +#define LEAN_DEFAULT_STRUCTURE_PROJ_MK false +#endif + namespace lean { -static name * g_tmp_prefix = nullptr; +static name * g_tmp_prefix = nullptr; +static name * g_gen_eta = nullptr; +static name * g_gen_proj_mk = nullptr; void initialize_structure_cmd() { - g_tmp_prefix = new name(name::mk_internal_unique_name()); + g_tmp_prefix = new name(name::mk_internal_unique_name()); + g_gen_eta = new name{"structure", "eta_thm"}; + g_gen_proj_mk = new name{"structure", "proj_mk_thm"}; + register_bool_option(*g_gen_eta, LEAN_DEFAULT_STRUCTURE_ETA, + "(structure) automatically generate 'eta' theorem whenever declaring a new structure"); + register_bool_option(*g_gen_proj_mk, LEAN_DEFAULT_STRUCTURE_PROJ_MK, + "(structure) automatically gneerate projection over introduction theorem when declaring a new structure, the theorem is never generated for proof irrelevant fields"); } void finalize_structure_cmd() { delete g_tmp_prefix; + delete g_gen_eta; + delete g_gen_proj_mk; } +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. @@ -111,10 +133,15 @@ struct structure_cmd_fn { levels m_ctx_levels; // context levels for creating aliases buffer m_ctx_locals; // context local constants for creating aliases + bool m_gen_eta; + bool m_gen_proj_mk; + structure_cmd_fn(parser & p):m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()), m_namespace(get_namespace(m_env)) { m_tc = mk_type_checker(m_env, m_p.mk_ngen(), false); m_infer_result_universe = false; m_using_explicit_levels = false; + m_gen_eta = get_structure_eta_thm(p.get_options()); + m_gen_proj_mk = get_structure_proj_mk_thm(p.get_options()); } /** \brief Parse structure name and (optional) universe parameters */ @@ -750,6 +777,8 @@ struct structure_cmd_fn { } void declare_eta() { + if (!m_gen_eta) + return; if (!has_eq_decls(m_env)) return; level_param_names lnames = to_list(m_level_names.begin(), m_level_names.end()); @@ -781,6 +810,8 @@ struct structure_cmd_fn { } void declare_proj_over_mk() { + if (!m_gen_proj_mk) + return; if (!has_eq_decls(m_env)) return; level_param_names lnames = to_list(m_level_names.begin(), m_level_names.end()); @@ -791,6 +822,8 @@ struct structure_cmd_fn { expr const & field = m_fields[i]; name const & field_name = mlocal_name(field); expr const & field_type = mlocal_type(field); + if (m_env.prop_proof_irrel() && m_tc->is_prop(field_type).first) + continue; level field_level = sort_level(m_tc->ensure_type(field_type).first); name proj_name = m_name + field_name; expr lhs = mk_app(mk_app(mk_constant(proj_name, st_ls), m_params), mk_fields); diff --git a/tests/lean/run/record4.lean b/tests/lean/run/record4.lean index 7df0184f7..fa54941df 100644 --- a/tests/lean/run/record4.lean +++ b/tests/lean/run/record4.lean @@ -1,5 +1,7 @@ import logic data.unit +set_option structure.eta_thm true + structure point (A : Type) (B : Type) := mk :: (x : A) (y : B)