Add basic definitions and axioms

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

src/kernel/CMakeLists.txt

@@ -1,4 +1,4 @@
 add_library(kernel expr.cpp max_sharing.cpp free_vars.cpp abstract.cpp
   instantiate.cpp deep_copy.cpp normalize.cpp level.cpp environment.cpp
-  type_check.cpp context.cpp builtin.cpp)
+  type_check.cpp context.cpp builtin.cpp toplevel.cpp)
 target_link_libraries(kernel ${EXTRA_LIBS})

src/kernel/abstract.h

@@ -33,9 +33,11 @@ inline expr abstract_p(expr const & e, expr const & s) { return abstract_p(e, 1,
 */
 inline expr fun(name const & n, expr const & t, expr const & b) { return lambda(n, t, abstract(b, constant(n))); }
 inline expr fun(char const * n, expr const & t, expr const & b) { return fun(name(n), t, b); }
+inline expr fun(expr const & n, expr const & t, expr const & b) { return lambda(const_name(n), t, abstract(b, n)); }
 /**
    \brief Create a Pi expression (pi (x : t) b), the term b is abstracted using abstract(b, constant(x)).
 */
 inline expr Fun(name const & n, expr const & t, expr const & b) { return pi(n, t, abstract(b, constant(n))); }
 inline expr Fun(char const * n, expr const & t, expr const & b) { return Fun(name(n), t, b); }
+inline expr Fun(expr const & n, expr const & t, expr const & b) { return pi(const_name(n), t, abstract(b, n)); }
 }

src/kernel/arith/arith.cpp

@@ -62,16 +62,15 @@ mpz const & int_value_numeral(expr const & e) {
 
 template<char const * Name, unsigned Hash, typename F>
 class int_bin_op : public value {
+    expr m_type;
 public:
     static char const * g_kind;
+    int_bin_op() {
+        m_type = arrow(int_type(), arrow(int_type(), int_type()));
+    }
     virtual ~int_bin_op() {}
     char const * kind() const { return g_kind; }
-    virtual expr get_type() const {
+    virtual expr get_type() const { return m_type; }
-        static thread_local expr r;
-        if (!r)
-            r = arrow(int_type(), arrow(int_type(), int_type()));
-        return r;
-    }
     virtual bool operator==(value const & other) const { return other.kind() == kind(); }
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
@@ -109,16 +108,15 @@ typedef int_bin_op<int_div_name, 61, int_div_eval> int_div_value;
 MK_BUILTIN(int_div, int_div_value);
 
 class int_leq_value : public value {
+    expr m_type;
 public:
     static char const * g_kind;
+    int_leq_value() {
+        m_type = arrow(int_type(), arrow(int_type(), bool_type()));
+    }
     virtual ~int_leq_value() {}
     char const * kind() const { return g_kind; }
-    virtual expr get_type() const {
+    virtual expr get_type() const { return m_type; }
-        static thread_local expr r;
-        if (!r)
-            r = arrow(int_type(), arrow(int_type(), bool_type()));
-        return r;
-    }
     virtual bool operator==(value const & other) const { return other.kind() == kind(); }
     virtual bool normalize(unsigned num_args, expr const * args, expr & r) const {
         if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
@@ -141,7 +139,6 @@ MK_CONSTANT(int_gt,  name(name("int"), "gt"));
 
 void add_int_theory(environment & env) {
     expr p = arrow(int_type(), arrow(int_type(), bool_type()));
-    env.add_definition(int_geq_name_obj, p, lambda("x", int_type(), lambda("y", int_type(), app(int_leq(), var(0), var(1)))));
+    env.add_definition(int_geq_name, p, lambda("x", int_type(), lambda("y", int_type(), app(int_leq(), var(0), var(1)))));
 }
-
 }

src/kernel/builtin.cpp

@@ -6,9 +6,32 @@ Author: Leonardo de Moura
 */
 #include "builtin.h"
 #include "environment.h"
+#include "abstract.h"
+
+#ifndef LEAN_DEFAULT_LEVEL_SEPARATION
+#define LEAN_DEFAULT_LEVEL_SEPARATION 512
+#endif
 
 namespace lean {
 
+expr mk_bin_op(expr const & op, expr const & unit, unsigned num_args, expr const * args) {
+    if (num_args == 0) {
+        return unit;
+    } else {
+        expr r = args[num_args - 1];
+        unsigned i = num_args - 1;
+        while (i > 0) {
+            --i;
+            r = app(op, args[i], r);
+        }
+        return r;
+    }
+}
+
+expr mk_bin_op(expr const & op, expr const & unit, std::initializer_list<expr> const & l) {
+    return mk_bin_op(op, unit, l.size(), l.begin());
+}
+
 class bool_type_value : public value {
 public:
     static char const * g_kind;
@@ -47,7 +70,9 @@ public:
 char const * bool_value_value::g_kind = "bool_value";
 
 expr bool_value(bool v) {
-    return to_expr(*(new bool_value_value(v)));
+    static thread_local expr true_val  = to_expr(*(new bool_value_value(true)));
+    static thread_local expr false_val = to_expr(*(new bool_value_value(false)));
+    return v ? true_val : false_val;
 }
 
 bool is_bool_value(expr const & e) {
@@ -67,6 +92,129 @@ bool is_false(expr const & e) {
     return is_bool_value(e) && !to_bool(e);
 }
 
+static level m_lvl(name("m"));
+static level u_lvl(name("u"));
+
+expr m_type() {
+    static thread_local expr r = type(m_lvl);
+    return r;
+}
+
+expr u_type() {
+    static thread_local expr r = type(u_lvl);
+    return r;
+}
+
+class if_fn_value : public value {
+    expr m_type;
+public:
+    static char const * g_kind;
+    if_fn_value() {
+        expr A = constant("A");
+        // Pi (A: Type), bool -> A -> A -> A
+        m_type = Fun("A", u_type(), arrow(bool_type(), arrow(A, arrow(A, A))));
+    }
+    virtual ~if_fn_value() {}
+    char const * kind() const { return g_kind; }
+    virtual expr get_type() const { return m_type; }
+    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]))
+                r = args[3]; // if A true a b  --> a
+            else
+                r = args[4]; // if A false a b --> b
+            return true;
+        } if (num_args == 5 && args[3] == args[4]) {
+            r = args[3];     // if A c a a --> a
+            return true;
+        } else {
+            return false;
+        }
+    }
+    virtual bool operator==(value const & other) const { return other.kind() == kind(); }
+    virtual void display(std::ostream & out) const { out << "if"; }
+    virtual format pp() const { return format("if"); }
+    virtual unsigned hash() const { return 23; }
+};
+char const * if_fn_value::g_kind = "if";
+
+MK_BUILTIN(if_fn, if_fn_value);
+
+MK_CONSTANT(and_fn, name("and"));
+MK_CONSTANT(or_fn,  name("or"));
+MK_CONSTANT(not_fn, name("not"));
+
+MK_CONSTANT(forall_fn, name("forall"));
+MK_CONSTANT(exists_fn, name("exists"));
+
+MK_CONSTANT(refl_fn, name("refl"));
+MK_CONSTANT(symm_fn, name("symm"));
+MK_CONSTANT(trans_fn, name("trans"));
+MK_CONSTANT(congr_fn, name("congr"));
+MK_CONSTANT(ext_fn, name("ext"));
+MK_CONSTANT(foralle_fn, name("foralle"));
+MK_CONSTANT(foralli_fn, name("foralli"));
+MK_CONSTANT(domain_inj_fn, name("domain_inj"));
+MK_CONSTANT(range_inj_fn, name("range_inj"));
+
 void add_basic_theory(environment & env) {
+    env.define_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
+    env.define_uvar(uvar_name(u_lvl), m_lvl + LEAN_DEFAULT_LEVEL_SEPARATION);
+    expr p1 = arrow(bool_type(), bool_type());
+    expr p2 = arrow(bool_type(), p1);
+
+    expr A  = constant("A");
+    expr a  = constant("a");
+    expr b  = constant("b");
+    expr c  = constant("a");
+    expr H  = constant("H");
+    expr H1 = constant("H1");
+    expr H2 = constant("H2");
+    expr B  = constant("B");
+    expr f  = constant("f");
+    expr g  = constant("g");
+    expr x  = constant("x");
+    expr y  = constant("y");
+    expr P  = constant("P");
+    expr A1 = constant("A1");
+    expr B1 = constant("B1");
+    expr a1 = constant("a1");
+
+    // and(x, y) = (if bool x y false)
+    env.add_definition(and_fn_name, p2, fun(x, bool_type(), fun(y, bool_type(), mk_bool_if(x, y, bool_value(false)))));
+    // or(x, y) = (if bool x true y)
+    env.add_definition(or_fn_name, p2, fun(x, bool_type(), fun(y, bool_type(),  mk_bool_if(x, bool_value(true), y))));
+    // not(x) = (if bool x false true)
+    env.add_definition(not_fn_name, p1, fun(x, bool_type(), mk_bool_if(x, bool_value(false), bool_value(true))));
+
+    // forall : Pi (A : Type u), (A -> Bool) -> Bool
+    expr A_pred = arrow(A, bool_type());
+    expr q_type = Fun(A, u_type(), arrow(A_pred, bool_type()));
+    env.add_var(forall_fn_name, q_type);
+    env.add_definition(exists_fn_name, q_type, fun(A, u_type(), fun(P, A_pred, mk_not(mk_forall(A, fun(x, A, mk_not(P(x))))))));
+
+    // refl : Pi (A : Type u) (a : A), a = a
+    env.add_axiom(refl_fn_name, Fun(A, u_type(), Fun(a, A, eq(a, a))));
+    // symm : Pi (A : Type u) (a b : A) (H : a = b), b = a
+    env.add_axiom(symm_fn_name, Fun(A, u_type(), Fun(a, A, Fun(b, A, Fun(H, eq(a, b), eq(b, a))))));
+    // trans: Pi (A: Type u) (a b c : A) (H1 : a = b) (H2 : b = c), a = c
+    env.add_axiom(trans_fn_name, Fun(A, u_type(), Fun(a, A, Fun(b, A, Fun(c, A, Fun(H1, eq(a, b), Fun(H2, eq(b, c), eq(a, c))))))));
+    // congr : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (a b : A) (H1 : f = g) (H2 : a = b), f a = g b
+    expr piABx = Fun(x, A, B(x));
+    expr A_arrow_u = arrow(A, u_type());
+    env.add_axiom(congr_fn_name, Fun(A, u_type(), Fun(B, A_arrow_u, Fun(f, piABx, Fun(g, piABx, Fun(a, A, Fun(b, A, Fun(H1, eq(f, g), Fun(H2, eq(a, b), eq(f(a), g(b)))))))))));
+    // ext : Pi (A : Type u) (B : A -> Type u) (f g : Pi (x : A) B x) (H : Pi x : A, (f x) = (g x)), f = g
+    env.add_axiom(ext_fn_name, Fun(A, u_type(), Fun(B, A_arrow_u, Fun(f, piABx, Fun(g, piABx, Fun(H, Fun(x, A, eq(f(x), g(x))), eq(f, g)))))));
+
+    // foralle : Pi (A : Type u) (P : A -> bool) (H : (forall A P)) (a : A), P a
+    env.add_axiom(foralle_fn_name, Fun(A, u_type(), Fun(P, A_pred, Fun(H, mk_forall(A, P), Fun(a, A, P(a))))));
+    // foralli : Pi (A : Type u) (P : A -> bool) (H : Pi (x : A), P x), (forall A P)
+    env.add_axiom(foralli_fn_name, Fun(A, u_type(), Fun(P, A_pred, Fun(H, Fun(x, A, P(x)), mk_forall(A, P)))));
+
+    // domain_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), A = A1
+    expr piA1B1x = Fun(x, A1, B1(x));
+    env.add_axiom(domain_inj_fn_name, Fun(A, u_type(), Fun(A1, u_type(), Fun(B, A_arrow_u, Fun(B1, arrow(A1, u_type()), Fun(H, eq(piABx, piA1B1x), eq(A, A1)))))));
+    // range_inj : Pi (A A1: Type u) (B : A -> Type u) (B1 : A1 -> Type u) (a : A) (a1 : A1) (H : (Pi (x : A), B x) = (Pi (x : A1), B1 x)), (B a) = (B1 a1)
+    env.add_axiom(range_inj_fn_name, Fun(A, u_type(), Fun(A1, u_type(), Fun(B, A_arrow_u, Fun(B1, arrow(A1, u_type()), Fun(a, A, Fun(a1, A1, Fun(H, eq(piABx, piA1B1x), eq(B(a), B1(a1))))))))));
 }
 }

src/kernel/builtin.h

@@ -8,16 +8,109 @@ Author: Leonardo de Moura
 #include "expr.h"
 
 namespace lean {
+/**
+   \brief Return unit if <tt>num_args == 0<\tt>, args[0] if <tt>num_args == 1<\tt>, and
+   <tt>(op args[0] (op args[1] (op ... )))<\tt>
+*/
+expr mk_bin_op(expr const & op, expr const & unit, unsigned num_args, expr const * args);
+expr mk_bin_op(expr const & op, expr const & unit, std::initializer_list<expr> const & l);
+
+/** \brief Return (Type m)  m >= bottom + Offset */
+expr m_type();
+
+/** \brief Return (Type u)  u >= m + Offset */
+expr u_type();
+
+/** \brief Return the Lean Boolean type. */
 expr bool_type();
+/** \brief Return true iff \c e is the Lean Boolean type. */
 bool is_bool_type(expr const & e);
 
+/** \brief Create a Lean Boolean value (true/false) */
 expr bool_value(bool v);
+/** \brief Return true iff \c e is a Lean Boolean value. */
 bool is_bool_value(expr const & e);
+/**
+    \brief Convert a Lean Boolean value into a C++ Boolean value.
+    \pre is_bool_value(e)
+*/
 bool to_bool(expr const & e);
+/** \brief Return true iff \c e is the Lean true value. */
 bool is_true(expr const & e);
+/** \brief Return true iff \c e is the Lean false value. */
 bool is_false(expr const & e);
 
+/** \brief Return the Lean If-Then-Else operator. It has type: pi (A : Type), bool -> A -> A -> A */
+expr if_fn();
+/** \brief Return true iff \c e is the Lean If-Then-Else operator */
+bool is_if_fn(expr const & e);
+
+/** \brief Return the term (if A c t e) */
+inline expr mk_if(expr const & A, expr const & c, expr const & t, expr const & e) { return app(if_fn(), A, c, t, e); }
+/** \brief Return the term (if bool c t e) */
+inline expr mk_bool_if(expr const & c, expr const & t, expr const & e) { return mk_if(bool_type(), c, t, e); }
+
+/** \brief Return the Lean and operator */
+expr and_fn();
+/** \brief Return true iff \c e is the Lean and operator. */
+bool is_and_fn(expr const & e);
+
+/** \brief Return (and e1 e2) */
+inline expr mk_and(expr const & e1, expr const & e2) { return app(and_fn(), e1, e2); }
+inline expr mk_and(unsigned num_args, expr const * args) { return mk_bin_op(and_fn(), bool_value(true), num_args, args); }
+inline expr mk_and(std::initializer_list<expr> const & l) { return mk_bin_op(and_fn(), bool_value(true), l); }
+
+/** \brief Return the Lean or operator */
+expr or_fn();
+bool is_or_fn(expr const & e);
+
+/** \brief Return (or e1 e2) */
+inline expr mk_or(expr const & e1, expr const & e2) { return app(or_fn(), e1, e2); }
+inline expr mk_or(unsigned num_args, expr const * args) { return mk_bin_op(or_fn(), bool_value(false), num_args, args); }
+inline expr mk_or(std::initializer_list<expr> const & l) { return mk_bin_op(or_fn(), bool_value(false), l); }
+
+/** \brief Return the Lean not operator */
+expr not_fn();
+bool is_not_fn(expr const & e);
+
+/** \brief Return (not e) */
+inline expr mk_not(expr const & e) { return app(not_fn(), e); }
+
+/** \brief Return the Lean forall operator. It has type: <tt>Pi (A : Type), (A -> bool) -> Bool<\tt> */
+expr forall_fn();
+/** \brief Return true iff \c e is the Lean forall operator */
+bool is_forall_fn(expr const & e);
+/** \brief Return the term (forall A P), where A is a type and P : A -> bool */
+inline expr mk_forall(expr const & A, expr const & P) { return app(forall_fn(), A, P); }
+
+/** \brief Return the Lean exists operator. It has type: <tt>Pi (A : Type), (A -> Bool) -> Bool<\tt> */
+expr exists_fn();
+/** \brief Return true iff \c e is the Lean exists operator */
+bool is_exists_fn(expr const & e);
+/** \brief Return the term (exists A P), where A is a type and P : A -> bool */
+inline expr mk_exists(expr const & A, expr const & P) { return app(exists_fn(), A, P); }
+
+expr refl_fn();
+bool is_refl_fn(expr const & e);
+expr symm_fn();
+bool is_symm_fn(expr const & e);
+expr trans_fn();
+bool is_trans_fn(expr const & e);
+expr congr_fn();
+bool is_congr_fn(expr const & e);
+expr ext_fn();
+bool is_ext_fn(expr const & e);
+expr foralle_fn();
+bool is_foralle_fn(expr const & e);
+expr foralli_fn();
+bool is_foralli_fn(expr const & e);
+expr domain_inj_fn();
+bool is_domain_inj_fn(expr const & e);
+expr range_inj_fn();
+bool is_range_inj_fn(expr const & e);
+
 class environment;
+/** \brief Initialize the environment with basic builtin declarations and axioms */
 void add_basic_theory(environment & env);
 
 /**
@@ -25,9 +118,7 @@ void add_basic_theory(environment & env);
 */
 #define MK_BUILTIN(Name, ClassName)                                     \
 expr Name() {                                                           \
-    static thread_local expr r;                                         \
+    static thread_local expr r = to_expr(*(new ClassName()));           \
-    if (!r)                                                             \
-        r = to_expr(*(new ClassName()));                                \
     return r;                                                           \
 }                                                                       \
 bool is_##Name(expr const & e) {                                        \
@@ -37,16 +128,13 @@ bool is_##Name(expr const & e) {                                        \
 /**
    \brief Helper macro for generating "defined" constants.
 */
-#define MK_CONSTANT(Name, NameObj)                                      \
+#define MK_CONSTANT(Name, NameObj)                              \
-static name Name ## _name_obj = NameObj;                                \
+static name Name ## _name = NameObj;                            \
-expr Name() {                                                           \
+expr Name() {                                                   \
-    static thread_local expr r;                                         \
+    static thread_local expr r = constant(Name ## _name);       \
-    if (!r)                                                             \
+    return r ;                                                  \
-        r = constant(Name ## _name_obj);                                \
+}                                                               \
-    return r;                                                           \
+bool is_##Name(expr const & e) {                                \
-}                                                                       \
+    return is_constant(e) && const_name(e) == Name ## _name;    \
-bool is_##Name(expr const & e) {                                        \
-    return is_constant(e) && const_name(e) == Name ## _name_obj;        \
 }
-
 }

src/kernel/environment.cpp

@@ -28,10 +28,6 @@ environment::definition::definition(name const & n, expr const & t, expr const &
 environment::definition::~definition() {
 }
 
-environment::object_kind environment::definition::kind() const {
-    return object_kind::Definition;
-}
-
 void environment::definition::display(std::ostream & out) const {
     out << "Definition " << m_name << " : " << m_type << " := " << m_value << "\n";
 }
@@ -44,12 +40,9 @@ environment::fact::fact(name const & n, expr const & t):
 environment::fact::~fact() {
 }
 
-environment::object_kind environment::fact::kind() const {
-    return object_kind::Fact;
-}
-
 void environment::fact::display(std::ostream & out) const {
-    out << "Fact " << m_name << " : " << m_type << "\n";
+    display_header(out);
+    out << " " << m_name << " : " << m_type << "\n";
 }
 
 /** \brief Implementation of the Lean environment. */
@@ -196,13 +189,23 @@ struct environment::imp {
         }
     }
 
+    void check_add(name const & n) {
+        check_no_children();
+        check_name(n);
+    }
+
     void add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
         m_objects.push_back(new definition(n, t, v, opaque));
         m_object_dictionary.insert(std::make_pair(n, m_objects.back()));
     }
 
-    void add_fact(name const & n, expr const & t) {
+    void add_axiom(name const & n, expr const & t) {
-        m_objects.push_back(new fact(n, t));
+        m_objects.push_back(new axiom(n, t));
+        m_object_dictionary.insert(std::make_pair(n, m_objects.back()));
+    }
+
+    void add_var(name const & n, expr const & t) {
+        m_objects.push_back(new variable(n, t));
         m_object_dictionary.insert(std::make_pair(n, m_objects.back()));
     }
 
@@ -229,6 +232,20 @@ struct environment::imp {
         }
     }
 
+    void display_objects(std::ostream & out) const {
+        for (object const * obj : m_objects) {
+            obj->display(out);
+        }
+    }
+
+    /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
+    void display(std::ostream & out) const {
+        if (has_parent())
+            m_parent->display(out);
+        display_uvars(out);
+        display_objects(out);
+    }
+
     imp():
         m_num_children(0) {
         init_uvars();
@@ -311,17 +328,21 @@ void environment::add_definition(name const & n, expr const & t, expr const & v,
 }
 
 void environment::add_definition(name const & n, expr const & v, bool opaque) {
-    m_imp->check_no_children();
+    m_imp->check_add(n);
-    m_imp->check_name(n);
     expr v_t = infer_type(v, *this);
     m_imp->add_definition(n, v_t, v, opaque);
 }
 
-void environment::add_fact(name const & n, expr const & t) {
+void environment::add_axiom(name const & n, expr const & t) {
-    m_imp->check_no_children();
+    m_imp->check_add(n);
-    m_imp->check_name(n);
     infer_universe(t, *this);
-    m_imp->add_fact(n, t);
+    m_imp->add_axiom(n, t);
+}
+
+void environment::add_var(name const & n, expr const & t) {
+    m_imp->check_add(n);
+    infer_universe(t, *this);
+    m_imp->add_var(n, t);
 }
 
 environment::object const & environment::get_object(name const & n) const {
@@ -331,4 +352,12 @@ environment::object const & environment::get_object(name const & n) const {
 environment::object const * environment::get_object_ptr(name const & n) const {
     return m_imp->get_object_ptr(n);
 }
+
+void environment::display_objects(std::ostream & out) const {
+    m_imp->display_objects(out);
+}
+
+void environment::display(std::ostream & out) const {
+    m_imp->display(out);
+}
 }

src/kernel/environment.h

@@ -69,7 +69,7 @@ public:
     */
     environment parent() const;
 
-    enum class object_kind { Definition, Fact };
+    enum class object_kind { Definition, Var, Axiom };
 
     /**
         \brief Base class for environment objects
@@ -95,7 +95,7 @@ public:
     public:
         definition(name const & n, expr const & t, expr const & v, bool opaque);
         virtual ~definition();
-        virtual object_kind kind() const;
+        virtual object_kind kind() const { return object_kind::Definition; }
         name const & get_name()  const { return m_name; }
         virtual expr const & get_type()  const { return m_type; }
         expr const & get_value() const { return m_value; }
@@ -104,19 +104,36 @@ public:
     };
 
     class fact : public object {
+    protected:
         name m_name;
         expr m_type;
+        virtual void display_header(std::ostream & out) const = 0;
     public:
         fact(name const & n, expr const & t);
         virtual ~fact();
-        virtual object_kind kind() const;
         name const & get_name()  const { return m_name; }
         virtual expr const & get_type()  const { return m_type; }
         virtual void display(std::ostream & out) const;
     };
 
+    class axiom : public fact {
+        virtual void display_header(std::ostream & out) const { out << "Axiom"; }
+    public:
+        axiom(name const & n, expr const & t):fact(n, t) {}
+        virtual object_kind kind() const { return object_kind::Axiom; }
+    };
+
+    class variable : public fact {
+        virtual void display_header(std::ostream & out) const { out << "Var"; }
+    public:
+        variable(name const & n, expr const & t):fact(n, t) {}
+        virtual object_kind kind() const { return object_kind::Var; }
+    };
+
     friend bool is_definition(object const & o) { return o.kind() == object_kind::Definition; }
-    friend bool is_fact(object const & o) { return o.kind() == object_kind::Fact; }
+    friend bool is_axiom(object const & o) { return o.kind() == object_kind::Axiom; }
+    friend bool is_var(object const & o) { return o.kind() == object_kind::Var; }
+    friend bool is_fact(object const & o) { return is_axiom(o) || is_var(o); }
 
     friend definition const & to_definition(object const & o) { lean_assert(is_definition(o)); return static_cast<definition const &>(o); }
     friend fact const & to_fact(object const & o) { lean_assert(is_fact(o)); return static_cast<fact const &>(o); }
@@ -139,11 +156,13 @@ public:
     void add_definition(char const * n, expr const & v, bool opaque = false) { add_definition(name(n), v, opaque); }
 
     /**
-       \brief Add a new fact to the environment.
+       \brief Add a new fact (Axiom or Fact) to the environment.
        It throws an exception if there is already an object with the given name.
     */
-    void add_fact(name const & n, expr const & t);
+    void add_axiom(name const & n, expr const & t);
-    void add_fact(char const * n, expr const & t) { add_fact(name(n), t); }
+    void add_axiom(char const * n, expr const & t) { add_axiom(name(n), t); }
+    void add_var(name const & n, expr const & t);
+    void add_var(char const * n, expr const & t) { add_var(name(n), t); }
 
     /**
        \brief Return the object with the given name.
@@ -156,5 +175,12 @@ public:
        Return nullptr if there is no object with the given name.
     */
     object const * get_object_ptr(name const & n) const;
+
+    /** \brief Display all objects stored in the environment */
+    void display_objects(std::ostream & out) const;
+
+    /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
+    void display(std::ostream & out) const;
 };
+inline std::ostream & operator<<(std::ostream & out, environment const & env) { env.display(out); return out; }
 }

src/kernel/free_vars.cpp

@@ -15,6 +15,7 @@ namespace lean {
 class has_free_vars_fn {
 protected:
     expr_cell_offset_set m_visited;
+    bool                 m_set_closed_flag;
 
     virtual bool process_var(expr const & x, unsigned offset) {
         return var_idx(x) >= offset;
@@ -62,17 +63,18 @@ protected:
             break;
         }
 
-        if (!result)
+        if (m_set_closed_flag && !result)
             e.raw()->set_closed();
 
         return result;
     }
 public:
+    has_free_vars_fn(bool s):m_set_closed_flag(s) {}
     bool operator()(expr const & e) { return apply(e, 0); }
 };
 
 bool has_free_vars(expr const & e) {
-    return has_free_vars_fn()(e);
+    return has_free_vars_fn(true)(e);
 }
 
 /** \brief Functional object for checking whether a kernel expression has a free variable in the range <tt>[low, high)</tt> or not. */
@@ -83,7 +85,10 @@ class has_free_var_in_range_fn : public has_free_vars_fn {
         return var_idx(x) >= offset + m_low && var_idx(x) < offset + m_high;
     }
 public:
-    has_free_var_in_range_fn(unsigned low, unsigned high):m_low(low), m_high(high) {
+    has_free_var_in_range_fn(unsigned low, unsigned high):
+        has_free_vars_fn(false /* We should not set the closed flag since we are only considering a range of free variables */),
+        m_low(low),
+        m_high(high) {
         lean_assert(low < high);
     }
 };

src/kernel/toplevel.cpp

@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "toplevel.h"
+#include "builtin.h"
+#include "arith.h"
+
+namespace lean {
+environment mk_toplevel() {
+    environment r;
+    add_basic_theory(r);
+    add_int_theory(r);
+    return r;
+}
+}

src/kernel/toplevel.h

@@ -0,0 +1,15 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "environment.h"
+
+namespace lean {
+/**
+   \brief Create top-level environment with builtin objects.
+*/
+environment mk_toplevel();
+}

src/tests/kernel/arith.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <thread>
 #include "environment.h"
 #include "type_check.h"
 #include "builtin.h"
@@ -77,13 +78,24 @@ static void tst4() {
 
 static void tst5() {
     environment env;
-    env.add_fact(name("a"), int_type());
+    env.add_var(name("a"), int_type());
     expr e = eq(int_value(3), int_value(4));
     std::cout << e << " --> " << normalize(e, env) << "\n";
     lean_assert(normalize(e, env) == bool_value(false));
     lean_assert(normalize(eq(constant("a"), int_value(3)), env) == eq(constant("a"), int_value(3)));
 }
 
+static void tst6() {
+    std::cout << "tst6\n";
+    std::cout << int_add().raw() << "\n";
+    std::cout << int_add().raw() << "\n";
+    std::thread t1([](){ std::cout << "t1: " << int_add().raw() << "\n"; });
+    t1.join();
+    std::thread t2([](){ std::cout << "t2: " << int_add().raw() << "\n"; });
+    t2.join();
+    std::cout << int_add().raw() << "\n";
+}
+
 int main() {
     continue_on_violation(true);
     tst1();
@@ -91,5 +103,6 @@ int main() {
     tst3();
     tst4();
     tst5();
+    tst6();
     return has_violations() ? 1 : 0;
 }

src/tests/kernel/environment.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "environment.h"
 #include "type_check.h"
+#include "toplevel.h"
 #include "builtin.h"
 #include "arith.h"
 #include "normalize.h"
@@ -98,7 +99,7 @@ static void tst3() {
     lean_assert(normalize(constant("c"), c_env) == int_value(3));
     try {
         expr r = normalize(constant("c"), env);
-        lean_assert(r == int_value(3))
+        lean_assert(r == int_value(3));
         lean_unreachable();
     } catch (exception const & ex) {
         std::cout << "expected error: " << ex.what() << std::endl;
@@ -133,7 +134,7 @@ static void tst6() {
     environment env;
     level u = env.define_uvar("u", level() + 1);
     level w = env.define_uvar("w", u + 1);
-    env.add_fact("f", arrow(type(u), type(u)));
+    env.add_var("f", arrow(type(u), type(u)));
     expr t = app(constant("f"), int_type());
     std::cout << "type of " << t << " is " << infer_type(t, env) << "\n";
     try {
@@ -156,6 +157,16 @@ static void tst6() {
     lean_assert(infer_type(arrow(int_type(), int_type()), env) == type());
 }
 
+static void tst7() {
+    environment env = mk_toplevel();
+    env.add_var("a", int_type());
+    env.add_var("b", int_type());
+    expr t = app(if_fn(), int_type(), bool_value(true), constant("a"), constant("b"));
+    std::cout << t << " --> " << normalize(t, env) << "\n";
+    std::cout << infer_type(t, env) << "\n";
+    std::cout << "Environment\n" << env;
+}
+
 int main() {
     enable_trace("is_convertible");
     continue_on_violation(true);
@@ -165,5 +176,6 @@ int main() {
     tst4();
     tst5();
     tst6();
+    tst7();
     return has_violations() ? 1 : 0;
 }

src/tests/kernel/normalize.cpp

@@ -80,10 +80,10 @@ unsigned count(expr const & a) {
 
 static void tst_church_numbers() {
     environment env;
-    env.add_fact("t", type(level()));
+    env.add_var("t", type(level()));
-    env.add_fact("N", type(level()));
+    env.add_var("N", type(level()));
-    env.add_fact("z", constant("N"));
+    env.add_var("z", constant("N"));
-    env.add_fact("s", constant("N"));
+    env.add_var("s", constant("N"));
     expr N = constant("N");
     expr z = constant("z");
     expr s = constant("s");
@@ -112,13 +112,13 @@ static void tst_church_numbers() {
 
 static void tst1() {
     environment env;
-    env.add_fact("t", type(level()));
+    env.add_var("t", type(level()));
     expr t = type(level());
-    env.add_fact("f", arrow(t, t));
+    env.add_var("f", arrow(t, t));
     expr f = constant("f");
-    env.add_fact("a", t);
+    env.add_var("a", t);
     expr a = constant("a");
-    env.add_fact("b", t);
+    env.add_var("b", t);
     expr b = constant("b");
     expr x = var(0);
     expr y = var(1);
@@ -140,13 +140,13 @@ static void tst1() {
 static void tst2() {
     environment env;
     expr t = type(level());
-    env.add_fact("f", arrow(t, t));
+    env.add_var("f", arrow(t, t));
     expr f = constant("f");
-    env.add_fact("a", t);
+    env.add_var("a", t);
     expr a = constant("a");
-    env.add_fact("b", t);
+    env.add_var("b", t);
     expr b = constant("b");
-    env.add_fact("h", arrow(t, t));
+    env.add_var("h", arrow(t, t));
     expr h = constant("h");
     expr x = var(0);
     expr y = var(1);
@@ -180,7 +180,7 @@ static void tst2() {
 
 static void tst3() {
     environment env;
-    env.add_fact("a", bool_type());
+    env.add_var("a", bool_type());
     expr t1 = constant("a");
     expr t2 = constant("a");
     expr e = eq(t1, t2);
@@ -190,7 +190,7 @@ static void tst3() {
 
 static void tst4() {
     environment env;
-    env.add_fact("b", type(level()));
+    env.add_var("b", type(level()));
     expr t1 = let("a", constant("b"), lambda("c", type(), var(1)(var(0))));
     std::cout << t1 << " --> " << normalize(t1, env) << "\n";
     lean_assert(normalize(t1, env) == lambda("c", type(), constant("b")(var(0))));

src/tests/kernel/threads.cpp

@@ -19,10 +19,10 @@ using namespace lean;
 
 expr normalize(expr const & e) {
     environment env;
-    env.add_fact("a", int_type());
+    env.add_var("a", int_type());
-    env.add_fact("b", int_type());
+    env.add_var("b", int_type());
-    env.add_fact("f", arrow(int_type(), arrow(int_type(), int_type())));
+    env.add_var("f", arrow(int_type(), arrow(int_type(), int_type())));
-    env.add_fact("h", arrow(int_type(), arrow(int_type(), int_type())));
+    env.add_var("h", arrow(int_type(), arrow(int_type(), int_type())));
     return normalize(e, env);
 }
 

src/util/name.cpp

@@ -266,5 +266,6 @@ std::ostream & operator<<(std::ostream & out, name::sep const & s) {
     name::imp::display(out, s.m_sep, s.m_name.m_ptr);
     return out;
 }
-
 }
+
+void pp(lean::name const & n) { std::cout << n << std::endl; }