Expose environment API in the frontend object. Add support for formatting objects.

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

src/exprlib/formatter.cpp

@@ -24,6 +24,9 @@ public:
         s << mk_pair(e,c);
         return format(s.str());
     }
+    virtual format operator()(object const & obj) {
+        std::ostringstream s; s << obj; return format(s.str());
+    }
     virtual format operator()(environment const & env) {
         std::ostringstream s; s << env; return format(s.str());
     }

src/exprlib/formatter.h

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 class environment;
+class object;
 /**
    \brief API for formatting expressions, contexts and environments.
 */
@@ -28,6 +29,8 @@ public:
         for the free variables
     */
     virtual format operator()(context const & c, expr const & e, bool format_ctx = false) = 0;
+    /** \brief Format the given object */
+    virtual format operator()(object const & obj) = 0;
     /** \brief Format the given environment */
     virtual format operator()(environment const & env) = 0;
 };

src/exprlib/printer.cpp

@@ -151,23 +151,24 @@ std::ostream & operator<<(std::ostream & out, context const & ctx) {
     return out;
 }
 
+std::ostream & operator<<(std::ostream & out, object const & obj) {
+    out << obj.keyword() << " ";
+    switch (obj.kind()) {
+    case object_kind::UVarDeclaration:
+        out << obj.get_name() << " >= " << obj.get_cnstr_level(); break;
+    case object_kind::Postulate:
+        out << obj.get_name() << " : " << obj.get_type(); break;
+    case object_kind::Definition:
+        out << obj.get_name() << " : " << obj.get_type() << " :=\n    " << obj.get_value(); break;
+    case object_kind::Neutral:
+        break;
+    }
+}
+
 std::ostream & operator<<(std::ostream & out, environment const & env) {
     std::for_each(env.begin_objects(),
                   env.end_objects(),
-                  [&](object const & obj) {
+                  [&](object const & obj) { out << obj << "\n"; });
-                      out << obj.keyword() << " ";
-                      switch (obj.kind()) {
-                      case object_kind::UVarDeclaration:
-                          out << obj.get_name() << " >= " << obj.get_cnstr_level(); break;
-                      case object_kind::Postulate:
-                          out << obj.get_name() << " : " << obj.get_type(); break;
-                      case object_kind::Definition:
-                          out << obj.get_name() << " : " << obj.get_type() << " :=\n    " << obj.get_value(); break;
-                      case object_kind::Neutral:
-                          break;
-                      }
-                      out << "\n";
-                  });
     return out;
 }
 }

src/exprlib/printer.h

@@ -13,6 +13,8 @@ namespace lean {
 std::ostream & operator<<(std::ostream & out, context const & ctx);
 std::ostream & operator<<(std::ostream & out, expr const & e);
 std::ostream & operator<<(std::ostream & out, std::pair<expr const &, context const &> const & p);
+class object;
+std::ostream & operator<<(std::ostream & out, object const & obj);
 class environment;
 std::ostream & operator<<(std::ostream & out, environment const & env);
 }

src/frontend/frontend.cpp

@@ -195,6 +195,17 @@ level frontend::add_uvar(name const & n, level const & l) { return m_imp->m_env.
 level frontend::add_uvar(name const & n) { return m_imp->m_env.add_uvar(n); }
 level frontend::get_uvar(name const & n) const { return m_imp->m_env.get_uvar(n); }
 
+void frontend::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
+    return m_imp->m_env.add_definition(n, t, v, opaque);
+}
+void frontend::add_theorem(name const & n, expr const & t, expr const & v) { return m_imp->m_env.add_theorem(n, t, v); }
+void frontend::add_definition(name const & n, expr const & v, bool opaque) { return m_imp->m_env.add_definition(n, v, opaque); }
+void frontend::add_axiom(name const & n, expr const & t) { return m_imp->m_env.add_axiom(n, t); }
+void frontend::add_var(name const & n, expr const & t) { return m_imp->m_env.add_var(n, t); }
+object const & frontend::get_object(name const & n) const { return m_imp->m_env.get_object(n); }
+object const & frontend::find_object(name const & n) const { return m_imp->m_env.find_object(n); }
+bool frontend::has_object(name const & n) const { return m_imp->m_env.has_object(n); }
+
 void frontend::add_infixl(name const & opn, unsigned p, name const & n)  { m_imp->add_infixl(opn, p, n); }
 void frontend::add_infixr(name const & opn, unsigned p, name const & n)  { m_imp->add_infixr(opn, p, n); }
 void frontend::add_prefix(name const & opn, unsigned p, name const & n)  { m_imp->add_prefix(opn, p, n); }
@@ -204,4 +215,3 @@ void frontend::add_mixfixr(unsigned sz, name const * opns, unsigned p, name cons
 void frontend::add_mixfixc(unsigned sz, name const * opns, unsigned p, name const & n) { m_imp->add_mixfixc(sz, opns, p, n); }
 operator_info frontend::find_op_for(name const & n) const { return m_imp->find_op_for(n); }
 }
-

src/frontend/frontend.h

@@ -46,9 +46,20 @@ public:
     environment const & get_environment() const;
     operator environment const &() const { return get_environment(); }
 
+    // =======================================
+    // Environment API
     level add_uvar(name const & n, level const & l);
     level add_uvar(name const & n);
     level get_uvar(name const & n) const;
+    void add_definition(name const & n, expr const & t, expr const & v, bool opaque = false);
+    void add_theorem(name const & n, expr const & t, expr const & v);
+    void add_definition(name const & n, expr const & v, bool opaque = false);
+    void add_axiom(name const & n, expr const & t);
+    void add_var(name const & n, expr const & t);
+    object const & get_object(name const & n) const;
+    object const & find_object(name const & n) const;
+    bool has_object(name const & n) const;
+    // =======================================
 
     // =======================================
     // Notation
@@ -64,7 +75,7 @@ public:
         given internal name.
 
         \remark If an operator is not associated with \c n, then
-        return the nil operator.
+        return the null operator.
     */
     operator_info find_op_for(name const & n) const;
     // =======================================

src/frontend/pp.cpp

@@ -683,6 +683,18 @@ public:
         }
     }
 
+    virtual format operator()(object const & obj) {
+        switch (obj.kind()) {
+        case object_kind::UVarDeclaration:  return pp_uvar_decl(obj);
+        case object_kind::Postulate:        return pp_postulate(obj);
+        case object_kind::Definition:       return pp_definition(obj);
+        case object_kind::Neutral:
+            return pp_notation_decl(obj);
+        }
+        lean_unreachable();
+        return format();
+    }
+
     virtual format operator()(environment const & env) {
         format r;
         bool first = true;
@@ -690,12 +702,7 @@ public:
                       env.end_objects(),
                       [&](object const & obj) {
                           if (first) first = false; else r += line();
-                          switch (obj.kind()) {
+                          r += operator()(obj);
-                          case object_kind::UVarDeclaration:  r += pp_uvar_decl(obj); break;
-                          case object_kind::Postulate:        r += pp_postulate(obj); break;
-                          case object_kind::Definition:       r += pp_definition(obj); break;
-                          case object_kind::Neutral:          r += pp_notation_decl(obj); break;
-                          }
                       });
         return r;
     }

src/kernel/environment.cpp

@@ -388,6 +388,10 @@ object const & environment::get_object(name const & n) const {
     return m_imp->get_object(n, *this);
 }
 
+object const & environment::find_object(name const & n) const {
+    return m_imp->get_object_core(n);
+}
+
 unsigned environment::get_num_objects(bool local) const {
     return m_imp->get_num_objects(local);
 }

src/kernel/environment.h

@@ -109,8 +109,16 @@ public:
     */
     object const & get_object(name const & n) const;
 
+    /**
+       \brief Find a given object in the environment. Return the null
+       object if there is no object with the given name.
+
+       \remark Object implements operator bool(), and the null object returns false.
+    */
+    object const & find_object(name const & n) const;
+
     /** \brief Return true iff the environment has an object with the given name */
-    bool has_object(name const & n) const { return get_object(n); }
+    bool has_object(name const & n) const { return find_object(n); }
 
     /** \brief Iterator for Lean environment objects. */
     class object_iterator {

src/kernel/object.h

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include "expr.h"
 #include "rc.h"
-
 /*
   Kernel objects.
 

src/tests/frontend/frontend.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "frontend.h"
 #include "environment.h"
 #include "operator_info.h"
+#include "kernel_exception.h"
 #include "pp.h"
 #include "test.h"
 using namespace lean;
@@ -68,10 +69,32 @@ static void tst4() {
     std::cout << fmt(c) << "\n";
 }
 
+static void tst5() {
+    std::cout << "=================\n";
+    frontend f;
+    std::shared_ptr<formatter> fmt_ptr = mk_pp_formatter(f);
+    formatter & fmt = *fmt_ptr;
+    f.add_var("A", Type());
+    f.add_var("x", Const("A"));
+    object const & obj = f.find_object("x");
+    lean_assert(obj);
+    lean_assert(obj.get_name() == "x");
+    std::cout << fmt(obj) << "\n";
+    object const & obj2 = f.find_object("y");
+    lean_assert(!obj2);
+    try {
+        f.get_object("y");
+        lean_unreachable();
+    } catch (unknown_name_exception & ex) {
+        std::cout << ex.what() << " " << ex.get_name() << "\n";
+    }
+}
+
 int main() {
     tst1();
     tst2();
     tst3();
     tst4();
+    tst5();
     return has_violations() ? 1 : 0;
 }