feat(library/tactic): start algebraic normalizer

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)

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

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)

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<data>();
+        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;
+}
+}

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 <memory>
+#include "library/type_context.h"
+#include "library/head_map.h"
+
+namespace lean {
+struct algebraic_info {
+    struct lr_info {
+        optional<expr> m_left_proof;
+        optional<expr> 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<expr>           m_comm;
+    optional<expr>           m_assoc;
+    optional<expr>           m_idempotent;
+    optional<lr_info>        m_cancel;
+    optional<lr_elem_info>   m_id;
+    optional<lr_elem_info>   m_null;
+    optional<lr_op_info>     m_distrib;
+    optional<inv_info>       m_left_inv;
+    optional<inv_info>       m_right_inv;
+    optional<cond_inv_info>  m_cond_left_inv;
+    optional<cond_inv_info>  m_cond_right_inv;
+};
+
+typedef std::shared_ptr<algebraic_info const> algebraic_info_ref;
+
+class algebraic_info_manager {
+public:
+    struct data {
+        environment                              m_env;
+        local_context                            m_lctx;
+        name_set                                 m_symbols;
+        head_map<pair<expr, algebraic_info_ref>> m_head_info;
+        expr_map<algebraic_info_ref>             m_op_info;
+    };
+    typedef std::shared_ptr<data>                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();
+}

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

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