From 5f4b1cf47e2fba98d6760c7a0503156bdbe378e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Feb 2014 17:55:59 -0800
Subject: [PATCH] feat(kernel): define metavar substitution based on red-black
 trees

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/metavar.cpp | 12 ++++++++++++
 src/kernel/metavar.h   | 40 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 52 insertions(+)
 create mode 100644 src/kernel/metavar.cpp
 create mode 100644 src/kernel/metavar.h

diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
new file mode 100644
index 0000000000..0cd4f5dc53
--- /dev/null
+++ b/src/kernel/metavar.cpp
@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/metavar.h"
+
+namespace lean {
+
+}
diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h
new file mode 100644
index 0000000000..93adc71d02
--- /dev/null
+++ b/src/kernel/metavar.h
@@ -0,0 +1,40 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <utility>
+#include "util/rb_map.h"
+#include "util/optional.h"
+#include "kernel/expr.h"
+#include "kernel/justification.h"
+
+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;
+    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);
+};
+/**
+   \brief Instantiate metavariables in \c e assigned in the substitution \c s.
+*/
+std::pair<expr, justification> instantiate_metavars(expr const & e, substitution const & s);
+/**
+   \brief Similar to the previous function, but it compress the substitution.
+   By compress, we mean, for any metavariable \c m reachable from \c e,
+   if s[m] = t, and t has asssigned metavariables, then s[m] <- instantiate_metavars(t, s).
+*/
+std::pair<expr, justification> d_instantiate_metavars(expr const & e, substitution & s);
+/**
+   \brief Instantiate metavariables in \c e assigned in the substitution \c s,
+   but does not return a justification object for the new expression.
+*/
+expr instantiate_metavars_wo_jst(expr const & e, substitution const & s);
+}