From 6571c4735342c87e2bc6a5951faa4d94ad43eafd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 4 May 2015 14:23:04 -0700 Subject: [PATCH] feat(library/normalize): add '[unfold-m]' hint See issue #496 --- src/emacs/lean-syntax.el | 3 +- src/frontends/lean/decl_cmds.cpp | 9 ++- src/frontends/lean/token_table.cpp | 3 +- src/frontends/lean/tokens.cpp | 4 ++ src/frontends/lean/tokens.h | 1 + src/library/definitional/brec_on.cpp | 6 +- src/library/normalize.cpp | 102 ++++++++++++++++++++++----- src/library/normalize.h | 8 +++ tests/lean/hott/unfoldm.hlean | 21 ++++++ 9 files changed, 136 insertions(+), 21 deletions(-) create mode 100644 tests/lean/hott/unfoldm.hlean diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index d26fdfd85..c1313e905 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -119,7 +119,8 @@ (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face) ;; modifiers (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]" - "\[coercion\]" "\[unfold-f\]" "\[reducible\]" "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]" + "\[coercion\]" "\[unfold-f\]" "\[unfold-m\]" "\[reducible\]" + "\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]" "\[whnf\]" "\[multiple-instances\]" "\[none\]" "\[decls\]" "\[declarations\]" "\[all-transparent\]" "\[coercions\]" "\[classes\]" "\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index bb2c775bf..fd1a113d6 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -354,6 +354,7 @@ struct decl_attributes { bool m_is_parsing_only; bool m_has_multiple_instances; bool m_unfold_f_hint; + bool m_unfold_m_hint; bool m_symm; bool m_trans; bool m_refl; @@ -376,6 +377,7 @@ struct decl_attributes { m_is_parsing_only = false; m_has_multiple_instances = false; m_unfold_f_hint = false; + m_unfold_m_hint = false; m_symm = false; m_trans = false; m_refl = false; @@ -484,6 +486,9 @@ struct decl_attributes { } else if (p.curr_is_token(get_unfold_f_tk())) { p.next(); m_unfold_f_hint = true; + } else if (p.curr_is_token(get_unfold_m_tk())) { + p.next(); + m_unfold_m_hint = true; } else if (p.curr_is_token(get_unfold_c_tk())) { p.next(); unsigned r = p.parse_small_nat(); @@ -547,7 +552,9 @@ struct decl_attributes { env = add_unfold_c_hint(env, d, *m_unfold_c_hint, m_persistent); if (m_unfold_f_hint) env = add_unfold_f_hint(env, d, m_persistent); - } + if (m_unfold_m_hint) + env = add_unfold_m_hint(env, d, m_persistent); + } if (m_symm) env = add_symm(env, d, m_persistent); if (m_refl) diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index d764ef67e..5e0fc0573 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -108,7 +108,8 @@ void init_token_table(token_table & t) { "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]", "[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", - "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-f]", "[unfold-c", "print", + "evaluate", "check", "eval", "[wf]", "[whnf]", "[all-transparent]", "[priority", "[unfold-f]", + "[unfold-m]", "[unfold-c", "print", "end", "namespace", "section", "prelude", "help", "import", "inductive", "record", "structure", "module", "universe", "universes", "local", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index 316d64a6d..d79c89692 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -105,6 +105,7 @@ static name * g_instance = nullptr; static name * g_priority = nullptr; static name * g_unfold_c = nullptr; static name * g_unfold_f = nullptr; +static name * g_unfold_m = nullptr; static name * g_coercion = nullptr; static name * g_reducible = nullptr; static name * g_quasireducible = nullptr; @@ -238,6 +239,7 @@ void initialize_tokens() { g_priority = new name("[priority"); g_unfold_c = new name("[unfold-c"); g_unfold_f = new name("[unfold-f]"); + g_unfold_m = new name("[unfold-m]"); g_coercion = new name("[coercion]"); g_reducible = new name("[reducible]"); g_quasireducible = new name("[quasireducible]"); @@ -310,6 +312,7 @@ void finalize_tokens() { delete g_priority; delete g_unfold_c; delete g_unfold_f; + delete g_unfold_m; delete g_coercion; delete g_symm; delete g_refl; @@ -507,6 +510,7 @@ name const & get_instance_tk() { return *g_instance; } name const & get_priority_tk() { return *g_priority; } name const & get_unfold_c_tk() { return *g_unfold_c; } name const & get_unfold_f_tk() { return *g_unfold_f; } +name const & get_unfold_m_tk() { return *g_unfold_m; } name const & get_coercion_tk() { return *g_coercion; } name const & get_symm_tk() { return *g_symm; } name const & get_trans_tk() { return *g_trans; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index 6ca75a8b4..678d53e8e 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -107,6 +107,7 @@ name const & get_instance_tk(); name const & get_priority_tk(); name const & get_unfold_c_tk(); name const & get_unfold_f_tk(); +name const & get_unfold_m_tk(); name const & get_coercion_tk(); name const & get_reducible_tk(); name const & get_semireducible_tk(); diff --git a/src/library/definitional/brec_on.cpp b/src/library/definitional/brec_on.cpp index 2751b212b..8071f4d3e 100644 --- a/src/library/definitional/brec_on.cpp +++ b/src/library/definitional/brec_on.cpp @@ -147,7 +147,8 @@ static environment mk_below(environment const & env, name const & n, bool ibelow opaque, rec_decl.get_module_idx(), use_conv_opt); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, below_name, reducible_status::Reducible); - new_env = add_unfold_c_hint(new_env, below_name, nparams + nindices + ntypeformers); + if (!ibelow) + new_env = add_unfold_c_hint(new_env, below_name, nparams + nindices + ntypeformers); return add_protected(new_env, below_name); } @@ -333,7 +334,8 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) opaque, rec_decl.get_module_idx(), use_conv_opt); environment new_env = module::add(env, check(env, new_d)); new_env = set_reducible(new_env, brec_on_name, reducible_status::Reducible); - new_env = add_unfold_c_hint(new_env, brec_on_name, nparams + nindices + ntypeformers); + if (!ind) + new_env = add_unfold_c_hint(new_env, brec_on_name, nparams + nindices + ntypeformers); return add_protected(new_env, brec_on_name); } diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index a2f825d77..c85004069 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -24,21 +24,25 @@ namespace lean { - unfold_c (f a_1 ... a_i ... a_n) should be unfolded when argument a_i is a constructor. - unfold_f (f a_1 ... a_i ... a_n) should be unfolded when it is fully applied. + - unfold_m (f ...) should be unfolded when it is the major premise of a recursor-like operator */ struct unfold_hint_entry { - bool m_unfold_c; //!< true if it is an unfold_c hint - bool m_add; //!< add/remove hint + enum kind {UnfoldC, UnfoldF, UnfoldM}; + kind m_kind; //!< true if it is an unfold_c hint + bool m_add; //!< add/remove hint name m_decl_name; unsigned m_arg_idx; - unfold_hint_entry():m_unfold_c(false), m_add(false), m_arg_idx(0) {} - unfold_hint_entry(bool unfold_c, bool add, name const & n, unsigned idx): - m_unfold_c(unfold_c), m_add(add), m_decl_name(n), m_arg_idx(idx) {} + unfold_hint_entry():m_kind(UnfoldC), m_add(false), m_arg_idx(0) {} + unfold_hint_entry(kind k, bool add, name const & n, unsigned idx): + m_kind(k), m_add(add), m_decl_name(n), m_arg_idx(idx) {} }; -unfold_hint_entry mk_add_unfold_c_entry(name const & n, unsigned idx) { return unfold_hint_entry(true, true, n, idx); } -unfold_hint_entry mk_erase_unfold_c_entry(name const & n) { return unfold_hint_entry(true, false, n, 0); } -unfold_hint_entry mk_add_unfold_f_entry(name const & n) { return unfold_hint_entry(false, true, n, 0); } -unfold_hint_entry mk_erase_unfold_f_entry(name const & n) { return unfold_hint_entry(false, false, n, 0); } +unfold_hint_entry mk_add_unfold_c_entry(name const & n, unsigned idx) { return unfold_hint_entry(unfold_hint_entry::UnfoldC, true, n, idx); } +unfold_hint_entry mk_erase_unfold_c_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldC, false, n, 0); } +unfold_hint_entry mk_add_unfold_f_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldF, true, n, 0); } +unfold_hint_entry mk_erase_unfold_f_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldF, false, n, 0); } +unfold_hint_entry mk_add_unfold_m_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldM, true, n, 0); } +unfold_hint_entry mk_erase_unfold_m_entry(name const & n) { return unfold_hint_entry(unfold_hint_entry::UnfoldM, false, n, 0); } static name * g_unfold_hint_name = nullptr; static std::string * g_key = nullptr; @@ -46,6 +50,7 @@ static std::string * g_key = nullptr; struct unfold_hint_state { name_map m_unfold_c; name_set m_unfold_f; + name_set m_unfold_m; }; struct unfold_hint_config { @@ -53,16 +58,25 @@ struct unfold_hint_config { typedef unfold_hint_entry entry; static void add_entry(environment const &, io_state const &, state & s, entry const & e) { - if (e.m_unfold_c) { + switch (e.m_kind) { + case unfold_hint_entry::UnfoldC: if (e.m_add) s.m_unfold_c.insert(e.m_decl_name, e.m_arg_idx); else s.m_unfold_c.erase(e.m_decl_name); - } else { + break; + case unfold_hint_entry::UnfoldF: if (e.m_add) s.m_unfold_f.insert(e.m_decl_name); else s.m_unfold_f.erase(e.m_decl_name); + break; + case unfold_hint_entry::UnfoldM: + if (e.m_add) + s.m_unfold_m.insert(e.m_decl_name); + else + s.m_unfold_m.erase(e.m_decl_name); + break; } } static name const & get_class_name() { @@ -72,11 +86,13 @@ struct unfold_hint_config { return *g_key; } static void write_entry(serializer & s, entry const & e) { - s << e.m_unfold_c << e.m_add << e.m_decl_name << e.m_arg_idx; + s << static_cast(e.m_kind) << e.m_add << e.m_decl_name << e.m_arg_idx; } static entry read_entry(deserializer & d) { + char k; entry e; - d >> e.m_unfold_c >> e.m_add >> e.m_decl_name >> e.m_arg_idx; + d >> k >> e.m_add >> e.m_decl_name >> e.m_arg_idx; + e.m_kind = static_cast(k); return e; } static optional get_fingerprint(entry const & e) { @@ -122,6 +138,22 @@ environment erase_unfold_f_hint(environment const & env, name const & n, bool pe return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_f_entry(n), persistent); } +environment add_unfold_m_hint(environment const & env, name const & n, bool persistent) { + declaration const & d = env.get(n); + if (!d.is_definition() || d.is_opaque()) + throw exception("invalid unfold-m hint, declaration must be a non-opaque definition"); + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_add_unfold_m_entry(n), persistent); +} + +bool has_unfold_m_hint(environment const & env, name const & d) { + unfold_hint_state const & s = unfold_hint_ext::get_state(env); + return s.m_unfold_m.contains(d); +} + +environment erase_unfold_m_hint(environment const & env, name const & n, bool persistent) { + return unfold_hint_ext::add_entry(env, get_dummy_ios(), mk_erase_unfold_m_entry(n), persistent); +} + void initialize_normalize() { g_unfold_hint_name = new name("unfold-hints"); g_key = new std::string("unfoldh"); @@ -159,6 +191,40 @@ class normalize_fn { return is_constant(f) && ::lean::has_unfold_f_hint(m_tc.env(), const_name(f)); } + optional is_constructor_like(expr const & e) { + if (is_constructor_app(m_tc.env(), e)) + return some_expr(e); + expr const & f = get_app_fn(e); + if (is_constant(f) && has_unfold_m_hint(m_tc.env(), const_name(f))) { + return unfold_app(m_tc.env(), e); + } else { + return none_expr(); + } + } + + optional unfold_recursor_core(expr const & f, unsigned idx, buffer & args, bool is_rec) { + if (idx < args.size()) { + expr & arg = args[args.size() - idx - 1]; + if (optional new_arg = is_constructor_like(arg)) { + flet set_arg(arg, *new_arg); + expr new_app = mk_rev_app(f, args); + if (is_rec) + return some_expr(normalize(new_app)); + else if (optional r = unfold_app(m_tc.env(), new_app)) + return some_expr(normalize(*r)); + } + } + return none_expr(); + } + + optional unfold_recursor_like(expr const & f, unsigned idx, buffer & args) { + return unfold_recursor_core(f, idx, args, false); + } + + optional unfold_recursor_major(expr const & f, unsigned idx, buffer & args) { + return unfold_recursor_core(f, idx, args, true); + } + expr normalize_app(expr const & e) { buffer args; bool modified = false; @@ -176,9 +242,13 @@ class normalize_fn { } } 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 (auto r = unfold_recursor_like(f, *idx, args)) + return *r; + } + if (is_constant(f)) { + if (auto idx = inductive::get_elim_major_idx(m_tc.env(), const_name(f))) { + if (auto r = unfold_recursor_major(f, *idx, args)) + return *r; } } if (!modified) diff --git a/src/library/normalize.h b/src/library/normalize.h index 7da2a0afa..fb6aa9139 100644 --- a/src/library/normalize.h +++ b/src/library/normalize.h @@ -52,6 +52,14 @@ environment erase_unfold_f_hint(environment const & env, name const & n, bool pe /** \brief Retrieve the hint added with the procedure add_unfold_f_hint. */ optional has_unfold_f_hint(environment const & env, name const & d); + +/** \brief unfold-m hint instructs normalizer (and simplifier) that function application + (f ...) should be unfolded when it is the major premise of a constructor like operator */ +environment add_unfold_m_hint(environment const & env, name const & n, bool persistent = true); +environment erase_unfold_m_hint(environment const & env, name const & n, bool persistent = true); +/** \brief Retrieve the hint added with the procedure add_unfold_m_hint. */ +optional has_unfold_m_hint(environment const & env, name const & d); + void initialize_normalize(); void finalize_normalize(); } diff --git a/tests/lean/hott/unfoldm.hlean b/tests/lean/hott/unfoldm.hlean new file mode 100644 index 000000000..7826a5fc7 --- /dev/null +++ b/tests/lean/hott/unfoldm.hlean @@ -0,0 +1,21 @@ +definition rr [unfold-m] {A : Type} {a : A} := eq.refl a + +constants f g : Π {A : Type}, A → A + +example (A : Type) (a b : A) (C : A → Type) (H : C a) (f g : C a → C a) : f = g → f (eq.rec H rr) = g H := +begin + intros, + esimp, + state, + congruence, + assumption +end + +example (A : Type) (a b : A) (C : A → Type) (H : C a) (f g : C a → C a) : f = g → f (eq.rec_on rr H) = g H := +begin + intros, + esimp, + state, + congruence, + assumption +end