From 0b3599851da065b45faa281a2877321540db3594 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 Feb 2014 23:20:21 -0800
Subject: [PATCH] refactor(library): remove unnecessary files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/context_to_lambda.cpp | 59 ------------------------------
 src/library/context_to_lambda.h   | 60 -------------------------------
 2 files changed, 119 deletions(-)
 delete mode 100644 src/library/context_to_lambda.cpp
 delete mode 100644 src/library/context_to_lambda.h

diff --git a/src/library/context_to_lambda.cpp b/src/library/context_to_lambda.cpp
deleted file mode 100644
index 6d234e1af..000000000
--- a/src/library/context_to_lambda.cpp
+++ /dev/null
@@ -1,59 +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 "library/context_to_lambda.h"
-
-namespace lean {
-static expr g_fake = Const(name::mk_internal_unique_name());
-expr context_to_lambda(context::iterator it, context::iterator const & end, expr const & e) {
-    if (it == end) {
-        return e;
-    } else {
-        context_entry const & entry = *it;
-        optional<expr> t;
-        optional<expr> const & d = entry.get_domain();
-        optional<expr> const & b = entry.get_body();
-        lean_assert(b || d);
-        if (b && d)
-            t = mk_app(g_fake, *d, *b);
-        else if (d)
-            t = mk_app(g_fake, *d, g_fake);
-        else
-            t = mk_app(g_fake, g_fake, *b);
-        lean_assert(t);
-        return context_to_lambda(++it, end, mk_lambda(entry.get_name(), *t, e));
-    }
-}
-expr context_to_lambda(context const & c, expr const & e) {
-    return context_to_lambda(c.begin(), c.end(), e);
-}
-bool is_fake_context(expr const & e) {
-    return is_lambda(e) && is_app(abst_domain(e)) && arg(abst_domain(e), 0) == g_fake;
-}
-name const & fake_context_name(expr const & e) {
-    lean_assert(is_fake_context(e));
-    return abst_name(e);
-}
-optional<expr> fake_context_domain(expr const & e) {
-    lean_assert(is_fake_context(e));
-    expr r = arg(abst_domain(e), 1);
-    if (!is_eqp(r, g_fake))
-        return some_expr(r);
-    else
-        return none_expr();
-}
-optional<expr> fake_context_value(expr const & e) {
-    lean_assert(is_fake_context(e));
-    expr r = arg(abst_domain(e), 2);
-    if (!is_eqp(r, g_fake))
-        return some_expr(r);
-    else
-        return none_expr();
-}
-expr const & fake_context_rest(expr const & e) {
-    return abst_body(e);
-}
-}
diff --git a/src/library/context_to_lambda.h b/src/library/context_to_lambda.h
deleted file mode 100644
index bc3ae3344..000000000
--- a/src/library/context_to_lambda.h
+++ /dev/null
@@ -1,60 +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 "kernel/context.h"
-namespace lean {
-/**
-   \brief Given the context (n_1 : T_1 [:= V_1]) ... (n_k : T_k [:= V_k]) and expression e into,
-   return the "meaningless" lambda expression:
-
-   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
-
-   The constant "fake" is irrelevant, it is just used as a marker.
-   It is used to "glue" T_i and V_i.
-
-   This little hack allows us to use the machinery for instantiating
-   lambdas with contexts.
-
-   \remark If a context entry (n_i : T_i [:= V_i]) does not have a
-   value V_i, then we just use (fake T_i).
-*/
-expr context_to_lambda(context const & c, expr const & e);
-/**
-   \brief Return true if \c e is a fake context created using
-   context_to_lambda.
-   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
-*/
-bool is_fake_context(expr const & e);
-/**
-   \brief Return the name n_1 of the head of the (fake) context
-   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
-
-   \pre is_fake_context(e)
-*/
-name const & fake_context_name(expr const & e);
-/**
-   \brief Return the domain T_1 of the head of the (fake) context
-   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
-
-   \pre is_fake_context(e)
-*/
-optional<expr> fake_context_domain(expr const & e);
-/**
-   \brief Return (if available) the value V_1 of the head of the (fake) context
-   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
-
-   \pre is_fake_context(e)
-*/
-optional<expr> fake_context_value(expr const & e);
-/**
-   \brief Return the rest (lambda (n_2 : (fake T_2 V_2)) ... (lambda (n_k : (fake T_k V_k)) e)) of the fake context
-   (lambda (n_1 : (fake T_1 V_1)) ... (lambda (n_k : (fake T_k V_k)) e))
-
-   \pre is_fake_context(e)
-*/
-expr const & fake_context_rest(expr const & e);
-}