Modify environment. Now, when a builtin value is declared, if it has a unicode alternative representation, then we add it as a definition. Now, everything that occurs in the environment has been 'declared'.

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

src/frontends/lean/lean_parser.cpp

@@ -119,7 +119,6 @@ class parser::imp {
     bool           m_found_errors;
     local_decls    m_local_decls;
     unsigned       m_num_local_decls;
-    builtins       m_builtins;
     expr_pos_info  m_expr_pos_info;
     pos_info       m_last_cmd_pos;
     // Reference to temporary parser used to process import command.
@@ -246,12 +245,6 @@ class parser::imp {
         return r;
     }
 
-    /** \brief Initialize \c m_builtins table with Lean builtin symbols that do not have notation associated with them. */
-    void init_builtins() {
-        m_builtins["\u22A4"] = True;
-        m_builtins["\u22A5"] = False;
-    }
-
     unsigned parse_unsigned(char const * msg) {
         lean_assert(curr_is_nat());
         mpz pval = curr_num().get_numerator();
@@ -577,14 +570,9 @@ class parser::imp {
             }
         }
         else {
-            auto it = m_builtins.find(id);
-            if (it != m_builtins.end()) {
-                return it->second;
-            } else {
             throw parser_error(sstream() << "unknown identifier '" << id << "'", p);
         }
     }
-    }
 
     /**
         \brief Parse an identifier that has a "null denotation" (See
@@ -1497,7 +1485,6 @@ public:
         m_found_errors = false;
         m_num_local_decls = 0;
         m_scanner.set_command_keywords(g_command_keywords);
-        init_builtins();
         scan();
     }
 

src/kernel/arith/arith.cpp

@@ -33,6 +33,7 @@ public:
     }
     virtual void display(std::ostream & out) const { out << m_val; }
     virtual format pp() const { return format(m_val); }
+    virtual format pp(bool unicode) const { return pp(); }
     virtual unsigned hash() const { return m_val.hash(); }
     mpz const & get_num() const { return m_val; }
 };
@@ -118,6 +119,7 @@ public:
     }
     virtual void display(std::ostream & out) const { out << m_val; }
     virtual format pp() const { return format(m_val); }
+    virtual format pp(bool unicode) const { return pp(); }
     virtual unsigned hash() const { return m_val.hash(); }
     mpz const & get_num() const { return m_val; }
 };
@@ -217,6 +219,7 @@ public:
     }
     virtual void display(std::ostream & out) const { out << m_val; }
     virtual format pp() const { return format(m_val); }
+    virtual format pp(bool unicode) const { return pp(); }
     virtual unsigned hash() const { return m_val.hash(); }
     mpq const & get_num() const { return m_val; }
 };

src/kernel/builtin.cpp

@@ -70,14 +70,10 @@ expr mk_bool_type() { return Bool; }
 
 // =======================================
 // Boolean values True and False
-static char const * g_true_u_str  = "\u22A4";
-static char const * g_false_u_str = "\u22A5";
-static format g_true_u_fmt(g_true_u_str);
-static format g_false_u_fmt(g_false_u_str);
 static name g_true_name("true");
 static name g_false_name("false");
-static format g_true_fmt(g_true_name);
+static name g_true_u_name("\u22A4"); // ⊤
-static format g_false_fmt(g_false_name);
+static name g_false_u_name("\u22A5"); // ⊥
 class bool_value_value : public value {
     bool m_val;
 public:
@@ -85,17 +81,11 @@ public:
     virtual ~bool_value_value() {}
     virtual expr get_type() const { return Bool; }
     virtual name get_name() const { return m_val ? g_true_name : g_false_name; }
+    virtual name get_unicode_name() const { return m_val ? g_true_u_name : g_false_u_name; }
     virtual bool operator==(value const & other) const {
         bool_value_value const * _other = dynamic_cast<bool_value_value const*>(&other);
         return _other && _other->m_val == m_val;
     }
-    virtual format pp(bool unicode) const {
-        if (unicode)
-            return m_val ? g_true_u_fmt : g_false_u_fmt;
-        else
-            return m_val ? g_true_fmt : g_false_fmt;
-    }
-    virtual format pp() const { return pp(true); }
     bool get_val() const { return m_val; }
 };
 expr const True  = mk_value(*(new bool_value_value(true)));

src/kernel/environment.cpp

@@ -235,11 +235,17 @@ struct environment::imp {
     }
 
     /** \brief Add a new builtin value to this environment */
-    void add_builtin(expr const & n, environment const & env) {
+    void add_builtin(expr const & v, environment const & env) {
-        if (!is_value(n))
+        if (!is_value(v))
-            throw invalid_builtin_value_declaration(env, n);
+            throw invalid_builtin_value_declaration(env, v);
-        check_name(to_value(n).get_name(), env);
+        name const & n = to_value(v).get_name();
-        register_named_object(mk_builtin(n));
+        check_name(n, env);
+        name const & u = to_value(v).get_unicode_name();
+        check_name(u, env);
+        register_named_object(mk_builtin(v));
+        if (u != n) {
+            add_definition(u, to_value(v).get_type(), mk_constant(n), false, env);
+        }
     }
 
     /** \brief Add a new builtin value set to this environment */

src/kernel/expr.cpp

@@ -101,11 +101,12 @@ expr_let::expr_let(name const & n, expr const & v, expr const & b):
     m_body(b) {
 }
 expr_let::~expr_let() {}
+name value::get_unicode_name() const { return get_name(); }
 bool value::normalize(unsigned num_args, expr const * args, expr & r) const { return false; }
 void value::display(std::ostream & out) const { out << get_name(); }
 bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); }
 format value::pp() const { return format(get_name()); }
-format value::pp(bool unicode) const { return pp(); }
+format value::pp(bool unicode) const { return unicode ? format(get_unicode_name()) : pp(); }
 unsigned value::hash() const { return get_name().hash(); }
 expr_value::expr_value(value & v):
     expr_cell(expr_kind::Value, v.hash()),

src/kernel/expr.h

@@ -205,6 +205,7 @@ public:
     virtual ~value() {}
     virtual expr get_type() const = 0;
     virtual name get_name() const = 0;
+    virtual name get_unicode_name() const;
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const;
     virtual bool operator==(value const & other) const;
     virtual void display(std::ostream & out) const;