feat(frontends/lean): add '#erase_cache' command (for debugging purposes)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/builtin_cmds.cpp

@@ -287,6 +287,12 @@ environment opaque_hint_cmd(parser & p) {
     return env;
 }
 
+environment erase_cache_cmd(parser & p) {
+    name n = p.check_id_next("invalid #erase_cache command, identifier expected");
+    p.erase_cached_definition(n);
+    return p.env();
+}
+
 cmd_table init_cmd_table() {
     cmd_table r;
     add_cmd(r, cmd_info("using",        "create aliases for declarations, and use objects defined in other namespaces", using_cmd));
@@ -299,6 +305,7 @@ cmd_table init_cmd_table() {
     add_cmd(r, cmd_info("check",        "type check given expression, and display its type", check_cmd));
     add_cmd(r, cmd_info("coercion",     "add a new coercion", coercion_cmd));
     add_cmd(r, cmd_info("opaque_hint",  "add hints for the elaborator/unifier", opaque_hint_cmd));
+    add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd));
 
     register_decl_cmds(r);
     register_inductive_cmd(r);

src/frontends/lean/parser.h

@@ -176,6 +176,7 @@ public:
                           level_param_names const & ls, expr const & type, expr const & value);
     /** \brief Try to find an elaborated definition for (n, pre_type, pre_value) in the cache */
     optional<std::tuple<level_param_names, expr, expr>> find_cached_definition(name const & n, expr const & pre_type, expr const & pre_value);
+    void erase_cached_definition(name const & n) { if (m_cache) m_cache->erase(n); }
 
     environment const & env() const { return m_env; }
     io_state const & ios() const { return m_ios; }

src/frontends/lean/token_table.cpp

@@ -78,7 +78,7 @@ token_table init_token_table() {
                                "abbreviation", "inductive", "record", "renaming", "extends", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
                                "exit", "set_option", "using", "calc_subst", "calc_refl", "calc_trans", "tactic_hint",
-                               "add_proof_qed", "set_proof_qed", "instance", nullptr};
+                               "add_proof_qed", "set_proof_qed", "instance", "#erase_cache", nullptr};
 
     std::pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

src/library/definitions_cache.h

@@ -34,5 +34,7 @@ public:
     void save(std::ostream & out);
     /** \brief Load the cache content from the given stream */
     void load(std::istream & in);
+    /** \brief Remove the entry named \c n from the cache. */
+    void erase(name const & n) { m_definitions.erase(n); }
 };
 }