From 18d9272f226757ce51fcfb1b5ac159840ce9976a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 31 Oct 2015 23:01:19 -0700
Subject: [PATCH] refactor(library/type_context): revise get_assignment

It is safer to return optional.
---
 src/library/blast/blast.cpp  | 14 ++++++++++----
 src/library/type_context.cpp | 16 +++++++++++-----
 src/library/type_context.h   | 16 ++++++++--------
 3 files changed, 29 insertions(+), 17 deletions(-)

diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index eadcfab7f1..e39bf5bb68 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -70,12 +70,18 @@ class blastenv {
             return blast::is_mref(e);
         }
 
-        virtual level const * get_assignment(level const & u) const {
-            return m_benv.m_curr_state.get_uref_assignment(u);
+        virtual optional<level> get_assignment(level const & u) const {
+            if (auto v = m_benv.m_curr_state.get_uref_assignment(u))
+                return some_level(*v);
+            else
+                return none_level();
         }
 
-        virtual expr const * get_assignment(expr const & m) const {
-            return m_benv.m_curr_state.get_mref_assignment(m);
+        virtual optional<expr> get_assignment(expr const & m) const {
+            if (auto v = m_benv.m_curr_state.get_mref_assignment(m))
+                return some_expr(*v);
+            else
+                return none_expr();
         }
 
         virtual void update_assignment(level const & u, level const & v) {
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 6fd7871520..247ce3d666 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -400,7 +400,7 @@ expr type_context::subst_mvar(expr const & e) {
     buffer<expr> args;
     expr const & m   = get_app_rev_args(e, args);
     lean_assert(is_mvar(m));
-    expr const * v = get_assignment(m);
+    optional<expr> v = get_assignment(m);
     lean_assert(v);
     return apply_beta(*v, args.size(), args.data());
 }
@@ -1705,12 +1705,18 @@ unsigned default_type_context::mvar_idx(expr const & m) const {
     return mlocal_name(m).get_numeral();
 }
 
-level const * default_type_context::get_assignment(level const & u) const {
-    return m_assignment.m_uassignment.find(uvar_idx(u));
+optional<level> default_type_context::get_assignment(level const & u) const {
+    if (auto v = m_assignment.m_uassignment.find(uvar_idx(u)))
+        return some_level(*v);
+    else
+        return none_level();
 }
 
-expr const * default_type_context::get_assignment(expr const & m) const {
-    return m_assignment.m_eassignment.find(mvar_idx(m));
+optional<expr> default_type_context::get_assignment(expr const & m) const {
+    if (auto v = m_assignment.m_eassignment.find(mvar_idx(m)))
+        return some_expr(*v);
+    else
+        return none_expr();
 }
 
 void default_type_context::update_assignment(level const & u, level const & v) {
diff --git a/src/library/type_context.h b/src/library/type_context.h
index c61c035798..90cc452df8 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -243,14 +243,14 @@ public:
     virtual bool is_mvar(expr const & e) const = 0;
 
     /** \brief Return the assignment for universe unification variable
-        \c u, and nullptr if it is not assigned.
+        \c u, and none if it is not assigned.
         \pre is_uvar(u) */
-    virtual level const * get_assignment(level const & u) const = 0;
+    virtual optional<level> get_assignment(level const & u) const = 0;
 
     /** \brief Return the assignment for unification variable
-        \c m, and nullptr if it is not assigned.
+        \c m, and none if it is not assigned.
         \pre is_mvar(u) */
-    virtual expr const * get_assignment(expr const & m) const = 0;
+    virtual optional<expr> get_assignment(expr const & m) const = 0;
 
     /** \brief Update the assignment for \c u.
         \pre is_uvar(u) */
@@ -297,8 +297,8 @@ public:
         assign unassigned metavariables in the given terms. */
     virtual bool on_is_def_eq_failure(expr &, expr &);
 
-    bool is_assigned(level const & u) const { return get_assignment(u) != nullptr; }
-    bool is_assigned(expr const & m) const { return get_assignment(m) != nullptr; }
+    bool is_assigned(level const & u) const { return static_cast<bool>(get_assignment(u)); }
+    bool is_assigned(expr const & m) const { return static_cast<bool>(get_assignment(m)); }
 
     bool has_assigned_uvar(level const & l) const;
     bool has_assigned_uvar(levels const & ls) const;
@@ -409,8 +409,8 @@ public:
     virtual bool is_tmp_local(expr const & e) const;
     virtual bool is_uvar(level const & l) const;
     virtual bool is_mvar(expr const & e) const;
-    virtual level const * get_assignment(level const & u) const;
-    virtual expr const * get_assignment(expr const & m) const;
+    virtual optional<level> get_assignment(level const & u) const;
+    virtual optional<expr> get_assignment(expr const & m) const;
     virtual void update_assignment(level const & u, level const & v);
     virtual void update_assignment(expr const & m, expr const & v);
     virtual level mk_uvar();