From e955c054ca70dbdc3943b8c1fab97b5db357e7c0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 4 Sep 2013 08:30:04 -0700
Subject: [PATCH] Modify type checker. Now, it only accepts builtin values that
 have been declared in the environment. The idea is to be able to track which
 classes of builtin values have been used in a given environment. We want to
 be able to quantify the size of the trusted code base for a particular
 development.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/lean_parser.cpp         |  8 +-
 src/frontends/lean/lean_pp.cpp             |  8 ++
 src/kernel/arith/arith.cpp                 | 23 ++++++
 src/kernel/builtin.cpp                     | 28 +++----
 src/kernel/environment.cpp                 | 24 ++++++
 src/kernel/environment.h                   | 21 ++++++
 src/kernel/kernel_exception.h              | 23 ++++++
 src/kernel/object.cpp                      | 88 ++++++++++++++--------
 src/kernel/object.h                        | 51 ++++++-------
 src/kernel/type_checker.cpp                | 12 ++-
 src/library/printer.cpp                    |  4 +-
 src/tests/frontends/lean/implicit_args.cpp | 20 ++---
 src/tests/kernel/arith.cpp                 |  8 +-
 src/tests/kernel/environment.cpp           |  6 +-
 src/tests/kernel/normalizer.cpp            |  5 +-
 src/tests/kernel/threads.cpp               |  3 +-
 src/tests/kernel/type_checker.cpp          |  6 +-
 tests/lean/arith7.lean.expected.out        |  2 +-
 tests/lean/tst1.lean.expected.out          |  2 +-
 tests/lean/tst10.lean.expected.out         |  2 +-
 tests/lean/tst17.lean.expected.out         |  2 +-
 21 files changed, 236 insertions(+), 110 deletions(-)

diff --git a/src/frontends/lean/lean_parser.cpp b/src/frontends/lean/lean_parser.cpp
index e397641e3..973e683a7 100644
--- a/src/frontends/lean/lean_parser.cpp
+++ b/src/frontends/lean/lean_parser.cpp
@@ -248,14 +248,8 @@ class parser::imp {
 
     /** \brief Initialize \c m_builtins table with Lean builtin symbols that do not have notation associated with them. */
     void init_builtins() {
-        m_builtins["Bool"]   = Bool;
-        m_builtins["true"]   = True;
-        m_builtins["false"]  = False;
         m_builtins["\u22A4"] = True;
         m_builtins["\u22A5"] = False;
-        m_builtins["Nat"]    = Nat;
-        m_builtins["Int"]    = Int;
-        m_builtins["Real"]   = Real;
     }
 
     unsigned parse_unsigned(char const * msg) {
@@ -576,6 +570,8 @@ class parser::imp {
                 } else {
                     return mk_constant(obj.get_name());
                 }
+            } if (k == object_kind::Builtin) {
+                return obj.get_value();
             } else {
                 throw parser_error(sstream() << "invalid object reference, object '" << id << "' is not an expression.", p);
             }
diff --git a/src/frontends/lean/lean_pp.cpp b/src/frontends/lean/lean_pp.cpp
index 0a69054c1..4900f9672 100644
--- a/src/frontends/lean/lean_pp.cpp
+++ b/src/frontends/lean/lean_pp.cpp
@@ -1166,6 +1166,12 @@ class pp_formatter_cell : public formatter_cell {
         return r;
     }
 
+    format pp_builtin_set(object const & obj, options const & opts) {
+        char const * kwd = obj.keyword();
+        name const & n = obj.get_name();
+        return format{highlight_command(format(kwd)), space(), format(n)};
+    }
+
     format pp_definition(object const & obj, options const & opts) {
         return pp_compact_definition(obj.keyword(), obj.get_name(), obj.get_type(), obj.get_value(), opts);
     }
@@ -1224,6 +1230,8 @@ public:
         case object_kind::UVarDeclaration:  return pp_uvar_decl(obj, opts);
         case object_kind::Postulate:        return pp_postulate(obj, opts);
         case object_kind::Definition:       return pp_definition(obj, opts);
+        case object_kind::Builtin:          return pp_postulate(obj, opts);
+        case object_kind::BuiltinSet:       return pp_builtin_set(obj, opts);
         case object_kind::Neutral:
             if (dynamic_cast<notation_declaration const *>(obj.cell())) {
                 return pp_notation_decl(obj, opts);
diff --git a/src/kernel/arith/arith.cpp b/src/kernel/arith/arith.cpp
index ddda46505..7af45633b 100644
--- a/src/kernel/arith/arith.cpp
+++ b/src/kernel/arith/arith.cpp
@@ -353,6 +353,29 @@ void add_arith_theory(environment & env) {
     expr x    = Const("x");
     expr y    = Const("y");
 
+    env.add_builtin(Nat);
+    env.add_builtin_set(nVal(0));
+    env.add_builtin(mk_nat_add_fn());
+    env.add_builtin(mk_nat_mul_fn());
+    env.add_builtin(mk_nat_le_fn());
+
+    env.add_builtin(Int);
+    env.add_builtin_set(iVal(0));
+    env.add_builtin(mk_int_add_fn());
+    env.add_builtin(mk_int_mul_fn());
+    env.add_builtin(mk_int_div_fn());
+    env.add_builtin(mk_int_le_fn());
+
+    env.add_builtin(Real);
+    env.add_builtin_set(rVal(0));
+    env.add_builtin(mk_real_add_fn());
+    env.add_builtin(mk_real_mul_fn());
+    env.add_builtin(mk_real_div_fn());
+    env.add_builtin(mk_real_le_fn());
+
+    env.add_builtin(mk_nat_to_int_fn());
+    env.add_builtin(mk_int_to_real_fn());
+
     env.add_definition(nat_ge_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, nLe(y, x)));
     env.add_definition(nat_lt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(y, x))));
     env.add_definition(nat_gt_fn_name, nn_b, Fun({{x, Nat}, {y, Nat}}, Not(nLe(x, y))));
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index c8b6758f3..ee19c4694 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -45,7 +45,6 @@ expr mk_bin_lop(expr const & op, expr const & unit, std::initializer_list<expr>
     return mk_bin_lop(op, unit, l.size(), l.begin());
 }
 
-
 // =======================================
 // Bultin universe variables m and u
 static level m_lvl(name("M"));
@@ -121,19 +120,19 @@ bool is_false(expr const & e) {
 
 // =======================================
 // If-then-else builtin operator
-static name   g_ite_name("ite");
-static format g_ite_fmt(g_ite_name);
-class ite_fn_value : public value {
+static name   g_if_name("if");
+static format g_if_fmt(g_if_name);
+class if_fn_value : public value {
     expr m_type;
 public:
-    ite_fn_value() {
+    if_fn_value() {
         expr A    = Const("A");
         // Pi (A: Type), bool -> A -> A -> A
         m_type = Pi({A, TypeU}, Bool >> (A >> (A >> A)));
     }
-    virtual ~ite_fn_value() {}
+    virtual ~if_fn_value() {}
     virtual expr get_type() const { return m_type; }
-    virtual name get_name() const { return g_ite_name; }
+    virtual name get_name() const { return g_if_name; }
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 5 && is_bool_value(args[2])) {
             if (to_bool(args[2]))
@@ -149,10 +148,9 @@ public:
         }
     }
 };
-MK_BUILTIN(ite_fn, ite_fn_value);
+MK_BUILTIN(if_fn, if_fn_value);
 // =======================================
 
-MK_CONSTANT(if_fn,      name("if"));
 MK_CONSTANT(implies_fn, name("implies"));
 MK_CONSTANT(iff_fn,     name("iff"));
 MK_CONSTANT(and_fn,     name("and"));
@@ -174,6 +172,7 @@ MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
 void add_basic_theory(environment & env) {
     env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
     env.add_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
+
     expr p1        = Bool >> Bool;
     expr p2        = Bool >> p1;
     expr f         = Const("f");
@@ -191,18 +190,19 @@ void add_basic_theory(environment & env) {
     expr H         = Const("H");
     expr H1        = Const("H1");
     expr H2        = Const("H2");
-    expr ite       = mk_ite_fn();
 
-    // if(A, x, y, z) := ite A x y z
-    env.add_definition(if_fn_name, to_value(ite).get_type(), ite);
+    env.add_builtin(mk_bool_type());
+    env.add_builtin(mk_bool_value(true));
+    env.add_builtin(mk_bool_value(false));
+    env.add_builtin(mk_if_fn());
 
-    // implies(x, y) := ite x y True
+    // implies(x, y) := if x y True
     env.add_definition(implies_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, bIf(x, y, True)));
 
     // iff(x, y) := x = y
     env.add_definition(iff_fn_name, p2, Fun({{x, Bool}, {y, Bool}}, Eq(x, y)));
 
-    // not(x) := ite x False True
+    // not(x) := if x False True
     env.add_definition(not_fn_name, p1, Fun({x, Bool}, bIf(x, False, True)));
 
     // or(x, y) := Not(x) => y
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 416706ac5..156273136 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -234,6 +234,22 @@ struct environment::imp {
         check_type(n, t, v, env);
     }
 
+    /** \brief Add a new builtin value to this environment */
+    void add_builtin(expr const & n, environment const & env) {
+        if (!is_value(n))
+            throw invalid_builtin_value_declaration(env, n);
+        check_name(to_value(n).get_name(), env);
+        register_named_object(mk_builtin(n));
+    }
+
+    /** \brief Add a new builtin value set to this environment */
+    void add_builtin_set(expr const & r, environment const & env) {
+        if (!is_value(r))
+            throw invalid_builtin_value_declaration(env, r);
+        check_name(to_value(r).get_name(), env);
+        register_named_object(mk_builtin_set(r));
+    }
+
     /** \brief Add new definition. */
     void add_definition(name const & n, expr const & t, expr const & v, bool opaque, environment const & env) {
         check_new_definition(n, t, v, env);
@@ -378,6 +394,14 @@ level environment::get_uvar(name const & n) const {
     return m_imp->get_uvar(n, *this);
 }
 
+void environment::add_builtin(expr const & v) {
+    return m_imp->add_builtin(v, *this);
+}
+
+void environment::add_builtin_set(expr const & r) {
+    return m_imp->add_builtin_set(r, *this);
+}
+
 void environment::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
     m_imp->add_definition(n, t, v, opaque, *this);
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index da32085eb..4bc0ec6ea 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -75,6 +75,27 @@ public:
 
     // =======================================
     // Environment Objects
+
+    /**
+        \brief Add builtin value to the environment.
+
+        \pre is_value(v)
+    */
+    void add_builtin(expr const & v);
+
+    /**
+       \brief Add a builtin value set to the environment.
+
+       The set is registered by providing a representative of the set.
+       Each builtin set of values is implemented by a C++ class.
+       The environment will only accept object of the same class of
+       the representative. This functionality is used to support
+       infinite set of builtin values such as the natural numbers.
+
+       \pre is_value(r);
+    */
+    void add_builtin_set(expr const & r);
+
     /**
        \brief Add a new definition n : t := v.
        It throws an exception if v does not have type t.
diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h
index 8fb6e885b..a7c4ad80f 100644
--- a/src/kernel/kernel_exception.h
+++ b/src/kernel/kernel_exception.h
@@ -170,4 +170,27 @@ public:
     expr const & get_value_type() const { return m_value_type; }
     virtual char const * what() const noexcept { return "definition type mismatch"; }
 };
+
+/**
+    \brief Invalid builtin value declaration.
+*/
+class invalid_builtin_value_declaration : public kernel_exception {
+    expr m_expr;
+public:
+    invalid_builtin_value_declaration(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
+    virtual ~invalid_builtin_value_declaration() {}
+    virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; }
+};
+
+/**
+    \brief Exception used to report that a builtin value is not
+    declared in the environment.
+*/
+class invalid_builtin_value_reference : public kernel_exception {
+    expr m_expr;
+public:
+    invalid_builtin_value_reference(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
+    virtual ~invalid_builtin_value_reference() {}
+    virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; }
+};
 }
diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
index 7564b7937..15fee829f 100644
--- a/src/kernel/object.cpp
+++ b/src/kernel/object.cpp
@@ -9,16 +9,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 neutral_object_cell::neutral_object_cell():object_cell(object_kind::Neutral) {}
-neutral_object_cell::~neutral_object_cell() {}
-bool         neutral_object_cell::has_name() const        { return false; }
-name const & neutral_object_cell::get_name() const        { lean_unreachable(); return name::anonymous(); }
-bool         neutral_object_cell::has_cnstr_level() const { return false; }
-level        neutral_object_cell::get_cnstr_level() const { lean_unreachable(); return level(); }
-bool         neutral_object_cell::has_type() const        { return false; }
-expr const & neutral_object_cell::get_type() const        { lean_unreachable(); return expr::null(); }
-bool         neutral_object_cell::is_definition() const   { return false; }
-bool         neutral_object_cell::is_opaque() const       { lean_unreachable(); return false; }
-expr const & neutral_object_cell::get_value() const       { lean_unreachable(); return expr::null(); }
 
 /**
    \brief Named kernel objects.
@@ -31,8 +21,8 @@ public:
     named_object_cell(object_kind k, name const & n):object_cell(k), m_name(n) {}
     virtual ~named_object_cell() {}
 
-    virtual bool has_name() const          { return true; }
-    virtual name const & get_name() const  { return m_name; }
+    virtual bool has_name() const { return true; }
+    virtual name get_name() const { return m_name; }
 };
 
 /**
@@ -45,18 +35,55 @@ public:
         named_object_cell(object_kind::UVarDeclaration, n), m_level(l) {}
     virtual ~uvar_declaration_object_cell() {}
 
-    virtual bool has_cnstr_level() const   { return true; }
-    virtual level get_cnstr_level() const  { return m_level; }
-
-    bool has_type() const          { return false; }
-    expr const & get_type() const  { lean_unreachable(); return expr::null(); }
-    bool is_definition() const     { return false; }
-    bool is_opaque() const         { lean_unreachable(); return false; }
-    expr const & get_value() const { lean_unreachable(); return expr::null(); }
-
+    virtual bool has_cnstr_level() const { return true; }
+    virtual level get_cnstr_level() const { return m_level; }
     virtual char const * keyword() const { return "Universe"; }
 };
 
+/**
+   \brief Base class for Axioms and Variable declarations.
+*/
+class builtin_object_cell : public object_cell {
+    expr m_value;
+public:
+    builtin_object_cell(expr const & v):
+        object_cell(object_kind::Builtin), m_value(v) { lean_assert(is_value(v)); }
+    virtual ~builtin_object_cell() {}
+    virtual bool has_name() const { return true; }
+    virtual name get_name() const { return to_value(m_value).get_name(); }
+    virtual bool has_type() const { return true; }
+    virtual expr get_type() const { return to_value(m_value).get_type(); }
+    virtual bool is_definition() const { return true; }
+    virtual bool is_opaque() const { return false; }
+    virtual expr get_value() const { return m_value; }
+    virtual char const * keyword() const { return "Builtin"; }
+    virtual bool is_builtin() const { return true; }
+};
+
+/**
+   \brief Base class for capturing a set of builtin objects such as
+      a) the natural numbers 0, 1, 2, ...
+      b) the integers 0, -1, 1, -2, 2, ...
+      c) the reals
+      d) ...
+   This object represents an infinite set of declarations.
+   This is just a markup to sign that an environment depends on a
+   particular builtin set of values.
+*/
+class builtin_set_object_cell : public object_cell {
+    // The representative is only used to test if a builtin value
+    // is in the same C++ class of the representative.
+    expr m_representative;
+public:
+    builtin_set_object_cell(expr const & r):object_cell(object_kind::BuiltinSet), m_representative(r) { lean_assert(is_value(r)); }
+    virtual ~builtin_set_object_cell() {}
+    virtual bool has_name() const { return true; }
+    virtual name get_name() const { return to_value(m_representative).get_name(); }
+    virtual bool is_builtin_set() const { return true; }
+    virtual bool in_builtin_set(expr const & v) const { return is_value(v) && typeid(to_value(v)) == typeid(to_value(m_representative)); }
+    virtual char const * keyword() const { return "BuiltinSet"; }
+};
+
 /**
    \brief Named (and typed) kernel objects.
 */
@@ -67,11 +94,8 @@ public:
         named_object_cell(k, n), m_type(t) {}
     virtual ~named_typed_object_cell() {}
 
-    virtual bool has_type() const          { return true; }
-    virtual expr const & get_type() const  { return m_type; }
-
-    virtual bool has_cnstr_level() const   { return false; }
-    virtual level get_cnstr_level() const  { lean_unreachable(); return level(); }
+    virtual bool has_type() const { return true; }
+    virtual expr get_type() const { return m_type; }
 };
 
 /**
@@ -81,10 +105,6 @@ class postulate_object_cell : public named_typed_object_cell {
 public:
     postulate_object_cell(name const & n, expr const & t):
         named_typed_object_cell(object_kind::Postulate, n, t) {}
-
-    bool is_definition() const     { return false; }
-    bool is_opaque() const         { lean_unreachable(); return false; }
-    expr const & get_value() const { lean_unreachable(); return expr::null(); }
 };
 
 /**
@@ -118,9 +138,9 @@ public:
         named_typed_object_cell(object_kind::Definition, n, t), m_value(v), m_opaque(opaque) {}
     virtual ~definition_object_cell() {}
 
-    bool is_definition() const     { return true; }
-    bool is_opaque() const         { return m_opaque; }
-    expr const & get_value() const { return m_value; }
+    virtual bool is_definition() const     { return true; }
+    virtual bool is_opaque() const         { return m_opaque; }
+    virtual expr get_value() const { return m_value; }
     virtual char const * keyword() const { return "Definition"; }
 };
 
@@ -140,6 +160,8 @@ object mk_definition(name const & n, expr const & t, expr const & v, bool opaque
 object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); }
 object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); }
 object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); }
+object mk_builtin(expr const & v) { return object(new builtin_object_cell(v)); }
+object mk_builtin_set(expr const & r) { return object(new builtin_set_object_cell(r)); }
 
 static object g_null_object;
 
diff --git a/src/kernel/object.h b/src/kernel/object.h
index 3271fa257..8794ff4a7 100644
--- a/src/kernel/object.h
+++ b/src/kernel/object.h
@@ -14,7 +14,7 @@ Author: Leonardo de Moura
   frontend may need to create new objects for bookkeeping.
 */
 namespace lean {
-enum class object_kind { UVarDeclaration, Definition, Postulate, Neutral };
+enum class object_kind { UVarDeclaration, Definition, Postulate, Builtin, BuiltinSet, Neutral };
 
 class object_cell {
     void dealloc() { delete this; }
@@ -33,30 +33,34 @@ public:
     virtual char const * keyword() const = 0;
 
     /** \brief Return true iff object has a name. */
-    virtual bool has_name() const = 0;
+    virtual bool has_name() const { return false; }
     /** \brief Return object name. \pre has_name() */
-    virtual name const & get_name() const = 0;
+    virtual name get_name() const { lean_unreachable(); return name(); }
 
     /** \brief Has constraint level associated with it (for universal variables). */
-    virtual bool has_cnstr_level() const = 0;
+    virtual bool has_cnstr_level() const { return false; }
     /** \brief Return the constraint level associated with the object. */
-    virtual level get_cnstr_level() const = 0;
+    virtual level get_cnstr_level() const { lean_unreachable(); return level(); }
 
     /** \brief Return true iff object has a type. */
-    virtual bool has_type() const = 0;
+    virtual bool has_type() const { return false; }
     /** \brief Return object type. \pre has_type() */
-    virtual expr const & get_type() const = 0;
+    virtual expr get_type() const { lean_unreachable(); return expr(); }
 
     /** \brief Return true iff object is a definition */
-    virtual bool is_definition() const = 0;
+    virtual bool is_definition() const { return false; }
     /** \brief Return true iff the definition is opaque. \pre is_definition() */
-    virtual bool is_opaque() const = 0;
+    virtual bool is_opaque() const { lean_unreachable(); return false; }
     /** \brief Return object value. \pre is_definition() */
-    virtual expr const & get_value() const = 0;
+    virtual expr get_value() const { lean_unreachable(); return expr(); }
 
     virtual bool is_axiom() const { return false; }
+    virtual bool is_builtin() const { return false; }
+    virtual bool is_builtin_set() const { return false; }
     virtual bool is_theorem() const { return false; }
     virtual bool is_var_decl() const { return false; }
+
+    virtual bool in_builtin_set(expr const & v) const { return false; }
 };
 
 /**
@@ -67,20 +71,6 @@ public:
 class neutral_object_cell : public object_cell {
 public:
     neutral_object_cell();
-    virtual ~neutral_object_cell();
-
-    virtual bool has_name() const;
-    virtual name const & get_name() const;
-
-    virtual bool has_cnstr_level() const;
-    virtual level get_cnstr_level() const;
-
-    virtual bool has_type() const;
-    virtual expr const & get_type() const;
-
-    virtual bool is_definition() const;
-    virtual bool is_opaque() const;
-    virtual expr const & get_value() const;
 };
 
 /**
@@ -115,25 +105,32 @@ public:
     friend object mk_axiom(name const & n, expr const & t);
     friend object mk_var_decl(name const & n, expr const & t);
     friend object mk_neutral(neutral_object_cell * c);
+    friend object mk_builtin(expr const & v);
+    friend object mk_builtin_set(expr const & r);
 
     char const * keyword() const { return m_ptr->keyword(); }
     bool has_name() const { return m_ptr->has_name(); }
-    name const & get_name() const { return m_ptr->get_name(); }
+    name get_name() const { return m_ptr->get_name(); }
     bool has_type() const { return m_ptr->has_type(); }
     bool has_cnstr_level() const { return m_ptr->has_cnstr_level(); }
     level get_cnstr_level() const { return m_ptr->get_cnstr_level(); }
-    expr const & get_type() const { return m_ptr->get_type(); }
+    expr get_type() const { return m_ptr->get_type(); }
     bool is_definition() const { return m_ptr->is_definition(); }
     bool is_opaque() const { return m_ptr->is_opaque(); }
-    expr const & get_value() const { return m_ptr->get_value(); }
+    expr get_value() const { return m_ptr->get_value(); }
 
     bool is_axiom() const { return m_ptr->is_axiom(); }
     bool is_theorem() const { return m_ptr->is_theorem(); }
     bool is_var_decl() const { return m_ptr->is_var_decl(); }
+    bool is_builtin() const { return m_ptr->is_builtin(); }
+    bool is_builtin_set() const { return m_ptr->is_builtin_set(); }
+    bool in_builtin_set(expr const & e) const { return m_ptr->in_builtin_set(e); }
 
     object_cell const * cell() const { return m_ptr; }
 };
 object mk_uvar_decl(name const & n, level const & l);
+object mk_builtin(expr const & v);
+object mk_builtin_set(expr const & r);
 object mk_definition(name const & n, expr const & t, expr const & v, bool opaque);
 object mk_theorem(name const & n, expr const & t, expr const & v);
 object mk_axiom(name const & n, expr const & t);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 02718befa..4aa954c8c 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -139,10 +139,18 @@ public:
             }
             break;
         }
-        case expr_kind::Value:
-            r = to_value(e).get_type();
+        case expr_kind::Value: {
+            // Check if the builtin value (or its set) is declared in the environment.
+            name const & n = to_value(e).get_name();
+            object const & obj = m_env.get_object(n);
+            if (obj && ((obj.is_builtin() && obj.get_value() == e) || (obj.is_builtin_set() && obj.in_builtin_set(e)))) {
+                r = to_value(e).get_type();
+            } else {
+                throw invalid_builtin_value_reference(m_env, e);
+            }
             break;
         }
+        }
 
         if (shared) {
             m_cache.insert(e, r);
diff --git a/src/library/printer.cpp b/src/library/printer.cpp
index b5645fead..6cf6352ec 100644
--- a/src/library/printer.cpp
+++ b/src/library/printer.cpp
@@ -184,8 +184,10 @@ std::ostream & operator<<(std::ostream & out, object const & obj) {
         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:
+    case object_kind::Definition: case object_kind::Builtin:
         out << obj.get_name() << " : " << obj.get_type() << " :=\n    " << obj.get_value(); break;
+    case object_kind::BuiltinSet:
+        out << obj.get_name(); break;
     case object_kind::Neutral:
         break;
     }
diff --git a/src/tests/frontends/lean/implicit_args.cpp b/src/tests/frontends/lean/implicit_args.cpp
index 3c3943e23..e84fa3488 100644
--- a/src/tests/frontends/lean/implicit_args.cpp
+++ b/src/tests/frontends/lean/implicit_args.cpp
@@ -71,10 +71,10 @@ static void tst1() {
     expr F = Const("F");
     expr g = Const("g");
     expr a = Const("a");
-    expr Nat  = Const("Nat");
-    expr Real = Const("Real");
-    env.add_var("Nat", Type());
-    env.add_var("Real", Type());
+    expr Nat  = Const("N");
+    expr Real = Const("R");
+    env.add_var("N", Type());
+    env.add_var("R", Type());
     env.add_var("F", Pi({{A, Type()}, {B, Type()}, {g, A >> B}}, A));
     env.add_var("f", Nat >> Real);
     expr f = Const("f");
@@ -109,8 +109,8 @@ static void tst2() {
 
 static void tst3() {
     frontend env;
-    expr Nat = Const("Nat");
-    env.add_var("Nat", Type());
+    expr Nat = Const("N");
+    env.add_var("N", Type());
     env.add_var("vec", Nat >> Type());
     expr n   = Const("n");
     expr vec = Const("vec");
@@ -139,8 +139,8 @@ static void tst3() {
 
 static void tst4() {
     frontend env;
-    expr Nat = Const("Nat");
-    env.add_var("Nat", Type());
+    expr Nat = Const("N");
+    env.add_var("N", Type());
     expr R   = Const("R");
     env.add_var("R", Type());
     env.add_var("a", Nat);
@@ -167,8 +167,8 @@ static void tst5() {
     expr b = Const("b");
     expr f = Const("f");
     expr g = Const("g");
-    expr Nat = Const("Nat");
-    env.add_var("Nat", Type());
+    expr Nat = Const("N");
+    env.add_var("N", Type());
     env.add_var("f", Pi({{A,Type()},{a,A},{b,A}}, A));
     env.add_var("g", Nat >> Nat);
     success(Fun({{a,_},{b,_}},g(f(_,a,b))),
diff --git a/src/tests/kernel/arith.cpp b/src/tests/kernel/arith.cpp
index 847af93b1..aff086366 100644
--- a/src/tests/kernel/arith.cpp
+++ b/src/tests/kernel/arith.cpp
@@ -17,7 +17,7 @@ Author: Leonardo de Moura
 using namespace lean;
 
 static void tst1() {
-    environment env;
+    environment env = mk_toplevel();
     expr e = mk_int_value(mpz(10));
     lean_assert(is_int_value(e));
     lean_assert(infer_type(e, env) == Int);
@@ -25,7 +25,7 @@ static void tst1() {
 }
 
 static void tst2() {
-    environment env;
+    environment env = mk_toplevel();
     expr e = iAdd(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
@@ -41,7 +41,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env;
+    environment env = mk_toplevel();
     expr e = iMul(iVal(10), iVal(30));
     std::cout << e << "\n";
     std::cout << normalize(e, env) << "\n";
@@ -73,7 +73,7 @@ static void tst4() {
 }
 
 static void tst5() {
-    environment env;
+    environment env = mk_toplevel();
     env.add_var(name("a"), Int);
     expr e = Eq(iVal(3), iVal(4));
     std::cout << e << " --> " << normalize(e, env) << "\n";
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index 7b4c9f2f0..ba597318e 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -62,7 +62,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env;
+    environment env = mk_toplevel();
     try {
         env.add_definition("a", Int, Const("a"));
         lean_unreachable();
@@ -123,7 +123,7 @@ static void tst4() {
 }
 
 static void tst5() {
-    environment env;
+    environment env = mk_toplevel();
     env.add_definition("a", Int, iVal(1), true); // add opaque definition
     try {
         std::cout << infer_type(iAdd(Const("a"), Int), env) << "\n";
@@ -134,7 +134,7 @@ static void tst5() {
 }
 
 static void tst6() {
-    environment env;
+    environment env = mk_toplevel();
     level u = env.add_uvar("u", level() + 1);
     level w = env.add_uvar("w", u + 1);
     env.add_var("f", mk_arrow(Type(u), Type(u)));
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index 05e1ecc77..787e28d35 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "expr_sets.h"
 #include "abstract.h"
 #include "kernel_exception.h"
+#include "toplevel.h"
 #include "printer.h"
 using namespace lean;
 
@@ -185,7 +186,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env;
+    environment env = mk_toplevel();
     env.add_var("a", Bool);
     expr t1 = Const("a");
     expr t2 = Const("a");
@@ -212,7 +213,7 @@ static expr mk_big(unsigned depth) {
 static void tst5() {
 #ifndef __APPLE__
     expr t = mk_big(18);
-    environment env;
+    environment env = mk_toplevel();
     env.add_var("f", Bool >> (Bool >> Bool));
     env.add_var("a", Bool);
     normalizer proc(env);
diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp
index 038768d86..436d8919b 100644
--- a/src/tests/kernel/threads.cpp
+++ b/src/tests/kernel/threads.cpp
@@ -13,12 +13,13 @@ Author: Leonardo de Moura
 #include "deep_copy.h"
 #include "abstract.h"
 #include "normalizer.h"
+#include "toplevel.h"
 #include "arith.h"
 #include "test.h"
 using namespace lean;
 
 expr normalize(expr const & e) {
-    environment env;
+    environment env = mk_toplevel();
     env.add_var("a", Int);
     env.add_var("b", Int);
     env.add_var("f", Int >> (Int >> Int));
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 81cac3759..7b9393be9 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -73,7 +73,7 @@ static void tst2() {
 }
 
 static void tst3() {
-    environment env;
+    environment env = mk_toplevel();
     expr f = Fun("a", Bool, Eq(Const("a"), True));
     std::cout << infer_type(f, env) << "\n";
     lean_assert(infer_type(f, env) == mk_arrow(Bool, Bool));
@@ -82,7 +82,7 @@ static void tst3() {
 }
 
 static void tst4() {
-    environment env;
+    environment env = mk_toplevel();
     expr a = Eq(iVal(1), iVal(2));
     expr pr   = mk_lambda("x", a, Var(0));
     std::cout << infer_type(pr, env) << "\n";
@@ -218,7 +218,7 @@ static expr mk_big(unsigned depth) {
 static void tst12() {
 #ifndef __APPLE__
     expr t = mk_big(18);
-    environment env;
+    environment env = mk_toplevel();
     env.add_var("f", Int >> (Int >> Int));
     env.add_var("a", Int);
     type_checker checker(env);
diff --git a/tests/lean/arith7.lean.expected.out b/tests/lean/arith7.lean.expected.out
index db3d0aa9e..bc8690699 100644
--- a/tests/lean/arith7.lean.expected.out
+++ b/tests/lean/arith7.lean.expected.out
@@ -6,7 +6,7 @@
 2
 ⊤
   Assumed: y
-ite Int (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
+if Int (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
 | x + y | > x
   Set: lean::pp::notation
 Int::gt (Int::abs (Int::add x y)) x
diff --git a/tests/lean/tst1.lean.expected.out b/tests/lean/tst1.lean.expected.out
index cddeeb831..f0f28b992 100644
--- a/tests/lean/tst1.lean.expected.out
+++ b/tests/lean/tst1.lean.expected.out
@@ -46,4 +46,4 @@ map normal form -->
   f (v1 i H) (v2 i H)
 
 update normal form --> 
-λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), ite A (j = i) d (v j H)
+λ (A : Type) (n : N) (v : Π (i : N) (H : i < n), A) (i : N) (d : A) (j : N) (H : j < n), if A (j = i) d (v j H)
diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out
index 9fd43784a..0de41e847 100644
--- a/tests/lean/tst10.lean.expected.out
+++ b/tests/lean/tst10.lean.expected.out
@@ -15,7 +15,7 @@ a ∨ b
 a ∨ a ∨ b
 a ⇒ b ⇒ a
 Bool
-ite Bool a a ⊤
+if Bool a a ⊤
 a
   Assumed: H1
   Assumed: H2
diff --git a/tests/lean/tst17.lean.expected.out b/tests/lean/tst17.lean.expected.out
index 001782e7f..d7c7552c0 100644
--- a/tests/lean/tst17.lean.expected.out
+++ b/tests/lean/tst17.lean.expected.out
@@ -5,6 +5,6 @@
 ∀ a b : Type, ∃ c : Type, (g a b) = (f c)
 Bool
 (λ a : Type,
-   (λ b : Type, ite Bool ((λ x : Type, ite Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
+   (λ b : Type, if Bool ((λ x : Type, if Bool ((g a b) = (f x)) ⊥ ⊤) = (λ x : Type, ⊤)) ⊥ ⊤) =
    (λ x : Type, ⊤)) =
 (λ x : Type, ⊤)