feat(library/type_context): add normalizer for type_context

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));

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<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

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<expr> normalizer::unfold_recursor_core(expr const & f, unsigned i,
+                                                buffer<unsigned> const & idxs, buffer<expr> & 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<expr> 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<expr> normalizer::unfold_recursor_major(expr const & f, unsigned idx, buffer<expr> & args) {
+    buffer<unsigned> idxs;
+    idxs.push_back(idx);
+    return unfold_recursor_core(f, 0, idxs, args, true);
+}
+
+expr normalizer::normalize_app(expr const & e) {
+    buffer<expr> 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"};

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<expr> unfold_recursor_core(expr const & f, unsigned i,
+                                        buffer<unsigned> const & idxs, buffer<expr> & args, bool is_rec);
+    optional<expr> unfold_recursor_major(expr const & f, unsigned idx, buffer<expr> & 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();
 }

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

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))))