feat(frontends/lean): hide builtin object in the 'Show Environment' command

The user can still display builtin objects by using

    Show Environment all

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

src/frontends/lean/frontend.cpp

@@ -26,15 +26,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/pp.h"
 
 namespace lean {
-/**
-   \brief Import all definitions and notation.
-*/
-void init_frontend(environment const & env, io_state & ios) {
-    ios.set_formatter(mk_pp_formatter(env));
-    import_all(env);
-    init_builtin_notation(env, ios);
-}
-
 static std::vector<bool> g_empty_vector;
 /**
    \brief Environment extension object for the Lean default frontend.
@@ -60,6 +51,19 @@ struct lean_extension : public environment_extension {
     coercion_map          m_coercion_map; // mapping from (given_type, expected_type) -> coercion
     coercion_set          m_coercion_set; // Set of coercions
     expr_to_coercions     m_type_coercions; // mapping type -> list (to-type, function)
+    unsigned              m_initial_size; // size of the environment after init_frontend was invoked
+
+    lean_extension() {
+        m_initial_size = 0;
+    }
+
+    void set_initial_size(unsigned sz) {
+        m_initial_size = sz;
+    }
+
+    unsigned get_initial_size() const {
+        return m_initial_size;
+    }
 
     lean_extension const * get_parent() const {
         return environment_extension::get_parent<lean_extension>();
@@ -441,6 +445,20 @@ static lean_extension & to_ext(environment const & env) {
     return env->get_extension<lean_extension>(g_lean_extension_initializer.m_extid);
 }
 
+/**
+   \brief Import all definitions and notation.
+*/
+void init_frontend(environment const & env, io_state & ios) {
+    ios.set_formatter(mk_pp_formatter(env));
+    import_all(env);
+    init_builtin_notation(env, ios);
+    to_ext(env).set_initial_size(env->get_num_objects(false));
+}
+
+unsigned get_initial_size(ro_environment const & env) {
+    return to_ext(env).get_initial_size();
+}
+
 void add_infix(environment const & env, io_state const & ios, name const & opn, unsigned p, expr const & d)  {
     to_ext(env).add_op(infix(opn, p), d, true, env, ios);
 }

src/frontends/lean/frontend.h

@@ -18,6 +18,12 @@ namespace lean {
 */
 void init_frontend(environment const & env, io_state & ios);
 
+/**
+   \brief Return the environment size after init_frontend invocation.
+   Return 0 if \c init_frontend was not invoked for this environment.
+*/
+unsigned get_initial_size(ro_environment const & env);
+
 /**
    @name Notation for parsing and pretty printing.
 */

src/frontends/lean/parser.cpp

@@ -1797,6 +1797,7 @@ class parser::imp {
     /** \brief Parse
            'Show' expr
            'Show' Environment [num]
+           'Show' Environment all
            'Show' Options
     */
     void parse_show() {
@@ -1805,23 +1806,28 @@ class parser::imp {
             name opt_id = curr_name();
             next();
             if (opt_id == g_env_kwd) {
+                unsigned beg = get_initial_size(m_env);
+                unsigned end = m_env->get_num_objects(false);
                 unsigned i;
                 if (curr_is_nat()) {
-                    i = parse_unsigned("invalid argument, value does not fit in a machine integer");
+                    i   = parse_unsigned("invalid argument, value does not fit in a machine integer");
+                } else if (curr_is_identifier() && curr_name() == "all") {
+                    next();
+                    i   = std::numeric_limits<unsigned>::max();
+                    beg = 0;
                 } else {
                     i = std::numeric_limits<unsigned>::max();
                 }
-                auto end = m_env->end_objects();
+                unsigned it  = end;
-                auto beg = m_env->begin_objects();
-                auto it  = end;
                 while (it != beg && i != 0) {
                     --it;
-                    if (!is_hidden_object(*it))
+                    if (!is_hidden_object(m_env->get_object(it, false)))
                         --i;
                 }
                 for (; it != end; ++it) {
-                    if (!is_hidden_object(*it))
+                    auto obj = m_env->get_object(it, false);
-                        regular(m_io_state) << *it << endl;
+                    if (!is_hidden_object(obj))
+                        regular(m_io_state) << obj << endl;
                 }
             } else if (opt_id == g_options_kwd) {
                 regular(m_io_state) << pp(m_io_state.get_options()) << endl;

tests/lean/elab4.lean.expected.out

@@ -5,9 +5,6 @@
   Assumed: R
   Proved: R2
   Set: lean::pp::implicit
-Coercion int_to_real
-Coercion nat_to_real
-Definition SubstP : Π (A : Type U) (a b : A) (P : A → Bool), P a → a == b → P b := Subst::explicit
 Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B
 Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) :
     eq::explicit Type A A'

tests/lean/elab5.lean.expected.out

@@ -5,9 +5,6 @@
   Assumed: R
   Proved: R2
   Set: lean::pp::implicit
-Coercion int_to_real
-Coercion nat_to_real
-Definition SubstP : Π (A : Type U) (a b : A) (P : A → Bool), P a → a == b → P b := Subst::explicit
 Variable C {A B : Type} (H : eq::explicit Type A B) (a : A) : B
 Variable D {A A' : Type} {B : A → Type} {B' : A' → Type} (H : eq::explicit Type (Π x : A, B x) (Π x : A', B' x)) :
     eq::explicit Type A A'