refactor(kernel): implement substitution methods

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

src/kernel/CMakeLists.txt

@@ -2,7 +2,7 @@ add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
 instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
 object.cpp environment.cpp replace_visitor.cpp io_state.cpp
-normalizer.cpp justification.cpp pos_info_provider.cpp
+normalizer.cpp justification.cpp pos_info_provider.cpp metavar.cpp
 # type_checker.cpp
 #  unification_constraint.cpp
 # type_checker_justification.cpp

src/kernel/metavar.cpp

@@ -4,9 +4,41 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#pragma once
-#include "util/metavar.h"
+#include <utility>
+#include "kernel/metavar.h"
 
 namespace lean {
-
+bool substitution::is_assigned(name const & m) const {
+    return m_subst.contains(m);
+}
+
+optional<std::pair<expr, justification>> substitution::get_assignment(name const & m) const {
+    auto it = m_subst.find(m);
+    if (it)
+        return optional<std::pair<expr, justification>>(*it);
+    else
+        return optional<std::pair<expr, justification>>();
+}
+
+optional<expr> substitution::get_expr(name const & m) const {
+    auto it = m_subst.find(m);
+    if (it)
+        return some_expr(it->first);
+    else
+        return none_expr();
+}
+
+void substitution::assign(name const & m, expr const & t, justification const & j) {
+    m_subst.insert(m, mk_pair(t, j));
+}
+
+void substitution::assign(name const & m, expr const & t) {
+    assign(m, t, justification());
+}
+
+void substitution::for_each(std::function<void(name const & n, expr const & e, justification const & j)> const & fn) {
+    m_subst.for_each([=](name const & n, std::pair<expr, justification> const & a) {
+            fn(n, a.first, a.second);
+        });
+}
 }

src/kernel/metavar.h

@@ -15,9 +15,9 @@ namespace lean {
 class substitution {
     rb_map<name, std::pair<expr, justification>, name_quick_cmp> m_subst;
 public:
-    substitution();
     bool is_assigned(name const & m) const;
     optional<std::pair<expr, justification>> get_assignment(name const & m) const;
+    optional<expr> get_expr(name const & m) const;
     void assign(name const & m, expr const & t, justification const & j);
     void assign(name const & m, expr const & t);
     void for_each(std::function<void(name const & n, expr const & e, justification const & j)> const & fn);