From 968c0d799f1b45b6a80563c9aff382be5ffc0cb9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 Feb 2014 08:41:45 -0800
Subject: [PATCH] refactor(kernel): implement substitution methods

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/CMakeLists.txt |  2 +-
 src/kernel/metavar.cpp    | 38 +++++++++++++++++++++++++++++++++++---
 src/kernel/metavar.h      |  2 +-
 3 files changed, 37 insertions(+), 5 deletions(-)

diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 99dac5603..a34065b1c 100644
--- a/src/kernel/CMakeLists.txt
+++ b/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
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index 0cd4f5dc5..c675ea90f 100644
--- a/src/kernel/metavar.cpp
+++ b/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);
+        });
+}
 }
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
index 93adc71d0..62cd55138 100644
--- a/src/kernel/metavar.h
+++ b/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);