From 2f88d6710cfb64411c289cdbc8a9ef49d7e5e641 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Dec 2013 10:34:38 -0800
Subject: [PATCH] feat(kernel/expr): add some_expr and none_expr for building
 values of type optional<expr>

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/frontend.cpp               |  4 ++--
 src/frontends/lean/frontend_elaborator.cpp    | 24 +++++++++----------
 src/frontends/lean/parser.cpp                 |  4 ++--
 src/frontends/lean/pp.cpp                     |  8 +++----
 src/kernel/builtin.cpp                        |  8 +++----
 src/kernel/expr.cpp                           |  2 +-
 src/kernel/expr.h                             | 12 ++++++----
 src/kernel/find_fn.h                          |  2 +-
 src/kernel/justification.cpp                  |  2 +-
 src/kernel/justification.h                    |  4 ++--
 src/kernel/kernel_exception.h                 | 18 +++++++-------
 src/kernel/metavar.cpp                        | 10 ++++----
 src/kernel/metavar.h                          |  4 ++--
 src/kernel/replace_fn.h                       |  4 ++--
 src/kernel/replace_visitor.cpp                |  4 ++--
 src/kernel/type_checker_justification.cpp     | 10 ++++----
 src/library/arith/int.cpp                     | 12 +++++-----
 src/library/arith/nat.cpp                     |  8 +++----
 src/library/arith/real.cpp                    | 12 +++++-----
 src/library/cast/cast.cpp                     | 14 +++++------
 src/library/context_to_lambda.cpp             |  8 +++----
 src/library/deep_copy.cpp                     |  2 +-
 .../elaborator/elaborator_justification.cpp   |  6 ++---
 src/library/kernel_bindings.cpp               |  4 ++--
 src/library/max_sharing.cpp                   |  2 +-
 src/library/placeholder.h                     |  2 +-
 src/library/tactic/apply_tactic.cpp           |  8 +++----
 src/library/tactic/goal.cpp                   |  8 +++----
 src/library/tactic/tactic.cpp                 |  4 ++--
 src/tests/kernel/expr.cpp                     |  4 ++--
 src/tests/kernel/normalizer.cpp               |  2 +-
 src/tests/kernel/type_checker.cpp             |  4 ++--
 src/tests/library/update_expr.cpp             |  4 ++--
 33 files changed, 114 insertions(+), 110 deletions(-)

diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index d17f787a5..407711bf3 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -319,12 +319,12 @@ struct lean_extension : public environment::extension {
         expr_pair p(from_type, to_type);
         auto it = m_coercion_map.find(p);
         if (it != m_coercion_map.end())
-            return optional<expr>(it->second);
+            return some_expr(it->second);
         lean_extension const * parent = get_parent();
         if (parent)
             return parent->get_coercion(from_type, to_type);
         else
-            return optional<expr>();
+            return none_expr();
     }
 
     list<expr_pair> get_coercions(expr const & from_type) const {
diff --git a/src/frontends/lean/frontend_elaborator.cpp b/src/frontends/lean/frontend_elaborator.cpp
index f2b9782c9..766982723 100644
--- a/src/frontends/lean/frontend_elaborator.cpp
+++ b/src/frontends/lean/frontend_elaborator.cpp
@@ -63,7 +63,7 @@ public:
         return r;
     }
     virtual void get_children(buffer<justification_cell*> &) const {}
-    virtual optional<expr> get_main_expr() const { return some(m_src); }
+    virtual optional<expr> get_main_expr() const { return some_expr(m_src); }
     context const & get_context() const { return m_ctx; }
 };
 
@@ -82,7 +82,7 @@ public:
         return r;
     }
     virtual void get_children(buffer<justification_cell*> &) const {}
-    virtual optional<expr> get_main_expr() const { return some(m_app); }
+    virtual optional<expr> get_main_expr() const { return some_expr(m_app); }
     context const & get_context() const { return m_ctx; }
     expr const & get_app() const { return m_app; }
 };
@@ -138,14 +138,14 @@ class frontend_elaborator::imp {
         */
         optional<expr> get_type(expr const & e, context const & ctx) {
             try {
-                return some(m_ref.m_type_inferer(e, ctx));
+                return some_expr(m_ref.m_type_inferer(e, ctx));
             } catch (exception &) {
-                return optional<expr>();
+                return none_expr();
             }
         }
 
         /**
-           \brief Make sure f_t is a Pi, if it is not, then return optional<expr>()
+           \brief Make sure f_t is a Pi, if it is not, then return none_expr()
         */
         optional<expr> check_pi(optional<expr> const & f_t, context const & ctx) {
             if (!f_t || is_pi(*f_t)) {
@@ -153,9 +153,9 @@ class frontend_elaborator::imp {
             } else {
                 expr r = m_ref.m_normalizer(*f_t, ctx);
                 if (is_pi(r))
-                    return optional<expr>(r);
+                    return some_expr(r);
                 else
-                    return optional<expr>();
+                    return none_expr();
             }
         }
 
@@ -176,10 +176,10 @@ class frontend_elaborator::imp {
         optional<expr> find_coercion(list<expr_pair> const & l, expr const & to_type) {
             for (auto p : l) {
                 if (p.first == to_type) {
-                    return optional<expr>(p.second);
+                    return some_expr(p.second);
                 }
             }
-            return optional<expr>();
+            return none_expr();
         }
 
         /**
@@ -225,7 +225,7 @@ class frontend_elaborator::imp {
                                 num_skipped_args++;
                             }
                         }
-                        f_t = some(::lean::instantiate(abst_body(*f_t), args[i]));
+                        f_t = some_expr(::lean::instantiate(abst_body(*f_t), args[i]));
                     }
                 }
                 if (i == num_args) {
@@ -279,7 +279,7 @@ class frontend_elaborator::imp {
             buffer<expr>   args;
             buffer<optional<expr>> arg_types;
             args.push_back(expr());      // placeholder
-            arg_types.push_back(optional<expr>()); // placeholder
+            arg_types.push_back(none_expr()); // placeholder
             for (unsigned i = 1; i < num_args(e); i++) {
                 expr a = arg(e, i);
                 expr new_a   = visit(a, ctx);
@@ -347,7 +347,7 @@ class frontend_elaborator::imp {
                 }
                 new_args.push_back(new_a);
                 if (f_t)
-                    f_t = some(::lean::instantiate(abst_body(*f_t), new_a));
+                    f_t = some_expr(::lean::instantiate(abst_body(*f_t), new_a));
             }
             return mk_app(new_args);
         }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 42caf0de6..7daa8bcc7 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -348,7 +348,7 @@ class parser::imp {
     void display_error(kernel_exception const & ex) {
         optional<expr> main_expr = ex.get_main_expr();
         if (main_expr)
-            display_error_pos(some(m_elaborator.get_original(*main_expr)));
+            display_error_pos(some_expr(m_elaborator.get_original(*main_expr)));
         else
             display_error_pos(main_expr);
         regular(m_frontend) << " " << ex << endl;
@@ -1185,7 +1185,7 @@ class parser::imp {
         expr t = parse_expr();
         check_next(scanner::token::By, "invalid 'show _ by _' expression, 'by' expected");
         tactic tac = parse_tactic_expr();
-        expr r = mk_placeholder(optional<expr>(t));
+        expr r = mk_placeholder(some_expr(t));
         m_tactic_hints[r] = tac;
         return save(r, p);
     }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index d215c87f2..d14561244 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -732,7 +732,7 @@ class pp_fn {
             r.emplace_back(n1, abst_domain(e));
             expr b = replace_var_with_name(abst_body(e), n1);
             if (T)
-                T = some(replace_var_with_name(abst_body(*T), n1));
+                T = some_expr(replace_var_with_name(abst_body(*T), n1));
             return collect_nested(b, T, k, r);
         } else {
             return mk_pair(e, T);
@@ -957,7 +957,7 @@ class pp_fn {
     }
 
     result pp_abstraction(expr const & e, unsigned depth) {
-        return pp_abstraction_core(e, depth, optional<expr>());
+        return pp_abstraction_core(e, depth, none_expr());
     }
 
     expr collect_nested_let(expr const & e, buffer<std::tuple<name, optional<expr>, expr>> & bindings) {
@@ -1166,12 +1166,12 @@ public:
 
     format pp_definition(expr const & v, expr const & t, std::vector<bool> const * implicit_args) {
         init(mk_app(v, t));
-        return pp_abstraction_core(v, 0, optional<expr>(t), implicit_args).first;
+        return pp_abstraction_core(v, 0, some_expr(t), implicit_args).first;
     }
 
     format pp_pi_with_implicit_args(expr const & e, std::vector<bool> const & implicit_args) {
         init(e);
-        return pp_abstraction_core(e, 0, optional<expr>(), &implicit_args).first;
+        return pp_abstraction_core(e, 0, none_expr(), &implicit_args).first;
     }
 
     void register_local(name const & n) {
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 39144c71d..b2da2e1a4 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -139,13 +139,13 @@ public:
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 5 && is_bool_value(args[2])) {
             if (to_bool(args[2]))
-                return some(args[3]); // if A true a b  --> a
+                return some_expr(args[3]); // if A true a b  --> a
             else
-                return some(args[4]); // if A false a b --> b
+                return some_expr(args[4]); // if A false a b --> b
         } else if (num_args == 5 && args[3] == args[4]) {
-            return some(args[3]);     // if A c a a --> a
+            return some_expr(args[3]);     // if A c a a --> a
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index e22326fcd..9d826f0ad 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -164,7 +164,7 @@ void expr_let::dealloc(buffer<expr_cell*> & todelete) {
 }
 expr_let::~expr_let() {}
 name value::get_unicode_name() const { return get_name(); }
-optional<expr> value::normalize(unsigned, expr const *) const { return optional<expr>(); }
+optional<expr> value::normalize(unsigned, expr const *) const { return none_expr(); }
 void value::display(std::ostream & out) const { out << get_name(); }
 bool value::operator==(value const & other) const { return typeid(*this) == typeid(other); }
 bool value::operator<(value const & other) const {
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 1f8594cf9..d5af9d137 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -155,6 +155,10 @@ inline bool operator!=(expr const & a, expr const & b) { return !operator==(a, b
 
 SPECIALIZE_OPTIONAL_FOR_SMART_PTR(expr)
 
+inline optional<expr> none_expr() { return optional<expr>(); }
+inline optional<expr> some_expr(expr const & e) { return optional<expr>(e); }
+inline optional<expr> some_expr(expr && e) { return optional<expr>(std::forward<expr>(e)); }
+
 inline bool is_eqp(optional<expr> const & a, optional<expr> const & b) {
     return static_cast<bool>(a) == static_cast<bool>(b) && (!a || is_eqp(*a, *b));
 }
@@ -394,8 +398,8 @@ inline bool is_abstraction(expr const & e) { return is_lambda(e) || is_pi(e); }
 inline expr mk_var(unsigned idx) { return expr(new expr_var(idx)); }
 inline expr Var(unsigned idx) { return mk_var(idx); }
 inline expr mk_constant(name const & n, optional<expr> const & t) { return expr(new expr_const(n, t)); }
-inline expr mk_constant(name const & n, expr const & t) { return mk_constant(n, optional<expr>(t)); }
-inline expr mk_constant(name const & n) { return mk_constant(n, optional<expr>()); }
+inline expr mk_constant(name const & n, expr const & t) { return mk_constant(n, some_expr(t)); }
+inline expr mk_constant(name const & n) { return mk_constant(n, none_expr()); }
 inline expr Const(name const & n) { return mk_constant(n); }
 inline expr mk_value(value & v) { return expr(new expr_value(v)); }
 inline expr to_expr(value & v) { return mk_value(v); }
@@ -413,8 +417,8 @@ inline expr mk_pi(name const & n, expr const & t, expr const & e) { return expr(
 inline expr mk_arrow(expr const & t, expr const & e) { return mk_pi(name("_"), t, e); }
 inline expr operator>>(expr const & t, expr const & e) { return mk_arrow(t, e); }
 inline expr mk_let(name const & n, optional<expr> const & t, expr const & v, expr const & e) { return expr(new expr_let(n, t, v, e)); }
-inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return mk_let(n, optional<expr>(t), v, e); }
-inline expr mk_let(name const & n, expr const & v, expr const & e) { return mk_let(n, optional<expr>(), v, e); }
+inline expr mk_let(name const & n, expr const & t, expr const & v, expr const & e) { return mk_let(n, some_expr(t), v, e); }
+inline expr mk_let(name const & n, expr const & v, expr const & e) { return mk_let(n, none_expr(), v, e); }
 inline expr mk_type(level const & l) { return expr(new expr_type(l)); }
        expr mk_type();
 inline expr Type(level const & l) { return mk_type(l); }
diff --git a/src/kernel/find_fn.h b/src/kernel/find_fn.h
index 6071d9bf7..d5e566912 100644
--- a/src/kernel/find_fn.h
+++ b/src/kernel/find_fn.h
@@ -65,6 +65,6 @@ optional<expr> find(context const * c, unsigned sz, expr const * es, P p) {
         if (optional<expr> r = finder(es[i]))
             return r;
     }
-    return optional<expr>();
+    return none_expr();
 }
 }
diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp
index 3fe51a28f..559009175 100644
--- a/src/kernel/justification.cpp
+++ b/src/kernel/justification.cpp
@@ -42,7 +42,7 @@ bool justification::has_children() const {
 
 assumption_justification::assumption_justification(unsigned idx):m_idx(idx) {}
 void assumption_justification::get_children(buffer<justification_cell*> &) const {}
-optional<expr> assumption_justification::get_main_expr() const { return optional<expr>(); }
+optional<expr> assumption_justification::get_main_expr() const { return none_expr(); }
 format assumption_justification::pp_header(formatter const &, options const &) const {
     return format{format("Assumption"), space(), format(m_idx)};
 }
diff --git a/src/kernel/justification.h b/src/kernel/justification.h
index 447281099..e59ba7241 100644
--- a/src/kernel/justification.h
+++ b/src/kernel/justification.h
@@ -33,7 +33,7 @@ public:
     virtual format pp_header(formatter const & fmt, options const & opts) const = 0;
     virtual format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, bool display_children) const;
     virtual void get_children(buffer<justification_cell*> & r) const = 0;
-    virtual optional<expr> get_main_expr() const { return optional<expr>(); }
+    virtual optional<expr> get_main_expr() const { return none_expr(); }
     bool is_shared() const { return get_rc() > 1; }
 };
 
@@ -73,7 +73,7 @@ public:
         lean_assert(m_ptr);
         return m_ptr->pp(fmt, opts, p, display_children);
     }
-    optional<expr> get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : optional<expr>(); }
+    optional<expr> get_main_expr() const { return m_ptr ? m_ptr->get_main_expr() : none_expr(); }
     void get_children(buffer<justification_cell*> & r) const { if (m_ptr) m_ptr->get_children(r); }
     bool has_children() const;
 };
diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h
index 3e89845ed..32dc19754 100644
--- a/src/kernel/kernel_exception.h
+++ b/src/kernel/kernel_exception.h
@@ -27,7 +27,7 @@ public:
         \brief Return a reference (if available) to the main expression associated with this exception.
         This information is used to provide better error messages.
     */
-    virtual optional<expr> get_main_expr() const { return optional<expr>(); }
+    virtual optional<expr> get_main_expr() const { return none_expr(); }
     virtual format pp(formatter const & fmt, options const & opts) const;
     virtual exception * clone() const { return new kernel_exception(m_env, m_msg.c_str()); }
     virtual void rethrow() const { throw *this; }
@@ -106,7 +106,7 @@ class has_no_type_exception : public type_checker_exception {
 public:
     has_no_type_exception(environment const & env, expr const & c):type_checker_exception(env), m_const(c) {}
     virtual ~has_no_type_exception() {}
-    virtual optional<expr> get_main_expr() const { return some(m_const); }
+    virtual optional<expr> get_main_expr() const { return some_expr(m_const); }
     virtual char const * what() const noexcept { return "object does not have a type associated with it"; }
     virtual format pp(formatter const & fmt, options const & opts) const;
     virtual exception * clone() const { return new has_no_type_exception(m_env, m_const); }
@@ -133,7 +133,7 @@ public:
     virtual ~app_type_mismatch_exception() {}
     context const & get_context() const { return m_context; }
     expr const & get_application() const { return m_app; }
-    virtual optional<expr> get_main_expr() const { return some(get_application()); }
+    virtual optional<expr> get_main_expr() const { return some_expr(get_application()); }
     std::vector<expr> const & get_arg_types() const { return m_arg_types; }
     virtual char const * what() const noexcept { return "application argument type mismatch"; }
     virtual format pp(formatter const & fmt, options const & opts) const;
@@ -158,7 +158,7 @@ public:
     virtual ~function_expected_exception() {}
     context const & get_context() const { return m_context; }
     expr const & get_expr() const { return m_expr; }
-    virtual optional<expr> get_main_expr() const { return some(get_expr()); }
+    virtual optional<expr> get_main_expr() const { return some_expr(get_expr()); }
     virtual char const * what() const noexcept { return "function expected"; }
     virtual format pp(formatter const & fmt, options const & opts) const;
     virtual exception * clone() const { return new function_expected_exception(m_env, m_context, m_expr); }
@@ -182,7 +182,7 @@ public:
     virtual ~type_expected_exception() {}
     context const & get_context() const { return m_context; }
     expr const & get_expr() const { return m_expr; }
-    virtual optional<expr> get_main_expr() const { return some(get_expr()); }
+    virtual optional<expr> get_main_expr() const { return some_expr(get_expr()); }
     virtual char const * what() const noexcept { return "type expected"; }
     virtual format pp(formatter const & fmt, options const & opts) const;
     virtual exception * clone() const { return new type_expected_exception(m_env, m_context, m_expr); }
@@ -218,7 +218,7 @@ public:
     expr const & get_type() const { return m_type; }
     expr const & get_value() const { return m_value; }
     expr const & get_value_type() const { return m_value_type; }
-    virtual optional<expr> get_main_expr() const { return some(m_value); }
+    virtual optional<expr> get_main_expr() const { return some_expr(m_value); }
     virtual char const * what() const noexcept { return "definition type mismatch"; }
     virtual format pp(formatter const & fmt, options const & opts) const;
     virtual exception * clone() const { return new def_type_mismatch_exception(m_env, m_context, m_name, m_type, m_value, m_value_type); }
@@ -234,7 +234,7 @@ 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"; }
-    virtual optional<expr> get_main_expr() const { return some(m_expr); }
+    virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
     virtual exception * clone() const { return new invalid_builtin_value_declaration(m_env, m_expr); }
     virtual void rethrow() const { throw *this; }
 };
@@ -249,7 +249,7 @@ 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"; }
-    virtual optional<expr> get_main_expr() const { return some(m_expr); }
+    virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
     virtual exception * clone() const { return new invalid_builtin_value_reference(m_env, m_expr); }
     virtual void rethrow() const { throw *this; }
 };
@@ -263,7 +263,7 @@ public:
     unexpected_metavar_occurrence(environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
     virtual ~unexpected_metavar_occurrence() {}
     virtual char const * what() const noexcept { return "unexpected metavariable occurrence"; }
-    virtual optional<expr> get_main_expr() const { return some(m_expr); }
+    virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
     virtual exception * clone() const { return new unexpected_metavar_occurrence(m_env, m_expr); }
     virtual void rethrow() const { throw *this; }
 };
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 20907e234..905e2b09c 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -48,7 +48,7 @@ public:
         append(r, m_jsts);
     }
 
-    virtual optional<expr> get_main_expr() const { return some(m_expr); }
+    virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
 };
 
 void swap(metavar_env & a, metavar_env & b) {
@@ -227,17 +227,17 @@ optional<std::pair<expr, justification>> metavar_env::get_subst_jst(name const &
 optional<expr> metavar_env::get_subst(name const & m) const {
     auto r = get_subst_jst(m);
     if (r)
-        return optional<expr>(r->first);
+        return some_expr(r->first);
     else
-        return optional<expr>();
+        return none_expr();
 }
 
 optional<expr> metavar_env::get_subst(expr const & m) const {
     auto r = get_subst_jst(m);
     if (r)
-        return optional<expr>(r->first);
+        return some_expr(r->first);
     else
-        return optional<expr>();
+        return none_expr();
 }
 
 class instantiate_metavars_proc : public replace_visitor {
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index fa01c349d..6b47b0c15 100644
--- a/src/kernel/metavar.h
+++ b/src/kernel/metavar.h
@@ -29,7 +29,7 @@ class metavar_env {
         optional<expr> m_type;          // type of the metavariable
         context        m_context;       // context where the metavariable was defined
         justification  m_justification; // justification for assigned metavariables.
-        data(optional<expr> const & t = optional<expr>(), context const & ctx = context()):m_type(t), m_context(ctx) {}
+        data(optional<expr> const & t = none_expr(), context const & ctx = context()):m_type(t), m_context(ctx) {}
     };
     typedef splay_map<name, data, name_quick_cmp> name2data;
 
@@ -62,7 +62,7 @@ public:
     /**
        \brief Create a new metavariable in the given context and with the given type.
     */
-    expr mk_metavar(context const & ctx = context(), optional<expr> const & type = optional<expr>());
+    expr mk_metavar(context const & ctx = context(), optional<expr> const & type = none_expr());
 
     /**
        \brief Return the context where the given metavariable was created.
diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h
index b90753a31..aaac21770 100644
--- a/src/kernel/replace_fn.h
+++ b/src/kernel/replace_fn.h
@@ -49,9 +49,9 @@ class replace_fn {
 
     optional<expr> apply(optional<expr> const & e, unsigned offset) {
         if (e)
-            return optional<expr>(apply(*e, offset));
+            return some_expr(apply(*e, offset));
         else
-            return optional<expr>();
+            return none_expr();
     }
 
     expr apply(expr const & e, unsigned offset) {
diff --git a/src/kernel/replace_visitor.cpp b/src/kernel/replace_visitor.cpp
index 1e962ce31..07a4ef370 100644
--- a/src/kernel/replace_visitor.cpp
+++ b/src/kernel/replace_visitor.cpp
@@ -89,8 +89,8 @@ expr replace_visitor::visit(expr const & e, context const & ctx) {
 }
 optional<expr> replace_visitor::visit(optional<expr> const & e, context const & ctx) {
     if (e)
-        return some(visit(*e, ctx));
+        return some_expr(visit(*e, ctx));
     else
-        return optional<expr>();
+        return none_expr();
 }
 }
diff --git a/src/kernel/type_checker_justification.cpp b/src/kernel/type_checker_justification.cpp
index da70ac680..e46056176 100644
--- a/src/kernel/type_checker_justification.cpp
+++ b/src/kernel/type_checker_justification.cpp
@@ -24,7 +24,7 @@ void function_expected_justification_cell::get_children(buffer<justification_cel
 }
 
 optional<expr> function_expected_justification_cell::get_main_expr() const {
-    return some(m_app);
+    return some_expr(m_app);
 }
 
 app_type_match_justification_cell::~app_type_match_justification_cell() {
@@ -52,7 +52,7 @@ void app_type_match_justification_cell::get_children(buffer<justification_cell*>
 }
 
 optional<expr> app_type_match_justification_cell::get_main_expr() const {
-    return some(m_app);
+    return some_expr(m_app);
 }
 
 type_expected_justification_cell::~type_expected_justification_cell() {
@@ -71,7 +71,7 @@ void type_expected_justification_cell::get_children(buffer<justification_cell*>
 }
 
 optional<expr> type_expected_justification_cell::get_main_expr() const {
-    return some(m_type);
+    return some_expr(m_type);
 }
 
 def_type_match_justification_cell::~def_type_match_justification_cell() {
@@ -89,7 +89,7 @@ void def_type_match_justification_cell::get_children(buffer<justification_cell*>
 }
 
 optional<expr> def_type_match_justification_cell::get_main_expr() const {
-    return some(m_value);
+    return some_expr(m_value);
 }
 
 type_match_justification_cell::~type_match_justification_cell() {
@@ -103,6 +103,6 @@ void type_match_justification_cell::get_children(buffer<justification_cell*> &)
 }
 
 optional<expr> type_match_justification_cell::get_main_expr() const {
-    return some(m_value);
+    return some_expr(m_value);
 }
 }
diff --git a/src/library/arith/int.cpp b/src/library/arith/int.cpp
index cd7dd3b00..5de8b87dd 100644
--- a/src/library/arith/int.cpp
+++ b/src/library/arith/int.cpp
@@ -74,9 +74,9 @@ public:
     int_bin_op():const_value(name("Int", Name), Int >> (Int >> Int)) {}
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
-            return some(mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2]))));
+            return some_expr(mk_int_value(F()(int_value_numeral(args[1]), int_value_numeral(args[2]))));
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
@@ -108,9 +108,9 @@ public:
     int_le_value():const_value(name{"Int", "le"}, Int >> (Int >> Bool)) {}
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 3 && is_int_value(args[1]) && is_int_value(args[2])) {
-            return some(mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2])));
+            return some_expr(mk_bool_value(int_value_numeral(args[1]) <= int_value_numeral(args[2])));
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
@@ -133,9 +133,9 @@ public:
     nat_to_int_value():const_value("nat_to_int", Nat >> Int) {}
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 2 && is_nat_value(args[1])) {
-            return some(mk_int_value(nat_value_numeral(args[1])));
+            return some_expr(mk_int_value(nat_value_numeral(args[1])));
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
diff --git a/src/library/arith/nat.cpp b/src/library/arith/nat.cpp
index a96549b4d..3f0837eaf 100644
--- a/src/library/arith/nat.cpp
+++ b/src/library/arith/nat.cpp
@@ -68,9 +68,9 @@ public:
     nat_bin_op():const_value(name("Nat", Name), Nat >> (Nat >> Nat)) {}
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
-            return some(mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2]))));
+            return some_expr(mk_nat_value(F()(nat_value_numeral(args[1]), nat_value_numeral(args[2]))));
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
@@ -96,9 +96,9 @@ public:
     nat_le_value():const_value(name{"Nat", "le"}, Nat >> (Nat >> Bool)) {}
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 3 && is_nat_value(args[1]) && is_nat_value(args[2])) {
-            return some(mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2])));
+            return some_expr(mk_bool_value(nat_value_numeral(args[1]) <= nat_value_numeral(args[2])));
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
diff --git a/src/library/arith/real.cpp b/src/library/arith/real.cpp
index 6ed5b8952..eaa074b21 100644
--- a/src/library/arith/real.cpp
+++ b/src/library/arith/real.cpp
@@ -77,9 +77,9 @@ public:
     real_bin_op():const_value(name("Real", Name), Real >> (Real >> Real)) {}
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
-            return some(mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2]))));
+            return some_expr(mk_real_value(F()(real_value_numeral(args[1]), real_value_numeral(args[2]))));
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
@@ -118,9 +118,9 @@ public:
     real_le_value():const_value(name{"Real", "le"}, Real >> (Real >> Bool)) {}
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 3 && is_real_value(args[1]) && is_real_value(args[2])) {
-            return some(mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2])));
+            return some_expr(mk_bool_value(real_value_numeral(args[1]) <= real_value_numeral(args[2])));
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
@@ -167,9 +167,9 @@ public:
     int_to_real_value():const_value("int_to_real", Int >> Real) {}
     virtual optional<expr> normalize(unsigned num_args, expr const * args) const {
         if (num_args == 2 && is_int_value(args[1])) {
-            return some(mk_real_value(mpq(int_value_numeral(args[1]))));
+            return some_expr(mk_real_value(mpq(int_value_numeral(args[1]))));
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
diff --git a/src/library/cast/cast.cpp b/src/library/cast/cast.cpp
index 6fadb8eeb..7348c3728 100644
--- a/src/library/cast/cast.cpp
+++ b/src/library/cast/cast.cpp
@@ -31,9 +31,9 @@ public:
         if (num_as > 4 && as[1] == as[2]) {
             // Cast T T H a == a
             if (num_as == 5)
-                return some(as[4]);
+                return some_expr(as[4]);
             else
-                return some(mk_app(num_as - 4, as + 4));
+                return some_expr(mk_app(num_as - 4, as + 4));
         } else if (is_app(as[4]) &&
                    arg(as[4], 0) == mk_Cast_fn() &&
                    num_args(as[4]) == 5 &&
@@ -48,12 +48,12 @@ public:
             expr const & a  = arg(nested, 4);
             expr c = Cast(T3, T2, Trans(TypeU, T3, T1, T2, H1, H2), a);
             if (num_as == 5) {
-                return optional<expr>(c);
+                return some_expr(c);
             } else {
                 buffer<expr> new_as;
                 new_as.push_back(c);
                 new_as.append(num_as - 5, as + 5);
-                return optional<expr>(mk_app(new_as));
+                return some_expr(mk_app(new_as));
             }
         } else if (num_as > 5 && is_pi(as[1]) && is_pi(as[2])) {
             // cast T1 T2 H f a_1 ... a_k
@@ -84,15 +84,15 @@ public:
             expr B1_eq_B2_at_a_1p = RanInj(A1, A2, B1f, B2f, H, a_1p);
             expr fa_1_B2     = Cast(B1, B2, B1_eq_B2_at_a_1p, fa_1);
             if (num_as == 6) {
-                return optional<expr>(fa_1_B2);
+                return some_expr(fa_1_B2);
             } else {
                 buffer<expr> new_as;
                 new_as.push_back(fa_1_B2);
                 new_as.append(num_as - 6, as + 6);
-                return optional<expr>(mk_app(new_as));
+                return some_expr(mk_app(new_as));
             }
         } else {
-            return optional<expr>();
+            return none_expr();
         }
     }
 };
diff --git a/src/library/context_to_lambda.cpp b/src/library/context_to_lambda.cpp
index 04507e58f..6d234e1af 100644
--- a/src/library/context_to_lambda.cpp
+++ b/src/library/context_to_lambda.cpp
@@ -41,17 +41,17 @@ optional<expr> fake_context_domain(expr const & e) {
     lean_assert(is_fake_context(e));
     expr r = arg(abst_domain(e), 1);
     if (!is_eqp(r, g_fake))
-        return optional<expr>(r);
+        return some_expr(r);
     else
-        return optional<expr>();
+        return none_expr();
 }
 optional<expr> fake_context_value(expr const & e) {
     lean_assert(is_fake_context(e));
     expr r = arg(abst_domain(e), 2);
     if (!is_eqp(r, g_fake))
-        return optional<expr>(r);
+        return some_expr(r);
     else
-        return optional<expr>();
+        return none_expr();
 }
 expr const & fake_context_rest(expr const & e) {
     return abst_body(e);
diff --git a/src/library/deep_copy.cpp b/src/library/deep_copy.cpp
index 4e9cc3ffd..3b8d180b6 100644
--- a/src/library/deep_copy.cpp
+++ b/src/library/deep_copy.cpp
@@ -21,7 +21,7 @@ class deep_copy_fn {
 
     optional<expr> apply(optional<expr> const & a) {
         if (a)
-            return some(apply(*a));
+            return some_expr(apply(*a));
         else
             return a;
     }
diff --git a/src/library/elaborator/elaborator_justification.cpp b/src/library/elaborator/elaborator_justification.cpp
index 51fb95445..dc803db4d 100644
--- a/src/library/elaborator/elaborator_justification.cpp
+++ b/src/library/elaborator/elaborator_justification.cpp
@@ -19,7 +19,7 @@ void propagation_justification::get_children(buffer<justification_cell*> & r) co
     push_back(r, m_constraint.get_justification());
 }
 optional<expr> propagation_justification::get_main_expr() const {
-    return optional<expr>();
+    return none_expr();
 }
 format propagation_justification::pp_header(formatter const & fmt, options const & opts) const {
     format r;
@@ -121,7 +121,7 @@ void synthesis_justification::get_children(buffer<justification_cell*> & r) cons
     append(r, m_substitution_justifications);
 }
 optional<expr> synthesis_justification::get_main_expr() const {
-    return some(m_mvar);
+    return some_expr(m_mvar);
 }
 
 char const * synthesis_failure_justification::get_label() const {
@@ -157,6 +157,6 @@ void next_solution_justification::get_children(buffer<justification_cell*> & r)
     append(r, m_assumptions);
 }
 optional<expr> next_solution_justification::get_main_expr() const {
-    return optional<expr>();
+    return none_expr();
 }
 }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 18c6dab64..9b2dacaf3 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -740,7 +740,7 @@ static int mk_context(lua_State * L) {
         return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3)));
     } else {
         if (lua_isnil(L, 3))
-            return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), optional<expr>(), to_expr(L, 4)));
+            return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), none_expr(), to_expr(L, 4)));
         else
             return push_context(L, context(to_context(L, 1), to_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4)));
     }
@@ -1445,7 +1445,7 @@ static int menv_mk_metavar(lua_State * L) {
     } else if (nargs == 2) {
         return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2)));
     } else {
-        return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2), optional<expr>(to_expr(L, 3))));
+        return push_expr(L, to_metavar_env(L, 1).mk_metavar(to_context(L, 2), some_expr(to_expr(L, 3))));
     }
 }
 
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index 50d0d3858..a09546a9a 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -27,7 +27,7 @@ struct max_sharing_fn::imp {
 
     optional<expr> apply(optional<expr> const & a) {
         if (a)
-            return some(apply(*a));
+            return some_expr(apply(*a));
         else
             return a;
     }
diff --git a/src/library/placeholder.h b/src/library/placeholder.h
index 443c57d18..b73d2f498 100644
--- a/src/library/placeholder.h
+++ b/src/library/placeholder.h
@@ -15,7 +15,7 @@ class metavar_env;
     type). To be able to track location, a new constant for each
     placeholder.
 */
-expr mk_placeholder(optional<expr> const & t = optional<expr>());
+expr mk_placeholder(optional<expr> const & t = none_expr());
 
 /**
     \brief Return true iff the given expression is a placeholder.
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp
index c04f78b95..691a4d666 100644
--- a/src/library/tactic/apply_tactic.cpp
+++ b/src/library/tactic/apply_tactic.cpp
@@ -66,21 +66,21 @@ static optional<proof_state> apply_tactic(environment const & env, proof_state c
                 for (auto const & mvar : mvars) {
                     expr mvar_sol = apply(*subst, mvar);
                     if (mvar_sol != mvar) {
-                        l = cons(mk_pair(optional<expr>(mvar_sol), name()), l);
+                        l = cons(mk_pair(some_expr(mvar_sol), name()), l);
                         th_type_c = instantiate(abst_body(th_type_c), mvar_sol);
                     } else {
                         if (inferer.is_proposition(abst_domain(th_type_c), context(), &new_menv)) {
                             name new_gname(gname, new_goal_idx);
                             new_goal_idx++;
-                            l = cons(mk_pair(optional<expr>(), new_gname), l);
+                            l = cons(mk_pair(none_expr(), new_gname), l);
                             new_goals_buf.emplace_back(new_gname, update(g, abst_domain(th_type_c)));
                             th_type_c = instantiate(abst_body(th_type_c), mk_constant(new_gname, abst_domain(th_type_c)));
                         } else {
                             // we have to create a new metavar in menv
                             // since we do not have a substitution for mvar, and
                             // it is not a proposition
-                            expr new_m = new_menv.mk_metavar(context(), optional<expr>(abst_domain(th_type_c)));
-                            l = cons(mk_pair(optional<expr>(new_m), name()), l);
+                            expr new_m = new_menv.mk_metavar(context(), some_expr(abst_domain(th_type_c)));
+                            l = cons(mk_pair(some_expr(new_m), name()), l);
                             // we use instantiate_with_closed_relaxed because we do not want
                             // to introduce a lift operator in the new_m
                             th_type_c = instantiate_with_closed_relaxed(abst_body(th_type_c), 1, &new_m);
diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index fdf9c1ebf..f66d069b7 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -136,10 +136,10 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
         name n = mk_unique_name(used_names, e.get_name());
         optional<expr> d = e.get_domain();
         optional<expr> b = e.get_body();
-        if (d) d = some(replacer(*d));
-        if (b) b = some(replacer(*b));
+        if (d) d = some_expr(replacer(*d));
+        if (b) b = some_expr(replacer(*b));
         if (b && !d) {
-            d = some(inferer(*b));
+            d = some_expr(inferer(*b));
         }
         replacer.clear();
         if (b && !inferer.is_proposition(*d)) {
@@ -148,7 +148,7 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
         } else {
             lean_assert(d);
             hypotheses.emplace_back(n, *d);
-            bodies.push_back(optional<expr>());
+            bodies.push_back(none_expr());
             consts.push_back(mk_constant(n, *d));
         }
     }
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 680135230..6f21f9a7d 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -76,11 +76,11 @@ optional<expr> to_proof(proof_state const & s) {
         try {
             assignment a(s.get_menv());
             proof_map  m;
-            return some(s.get_proof_builder()(m, a));
+            return some_expr(s.get_proof_builder()(m, a));
         } catch (...) {
         }
     }
-    return optional<expr>();
+    return none_expr();
 }
 
 /**
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index fa83c7ea2..a34e0c388 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -278,7 +278,7 @@ static void tst13() {
 static void tst14() {
     expr t = Eq(Const("a"), Const("b"));
     std::cout << t << "\n";
-    expr l = mk_let("a", optional<expr>(), Const("b"), Var(0));
+    expr l = mk_let("a", none_expr(), Const("b"), Var(0));
     std::cout << l << "\n";
     lean_assert(closed(l));
 }
@@ -327,7 +327,7 @@ static void tst16() {
     check_copy(mk_metavar("M"));
     check_copy(mk_lambda("x", a, Var(0)));
     check_copy(mk_pi("x", a, Var(0)));
-    check_copy(mk_let("x", optional<expr>(), a, Var(0)));
+    check_copy(mk_let("x", none_expr(), a, Var(0)));
 }
 
 static void tst17() {
diff --git a/src/tests/kernel/normalizer.cpp b/src/tests/kernel/normalizer.cpp
index af7d07ecd..b36468979 100644
--- a/src/tests/kernel/normalizer.cpp
+++ b/src/tests/kernel/normalizer.cpp
@@ -200,7 +200,7 @@ static void tst3() {
 static void tst4() {
     environment env;
     env.add_var("b", Type());
-    expr t1 = mk_let("a", optional<expr>(), Const("b"), mk_lambda("c", Type(), Var(1)(Var(0))));
+    expr t1 = mk_let("a", none_expr(), Const("b"), mk_lambda("c", Type(), Var(1)(Var(0))));
     std::cout << t1 << " --> " << normalize(t1, env) << "\n";
     lean_assert(normalize(t1, env) == mk_lambda("c", Type(), Const("b")(Var(0))));
 }
diff --git a/src/tests/kernel/type_checker.cpp b/src/tests/kernel/type_checker.cpp
index 7b28acbe3..2434cf2a6 100644
--- a/src/tests/kernel/type_checker.cpp
+++ b/src/tests/kernel/type_checker.cpp
@@ -82,7 +82,7 @@ static void tst3() {
     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));
-    expr t = mk_let("a", optional<expr>(), True, Var(0));
+    expr t = mk_let("a", none_expr(), True, Var(0));
     std::cout << infer_type(t, env) << "\n";
 }
 
@@ -205,7 +205,7 @@ static void tst11() {
     expr t3 = f(b, b);
     for (unsigned i = 0; i < n; i++) {
         t1 = f(t1, t1);
-        t2 = mk_let("x", optional<expr>(), t2, f(Var(0), Var(0)));
+        t2 = mk_let("x", none_expr(), t2, f(Var(0), Var(0)));
         t3 = f(t3, t3);
     }
     lean_assert(t1 != t2);
diff --git a/src/tests/library/update_expr.cpp b/src/tests/library/update_expr.cpp
index 1b16f854d..cbd1f34b5 100644
--- a/src/tests/library/update_expr.cpp
+++ b/src/tests/library/update_expr.cpp
@@ -40,9 +40,9 @@ void tst3() {
     expr b   = Const("b");
     expr f   = Const("f");
     expr t1  = Let(a, b, f(a));
-    expr t2  = update_let(t1, optional<expr>(), b, let_body(t1));
+    expr t2  = update_let(t1, none_expr(), b, let_body(t1));
     lean_assert(is_eqp(t1, t2));
-    t2  = update_let(t1, optional<expr>(), a, let_body(t1));
+    t2  = update_let(t1, none_expr(), a, let_body(t1));
     lean_assert(!is_eqp(t1, t2));
     lean_assert(t2 == Let(a, a, f(a)));
 }