From 0091cef9f28e2c1f333d025d18636ccccd980dc7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 15 May 2017 21:34:05 -0700 Subject: [PATCH] feat(library/tactic): start algebraic normalizer --- library/init/meta/simp_tactic.lean | 5 ++ src/library/class.cpp | 5 +- src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/algebraic_normalizer.cpp | 73 +++++++++++++++++++ src/library/tactic/algebraic_normalizer.h | 77 +++++++++++++++++++++ src/library/tactic/init_module.cpp | 3 + tests/lean/run/alg_info1.lean | 8 +++ 7 files changed, 168 insertions(+), 5 deletions(-) create mode 100644 src/library/tactic/algebraic_normalizer.cpp create mode 100644 src/library/tactic/algebraic_normalizer.h create mode 100644 tests/lean/run/alg_info1.lean diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 5e381451b4..074aa4def5 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -435,6 +435,11 @@ meta def simp_bottom_up (post : expr → tactic (expr × expr)) (cfg : simp_conf do t ← target, (_, new_target, pr) ← simplify_bottom_up () (λ _ e, do (new_e, pr) ← post e, return ((), new_e, pr)) t cfg, replace_target new_target pr + +/- debugging support for algebraic normalizer -/ + +meta constant trace_algebra_info : expr → tactic unit + end tactic export tactic (mk_simp_attr) diff --git a/src/library/class.cpp b/src/library/class.cpp index d1e9147eed..db3b9ddf3c 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -368,7 +368,7 @@ void initialize_class() { [](environment const & env, io_state const &, name const & d, unsigned, bool persistent) { return add_class_core(env, d, persistent); - })); + })); register_system_attribute(basic_attribute(*g_instance_attr_name, "type class instance", [](environment const & env, io_state const &, name const & d, @@ -376,9 +376,6 @@ void initialize_class() { return add_instance_core(env, d, prio, persistent); })); - /* TODO(Leo): move to a different file */ - register_class_symbol_tracking_attribute("algebra", "mark class whose instances are relevant for the algebraic normalizer"); - g_anonymous_inst_name_prefix = new name("_inst"); } diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 904616e4b0..cea150df79 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -9,4 +9,4 @@ add_library(tactic OBJECT occurrences.cpp kabstract.cpp tactic_state.cpp simp_result.cpp user_attribute.cpp eval.cpp simp_lemmas.cpp eqn_lemmas.cpp dsimplify.cpp simplify.cpp vm_monitor.cpp destruct_tactic.cpp norm_num_tactic.cpp - elaborator_exception.cpp) + elaborator_exception.cpp algebraic_normalizer.cpp) diff --git a/src/library/tactic/algebraic_normalizer.cpp b/src/library/tactic/algebraic_normalizer.cpp new file mode 100644 index 0000000000..c5f7bd6952 --- /dev/null +++ b/src/library/tactic/algebraic_normalizer.cpp @@ -0,0 +1,73 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/class.h" +#include "library/trace.h" +#include "library/tactic/tactic_state.h" +#include "library/tactic/algebraic_normalizer.h" + +namespace lean { +static name * g_algebra = nullptr; + +MK_THREAD_LOCAL_GET_DEF(algebraic_info_manager::data_ptr, get_alg_info_data); + +algebraic_info_manager::algebraic_info_manager(type_context & ctx): + m_ctx(ctx) { + data_ptr p = get_alg_info_data(); + if (p && + is_eqp(ctx.env(), p->m_env) && + is_decl_eqp(ctx.lctx(), p->m_lctx)) { + m_data = p; + } else { + m_data = std::make_shared(); + m_data->m_env = ctx.env(); + m_data->m_lctx = ctx.lctx(); + m_data->m_symbols = get_class_attribute_symbols(ctx.env(), *g_algebra); + } +} + +algebraic_info_manager::~algebraic_info_manager() { + get_alg_info_data() = m_data; +} + +algebraic_info_ref algebraic_info_manager::get_info(expr const & op) { + expr const & fn = get_app_fn(op); + if (!is_constant(fn)) + return algebraic_info_ref(nullptr); + if (!m_data->m_symbols.contains(const_name(fn))) + return algebraic_info_ref(nullptr); + auto it = m_data->m_op_info.find(op); + if (it != m_data->m_op_info.end()) + return it->second; + // TODO(Leo): + return algebraic_info_ref(nullptr); +} + +vm_obj tactic_trace_algebra_info(vm_obj const & op, vm_obj const & _s) { + tactic_state const & s = tactic::to_state(_s); + type_context ctx = mk_type_context_for(s); + algebraic_info_manager m(ctx); + if (m.get_info(to_expr(op))) { + tout() << "operator has algebraic info\n"; + } else { + tout() << "operator does not have algebraic info\n"; + } + return tactic::mk_success(mk_vm_unit(), s); +} + +void initialize_algebraic_normalizer() { + register_trace_class("algebra"); + + g_algebra = new name("algebra"); + register_class_symbol_tracking_attribute(*g_algebra, "mark class whose instances are relevant for txhe algebraic normalizer"); + + DECLARE_VM_BUILTIN(name({"tactic", "trace_algebra_info"}), tactic_trace_algebra_info); +} + +void finalize_algebraic_normalizer() { + delete g_algebra; +} +} diff --git a/src/library/tactic/algebraic_normalizer.h b/src/library/tactic/algebraic_normalizer.h new file mode 100644 index 0000000000..3d96e87beb --- /dev/null +++ b/src/library/tactic/algebraic_normalizer.h @@ -0,0 +1,77 @@ +/* +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "library/type_context.h" +#include "library/head_map.h" + +namespace lean { +struct algebraic_info { + struct lr_info { + optional m_left_proof; + optional m_right_proof; + }; + + struct lr_op_info : public lr_info { + expr m_op; + }; + + struct lr_elem_info : public lr_info { + expr m_elem; + }; + + struct inv_info { + expr m_inv; + expr m_o; + expr m_proof; + }; + + struct cond_inv_info : public inv_info { + expr m_p; + }; + + expr m_op; + optional m_comm; + optional m_assoc; + optional m_idempotent; + optional m_cancel; + optional m_id; + optional m_null; + optional m_distrib; + optional m_left_inv; + optional m_right_inv; + optional m_cond_left_inv; + optional m_cond_right_inv; +}; + +typedef std::shared_ptr algebraic_info_ref; + +class algebraic_info_manager { +public: + struct data { + environment m_env; + local_context m_lctx; + name_set m_symbols; + head_map> m_head_info; + expr_map m_op_info; + }; + typedef std::shared_ptr data_ptr; + +private: + type_context & m_ctx; + data_ptr m_data; + +public: + algebraic_info_manager(type_context & ctx); + ~algebraic_info_manager(); + type_context & ctx() const { return m_ctx; } + algebraic_info_ref get_info(expr const & op); +}; + +void initialize_algebraic_normalizer(); +void finalize_algebraic_normalizer(); +} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index b3c7b44a82..a106eff9db 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -34,6 +34,7 @@ Author: Leonardo de Moura #include "library/tactic/vm_monitor.h" #include "library/tactic/norm_num_tactic.h" #include "library/tactic/destruct_tactic.h" +#include "library/tactic/algebraic_normalizer.h" #include "library/tactic/backward/init_module.h" #include "library/tactic/smt/init_module.h" @@ -70,10 +71,12 @@ void initialize_tactic_module() { initialize_norm_num_tactic(); initialize_vm_monitor(); initialize_destruct_tactic(); + initialize_algebraic_normalizer(); initialize_smt_module(); } void finalize_tactic_module() { finalize_smt_module(); + finalize_algebraic_normalizer(); finalize_destruct_tactic(); finalize_vm_monitor(); finalize_norm_num_tactic(); diff --git a/tests/lean/run/alg_info1.lean b/tests/lean/run/alg_info1.lean new file mode 100644 index 0000000000..9122885bd7 --- /dev/null +++ b/tests/lean/run/alg_info1.lean @@ -0,0 +1,8 @@ +open tactic + +example : true := +by do + let op : expr := `((+) : nat → nat → nat), + trace op, + trace_algebra_info op, + constructor