From 550cac60651d25d6e48481c6a0b160cfce024c1a Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Mon, 16 Nov 2015 14:09:34 -0800 Subject: [PATCH] feat(library/norm_num): use type_context --- src/library/blast/simplifier.cpp | 36 +++++++++++++++++++++++++++ src/library/norm_num.cpp | 40 +++++++++++++++--------------- src/library/norm_num.h | 25 +++++++++---------- src/library/tactic/CMakeLists.txt | 3 +-- src/library/tactic/init_module.cpp | 3 --- 5 files changed, 69 insertions(+), 38 deletions(-) diff --git a/src/library/blast/simplifier.cpp b/src/library/blast/simplifier.cpp index a661d32bf..7577f2bbe 100644 --- a/src/library/blast/simplifier.cpp +++ b/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 simplify_numeral(expr const & e); /* Proving */ optional 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 simplifier::simplify_numeral(expr const & e) { + if (is_num(e)) { + return optional(result(e)); + } + else if (is_add_app(e) || is_mul_app(e)) { + buffer 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(r.first, r.second)); + } + } + // TODO(dhs): simplify division and substraction as well + return optional(); +} + /* Proving */ optional 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; diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp index 9d3dcb851..2a7618dd1 100644 --- a/src/library/norm_num.cpp +++ b/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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional 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 inst = mk_class_instance(m_env, m_ctx, t); + optional inst = m_type_ctx.mk_class_instance(t); if (inst) { instances[l_name] = *inst; return *inst; diff --git a/src/library/norm_num.h b/src/library/norm_num.h index a6ca10460..94e75ffec 100644 --- a/src/library/norm_num.h +++ b/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,9 +21,8 @@ struct hash_name { }; class norm_num_context { - environment m_env; - local_context m_ctx; - levels m_lvls; + type_context & m_type_ctx; + levels m_lvls; pair mk_norm_add(expr const &, expr const &); pair mk_norm_add1(expr const &); pair mk_norm_mul(expr const &, expr const &); @@ -72,7 +71,7 @@ class norm_num_context { std::unordered_map 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) { - return norm_num_context(env, local_context()).is_numeral(e); +inline bool is_numeral(type_context & type_ctx, expr const & e) { + return norm_num_context(type_ctx).is_numeral(e); } -inline pair mk_norm_num(environment const & env, local_context const & ctx, expr const & e) { - return norm_num_context(env, ctx).mk_norm(e); +inline pair mk_norm_num(type_context & type_ctx, expr const & 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) { - return norm_num_context(env, ctx).num_of_expr(e); +inline mpz num_of_expr(type_context & type_ctx, expr const & 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) { - return norm_num_context(env, ctx).mpq_of_expr(e); +inline mpq mpq_of_expr(type_context & type_ctx, expr const & e) { + return norm_num_context(type_ctx).mpq_of_expr(e); } void initialize_norm_num(); diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 469fe60de..f701a25a3 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/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 -norm_num_tactic.cpp) +induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp) \ No newline at end of file diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 1ad835195..76c457dd7 100644 --- a/src/library/tactic/init_module.cpp +++ b/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();