From 4348d5e63feb3ae07bafc4ed0591f3872d91caad Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 17 May 2014 12:35:41 -0700
Subject: [PATCH] refactor(kernel): remove unnecessary module

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/CMakeLists.txt        |  2 +-
 src/kernel/context.cpp           | 29 -----------------------------
 src/kernel/context.h             | 20 --------------------
 src/kernel/inductive/inductive.h |  1 -
 src/kernel/kernel_exception.h    |  1 -
 5 files changed, 1 insertion(+), 52 deletions(-)
 delete mode 100644 src/kernel/context.cpp
 delete mode 100644 src/kernel/context.h

diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 9bca07cd5..5c6aacdb5 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(kernel level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
-replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp context.cpp
+replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
 formatter.cpp definition.cpp replace_visitor.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
 constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp )
diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp
deleted file mode 100644
index a7d657ec4..000000000
--- a/src/kernel/context.cpp
+++ /dev/null
@@ -1,29 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <utility>
-#include "util/exception.h"
-#include "kernel/context.h"
-
-namespace lean {
-binder const & lookup(context const & c, unsigned i) {
-    auto const * it = &c;
-    while (*it) {
-        if (i == 0)
-            return head(*it);
-        --i;
-        it = &tail(*it);
-    }
-    throw exception("unknown free variable");
-}
-optional<binder> find(context const & c, unsigned i) {
-    try {
-        return optional<binder>(lookup(c, i));
-    } catch (exception &) {
-        return optional<binder>();
-    }
-}
-}
diff --git a/src/kernel/context.h b/src/kernel/context.h
deleted file mode 100644
index 17fd2f10c..000000000
--- a/src/kernel/context.h
+++ /dev/null
@@ -1,20 +0,0 @@
-/*
-Copyright (c) 2013 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/list.h"
-#include "util/optional.h"
-#include "kernel/expr.h"
-
-namespace lean {
-// Remark: in a nonempty context C, variable 0 is head(C)
-typedef list<binder> context;
-inline context extend(context const & c, name const & n, expr const & t) { return cons(binder(n, t), c); }
-inline context extend(context const & c, binder const & b) { return cons(b, c); }
-binder const & lookup(context const & c, unsigned i);
-optional<binder> find(context const & c, unsigned i);
-}
diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h
index 6f7db7137..712571bfd 100644
--- a/src/kernel/inductive/inductive.h
+++ b/src/kernel/inductive/inductive.h
@@ -10,7 +10,6 @@ Author: Leonardo de Moura
 #include <tuple>
 #include "util/list.h"
 #include "kernel/environment.h"
-#include "kernel/context.h"
 
 namespace lean {
 namespace inductive {
diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h
index bb9e45f8a..9b603db4c 100644
--- a/src/kernel/kernel_exception.h
+++ b/src/kernel/kernel_exception.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include <vector>
 #include "util/exception.h"
 #include "util/sexpr/options.h"
-#include "kernel/context.h"
 #include "kernel/environment.h"
 #include "kernel/formatter.h"