feat(library/norm_num): use type_context

src/library/blast/simplifier.cpp

@@ -18,6 +18,7 @@
 #include "library/simplifier/ceqv.h"
 #include "library/app_builder.h"
 #include "library/num.h"
+#include "library/norm_num.h"
 #include "util/flet.h"
 #include "util/pair.h"
 #include "util/sexpr/option_declarations.h"
@@ -48,6 +49,9 @@
 #ifndef LEAN_DEFAULT_SIMPLIFY_FUSE
 #define LEAN_DEFAULT_SIMPLIFY_FUSE false
 #endif
+#ifndef LEAN_DEFAULT_SIMPLIFY_NUMERALS
+#define LEAN_DEFAULT_SIMPLIFY_NUMERALS true
+#endif
 
 namespace lean {
 namespace blast {
@@ -71,6 +75,7 @@ static name * g_simplify_contextual    = nullptr;
 static name * g_simplify_expand_macros = nullptr;
 static name * g_simplify_trace         = nullptr;
 static name * g_simplify_fuse          = nullptr;
+static name * g_simplify_numerals      = nullptr;
 
 unsigned get_simplify_max_steps() {
     return ios().get_options().get_unsigned(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS);
@@ -104,6 +109,10 @@ bool get_simplify_fuse() {
     return ios().get_options().get_bool(*g_simplify_fuse, LEAN_DEFAULT_SIMPLIFY_FUSE);
 }
 
+bool get_simplify_numerals() {
+    return ios().get_options().get_bool(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS);
+}
+
 /* Miscellaneous helpers */
 
 static bool is_add_app(expr const & e) {
@@ -141,6 +150,7 @@ class simplifier {
     bool                                         m_expand_macros{get_simplify_expand_macros()};
     bool                                         m_trace{get_simplify_trace()};
     bool                                         m_fuse{get_simplify_fuse()};
+    bool                                         m_numerals{get_simplify_numerals()};
 
     /* Cache */
     struct key {
@@ -205,6 +215,7 @@ class simplifier {
     result simplify_pi(expr const & e);
     result simplify_app(expr const & e);
     result simplify_fun(expr const & e);
+    optional<result> simplify_numeral(expr const & e);
 
     /* Proving */
     optional<expr> prove(expr const & thm);
@@ -364,6 +375,11 @@ result simplifier::simplify(expr const & e, bool is_root) {
         if (auto it = cache_lookup(e)) return *it;
     }
 
+    if (m_numerals) {
+        // TODO(dhs): cache these?
+        if (auto r = simplify_numeral(e)) return *r;
+    }
+
     result r(e);
 
     if (m_top_down) r = join(r, rewrite(whnf(r.get_new())));
@@ -501,6 +517,22 @@ result simplifier::simplify_fun(expr const & e) {
     return congr_funs(r_f, args);
 }
 
+optional<result> simplifier::simplify_numeral(expr const & e) {
+    if (is_num(e)) {
+        return optional<result>(result(e));
+    }
+    else if (is_add_app(e) || is_mul_app(e)) {
+        buffer<expr> args;
+        get_app_args(e, args);
+        if (is_num(args[2]) && is_num(args[3])){
+            expr_pair r = mk_norm_num(*m_tmp_tctx, e);
+            return optional<result>(result(r.first, r.second));
+        }
+    }
+    // TODO(dhs): simplify division and substraction as well
+    return optional<result>();
+}
+
 /* Proving */
 
 optional<expr> simplifier::prove(expr const & thm) {
@@ -984,6 +1016,7 @@ void initialize_simplifier() {
     g_simplify_expand_macros = new name{"simplify", "expand_macros"};
     g_simplify_trace         = new name{"simplify", "trace"};
     g_simplify_fuse          = new name{"simplify", "fuse"};
+    g_simplify_numerals      = new name{"simplify", "numerals"};
 
     register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS,
                              "(simplify) max allowed steps in simplification");
@@ -1001,9 +1034,12 @@ void initialize_simplifier() {
                          "(simplify) trace");
     register_bool_option(*g_simplify_fuse, LEAN_DEFAULT_SIMPLIFY_FUSE,
                          "(simplify) fuse addition in distrib structures");
+    register_bool_option(*g_simplify_numerals, LEAN_DEFAULT_SIMPLIFY_NUMERALS,
+                         "(simplify) simplify (+, *, -, /) over numerals");
 }
 
 void finalize_simplifier() {
+    delete g_simplify_numerals;
     delete g_simplify_fuse;
     delete g_simplify_trace;
     delete g_simplify_expand_macros;

src/library/norm_num.cpp

@@ -126,7 +126,7 @@ expr norm_num_context::mk_has_add(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -141,7 +141,7 @@ expr norm_num_context::mk_has_mul(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -156,7 +156,7 @@ expr norm_num_context::mk_has_one(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -171,7 +171,7 @@ expr norm_num_context::mk_has_zero(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -186,7 +186,7 @@ expr norm_num_context::mk_add_monoid(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -201,7 +201,7 @@ expr norm_num_context::mk_monoid(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -212,7 +212,7 @@ expr norm_num_context::mk_monoid(expr const & e) {
 
 expr norm_num_context::mk_field(expr const & e) {
     expr t = mk_app(mk_constant(*g_field, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         return *inst;
     } else {
@@ -226,7 +226,7 @@ expr norm_num_context::mk_add_comm(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -241,7 +241,7 @@ expr norm_num_context::mk_add_group(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -256,7 +256,7 @@ expr norm_num_context::mk_has_distrib(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -271,7 +271,7 @@ expr norm_num_context::mk_mul_zero_class(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -286,7 +286,7 @@ expr norm_num_context::mk_semiring(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -301,7 +301,7 @@ expr norm_num_context::mk_has_neg(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -316,7 +316,7 @@ expr norm_num_context::mk_has_sub(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -331,7 +331,7 @@ expr norm_num_context::mk_has_div(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -346,7 +346,7 @@ expr norm_num_context::mk_add_comm_group(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -361,7 +361,7 @@ expr norm_num_context::mk_ring(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -376,7 +376,7 @@ expr norm_num_context::mk_lin_ord_ring(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -391,7 +391,7 @@ expr norm_num_context::mk_lin_ord_semiring(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;
@@ -406,7 +406,7 @@ expr norm_num_context::mk_wk_order(expr const & e) {
         return instances[l_name];
     }
     expr t = mk_app(mk_constant(l_name, m_lvls), e);
-    optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
+    optional<expr> inst = m_type_ctx.mk_class_instance(t);
     if (inst) {
         instances[l_name] = *inst;
         return *inst;

src/library/norm_num.h

@@ -5,7 +5,7 @@ Author: Robert Y. Lewis
 */
 #pragma once
 #include "kernel/environment.h"
-#include "library/local_context.h"
+#include "library/type_context.h"
 #include "library/num.h"
 #include "library/class_instance_resolution.h"
 #include "util/numerics/mpq.h"
@@ -21,8 +21,7 @@ struct hash_name {
 };
 
 class norm_num_context {
-    environment   m_env;
+    type_context & m_type_ctx;
-    local_context m_ctx;
     levels m_lvls;
     pair<expr, expr> mk_norm_add(expr const &, expr const &);
     pair<expr, expr> mk_norm_add1(expr const &);
@@ -72,7 +71,7 @@ class norm_num_context {
     std::unordered_map<name, expr, hash_name> instances;
 
 public:
-    norm_num_context(environment const & env, local_context const & ctx):m_env(env), m_ctx(ctx) {}
+    norm_num_context(type_context & type_ctx): m_type_ctx(type_ctx) {}
 
     bool is_numeral(expr const & e) const;
     bool is_neg_app(expr const &) const;
@@ -89,20 +88,20 @@ public:
 
 inline bool is_neg(expr const & e);
 
-inline bool is_numeral(environment const & env, expr const & e) {
+inline bool is_numeral(type_context & type_ctx, expr const & e) {
-    return norm_num_context(env, local_context()).is_numeral(e);
+    return norm_num_context(type_ctx).is_numeral(e);
 }
 
-inline pair<expr, expr> mk_norm_num(environment const & env, local_context const & ctx, expr const & e) {
+inline pair<expr, expr> mk_norm_num(type_context & type_ctx, expr const & e) {
-    return norm_num_context(env, ctx).mk_norm(e);
+    return norm_num_context(type_ctx).mk_norm(e);
 }
 
-inline mpz num_of_expr(environment const & env, local_context const & ctx, expr const & e) {
+inline mpz num_of_expr(type_context & type_ctx, expr const & e) {
-    return norm_num_context(env, ctx).num_of_expr(e);
+    return norm_num_context(type_ctx).num_of_expr(e);
 }
 
-inline mpq mpq_of_expr(environment const & env, local_context const & ctx, expr const & e) {
+inline mpq mpq_of_expr(type_context & type_ctx, expr const & e) {
-    return norm_num_context(env, ctx).mpq_of_expr(e);
+    return norm_num_context(type_ctx).mpq_of_expr(e);
 }
 
 void initialize_norm_num();

src/library/tactic/CMakeLists.txt

@@ -6,5 +6,4 @@ expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp
 init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp
 contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp
 injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp
-induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp
+induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp)
-norm_num_tactic.cpp)

src/library/tactic/init_module.cpp

@@ -32,7 +32,6 @@ Author: Leonardo de Moura
 #include "library/tactic/subst_tactic.h"
 #include "library/tactic/location.h"
 #include "library/tactic/with_options_tactic.h"
-#include "library/tactic/norm_num_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -63,11 +62,9 @@ void initialize_tactic_module() {
     initialize_subst_tactic();
     initialize_location();
     initialize_with_options_tactic();
-    initialize_norm_num_tactic();
 }
 
 void finalize_tactic_module() {
-    finalize_norm_num_tactic();
     finalize_with_options_tactic();
     finalize_location();
     finalize_subst_tactic();