feat(frontends/lean): add commands 'add_key_equivalence' and 'print key_equivalences'

src/emacs/lean-syntax.el

@@ -13,7 +13,7 @@
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises" "theory"
     "print" "theorem" "proposition" "example" "abbreviation" "abstract"
     "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
-    "alias" "help" "precedence" "reserve" "declare_trace"
+    "alias" "help" "precedence" "reserve" "declare_trace" "add_key_equivalence"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"
     "eval" "vm_eval" "check" "end" "reveal" "this" "suppose"
     "using" "namespace" "section" "fields" "find_decl"

src/frontends/lean/builtin_cmds.cpp

@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/legacy_type_context.h"
 #include "library/reducible.h"
+#include "library/kabstract.h"
 #include "library/tactic/defeq_simplifier/defeq_simp_lemmas.h"
 #include "library/tactic/defeq_simplifier/defeq_simplifier.h"
 #include "library/tactic/simplifier/simp_extensions.h"
@@ -681,6 +682,12 @@ static void declare_trace_reader(deserializer & d, shared_environment &,
     register_trace_class(cls);
 }
 
+environment add_key_equivalence_cmd(parser & p) {
+    name h1 = p.check_constant_next("invalid add_key_equivalence command, constant expected");
+    name h2 = p.check_constant_next("invalid add_key_equivalence command, constant expected");
+    return add_key_equivalence(p.env(), h1, h2);
+}
+
 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));
@@ -704,6 +711,7 @@ void init_cmd_table(cmd_table & r) {
     add_cmd(r, cmd_info("init_hits",         "initialize builtin HITs", init_hits_cmd));
     add_cmd(r, cmd_info("declare_trace",     "declare a new trace class (for debugging Lean tactics)", declare_trace_cmd));
     add_cmd(r, cmd_info("register_simp_ext", "register simplifier extension", register_simp_ext_cmd));
+    add_cmd(r, cmd_info("add_key_equivalence", "register that to symbols are equivalence for key-matching", add_key_equivalence_cmd));
     add_cmd(r, cmd_info("#erase_cache",      "erase cached definition (for debugging purposes)", erase_cache_cmd));
     add_cmd(r, cmd_info("#normalizer",       "(for debugging purposes)", normalizer_cmd));
     add_cmd(r, cmd_info("#unify",            "(for debugging purposes)", unify_cmd));

src/frontends/lean/print_cmd.cpp

@@ -32,6 +32,7 @@ Author: Leonardo de Moura
 #include "library/tactic/simplifier/simp_lemmas.h"
 #include "library/tactic/simplifier/simp_extensions.h"
 #include "library/reducible.h"
+#include "library/kabstract.h"
 #include "library/definitional/projection.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
@@ -649,6 +650,18 @@ static void print_aliases(parser const & p) {
         });
 }
 
+static void print_key_equivalences(parser & p) {
+    std::ostream & out = p.ios().get_regular_stream();
+    for_each_key_equivalence(p.env(), [&](buffer<name> const & ns) {
+            out << "[";
+            for (unsigned i = 0; i < ns.size(); i++) {
+                if (i > 0) out << ", ";
+                out << ns[i];
+            }
+            out << "]\n";
+        });
+}
+
 environment print_cmd(parser & p) {
     flycheck_information info(p.ios());
     environment const & env = p.env();
@@ -682,6 +695,9 @@ environment print_cmd(parser & p) {
     } else if (p.curr_is_token_or_id(get_trust_tk())) {
         p.next();
         out << "trust level: " << p.env().trust_lvl() << endl;
+    } else if (p.curr_is_token_or_id(get_key_equivalences_tk())) {
+        p.next();
+        print_key_equivalences(p);
     } else if (p.curr_is_token_or_id(get_definition_tk())) {
         p.next();
         auto pos = p.pos();

src/frontends/lean/token_table.cpp

@@ -118,7 +118,8 @@ void init_token_table(token_table & t) {
          "exit", "set_option", "open", "export", "override", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent", "inline",
-         "include", "omit", "migrate", "init_quotient", "init_hits", "declare_trace", "register_simp_ext", "#erase_cache",
+         "include", "omit", "migrate", "init_quotient", "init_hits", "declare_trace", "register_simp_ext",
+         "add_key_equivalence", "#erase_cache",
          "#compile", "#normalizer", "#unify", "#elab", nullptr};
 
     pair<char const *, char const *> aliases[] =

src/frontends/lean/tokens.cpp

@@ -145,6 +145,7 @@ static name const * g_inductive_tk = nullptr;
 static name const * g_this_tk = nullptr;
 static name const * g_noncomputable_tk = nullptr;
 static name const * g_theory_tk = nullptr;
+static name const * g_key_equivalences_tk = nullptr;
 void initialize_tokens() {
     g_aliases_tk = new name{"aliases"};
     g_period_tk = new name{"."};
@@ -288,6 +289,7 @@ void initialize_tokens() {
     g_this_tk = new name{"this"};
     g_noncomputable_tk = new name{"noncomputable"};
     g_theory_tk = new name{"theory"};
+    g_key_equivalences_tk = new name{"key_equivalences"};
 }
 void finalize_tokens() {
     delete g_aliases_tk;
@@ -432,6 +434,7 @@ void finalize_tokens() {
     delete g_this_tk;
     delete g_noncomputable_tk;
     delete g_theory_tk;
+    delete g_key_equivalences_tk;
 }
 name const & get_aliases_tk() { return *g_aliases_tk; }
 name const & get_period_tk() { return *g_period_tk; }
@@ -575,4 +578,5 @@ name const & get_inductive_tk() { return *g_inductive_tk; }
 name const & get_this_tk() { return *g_this_tk; }
 name const & get_noncomputable_tk() { return *g_noncomputable_tk; }
 name const & get_theory_tk() { return *g_theory_tk; }
+name const & get_key_equivalences_tk() { return *g_key_equivalences_tk; }
 }

src/frontends/lean/tokens.h

@@ -147,4 +147,5 @@ name const & get_inductive_tk();
 name const & get_this_tk();
 name const & get_noncomputable_tk();
 name const & get_theory_tk();
+name const & get_key_equivalences_tk();
 }

src/frontends/lean/tokens.txt

@@ -140,3 +140,4 @@ inductive    inductive
 this         this
 noncomputable noncomputable
 theory       theory
+key_equivalences key_equivalences

tests/lean/key_eqv1.lean

@@ -0,0 +1,4 @@
+add_key_equivalence add nat.add
+add_key_equivalence nat.add nat.succ
+add_key_equivalence mul nat.mul
+print key_equivalences

tests/lean/key_eqv1.lean.expected.out

@@ -0,0 +1,2 @@
+[nat.succ, add, nat.add]
+[nat.mul, mul]