From e1f81cfdcd3342158f66e8f6fbdf0c677f319bd1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Nov 2015 20:31:36 -0800 Subject: [PATCH] feat(library/type_context): add normalizer for type_context --- src/frontends/lean/builtin_cmds.cpp | 11 ++++ src/frontends/lean/token_table.cpp | 2 +- src/library/type_context.cpp | 94 +++++++++++++++++++++++++++++ src/library/type_context.h | 31 ++++++++++ tests/lean/norm1.lean | 21 +++++++ tests/lean/norm1.lean.expected.out | 15 +++++ 6 files changed, 173 insertions(+), 1 deletion(-) create mode 100644 tests/lean/norm1.lean create mode 100644 tests/lean/norm1.lean.expected.out diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 4c9b54b0d..189e1bddb 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -1355,6 +1355,16 @@ static environment simplify_cmd(parser & p) { return p.env(); } +static environment normalizer_cmd(parser & p) { + environment const & env = p.env(); + expr e; level_param_names ls; + std::tie(e, ls) = parse_local_expr(p); + tmp_type_context ctx(env, p.ios()); + expr r = normalizer(ctx)(e); + p.regular_stream() << r << endl; + return env; +} + void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces", open_cmd)); @@ -1386,6 +1396,7 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("#replace", "(for debugging purposes)", replace_cmd)); add_cmd(r, cmd_info("#congr", "(for debugging purposes)", congr_cmd)); add_cmd(r, cmd_info("#congr_simp", "(for debugging purposes)", congr_simp_cmd)); + add_cmd(r, cmd_info("#normalizer", "(for debugging purposes)", normalizer_cmd)); add_cmd(r, cmd_info("#accessible", "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd)); add_cmd(r, cmd_info("#decl_stats", "(for debugging purposes) display declaration statistics", decl_stats_cmd)); add_cmd(r, cmd_info("#relevant_thms", "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd)); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 5397946dd..7f7613d2e 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -121,7 +121,7 @@ void init_token_table(token_table & t) { "multiple_instances", "find_decl", "attribute", "persistent", "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq", "#compile", "#accessible", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm", - "#trans", "#replace", "#congr", "#congr_simp", nullptr}; + "#trans", "#replace", "#congr", "#congr_simp", "#normalizer", nullptr}; pair aliases[] = {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"}, diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index de1be8af9..38e437153 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/for_each_fn.h" +#include "kernel/inductive/inductive.h" #include "library/projection.h" #include "library/normalize.h" #include "library/replace_visitor.h" @@ -1818,6 +1819,99 @@ bool default_type_context::ignore_universe_def_eq(level const & l1, level const } } +expr normalizer::normalize_binding(expr const & e) { + expr d = normalize(binding_domain(e)); + expr l = m_ctx.mk_tmp_local(binding_name(e), d, binding_info(e)); + expr b = abstract(normalize(instantiate(binding_body(e), l)), l); + return update_binding(e, d, b); +} + +optional normalizer::unfold_recursor_core(expr const & f, unsigned i, + buffer const & idxs, buffer & args, bool is_rec) { + if (i == idxs.size()) { + expr new_app = mk_rev_app(f, args); + if (is_rec) + return some_expr(normalize(new_app)); + else if (optional r = unfold_app(env(), new_app)) + return some_expr(normalize(*r)); + else + return none_expr(); + } else { + unsigned idx = idxs[i]; + if (idx >= args.size()) + return none_expr(); + expr & arg = args[args.size() - idx - 1]; + if (!is_constructor_app(env(), arg)) + return none_expr(); + return unfold_recursor_core(f, i+1, idxs, args, is_rec); + } +} + +optional normalizer::unfold_recursor_major(expr const & f, unsigned idx, buffer & args) { + buffer idxs; + idxs.push_back(idx); + return unfold_recursor_core(f, 0, idxs, args, true); +} + +expr normalizer::normalize_app(expr const & e) { + buffer args; + bool modified = false; + expr f = get_app_rev_args(e, args); + for (expr & a : args) { + expr new_a = a; + if (m_eval_nested_prop || !m_ctx.is_prop(m_ctx.infer(a))) + new_a = normalize(a); + if (new_a != a) + modified = true; + a = new_a; + } + + if (is_constant(f)) { + if (auto idx = inductive::get_elim_major_idx(env(), const_name(f))) { + if (auto r = unfold_recursor_major(f, *idx, args)) + return *r; + } + } + if (!modified) + return e; + expr r = mk_rev_app(f, args); + if (is_constant(f) && env().is_recursor(const_name(f))) { + return normalize(r); + } else { + return r; + } +} + +expr normalizer::normalize(expr e) { + check_system("normalize"); + if (!should_normalize(e)) + return e; + e = m_ctx.whnf(e); + switch (e.kind()) { + case expr_kind::Var: case expr_kind::Constant: case expr_kind::Sort: + case expr_kind::Meta: case expr_kind::Local: case expr_kind::Macro: + return e; + case expr_kind::Lambda: { + e = normalize_binding(e); + if (m_use_eta) + return try_eta(e); + else + return e; + } + case expr_kind::Pi: + return normalize_binding(e); + case expr_kind::App: + return normalize_app(e); + } + lean_unreachable(); // LCOV_EXCL_LINE +} + +normalizer::normalizer(type_context & ctx, bool eta, bool nested_prop): + m_ctx(ctx), m_use_eta(eta), m_eval_nested_prop(nested_prop) { + if (!is_standard(env())) + nested_prop = true; +} + void initialize_type_context() { g_prefix = new name(name::mk_internal_unique_name()); g_class_trace_instances = new name{"class", "trace_instances"}; diff --git a/src/library/type_context.h b/src/library/type_context.h index b03f30ba1..5dbd6bc05 100644 --- a/src/library/type_context.h +++ b/src/library/type_context.h @@ -556,6 +556,37 @@ public: bool & get_ignore_if_zero() { return m_ignore_if_zero; } }; +/** \brief Simple normalizer */ +class normalizer { + type_context & m_ctx; + bool m_use_eta; + bool m_eval_nested_prop; + + expr normalize_binding(expr const & e); + optional unfold_recursor_core(expr const & f, unsigned i, + buffer const & idxs, buffer & args, bool is_rec); + optional unfold_recursor_major(expr const & f, unsigned idx, buffer & args); + expr normalize_app(expr const & e); + expr normalize(expr e); + +public: + /* + eta == true : enable eta reduction + nested_prop == true : nested propositions are simplified (ignored if HoTT library) + */ + normalizer(type_context & ctx, bool eta = true, bool nested_prop = false); + virtual ~normalizer() {} + + /** \brief Auxiliary predicate for controlling which subterms will be normalized. */ + virtual bool should_normalize(expr const &) const { return true; } + + environment const & env() const { return m_ctx.env(); } + + expr operator()(expr const & e) { + return normalize(e); + } +}; + void initialize_type_context(); void finalize_type_context(); } diff --git a/tests/lean/norm1.lean b/tests/lean/norm1.lean new file mode 100644 index 000000000..9687567a5 --- /dev/null +++ b/tests/lean/norm1.lean @@ -0,0 +1,21 @@ +import data.int +open algebra nat int + +variables a b c : nat +variables i j : int + +set_option pp.notation false +set_option pp.numerals false +set_option pp.implicit true +set_option pp.coercions true + +#normalizer a + b +#normalizer (a + b) * c + 1 +#normalizer a + i + 15 + +variables A : Type +variables [s : ring A] +include s +variables x y : A +#normalizer x + y * x +#normalizer x + 3 diff --git a/tests/lean/norm1.lean.expected.out b/tests/lean/norm1.lean.expected.out new file mode 100644 index 000000000..76fa2f357 --- /dev/null +++ b/tests/lean/norm1.lean.expected.out @@ -0,0 +1,15 @@ +@add nat (@has_add.mk nat nat.add) a b +@add nat (@has_add.mk nat nat.add) (@mul nat (@has_mul.mk nat nat.mul) (@add nat (@has_add.mk nat nat.add) a b) c) + (@one nat (@has_one.mk nat (succ zero))) +@add int (@has_add.mk int int.add) (@add int (@has_add.mk int int.add) (of_nat a) i) + (@bit1 int (@has_one.mk int (@one int (@has_one.mk int (of_nat (@one nat (@has_one.mk nat (succ zero))))))) + (@has_add.mk int int.add) + (@bit1 int (@has_one.mk int (@one int (@has_one.mk int (of_nat (@one nat (@has_one.mk nat (succ zero))))))) + (@has_add.mk int int.add) + (@bit1 int (@has_one.mk int (@one int (@has_one.mk int (of_nat (@one nat (@has_one.mk nat (succ zero))))))) + (@has_add.mk int int.add) + (@one int + (@has_one.mk int (@one int (@has_one.mk int (of_nat (@one nat (@has_one.mk nat (succ zero))))))))))) +@add A (@has_add.mk A (@ring.add A s)) x (@mul A (@has_mul.mk A (@ring.mul A s)) y x) +@add A (@has_add.mk A (@ring.add A s)) x + (@bit1 A (@has_one.mk A (@ring.one A s)) (@has_add.mk A (@ring.add A s)) (@one A (@has_one.mk A (@ring.one A s))))