Rename define_uv -> add_uvar

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

src/CMakeLists.txt

@@ -56,6 +56,7 @@ include_directories(${LEAN_SOURCE_DIR}/interval)
 include_directories(${LEAN_SOURCE_DIR}/kernel)
 include_directories(${LEAN_SOURCE_DIR}/kernel/arith)
 include_directories(${LEAN_SOURCE_DIR}/parsers)
+include_directories(${LEAN_SOURCE_DIR}/frontend)
 
 add_subdirectory(util)
 set(EXTRA_LIBS ${EXTRA_LIBS} util)
@@ -67,6 +68,8 @@ add_subdirectory(kernel)
 set(EXTRA_LIBS ${EXTRA_LIBS} kernel)
 add_subdirectory(kernel/arith)
 set(EXTRA_LIBS ${EXTRA_LIBS} kernel_arith)
+add_subdirectory(frontend)
+set(EXTRA_LIBS ${EXTRA_LIBS} frontend)
 add_subdirectory(parsers)
 set(EXTRA_LIBS ${EXTRA_LIBS} parser_common)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")
@@ -75,3 +78,4 @@ add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)
 add_subdirectory(tests/interval)
 add_subdirectory(tests/kernel)
+add_subdirectory(tests/frontend)

src/kernel/builtin.cpp

@@ -187,8 +187,8 @@ MK_CONSTANT(eta_fn,         name("Eta"));
 MK_CONSTANT(imp_antisym_fn, name("ImpAntisym"));
 
 void add_basic_theory(environment & env) {
-    env.define_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
+    env.add_uvar(uvar_name(m_lvl), level() + LEAN_DEFAULT_LEVEL_SEPARATION);
-    env.define_uvar(uvar_name(u_lvl), m_lvl + 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");

src/kernel/environment.cpp

@@ -152,7 +152,7 @@ struct environment::imp {
         lean_unreachable();
     }
 
-    level define_uvar(name const & n, level const & l) {
+    level add_uvar(name const & n, level const & l) {
         if (has_parent())
             throw exception("invalid universe declaration, universe variables can only be declared in top-level environments");
         if (has_children())
@@ -298,18 +298,6 @@ environment::environment(std::shared_ptr<imp> const & ptr):
 environment::~environment() {
 }
 
-level environment::define_uvar(name const & n, level const & l) {
-    return m_imp->define_uvar(n, l);
-}
-
-bool environment::is_ge(level const & l1, level const & l2) const {
-    return m_imp->is_ge(l1, l2);
-}
-
-void environment::display_uvars(std::ostream & out) const {
-    m_imp->display_uvars(out);
-}
-
 environment environment::mk_child() const {
     return environment(new imp(m_imp));
 }
@@ -327,6 +315,18 @@ environment environment::parent() const {
     return environment(m_imp->m_parent);
 }
 
+level environment::add_uvar(name const & n, level const & l) {
+    return m_imp->add_uvar(n, l);
+}
+
+bool environment::is_ge(level const & l1, level const & l2) const {
+    return m_imp->is_ge(l1, l2);
+}
+
+void environment::display_uvars(std::ostream & out) const {
+    m_imp->display_uvars(out);
+}
+
 level environment::get_uvar(name const & n) const {
     return m_imp->get_uvar(n);
 }

src/kernel/environment.h

@@ -30,30 +30,8 @@ public:
     environment();
     ~environment();
 
-    /**
+    // =======================================
-       \brief Define a new universe variable with name \c n and constraint <tt>n >= l</tt>.
+    // Parent/Child environment management
-       Return the new variable.
-
-       \remark An exception is thrown if a universe inconsistency is detected.
-    */
-    level define_uvar(name const & n, level const & l);
-    level define_uvar(name const & n) { return define_uvar(n, level()); }
-
-    /**
-       \brief Return true iff the constraint l1 >= l2 is implied by the constraints
-       in the environment.
-    */
-    bool is_ge(level const & l1, level const & l2) const;
-
-    /** \brief Display universal variables, and their constraints */
-    void display_uvars(std::ostream & out) const;
-
-    /**
-       \brief Return universal variable with the given name.
-       Throw an exception if variable is not defined in this environment.
-    */
-    level get_uvar(name const & n) const;
-
     /**
        \brief Create a child environment. This environment will only allow "read-only" operations until
        all children environments are deleted.
@@ -71,9 +49,38 @@ public:
         \pre has_parent()
     */
     environment parent() const;
+    // =======================================
 
+    // =======================================
+    // Universe variables
+    /**
+       \brief Add a new universe variable with name \c n and constraint <tt>n >= l</tt>.
+       Return the new variable.
+
+       \remark An exception is thrown if a universe inconsistency is detected.
+    */
+    level add_uvar(name const & n, level const & l);
+    level add_uvar(name const & n) { return add_uvar(n, level()); }
+
+    /**
+       \brief Return true iff the constraint l1 >= l2 is implied by the constraints
+       in the environment.
+    */
+    bool is_ge(level const & l1, level const & l2) const;
+
+    /** \brief Display universal variables, and their constraints */
+    void display_uvars(std::ostream & out) const;
+
+    /**
+       \brief Return universal variable with the given name.
+       Throw an exception if variable is not defined in this environment.
+    */
+    level get_uvar(name const & n) const;
+    // =======================================
+
+    // =======================================
+    // Environment Objects
     enum class object_kind { Definition, Theorem, Var, Axiom };
-
     /**
         \brief Base class for environment objects
         It is just a place holder at this point.
@@ -208,12 +215,16 @@ public:
 
     /** \brief Return an iterator to the end of the sequence of objects stored in this environment */
     object_iterator end_objects() const { return object_iterator(*this, get_num_objects()); }
+    // =======================================
 
+    // =======================================
+    // Pretty printing
     /** \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/tests/kernel/environment.cpp

@@ -18,8 +18,8 @@ using namespace lean;
 
 static void tst1() {
     environment env;
-    level u = env.define_uvar("u", level() + 1);
+    level u = env.add_uvar("u", level() + 1);
-    level w = env.define_uvar("w", u + 1);
+    level w = env.add_uvar("w", u + 1);
     lean_assert(!env.has_children());
     lean_assert(!env.has_parent());
     {
@@ -31,21 +31,21 @@ static void tst1() {
         lean_assert(child.has_parent());
         lean_assert(!env.has_parent());
         try {
-            level o = env.define_uvar("o", w + 1);
+            level o = env.add_uvar("o", w + 1);
             lean_unreachable();
         } catch (exception const & ex) {
             std::cout << "expected error: " << ex.what() << "\n";
         }
     }
     std::cout << "tst1 checkpoint" << std::endl;
-    level o = env.define_uvar("o", w + 1);
+    level o = env.add_uvar("o", w + 1);
     lean_assert(!env.has_children());
     env.display_uvars(std::cout);
 }
 
 static environment mk_child() {
     environment env;
-    level u = env.define_uvar("u", level() + 1);
+    level u = env.add_uvar("u", level() + 1);
     return env.mk_child();
 }
 
@@ -132,8 +132,8 @@ static void tst5() {
 
 static void tst6() {
     environment env;
-    level u = env.define_uvar("u", level() + 1);
+    level u = env.add_uvar("u", level() + 1);
-    level w = env.define_uvar("w", u + 1);
+    level w = env.add_uvar("w", u + 1);
     env.add_var("f", arrow(Type(u), Type(u)));
     expr t = Const("f")(Int);
     std::cout << "type of " << t << " is " << infer_type(t, env) << "\n";

src/tests/kernel/level.cpp

@@ -12,10 +12,10 @@ using namespace lean;
 
 static void tst1() {
     environment env;
-    level l1 = env.define_uvar(name(name("l1"), "suffix"), level());
+    level l1 = env.add_uvar(name(name("l1"), "suffix"), level());
-    level l2 = env.define_uvar("l2", l1 + 10);
+    level l2 = env.add_uvar("l2", l1 + 10);
-    level l3 = env.define_uvar("l3", max(l2, l1 + 3));
+    level l3 = env.add_uvar("l3", max(l2, l1 + 3));
-    level l4 = env.define_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20)));
+    level l4 = env.add_uvar("l4", max(l1 + 8, max(l2 + 2, l3 + 20)));
     std::cout << pp(max(l1 + 8, max(l2 + 2, l3 + 20))) << "\n";
     std::cout << pp(level()) << "\n";
     std::cout << pp(level()+1) << "\n";
@@ -26,9 +26,9 @@ static void tst1() {
 
 static void tst2() {
     environment env;
-    level l1 = env.define_uvar("l1", level());
+    level l1 = env.add_uvar("l1", level());
     try {
-        level l2 = env.define_uvar("l1", level());
+        level l2 = env.add_uvar("l1", level());
         lean_unreachable();
     }
     catch (exception ex) {
@@ -38,10 +38,10 @@ static void tst2() {
 
 static void tst3() {
     environment env;
-    level l1 = env.define_uvar("l1", level());
+    level l1 = env.add_uvar("l1", level());
-    level l2 = env.define_uvar("l2", l1 + ((1<<30) + 1024));
+    level l2 = env.add_uvar("l2", l1 + ((1<<30) + 1024));
     try {
-        level l3 = env.define_uvar("l3", l2 + (1<<30));
+        level l3 = env.add_uvar("l3", l2 + (1<<30));
         lean_unreachable();
     }
     catch (exception ex) {
@@ -51,12 +51,12 @@ static void tst3() {
 
 static void tst4() {
     environment env;
-    level l1 = env.define_uvar("l1", level() + 1);
+    level l1 = env.add_uvar("l1", level() + 1);
-    level l2 = env.define_uvar("l2", level() + 1);
+    level l2 = env.add_uvar("l2", level() + 1);
-    level l3 = env.define_uvar("l3", max(l1, l2) + 1);
+    level l3 = env.add_uvar("l3", max(l1, l2) + 1);
-    level l4 = env.define_uvar("l4", l3 + 1);
+    level l4 = env.add_uvar("l4", l3 + 1);
-    level l5 = env.define_uvar("l5", l3 + 1);
+    level l5 = env.add_uvar("l5", l3 + 1);
-    level l6 = env.define_uvar("l6", max(l4, l5) + 1);
+    level l6 = env.add_uvar("l6", max(l4, l5) + 1);
     lean_assert(!env.is_ge(l5 + 1, l6));
     lean_assert(env.is_ge(l6, l5));
     lean_assert(env.is_ge(l6, max({l1, l2, l3, l4, l5})));
@@ -79,8 +79,8 @@ static void tst4() {
 
 static void tst5() {
     environment env;
-    level l1 = env.define_uvar("l1", level() + 1);
+    level l1 = env.add_uvar("l1", level() + 1);
-    level l2 = env.define_uvar("l2", level() + 1);
+    level l2 = env.add_uvar("l2", level() + 1);
     std::cout << max(l1, l1) << "\n";
     lean_assert(max(l1, l1) == l1);
     lean_assert(max(l1+1, l1+1) == l1+1);

src/tests/kernel/type_check.cpp

@@ -25,8 +25,8 @@ static void tst1() {
     expr f = mk_pi("_", t0, t0);
     std::cout << infer_type(f, env) << "\n";
     lean_assert(infer_type(f, env) == Type(level()+1));
-    level u = env.define_uvar("u", level() + 1);
+    level u = env.add_uvar("u", level() + 1);
-    level v = env.define_uvar("v", level() + 1);
+    level v = env.add_uvar("v", level() + 1);
     expr g = mk_pi("_", Type(u), Type(v));
     std::cout << infer_type(g, env) << "\n";
     lean_assert(infer_type(g, env) == Type(max(u+1, v+1)));
@@ -48,7 +48,7 @@ static void tst1() {
 static void tst2() {
     try{
         environment env;
-        level l1      = env.define_uvar("l1", level() + 1);
+        level l1      = env.add_uvar("l1", level() + 1);
         expr t0       = Type();
         expr t1       = Type(l1);
         expr F =