From 66d583d279fdd149e3d0e7b777953969bdc7d5f2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Mar 2016 13:09:36 -0800
Subject: [PATCH] feat(library/local_context): add well_formed debugging
 methods

---
 src/library/local_context.cpp | 47 +++++++++++++++++++++++++++++++++++
 src/library/local_context.h   | 14 +++++++++++
 2 files changed, 61 insertions(+)

diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp
index 2d4b3143a2..645fba02cb 100644
--- a/src/library/local_context.cpp
+++ b/src/library/local_context.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <limits>
 #include "util/fresh_name.h"
+#include "kernel/for_each_fn.h"
 #include "library/local_context.h"
 
 namespace lean {
@@ -87,6 +88,52 @@ void local_context::for_each_after(local_decl const & d, std::function<void(loca
     m_idx2local_decl.for_each_greater(d.get_idx(), [&](unsigned, local_decl const & d) { return fn(d); });
 }
 
+/* Return true iff all local_decl references in \c e are in \c s. */
+static bool locals_subset_of(expr const & e, name_set const & s) {
+    bool ok = true;
+    for_each(e, [&](expr const & e, unsigned) {
+            if (!ok) return false; // stop search
+            if (is_local_decl_ref(e) && !s.contains(mlocal_name(e))) {
+                ok = false;
+                return false;
+            }
+            return true;
+        });
+    return ok;
+}
+
+bool local_context::well_formed() const {
+    bool ok = true;
+    name_set found_locals;
+    for_each([&](local_decl const & d) {
+            if (!locals_subset_of(d.get_type(), found_locals)) {
+                ok = false;
+                lean_unreachable();
+            }
+            if (auto v = d.get_value()) {
+                if (!locals_subset_of(*v, found_locals)) {
+                    ok = false;
+                    lean_unreachable();
+                }
+            }
+            found_locals.insert(d.get_name());
+        });
+    return ok;
+}
+
+bool local_context::well_formed(expr const & e) const {
+    bool ok = true;
+    ::lean::for_each(e, [&](expr const & e, unsigned) {
+            if (!ok) return false;
+            if (is_local_decl_ref(e) && !get_local_decl(e)) {
+                ok = false;
+                lean_unreachable();
+            }
+            return true;
+        });
+    return ok;
+}
+
 void local_context::freeze(name const & n) {
     lean_assert(m_name2local_decl.contains(n));
     m_frozen_decls.insert(n);
diff --git a/src/library/local_context.h b/src/library/local_context.h
index dc102f0caa..dbc81a670c 100644
--- a/src/library/local_context.h
+++ b/src/library/local_context.h
@@ -95,9 +95,23 @@ public:
     optional<local_decl> find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT
     /** \brief Execute fn for each local declaration created after \c d. */
     void for_each_after(local_decl const & d, std::function<void(local_decl const &)> const & fn) const;
+
     local_decls to_local_decls() const { return local_decls(m_name2local_decl); }
+
     void freeze(name const & n);
     bool is_frozen(name const & n) const { return m_frozen_decls.contains(n); }
+
+    /** \brief We say a local context is well-formed iff all local declarations only
+        contain local_decl references that were defined before them.
+
+        \remark This method is for debugging purposes. */
+    bool well_formed() const;
+
+    /** \brief Return true iff \c e is well-formed with respect to this local context.
+        That is, all local_decl references in \c e are defined in this context.
+
+        \remark This method is for debugging purposes. */
+    bool well_formed(expr const & e) const;
 };
 
 void initialize_local_context();